From Coq Require Import Init.Nat Lia List.
From PCF2 Require Import pcf_2_system preliminaries.
From PCF2.Autosubst Require Import unscoped pcf_2.
Definition base_fun n T :=
iter n (fun T => Base ⟶ T) T.
Definition apply_args (t: tm) (l: list tm) :=
fold_right (fun arg t => app t arg) t (rev l).
Definition base_context n := iter n (fun l => cons Base l) nil.
Definition lam_T n t :=
iter n (fun t => lam t) t.
Definition var_seq start length := map (fun n => var_tm n) (seq start length).
Definition list_to_fun (L: list ty) (A: ty) :=
fold_right (fun A B => A ⟶ B) A L.
Lemma apply_args_app (s: tm) (l l': list tm):
apply_args s (l ++ l') = apply_args (apply_args s l) l'.
Proof.
unfold apply_args. rewrite rev_app_distr. now rewrite fold_right_app.
Qed.
Lemma apply_args_cons (s: tm) (a: tm) (l: list tm):
apply_args s (a :: l) = apply_args (app s a) l.
Proof.
assert (eq: a :: l = (a :: nil) ++ l) by easy.
rewrite eq. apply apply_args_app.
Qed.
Lemma apply_args_typed (l1: list ty) (l2: list tm) (t: tm) (A: ty) (Γ: context):
Γ ⊢ t: list_to_fun l1 A -> length l1 = length l2 -> (forall n A' t', nth_error l1 n = Some A' -> nth_error l2 n = Some t' -> Γ ⊢ t': A') -> Γ ⊢ apply_args t l2: A.
Proof.
intros typed_t len H. induction l1 as [| a1 l1] in l2, t, len, typed_t, H |-*.
1: destruct l2; try easy.
destruct l2 as [| a2 l2]; try easy. rewrite apply_args_cons.
apply IHl1.
- eapply app_typed with (typ1 := a1).
1: exact typed_t.
now apply H with (n := 0).
- cbn in len. lia.
- intros n A' t' H1 H2. now apply H with (n := S n).
Qed.
Lemma subst_apply_args (σ: nat -> tm) (s: tm) (l: list tm):
Subst_tm σ (apply_args s l) = apply_args (Subst_tm σ s) (map (Subst_tm σ) l).
Proof.
induction l in s |-*.
1: easy.
rewrite apply_args_cons.
rewrite IHl. rewrite map_cons. now rewrite apply_args_cons.
Qed.
Lemma ren_apply_args (σ: nat -> nat) (s: tm) (l: list tm):
ren_tm σ (apply_args s l) = apply_args (ren_tm σ s) (map (ren_tm σ) l).
Proof.
induction l in s |-*.
1: easy.
rewrite apply_args_cons.
rewrite IHl. rewrite map_cons. now rewrite apply_args_cons.
Qed.
Lemma apply_args_steps_body (t t': tm) (l: list tm):
t ≻* t' -> apply_args t l ≻* apply_args t' l.
Proof.
intros steps_t.
induction l in t, t', steps_t |-*. 1: easy.
rewrite apply_args_cons, apply_args_cons.
rewrite IHl with (t := app t a). 1: constructor 2. now rewrite steps_t.
Qed.
Lemma apply_args_steps_list (t: tm) (l l': list tm):
length l = length l' -> (forall n t t', nth_error l n = Some t -> nth_error l' n = Some t' -> t ≻* t') -> apply_args t l ≻* apply_args t l'.
Proof.
intros H_len H_steps.
induction l as [| a l] in l', t, H_len, H_steps |-*.
- cbn. destruct l'; easy.
- destruct l' as [| a' l'].
1: easy. rewrite apply_args_cons, apply_args_cons.
eapply steps_PreOrder. 1: eapply apply_args_steps_body; rewrite (H_steps 0 a a'); eauto.
erewrite (IHl _ l'). 1: easy. 1: now injection H_len.
intros n s u H_s H_u. now apply (H_steps (S n)).
Qed.
Lemma apply_args_steps_list' (t: tm) (l l' m: list tm):
length l = length l' -> (forall n t t', nth_error l n = Some t -> nth_error l' n = Some t' -> t ≻* t') -> apply_args t (l ++ m) ≻* apply_args t (l' ++ m).
Proof.
intros H1 H2. eapply apply_args_steps_list.
1: simpl_list; now rewrite H1.
intros n s u Hs Hu. destruct (nat_ord_dec (length l) n).
- rewrite nth_error_app2 in Hs. 2: easy.
rewrite nth_error_app2 in Hu. 2: lia. rewrite H1 in Hs. rewrite Hs in Hu. injection Hu. intro. subst. constructor 2.
- rewrite nth_error_app1 in Hs. 2: easy. rewrite nth_error_app1 in Hu. 2: lia.
eapply H2; eauto.
Qed.
Lemma list_to_fun_app' l l' A:
list_to_fun (l ++ l') A = list_to_fun l (list_to_fun l' A).
Proof.
unfold list_to_fun. now rewrite fold_right_app.
Qed.
Lemma lam_T_shift_subst (t: tm) (n: nat) (σ: nat -> tm):
Subst_tm σ (lam_T n t) = lam_T n (Subst_tm (iter n Up_tm_tm σ) t).
Proof.
induction n in σ |-*.
1: easy. unfold lam_T.
cbn. erewrite IHn. unfold lam_T. rewrite <- iter_succ_r. easy.
Qed.
Lemma lam_T_split (t: tm) (n m: nat):
lam_T (n + m) t = lam_T n (lam_T m t).
Proof.
induction n.
1: easy.
unfold lam_T. unfold lam_T in IHn. assert (eq: S n + m = S(n + m)) by lia.
rewrite eq. rewrite iter_succ_l. now rewrite IHn.
Qed.
Lemma lam_list_to_type t Γ A:
Γ ⊢ t: A -> nil ⊢ lam_T (length Γ) t: list_to_fun (rev Γ) A.
Proof.
intros typed_t. induction Γ in t, A, typed_t |-*.
1: easy.
assert (eq: length (a :: Γ) = length Γ + 1). 1: cbn; lia.
rewrite eq, lam_T_split. cbn. rewrite fold_right_app. cbn. fold (list_to_fun (rev Γ) (a ⟶ A)).
apply IHΓ. now constructor.
Qed.
Lemma lam_list_to_type' t Γ Γ' A:
(Γ ++ Γ') ⊢ t: A -> Γ' ⊢ lam_T (length Γ) t: list_to_fun (rev Γ) A.
Proof.
intros typed_t. induction Γ in t, A, typed_t |-*.
1: easy.
assert (eq: length (a :: Γ) = length Γ + 1). 1: cbn; lia.
rewrite eq, lam_T_split. cbn. rewrite fold_right_app. cbn. fold (list_to_fun (rev Γ) (a ⟶ A)).
apply IHΓ. now constructor.
Qed.
Lemma length_var_seq :
forall len start, length (var_seq start len) = len.
Proof.
intros n m. unfold var_seq. now simpl_list.
Qed.
Lemma var_seq_split (start n m: nat):
var_seq start (n + m) = var_seq start n ++ var_seq (start + n) m.
Proof.
unfold var_seq. rewrite seq_app. now rewrite map_app.
Qed.
Lemma var_seq_nth n start len:
n < len -> nth_error (var_seq start len) n = Some (var_tm (start + n)).
Proof.
intros H.
enough (H': nth n (var_seq start len) (var_tm 0) = var_tm (start + n)).
- rewrite <- H'. apply nth_error_nth'. now rewrite length_var_seq.
- unfold var_seq. rewrite map_nth. now rewrite seq_nth.
Qed.
Lemma var_seq_map_nth n start length (σ: nat -> tm):
n < length -> nth_error (map (Subst_tm σ) (var_seq start length)) n = Some (σ (start + n)).
Proof.
intros H. rewrite nth_error_map. rewrite var_seq_nth. 2: easy.
now cbn.
Qed.
Lemma length_base_context (n: nat):
length (base_context n) = n.
Proof.
induction n.
1: easy.
unfold base_context in IHn. unfold base_context. rewrite iter_succ_l.
cbn. now rewrite IHn.
Qed.
Lemma base_context_some_base (n m: nat) (T: ty):
nth_error (base_context n) m = Some T -> T = Base.
Proof.
intros H. induction n in m, H |-*.
1: destruct m; easy.
destruct m.
- cbn in H. intuition congruence.
- apply (IHn m). easy.
Qed.
Lemma base_context_le_base (n m: nat):
m < n -> nth_error (base_context n) m = Some Base.
Proof.
intros H. rewrite <- length_base_context in H. apply nth_error_Some in H.
destruct (nth_error (base_context n) m) eqn: e. 2: easy.
erewrite (base_context_some_base _ _ t); eauto.
Qed.
Lemma base_context_rev' n A:
rev (iter n (fun l : list ty => Base :: l) A) = rev A ++ iter n (fun l : list ty => Base :: l) nil.
induction n in A |-*.
1: now simpl_list. rewrite iter_succ_r at 1. cbn.
rewrite IHn. cbn. now rewrite <- app_assoc.
Qed.
Lemma base_context_rev n:
rev (base_context n) = base_context n.
unfold base_context. now rewrite base_context_rev'.
Qed.
Lemma base_fun_applied_typed t l Γ:
Γ ⊢ t: base_fun (length l) Base -> (Forall (fun t => Γ ⊢ t: Base) l) -> Γ ⊢ apply_args t l: Base.
Proof.
intros typed_t H. induction l in t, typed_t, H |-*.
1: easy.
rewrite apply_args_cons. rewrite Forall_cons_iff in H. eapply IHl.
1: now apply app_typed with (typ1 := Base).
easy.
Qed.
Lemma fun_rev_to_context t Γ A:
nil ⊢ t: list_to_fun (rev Γ) A -> Γ ⊢ apply_args t (rev (var_seq 0 (length Γ))): A.
Proof.
intros typed_t. induction (length Γ) eqn: e in t, Γ, typed_t |-*.
- cbn. rewrite length_zero_iff_nil in e. now subst.
- assert (H: Γ <> nil). 1: intros H; rewrite <- length_zero_iff_nil in H; lia.
specialize (exists_last H). intros [l' [a Hl']]. rewrite Hl'.
assert (eq1: S n = n + 1) by lia. rewrite eq1, var_seq_split, rev_app_distr, apply_args_app.
cbn. rewrite Hl' in e. rewrite app_length in e. cbn in e. assert (eq2: length l' = n) by lia.
apply apply_args_typed with (l1 := rev l').
+ apply app_typed with (typ1 := a).
* rewrite Hl', rev_app_distr, list_to_fun_app' in typed_t. cbn in typed_t.
assert (eq3: l' ++ a :: nil = nil ++ l' ++ a :: nil) by now simpl_list.
rewrite eq3. now apply type_weakening.
* constructor. rewrite nth_error_app2. 2: lia. rewrite eq2. assert (eq3: n - n = 0) by lia.
now rewrite eq3.
+ simpl_list. now rewrite eq2, length_var_seq.
+ intros n' A' t' H1 H2. assert (H3: n' < length (rev (var_seq 0 n))).
{ apply nth_error_Some. intros ?. now destruct (nth_error (rev (var_seq 0 n)) n'). }
rewrite rev_length in H3.
rewrite <- rev_nth_error2 in H2; eauto. rewrite var_seq_nth in H2.
2: { rewrite length_var_seq. destruct n. 1: easy. lia. }
injection H2. rewrite length_var_seq. intros eq. rewrite <- eq.
constructor. rewrite <- H1. assert (eq3: n' < length l').
{ rewrite <- rev_length. apply nth_error_Some. intros ?. now destruct (nth_error (rev l') n'). }
rewrite <- rev_nth_error2; eauto.
assert (eq4: n - S n' < length l').
{rewrite eq2. destruct n. 1: easy. lia. }
rewrite nth_error_app1; eauto.
Qed.
Lemma basefun_var_applied_typed n t:
nil ⊢ t: base_fun n Base -> base_context n ⊢ apply_args t (var_seq 0 n): Base.
Proof.
intros typed_t. apply base_fun_applied_typed.
- assert (eq: base_context n = nil ++ base_context n) by easy.
rewrite eq. apply type_weakening. now rewrite length_var_seq.
- rewrite Forall_forall. intros a Ha.
specialize (In_nth_error _ _ Ha). intros [n' Hn'].
assert (H: n' < n).
{ rewrite <- (length_var_seq n 0). apply nth_error_Some.
intros H. now rewrite H in Hn'. }
rewrite (var_seq_nth _ _ _ H) in Hn'.
cbn in Hn'. injection Hn'.
intros ?; subst. constructor.
destruct (nth_error (base_context n) n') eqn: e.
1: now rewrite (base_context_some_base _ _ _ e).
rewrite nth_error_None in e. rewrite length_base_context in e. lia.
Qed.