stlc
(* -------------------------------------------------------------------- *)
(* -------- *) Require Import Arith List Omega.
From Autosubst Require Import Autosubst.
(* -------------------------------------------------------------------- *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* -------------------------------------------------------------------- *)
Fixpoint loop {T : Type} n (f : T -> T) (x : T) :=
match n with 0 => x | S n => f (loop n f x) end.
(* -------------------------------------------------------------------- *)
Inductive term : Type :=
| Var (_ : var)
| App (_ : term) (_ : term)
| Lam (_ : {bind term}).
(* -------------------------------------------------------------------- *)
Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
(* -------------------------------------------------------------------- *)
Inductive step : term -> term -> Prop :=
| Step_beta (s1 s2 t : term) :
s1.[t/] = s2 -> step (App (Lam s1) t) s2
| Step_appL (s1 s2 t : term) :
step s1 s2 -> step (App s1 t) (App s2 t)
| Step_appR (s t1 t2 : term) :
step t1 t2 -> step (App s t1) (App s t2)
| Step_lam (s1 s2 : term) :
step s1 s2 -> step (Lam s1) (Lam s2).
Notation red := (fun s t => step t s).
Hint Constructors step : ty.
(* -------------------------------------------------------------------- *)
Derive Inversion_clear step_var with
(forall x t, step (Var x) t) Sort Prop.
Derive Inversion_clear step_lam with
(forall s t, step (Lam s) t) Sort Prop.
Derive Inversion_clear step_redex with
(forall s1 s2 t, step (App (Lam s1) s2) t) Sort Prop.
Derive Inversion_clear step_app with
(forall s1 s2 t, step (App s1 s2) t) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma step_subst t u : step t u -> forall xi, step t.[xi] u.[xi].
Proof. now induction 1; constructor; subst; autosubst. Qed.
(* -------------------------------------------------------------------- *)
Inductive type := Base | Arr (_ : type) (_ : type).
(* -------------------------------------------------------------------- *)
Inductive ty (G : var -> type) : term -> type -> Prop :=
| Ty_Var x A :
G x = A -> ty G (Var x) A
| Ty_Lam s A B :
ty (A .: G) s B -> ty G (Lam s) (Arr A B)
| Ty_App s t A B :
ty G s (Arr A B) -> ty G t A -> ty G (App s t) B.
Hint Constructors ty : ty.
(* -------------------------------------------------------------------- *)
Derive Inversion_clear ty_var with
(forall G x A, ty G (Var x) A) Sort Prop.
Derive Inversion_clear ty_lam with
(forall G t A, ty G (Lam t) A) Sort Prop.
Derive Inversion_clear ty_app with
(forall G s t A, ty G (App s t) A) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma ty_ren G s A :
ty G s A -> forall D xi, G = xi >>> D -> ty D s.[ren xi] A.
Proof.
induction 1; intros; subst; asimpl; econstructor; eauto.
- now eapply IHty; autosubst.
Qed.
(* -------------------------------------------------------------------- *)
Lemma ty_subst G s A :
ty G s A -> forall D xi,
(forall x, ty D (xi x) (G x)) -> ty D s.[xi] A.
Proof.
induction 1; intros; subst; asimpl; eauto using ty.
- econstructor; eapply IHty.
now intros [|]; asimpl; eauto using ty, ty_ren.
Qed.
(* -------------------------------------------------------------------- *)
Lemma ty_pres G s A : ty G s A -> forall s', step s s' -> ty G s' A.
Proof.
induction 1; intros s' h; asimpl; inversion h; ainv; eauto using ty.
- eapply ty_subst; try eassumption.
now intros [|]; simpl; eauto using ty.
Qed.
(* -------------------------------------------------------------------- *)
Notation SN := (Acc red).
(* -------------------------------------------------------------------- *)
Definition allSN (ts : list term) := forall t, In t ts -> SN t.
(* -------------------------------------------------------------------- *)
Fact allSN0 : allSN nil.
Proof. easy. Qed.
(* -------------------------------------------------------------------- *)
Fixpoint CR (ty : type) :=
match ty with
| Base => fun t => SN t
| Arr ty1 ty2 => fun t => forall u, CR ty1 u -> CR ty2 (App t u)
end.
(* -------------------------------------------------------------------- *)
Definition neutral (t : term) :=
match t with Lam _ => false | _ => true end.
(* -------------------------------------------------------------------- *)
Lemma SN_stepI t : (forall u, step t u -> SN u) -> SN t.
Proof. now intros h; constructor. Qed.
(* -------------------------------------------------------------------- *)
Inductive subterm : term -> term -> Prop :=
| SubTop t :
subterm t t
| SubAppL t1 t2 u :
subterm t1 u -> subterm (App t1 t2) u
| SubAppR t1 t2 u :
subterm t2 u -> subterm (App t1 t2) u
| SubLam t u :
subterm t u -> subterm (Lam t) u.
Hint Constructors subterm : ty.
(* -------------------------------------------------------------------- *)
Lemma step_subterm t u u' :
subterm t u -> step u u' -> exists t', step t t' /\ subterm t' u'.
Proof.
induction 1; intros; solve
[ exists u'; eauto using subterm
| apply IHsubterm in H0; destruct H0 as [? [? ?]];
eexists; split; econstructor; eauto ].
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_subterm t : SN t -> forall u, subterm t u -> SN u.
Proof.
induction 1 as [t acc ih]; intros u sub_t_u; constructor.
intros u' st_u_u'; case (step_subterm sub_t_u st_u_u').
now intros t' [st_t_t' sub_t'_u']; eauto.
Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_appIL t u : SN (App t u) -> SN t.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_appIR t u : SN (App t u) -> SN u.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_lamI t : SN (Lam t) -> SN t.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_var n : SN (Var n).
Proof. now ainv. Qed.
Hint Resolve SN_var.
(* -------------------------------------------------------------------- *)
Inductive steps {n : nat} (ts us : list term) : Prop :=
| Step1 ts1 t u ts2
(_ : length ts = n)
(_ : ts = ts1 ++ t :: ts2)
(_ : us = ts1 ++ u :: ts2)
(_ : step t u).
Notation reds n := (fun x y => @steps n y x).
(* -------------------------------------------------------------------- *)
Lemma allSN_acc (ts : list term) :
allSN ts -> forall n, n = length ts -> Acc (reds n) ts.
Proof.
induction ts as [|t ts ih]; intros h n nE.
+ now simpl; constructor; intros us []; case ts1 in H0.
+ revert nE; destruct n as [|n]; try discriminate.
intros nE; injection nE; clear nE; intros nE.
assert (SN_t : SN t) by now apply h; apply in_eq.
assert (SN_ts : Acc (reds n) ts).
- now apply ih; trivial; intros t' t'_ts; auto using in_cons.
- clear ih h; revert ts nE SN_ts; generalize SN_t.
induction SN_t as [t acct iht]; intros SN_t ts nE SN_ts.
revert nE SN_t acct iht; generalize SN_ts.
induction SN_ts as [ts accts ihts]; intros SN_ts nE SN_t acct iht.
constructor; intros us [ts1 t' u' ts2 _ eq usE st_t'_u']; subst us.
destruct ts1 as [|t1' ts1'] in eq |- *; simpl in *.
* injection eq; clear eq; intros; subst t' ts2.
now apply iht; trivial; apply SN_t.
* injection eq; clear eq; intros; subst ts t1'; apply ihts; trivial.
++ now exists ts1' t' u' ts2; trivial; rewrite <- nE.
++ case SN_ts; intros h; apply h.
now exists ts1' t' u' ts2; trivial; rewrite <- nE.
++ now rewrite nE; rewrite !app_length; simpl.
Qed.
(* -------------------------------------------------------------------- *)
Lemma pairSN_acc t u : SN t -> SN u -> Acc (reds 2) (t :: u :: nil).
Proof.
intros SN_t SN_u; apply allSN_acc; trivial.
now intros s; simpl; intuition; subst.
Qed.
(* -------------------------------------------------------------------- *)
Lemma step_apps_varI x ts u :
step (fold_left App ts (Var x)) u
-> exists us, @steps (length ts) ts us /\ u = fold_left App us (Var x).
Proof.
revert u; induction ts as [|t ts ih] using rev_ind; simpl.
+ now intros u; inversion 1.
+ intros u; rewrite fold_left_app; simpl; inversion 1; subst.
* absurd (Lam s1 = fold_left App ts (Var x)); trivial.
clear ih H H0; destruct ts as [|u us] using rev_ind; simpl.
- discriminate.
- now rewrite fold_left_app; simpl; discriminate.
* case (ih _ H3); clear H3; intros us [st ?]; subst s2.
exists (us ++ t :: nil); split; trivial.
destruct st as [ts1 t' u' ts2 _ tsE usE st].
exists ts1 t' u' (ts2 ++ t :: nil); trivial.
- now rewrite tsE, <- app_assoc.
- now rewrite usE, <- app_assoc.
- now rewrite fold_left_app.
* exists (ts ++ t2 :: nil); split.
- now exists ts t t2 nil.
- now rewrite fold_left_app.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_apps_var x ts : allSN ts -> SN (fold_left App ts (Var x)).
Proof.
intros SNts; assert (hn : exists n, n = length ts) by now eexists.
destruct hn as [n eqn]; assert (h := allSN_acc SNts eqn); clear SNts.
revert eqn; induction h as [ts acc ih]; intros eqn.
constructor; intros u st; apply step_apps_varI in st.
destruct st as [us [st uE]]; subst u; apply ih.
+ now rewrite eqn.
+ now destruct st; rewrite eqn; subst ts us; rewrite !app_length.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_step t u : step t u -> SN t -> SN u.
Proof. now intros st_t_u [h]; apply h in st_t_u. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_SN_r ty :
(forall t, CR ty t -> SN t)
/\ (forall n ts, allSN ts -> CR ty (fold_left App ts (Var n))).
Proof.
induction ty as [|ty1 ih1 ty2 ih2]; split; trivial.
+ now intros; apply SN_apps_var.
+ intros t CR_tu; case ih1 as [_ ih1]; generalize (ih1 0 _ allSN0).
simpl in CR_tu |- *; intros CR_0; apply CR_tu in CR_0.
now case ih2; intros h1 h2; apply h1 in CR_0; apply SN_appIL in CR_0.
+ intros n ts SN_ts u CR_u; destruct ih2 as [ih2 h].
generalize (h n (ts ++ u :: nil)); clear h; rewrite fold_left_app.
intros h; apply h; intros s; rewrite in_app_iff; intros hin.
destruct hin as [hin|eq]; eauto; destruct eq as [eq|F].
* now subst u; destruct ih1 as [ih1 _]; auto.
* now case F.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_SN ty t : CR ty t -> SN t.
Proof. now case (CR_SN_r ty); auto. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_var ty n : CR ty (Var n).
Proof.
destruct (CR_SN_r ty) as [_ h].
now generalize (h n nil); eauto using allSN0.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_step_r ty :
(forall t u, step t u -> CR ty t -> CR ty u)
/\ (forall t, neutral t = true -> (forall u, step t u -> CR ty u) -> CR ty t).
Proof.
induction ty as [|ty1 ih1 ty2 ih2]; split;
simpl; eauto using SN_step, SN_stepI.
+ intros t u st_t_u CR_appt v CR_v; generalize (CR_appt _ CR_v).
now destruct ih2 as [ih2 _]; apply ih2; eauto using step.
+ intros t nt clost u CR_u; assert (SN_u := CR_SN CR_u).
revert CR_u; induction SN_u as [u _ ih]; intros CR_u.
destruct ih2 as [ih2 h]; apply h; clear h; trivial.
intros t' st; revert ih2 nt; inversion st using step_app.
* discriminate.
* now clear st t'; intros t' st ih2 _; apply clost.
* clear t' st; intros u' st _ _; apply ih; trivial.
now destruct ih1 as [ih1 _]; apply (ih1 u).
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_step ty t u : step t u -> CR ty t -> CR ty u.
Proof. now case (CR_step_r ty); eauto. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_stepI ty t :
neutral t = true -> (forall u, step t u -> CR ty u) -> CR ty t.
Proof. now case (CR_step_r ty); eauto. Qed.
(* -------------------------------------------------------------------- *)
Inductive sim n : term -> term -> Prop :=
| SimVar x y : n <= x -> n <= y -> sim n (Var x) (Var y)
| SimBnd x : x < n -> sim n (Var x) (Var x)
| SimLam t u : sim (S n) t u -> sim n (Lam t) (Lam u)
| SimApp t1 t2 u1 u2 : sim n t1 u1 -> sim n t2 u2 -> sim n (App t1 t2) (App u1 u2).
(* -------------------------------------------------------------------- *)
Derive Inversion_clear sim_var with
(forall n x u, sim n (Var x) u) Sort Prop.
Derive Inversion_clear sim_app with
(forall n t1 t2 u, sim n (App t1 t2) u) Sort Prop.
Derive Inversion_clear sim_lam with
(forall n t u, sim n (Lam t) u) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma sim_refl n t : sim n t t.
Proof.
revert n; induction t as [x|t1 ih1 t2 ih2|t ih]; intros n.
* case (le_lt_dec n x); intros h.
- now apply SimVar. - now apply SimBnd.
* now apply SimApp.
* now apply SimLam.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_sym n t u : sim n t u -> sim n u t.
Proof. now induction 1; eauto using sim. Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_trans n t u v : sim n t u -> sim n u v -> sim n t v.
Proof. now intros h; revert v; induction h; inversion 1; eauto using sim. Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_weak n p t u : sim n t u -> p <= n -> sim p t u.
Proof.
intros h; revert p; elim h; clear h n t u; intros n.
* now intros x y lex ley p lepn; apply SimVar; omega.
* now intros x ltxn p lepn; apply sim_refl.
* now intros t u h ih p lepn; constructor; apply ih; omega.
* now eauto using sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_ren n t u k f :
(forall i, n <= i -> k <= f i)
-> sim n t u -> sim k t.[ren f] u.[ren f].
Proof.
intros hf h; revert k f hf; elim h; clear h n t u; asimpl.
* now intros n x y lex ley k f hf; apply SimVar; auto.
* now intros n x lt k f hf; apply sim_refl.
* intros n t u sm ih k f hf; constructor; asimpl; apply ih.
intros [|i]; try omega; intros h; apply le_S_n in h.
now asimpl; apply le_n_S; auto.
* now eauto using sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_ren_n n k t u :
sim n t u -> sim (n+k) t.[ren (+k)] u.[ren (+k)].
Proof.
intros h; apply (sim_ren (n := n)); trivial.
now intros i; asimpl; omega.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_renL_r n t k : sim n t t.[loop n up (ren (+k))].
Proof.
revert n; induction t as [x|t1 ih1 t2 ih2|t ih]; asimpl; intros n.
* case (le_lt_dec n x); intros cmp.
- assert (eq : loop n up (ren (+k)) x = Var (x + k)).
+ revert x cmp; induction n as [|n ih]; simpl; intros x cmp.
now rewrite Nat.add_comm.
destruct x as [|x]; asimpl; [omega | idtac].
now rewrite ih; try autosubst; omega.
+ now rewrite eq; apply SimVar; omega.
- assert (eq : loop n up (ren (+k)) x = Var x).
+ revert x cmp; induction n as [|n ih]; simpl; intros x cmp.
omega.
destruct x as [|x]; asimpl; trivial.
now rewrite ih; try autosubst; omega.
+ now rewrite eq; apply SimBnd.
* now constructor.
* now constructor; apply (ih (S n)).
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_renL t k : sim 0 t t.[ren (+k)].
Proof. now apply (@sim_renL_r 0). Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_subst n z t u xit xiu :
(forall k1 k2, z <= k1 -> z <= k2 -> sim n (xit k1) (xiu k2))
-> (forall k, k < z -> sim n (xit k) (xiu k))
-> sim z t u
-> sim n t.[xit] u.[xiu].
Proof.
revert n z u xit xiu; induction t as [x|t1 ih1 t2 ih2|t ih];
intros n z u xit xiu hxio hxi h.
* inversion h using sim_var; clear h.
- now intros y lex ley; asimpl; apply hxio.
- now intros lt; asimpl; apply hxi.
* inversion h using sim_app; intros u1 u2 sm1 sm2.
now eauto using sim.
* inversion h using sim_lam; intros t' sm; constructor; apply (ih _ (S z)).
- intros [|k1] [|k2]; try omega; intros le1 le2.
apply le_S_n in le1; apply le_S_n in le2; asimpl.
rewrite <- Nat.add_1_r; apply sim_ren_n; auto.
- intros [|k]; asimpl; intros cmp.
now apply sim_refl.
rewrite <- Nat.add_1_r; apply sim_ren_n.
now apply lt_S_n in cmp; auto.
- easy.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_subst_0 n t1 t2 u1 u2 :
sim (S n) t1 u1 -> sim n t2 u2 -> sim n t1.[t2/] u1.[u2/].
Proof.
intros h1 h2; apply (sim_subst (z := S n)); trivial.
* intros [|k1] [|k2]; try omega; intros le1 le2.
now apply le_S_n in le1; apply le_S_n in le2; asimpl; apply SimVar.
* now intros [|k]; asimpl; trivial; intros _; apply sim_refl.
Qed.
(* -------------------------------------------------------------------- *)
Lemma step_sim t t' u n :
step t t' -> sim n t u -> exists u', step u u' /\ sim n t' u'.
Proof.
intros h; revert n u; elim h; clear h t t'.
* intros t1 ? t2 ? n u h; subst; inversion h using sim_app; clear h.
intros u1 u2 h; inversion h using sim_lam; clear h u1; intros u1.
intros h1 h2; exists u1.[u2/]; split; [now constructor | idtac].
now apply sim_subst_0.
* intros t t' u st ih n w h; inversion h using sim_app; clear h.
intros t2 u2 smt smu; elim (ih _ _ smt).
now intuition; eauto using step, sim.
* intros t u u' st ih n w h; inversion h using sim_app; clear h.
intros t1 u2 smt smu; elim (ih _ _ smu).
now intuition; eauto using step, sim.
* intros t u st ih n w h; inversion h using sim_lam; clear h.
now intros t2 sm; elim (ih _ _ sm); intuition; eauto using step, sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_sim t : SN t -> forall n u, sim n t u -> SN u.
Proof.
induction 1 as [t acc ih]; intros n u sm; constructor.
intros u' st_u_u'; case (step_sim st_u_u' (sim_sym sm)).
now intros t' [st_t_t' sm']; apply (ih _ st_t_t' _ _ (sim_sym sm')).
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_ren_apps n t us :
SN (fold_left App us t)
-> SN (fold_left App us t.[ren (+n)]).
Proof.
set (u1 := fold_left App us t); set (u2 := fold_left App us t.[ren (+n)]).
intros SN1; assert (h : sim 0 u1 u2).
- subst u1 u2; clear SN1; induction us as [|u us ih] using rev_ind.
+ now simpl; apply sim_renL.
+ rewrite !fold_left_app; simpl; constructor.
* now apply ih. * now apply sim_refl.
- now apply (SN_sim SN1 h).
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_ren_apps n ty t us :
CR ty (fold_left App us t)
-> CR ty (fold_left App us (t.[ren (+n)])).
Proof.
revert us; induction ty as [|ty1 ih1 ty2 ih2]; simpl.
* now intros us; apply SN_ren_apps.
* intros us h v CR1_v; assert (ih2 := ih2 (us ++ v :: nil)).
now rewrite !fold_left_app in ih2; apply ih2; simpl; apply h.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_ren n ty t : CR ty t -> CR ty t.[ren (+n)].
Proof. now apply (@CR_ren_apps n ty t nil). Qed.
(* -------------------------------------------------------------------- *)
Local Notation onth ts i := (nth i ts (Var 0)).
Lemma ty_CR G t A xi :
(forall x, CR (G x) (xi x)) -> ty G t A -> CR A (t.[xi]).
Proof.
intros CR_G h; revert xi CR_G; elim h; clear h G t A; intros G.
+ now intros x A GxA xi CR_G; simpl; rewrite <- GxA; apply CR_G.
+ intros t A B ty_t ih xi CR_G; simpl; intros u CR_u.
assert (SN_t: SN t.[up xi]).
apply (@CR_SN B); apply ih; intros [|n]; asimpl.
* now apply CR_var.
* now apply CR_ren.
* generalize (pairSN_acc SN_t (CR_SN CR_u)).
set (txi := t.[_]); set (zs := (txi :: u :: nil)); intros h; subst txi.
change (t.[up xi]) with (onth zs 0); change u with (onth zs 1).
assert (h1 : forall v, CR A v -> CR B (onth zs 0).[v/]).
intros v CR_v; unfold zs; asimpl; apply ih.
now intros [|n]; asimpl.
assert (h2 : CR A (onth zs 1)) by easy.
assert (h3 : length zs = 2) by easy.
revert h h3 h2 h1; fold zs; intros h; elim h; clear h zs.
intros zs acc ihzs sz_zs CR_zs1 ezs; apply CR_stepI; trivial.
intros v h; inversion h using step_redex; clear h.
now intros ?; subst v; apply ezs.
- intros s h; inversion h using step_lam; clear h s.
intros s sts; apply (ihzs (s :: onth zs 1 :: nil)); trivial.
++ apply (@Step1 _ _ _ nil (onth zs 0) s (onth zs 1 :: nil));
trivial; simpl.
now generalize zs sz_zs; intros [|?[|?[|]]].
++ intros v' CR_v'; simpl; assert (h : step (onth zs 0).[v'/] s.[v'/]).
now apply step_subst.
now apply (@CR_step B) in h; trivial; apply ezs.
- intros s sts; apply (ihzs (onth zs 0 :: s :: nil)); trivial.
++ apply (@Step1 _ _ _ (onth zs 0 :: nil) (onth zs 1) s nil);
trivial; simpl.
now generalize zs sz_zs; intros [|?[|?[|]]].
++ now apply (CR_step sts).
+ intros s t A B ty_s ih_s ty_t ih_t xi CR_G; simpl.
now generalize (ih_s xi CR_G _ (ih_t xi CR_G)).
Qed.
(* -------------------------------------------------------------------- *)
Theorem ty_SN G t A : ty G t A -> SN t.
Proof.
intros hty; apply (@CR_SN A t); assert (hS : forall x, CR (G x) (Var x)).
* now intros x; apply CR_var.
* assert (h := ty_CR (xi := Var) hS hty).
now rewrite <- subst_id; apply h.
Qed.
(* -------------------------------------------------------------------- *)
Print Assumptions ty_SN.
(* -------- *) Require Import Arith List Omega.
From Autosubst Require Import Autosubst.
(* -------------------------------------------------------------------- *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* -------------------------------------------------------------------- *)
Fixpoint loop {T : Type} n (f : T -> T) (x : T) :=
match n with 0 => x | S n => f (loop n f x) end.
(* -------------------------------------------------------------------- *)
Inductive term : Type :=
| Var (_ : var)
| App (_ : term) (_ : term)
| Lam (_ : {bind term}).
(* -------------------------------------------------------------------- *)
Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
(* -------------------------------------------------------------------- *)
Inductive step : term -> term -> Prop :=
| Step_beta (s1 s2 t : term) :
s1.[t/] = s2 -> step (App (Lam s1) t) s2
| Step_appL (s1 s2 t : term) :
step s1 s2 -> step (App s1 t) (App s2 t)
| Step_appR (s t1 t2 : term) :
step t1 t2 -> step (App s t1) (App s t2)
| Step_lam (s1 s2 : term) :
step s1 s2 -> step (Lam s1) (Lam s2).
Notation red := (fun s t => step t s).
Hint Constructors step : ty.
(* -------------------------------------------------------------------- *)
Derive Inversion_clear step_var with
(forall x t, step (Var x) t) Sort Prop.
Derive Inversion_clear step_lam with
(forall s t, step (Lam s) t) Sort Prop.
Derive Inversion_clear step_redex with
(forall s1 s2 t, step (App (Lam s1) s2) t) Sort Prop.
Derive Inversion_clear step_app with
(forall s1 s2 t, step (App s1 s2) t) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma step_subst t u : step t u -> forall xi, step t.[xi] u.[xi].
Proof. now induction 1; constructor; subst; autosubst. Qed.
(* -------------------------------------------------------------------- *)
Inductive type := Base | Arr (_ : type) (_ : type).
(* -------------------------------------------------------------------- *)
Inductive ty (G : var -> type) : term -> type -> Prop :=
| Ty_Var x A :
G x = A -> ty G (Var x) A
| Ty_Lam s A B :
ty (A .: G) s B -> ty G (Lam s) (Arr A B)
| Ty_App s t A B :
ty G s (Arr A B) -> ty G t A -> ty G (App s t) B.
Hint Constructors ty : ty.
(* -------------------------------------------------------------------- *)
Derive Inversion_clear ty_var with
(forall G x A, ty G (Var x) A) Sort Prop.
Derive Inversion_clear ty_lam with
(forall G t A, ty G (Lam t) A) Sort Prop.
Derive Inversion_clear ty_app with
(forall G s t A, ty G (App s t) A) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma ty_ren G s A :
ty G s A -> forall D xi, G = xi >>> D -> ty D s.[ren xi] A.
Proof.
induction 1; intros; subst; asimpl; econstructor; eauto.
- now eapply IHty; autosubst.
Qed.
(* -------------------------------------------------------------------- *)
Lemma ty_subst G s A :
ty G s A -> forall D xi,
(forall x, ty D (xi x) (G x)) -> ty D s.[xi] A.
Proof.
induction 1; intros; subst; asimpl; eauto using ty.
- econstructor; eapply IHty.
now intros [|]; asimpl; eauto using ty, ty_ren.
Qed.
(* -------------------------------------------------------------------- *)
Lemma ty_pres G s A : ty G s A -> forall s', step s s' -> ty G s' A.
Proof.
induction 1; intros s' h; asimpl; inversion h; ainv; eauto using ty.
- eapply ty_subst; try eassumption.
now intros [|]; simpl; eauto using ty.
Qed.
(* -------------------------------------------------------------------- *)
Notation SN := (Acc red).
(* -------------------------------------------------------------------- *)
Definition allSN (ts : list term) := forall t, In t ts -> SN t.
(* -------------------------------------------------------------------- *)
Fact allSN0 : allSN nil.
Proof. easy. Qed.
(* -------------------------------------------------------------------- *)
Fixpoint CR (ty : type) :=
match ty with
| Base => fun t => SN t
| Arr ty1 ty2 => fun t => forall u, CR ty1 u -> CR ty2 (App t u)
end.
(* -------------------------------------------------------------------- *)
Definition neutral (t : term) :=
match t with Lam _ => false | _ => true end.
(* -------------------------------------------------------------------- *)
Lemma SN_stepI t : (forall u, step t u -> SN u) -> SN t.
Proof. now intros h; constructor. Qed.
(* -------------------------------------------------------------------- *)
Inductive subterm : term -> term -> Prop :=
| SubTop t :
subterm t t
| SubAppL t1 t2 u :
subterm t1 u -> subterm (App t1 t2) u
| SubAppR t1 t2 u :
subterm t2 u -> subterm (App t1 t2) u
| SubLam t u :
subterm t u -> subterm (Lam t) u.
Hint Constructors subterm : ty.
(* -------------------------------------------------------------------- *)
Lemma step_subterm t u u' :
subterm t u -> step u u' -> exists t', step t t' /\ subterm t' u'.
Proof.
induction 1; intros; solve
[ exists u'; eauto using subterm
| apply IHsubterm in H0; destruct H0 as [? [? ?]];
eexists; split; econstructor; eauto ].
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_subterm t : SN t -> forall u, subterm t u -> SN u.
Proof.
induction 1 as [t acc ih]; intros u sub_t_u; constructor.
intros u' st_u_u'; case (step_subterm sub_t_u st_u_u').
now intros t' [st_t_t' sub_t'_u']; eauto.
Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_appIL t u : SN (App t u) -> SN t.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_appIR t u : SN (App t u) -> SN u.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Corollary SN_lamI t : SN (Lam t) -> SN t.
Proof. now eauto using SN_subterm, subterm. Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_var n : SN (Var n).
Proof. now ainv. Qed.
Hint Resolve SN_var.
(* -------------------------------------------------------------------- *)
Inductive steps {n : nat} (ts us : list term) : Prop :=
| Step1 ts1 t u ts2
(_ : length ts = n)
(_ : ts = ts1 ++ t :: ts2)
(_ : us = ts1 ++ u :: ts2)
(_ : step t u).
Notation reds n := (fun x y => @steps n y x).
(* -------------------------------------------------------------------- *)
Lemma allSN_acc (ts : list term) :
allSN ts -> forall n, n = length ts -> Acc (reds n) ts.
Proof.
induction ts as [|t ts ih]; intros h n nE.
+ now simpl; constructor; intros us []; case ts1 in H0.
+ revert nE; destruct n as [|n]; try discriminate.
intros nE; injection nE; clear nE; intros nE.
assert (SN_t : SN t) by now apply h; apply in_eq.
assert (SN_ts : Acc (reds n) ts).
- now apply ih; trivial; intros t' t'_ts; auto using in_cons.
- clear ih h; revert ts nE SN_ts; generalize SN_t.
induction SN_t as [t acct iht]; intros SN_t ts nE SN_ts.
revert nE SN_t acct iht; generalize SN_ts.
induction SN_ts as [ts accts ihts]; intros SN_ts nE SN_t acct iht.
constructor; intros us [ts1 t' u' ts2 _ eq usE st_t'_u']; subst us.
destruct ts1 as [|t1' ts1'] in eq |- *; simpl in *.
* injection eq; clear eq; intros; subst t' ts2.
now apply iht; trivial; apply SN_t.
* injection eq; clear eq; intros; subst ts t1'; apply ihts; trivial.
++ now exists ts1' t' u' ts2; trivial; rewrite <- nE.
++ case SN_ts; intros h; apply h.
now exists ts1' t' u' ts2; trivial; rewrite <- nE.
++ now rewrite nE; rewrite !app_length; simpl.
Qed.
(* -------------------------------------------------------------------- *)
Lemma pairSN_acc t u : SN t -> SN u -> Acc (reds 2) (t :: u :: nil).
Proof.
intros SN_t SN_u; apply allSN_acc; trivial.
now intros s; simpl; intuition; subst.
Qed.
(* -------------------------------------------------------------------- *)
Lemma step_apps_varI x ts u :
step (fold_left App ts (Var x)) u
-> exists us, @steps (length ts) ts us /\ u = fold_left App us (Var x).
Proof.
revert u; induction ts as [|t ts ih] using rev_ind; simpl.
+ now intros u; inversion 1.
+ intros u; rewrite fold_left_app; simpl; inversion 1; subst.
* absurd (Lam s1 = fold_left App ts (Var x)); trivial.
clear ih H H0; destruct ts as [|u us] using rev_ind; simpl.
- discriminate.
- now rewrite fold_left_app; simpl; discriminate.
* case (ih _ H3); clear H3; intros us [st ?]; subst s2.
exists (us ++ t :: nil); split; trivial.
destruct st as [ts1 t' u' ts2 _ tsE usE st].
exists ts1 t' u' (ts2 ++ t :: nil); trivial.
- now rewrite tsE, <- app_assoc.
- now rewrite usE, <- app_assoc.
- now rewrite fold_left_app.
* exists (ts ++ t2 :: nil); split.
- now exists ts t t2 nil.
- now rewrite fold_left_app.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_apps_var x ts : allSN ts -> SN (fold_left App ts (Var x)).
Proof.
intros SNts; assert (hn : exists n, n = length ts) by now eexists.
destruct hn as [n eqn]; assert (h := allSN_acc SNts eqn); clear SNts.
revert eqn; induction h as [ts acc ih]; intros eqn.
constructor; intros u st; apply step_apps_varI in st.
destruct st as [us [st uE]]; subst u; apply ih.
+ now rewrite eqn.
+ now destruct st; rewrite eqn; subst ts us; rewrite !app_length.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_step t u : step t u -> SN t -> SN u.
Proof. now intros st_t_u [h]; apply h in st_t_u. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_SN_r ty :
(forall t, CR ty t -> SN t)
/\ (forall n ts, allSN ts -> CR ty (fold_left App ts (Var n))).
Proof.
induction ty as [|ty1 ih1 ty2 ih2]; split; trivial.
+ now intros; apply SN_apps_var.
+ intros t CR_tu; case ih1 as [_ ih1]; generalize (ih1 0 _ allSN0).
simpl in CR_tu |- *; intros CR_0; apply CR_tu in CR_0.
now case ih2; intros h1 h2; apply h1 in CR_0; apply SN_appIL in CR_0.
+ intros n ts SN_ts u CR_u; destruct ih2 as [ih2 h].
generalize (h n (ts ++ u :: nil)); clear h; rewrite fold_left_app.
intros h; apply h; intros s; rewrite in_app_iff; intros hin.
destruct hin as [hin|eq]; eauto; destruct eq as [eq|F].
* now subst u; destruct ih1 as [ih1 _]; auto.
* now case F.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_SN ty t : CR ty t -> SN t.
Proof. now case (CR_SN_r ty); auto. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_var ty n : CR ty (Var n).
Proof.
destruct (CR_SN_r ty) as [_ h].
now generalize (h n nil); eauto using allSN0.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_step_r ty :
(forall t u, step t u -> CR ty t -> CR ty u)
/\ (forall t, neutral t = true -> (forall u, step t u -> CR ty u) -> CR ty t).
Proof.
induction ty as [|ty1 ih1 ty2 ih2]; split;
simpl; eauto using SN_step, SN_stepI.
+ intros t u st_t_u CR_appt v CR_v; generalize (CR_appt _ CR_v).
now destruct ih2 as [ih2 _]; apply ih2; eauto using step.
+ intros t nt clost u CR_u; assert (SN_u := CR_SN CR_u).
revert CR_u; induction SN_u as [u _ ih]; intros CR_u.
destruct ih2 as [ih2 h]; apply h; clear h; trivial.
intros t' st; revert ih2 nt; inversion st using step_app.
* discriminate.
* now clear st t'; intros t' st ih2 _; apply clost.
* clear t' st; intros u' st _ _; apply ih; trivial.
now destruct ih1 as [ih1 _]; apply (ih1 u).
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_step ty t u : step t u -> CR ty t -> CR ty u.
Proof. now case (CR_step_r ty); eauto. Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_stepI ty t :
neutral t = true -> (forall u, step t u -> CR ty u) -> CR ty t.
Proof. now case (CR_step_r ty); eauto. Qed.
(* -------------------------------------------------------------------- *)
Inductive sim n : term -> term -> Prop :=
| SimVar x y : n <= x -> n <= y -> sim n (Var x) (Var y)
| SimBnd x : x < n -> sim n (Var x) (Var x)
| SimLam t u : sim (S n) t u -> sim n (Lam t) (Lam u)
| SimApp t1 t2 u1 u2 : sim n t1 u1 -> sim n t2 u2 -> sim n (App t1 t2) (App u1 u2).
(* -------------------------------------------------------------------- *)
Derive Inversion_clear sim_var with
(forall n x u, sim n (Var x) u) Sort Prop.
Derive Inversion_clear sim_app with
(forall n t1 t2 u, sim n (App t1 t2) u) Sort Prop.
Derive Inversion_clear sim_lam with
(forall n t u, sim n (Lam t) u) Sort Prop.
(* -------------------------------------------------------------------- *)
Lemma sim_refl n t : sim n t t.
Proof.
revert n; induction t as [x|t1 ih1 t2 ih2|t ih]; intros n.
* case (le_lt_dec n x); intros h.
- now apply SimVar. - now apply SimBnd.
* now apply SimApp.
* now apply SimLam.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_sym n t u : sim n t u -> sim n u t.
Proof. now induction 1; eauto using sim. Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_trans n t u v : sim n t u -> sim n u v -> sim n t v.
Proof. now intros h; revert v; induction h; inversion 1; eauto using sim. Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_weak n p t u : sim n t u -> p <= n -> sim p t u.
Proof.
intros h; revert p; elim h; clear h n t u; intros n.
* now intros x y lex ley p lepn; apply SimVar; omega.
* now intros x ltxn p lepn; apply sim_refl.
* now intros t u h ih p lepn; constructor; apply ih; omega.
* now eauto using sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_ren n t u k f :
(forall i, n <= i -> k <= f i)
-> sim n t u -> sim k t.[ren f] u.[ren f].
Proof.
intros hf h; revert k f hf; elim h; clear h n t u; asimpl.
* now intros n x y lex ley k f hf; apply SimVar; auto.
* now intros n x lt k f hf; apply sim_refl.
* intros n t u sm ih k f hf; constructor; asimpl; apply ih.
intros [|i]; try omega; intros h; apply le_S_n in h.
now asimpl; apply le_n_S; auto.
* now eauto using sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_ren_n n k t u :
sim n t u -> sim (n+k) t.[ren (+k)] u.[ren (+k)].
Proof.
intros h; apply (sim_ren (n := n)); trivial.
now intros i; asimpl; omega.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_renL_r n t k : sim n t t.[loop n up (ren (+k))].
Proof.
revert n; induction t as [x|t1 ih1 t2 ih2|t ih]; asimpl; intros n.
* case (le_lt_dec n x); intros cmp.
- assert (eq : loop n up (ren (+k)) x = Var (x + k)).
+ revert x cmp; induction n as [|n ih]; simpl; intros x cmp.
now rewrite Nat.add_comm.
destruct x as [|x]; asimpl; [omega | idtac].
now rewrite ih; try autosubst; omega.
+ now rewrite eq; apply SimVar; omega.
- assert (eq : loop n up (ren (+k)) x = Var x).
+ revert x cmp; induction n as [|n ih]; simpl; intros x cmp.
omega.
destruct x as [|x]; asimpl; trivial.
now rewrite ih; try autosubst; omega.
+ now rewrite eq; apply SimBnd.
* now constructor.
* now constructor; apply (ih (S n)).
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_renL t k : sim 0 t t.[ren (+k)].
Proof. now apply (@sim_renL_r 0). Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_subst n z t u xit xiu :
(forall k1 k2, z <= k1 -> z <= k2 -> sim n (xit k1) (xiu k2))
-> (forall k, k < z -> sim n (xit k) (xiu k))
-> sim z t u
-> sim n t.[xit] u.[xiu].
Proof.
revert n z u xit xiu; induction t as [x|t1 ih1 t2 ih2|t ih];
intros n z u xit xiu hxio hxi h.
* inversion h using sim_var; clear h.
- now intros y lex ley; asimpl; apply hxio.
- now intros lt; asimpl; apply hxi.
* inversion h using sim_app; intros u1 u2 sm1 sm2.
now eauto using sim.
* inversion h using sim_lam; intros t' sm; constructor; apply (ih _ (S z)).
- intros [|k1] [|k2]; try omega; intros le1 le2.
apply le_S_n in le1; apply le_S_n in le2; asimpl.
rewrite <- Nat.add_1_r; apply sim_ren_n; auto.
- intros [|k]; asimpl; intros cmp.
now apply sim_refl.
rewrite <- Nat.add_1_r; apply sim_ren_n.
now apply lt_S_n in cmp; auto.
- easy.
Qed.
(* -------------------------------------------------------------------- *)
Lemma sim_subst_0 n t1 t2 u1 u2 :
sim (S n) t1 u1 -> sim n t2 u2 -> sim n t1.[t2/] u1.[u2/].
Proof.
intros h1 h2; apply (sim_subst (z := S n)); trivial.
* intros [|k1] [|k2]; try omega; intros le1 le2.
now apply le_S_n in le1; apply le_S_n in le2; asimpl; apply SimVar.
* now intros [|k]; asimpl; trivial; intros _; apply sim_refl.
Qed.
(* -------------------------------------------------------------------- *)
Lemma step_sim t t' u n :
step t t' -> sim n t u -> exists u', step u u' /\ sim n t' u'.
Proof.
intros h; revert n u; elim h; clear h t t'.
* intros t1 ? t2 ? n u h; subst; inversion h using sim_app; clear h.
intros u1 u2 h; inversion h using sim_lam; clear h u1; intros u1.
intros h1 h2; exists u1.[u2/]; split; [now constructor | idtac].
now apply sim_subst_0.
* intros t t' u st ih n w h; inversion h using sim_app; clear h.
intros t2 u2 smt smu; elim (ih _ _ smt).
now intuition; eauto using step, sim.
* intros t u u' st ih n w h; inversion h using sim_app; clear h.
intros t1 u2 smt smu; elim (ih _ _ smu).
now intuition; eauto using step, sim.
* intros t u st ih n w h; inversion h using sim_lam; clear h.
now intros t2 sm; elim (ih _ _ sm); intuition; eauto using step, sim.
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_sim t : SN t -> forall n u, sim n t u -> SN u.
Proof.
induction 1 as [t acc ih]; intros n u sm; constructor.
intros u' st_u_u'; case (step_sim st_u_u' (sim_sym sm)).
now intros t' [st_t_t' sm']; apply (ih _ st_t_t' _ _ (sim_sym sm')).
Qed.
(* -------------------------------------------------------------------- *)
Lemma SN_ren_apps n t us :
SN (fold_left App us t)
-> SN (fold_left App us t.[ren (+n)]).
Proof.
set (u1 := fold_left App us t); set (u2 := fold_left App us t.[ren (+n)]).
intros SN1; assert (h : sim 0 u1 u2).
- subst u1 u2; clear SN1; induction us as [|u us ih] using rev_ind.
+ now simpl; apply sim_renL.
+ rewrite !fold_left_app; simpl; constructor.
* now apply ih. * now apply sim_refl.
- now apply (SN_sim SN1 h).
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_ren_apps n ty t us :
CR ty (fold_left App us t)
-> CR ty (fold_left App us (t.[ren (+n)])).
Proof.
revert us; induction ty as [|ty1 ih1 ty2 ih2]; simpl.
* now intros us; apply SN_ren_apps.
* intros us h v CR1_v; assert (ih2 := ih2 (us ++ v :: nil)).
now rewrite !fold_left_app in ih2; apply ih2; simpl; apply h.
Qed.
(* -------------------------------------------------------------------- *)
Lemma CR_ren n ty t : CR ty t -> CR ty t.[ren (+n)].
Proof. now apply (@CR_ren_apps n ty t nil). Qed.
(* -------------------------------------------------------------------- *)
Local Notation onth ts i := (nth i ts (Var 0)).
Lemma ty_CR G t A xi :
(forall x, CR (G x) (xi x)) -> ty G t A -> CR A (t.[xi]).
Proof.
intros CR_G h; revert xi CR_G; elim h; clear h G t A; intros G.
+ now intros x A GxA xi CR_G; simpl; rewrite <- GxA; apply CR_G.
+ intros t A B ty_t ih xi CR_G; simpl; intros u CR_u.
assert (SN_t: SN t.[up xi]).
apply (@CR_SN B); apply ih; intros [|n]; asimpl.
* now apply CR_var.
* now apply CR_ren.
* generalize (pairSN_acc SN_t (CR_SN CR_u)).
set (txi := t.[_]); set (zs := (txi :: u :: nil)); intros h; subst txi.
change (t.[up xi]) with (onth zs 0); change u with (onth zs 1).
assert (h1 : forall v, CR A v -> CR B (onth zs 0).[v/]).
intros v CR_v; unfold zs; asimpl; apply ih.
now intros [|n]; asimpl.
assert (h2 : CR A (onth zs 1)) by easy.
assert (h3 : length zs = 2) by easy.
revert h h3 h2 h1; fold zs; intros h; elim h; clear h zs.
intros zs acc ihzs sz_zs CR_zs1 ezs; apply CR_stepI; trivial.
intros v h; inversion h using step_redex; clear h.
now intros ?; subst v; apply ezs.
- intros s h; inversion h using step_lam; clear h s.
intros s sts; apply (ihzs (s :: onth zs 1 :: nil)); trivial.
++ apply (@Step1 _ _ _ nil (onth zs 0) s (onth zs 1 :: nil));
trivial; simpl.
now generalize zs sz_zs; intros [|?[|?[|]]].
++ intros v' CR_v'; simpl; assert (h : step (onth zs 0).[v'/] s.[v'/]).
now apply step_subst.
now apply (@CR_step B) in h; trivial; apply ezs.
- intros s sts; apply (ihzs (onth zs 0 :: s :: nil)); trivial.
++ apply (@Step1 _ _ _ (onth zs 0 :: nil) (onth zs 1) s nil);
trivial; simpl.
now generalize zs sz_zs; intros [|?[|?[|]]].
++ now apply (CR_step sts).
+ intros s t A B ty_s ih_s ty_t ih_t xi CR_G; simpl.
now generalize (ih_s xi CR_G _ (ih_t xi CR_G)).
Qed.
(* -------------------------------------------------------------------- *)
Theorem ty_SN G t A : ty G t A -> SN t.
Proof.
intros hty; apply (@CR_SN A t); assert (hS : forall x, CR (G x) (Var x)).
* now intros x; apply CR_var.
* assert (h := ty_CR (xi := Var) hS hty).
now rewrite <- subst_id; apply h.
Qed.
(* -------------------------------------------------------------------- *)
Print Assumptions ty_SN.