diff --git a/syntax.sig b/syntax.sig index 5448432..e63c3b4 100644 --- a/syntax.sig +++ b/syntax.sig @@ -14,9 +14,11 @@ PAbs : (bind PTm in PTm) -> PTm PApp : PTm -> PTm -> PTm PPair : PTm -> PTm -> PTm PProj : PTag -> PTm -> PTm -PConst : nat -> PTm +PConst : TTag -> PTm +PUniv : nat -> PTm +PBot : PTm -Abs : Tm -> (bind Tm in Tm) -> Tm +Abs : (bind Tm in Tm) -> Tm App : Tm -> Tm -> Tm Pair : Tm -> Tm -> Tm Proj : PTag -> Tm -> Tm diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 26f4c0d..659d8b0 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -19,13 +19,29 @@ Proof. exact (eq_refl). Qed. +Inductive TTag : Type := + | TPi : TTag + | TSig : TTag. + +Lemma congr_TPi : TPi = TPi. +Proof. +exact (eq_refl). +Qed. + +Lemma congr_TSig : TSig = TSig. +Proof. +exact (eq_refl). +Qed. + Inductive PTm : Type := | VarPTm : nat -> PTm | PAbs : PTm -> PTm | PApp : PTm -> PTm -> PTm | PPair : PTm -> PTm -> PTm | PProj : PTag -> PTm -> PTm - | PConst : nat -> PTm. + | PConst : TTag -> PTm + | PUniv : nat -> PTm + | PBot : PTm. Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0. Proof. @@ -53,12 +69,22 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0)) (ap (fun x => PProj t0 x) H1)). Qed. -Lemma congr_PConst {s0 : nat} {t0 : nat} (H0 : s0 = t0) : +Lemma congr_PConst {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) : PConst s0 = PConst t0. Proof. exact (eq_trans eq_refl (ap (fun x => PConst x) H0)). Qed. +Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)). +Qed. + +Lemma congr_PBot : PBot = PBot. +Proof. +exact (eq_refl). +Qed. + Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat. Proof. exact (up_ren xi). @@ -72,6 +98,8 @@ Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm := | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1) | PConst s0 => PConst s0 + | PUniv s0 => PUniv s0 + | PBot => PBot end. Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm. @@ -87,6 +115,8 @@ Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm := | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1) | PConst s0 => PConst s0 + | PUniv s0 => PUniv s0 + | PBot => PBot end. Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) : @@ -115,6 +145,8 @@ subst_PTm sigma_PTm s = s := (idSubst_PTm sigma_PTm Eq_PTm s1) | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) @@ -145,6 +177,8 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s := | PProj s0 s1 => congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm) @@ -176,6 +210,8 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s := | PProj s0 s1 => congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) @@ -206,6 +242,8 @@ Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) congr_PProj (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm) @@ -240,6 +278,8 @@ Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) congr_PProj (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat) @@ -285,6 +325,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := congr_PProj (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm) @@ -331,6 +373,8 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := congr_PProj (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) : @@ -420,6 +464,8 @@ Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm) | PProj s0 s1 => congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) : @@ -481,23 +527,9 @@ Proof. exact (fun x => eq_refl). Qed. -Inductive TTag : Type := - | TPi : TTag - | TSig : TTag. - -Lemma congr_TPi : TPi = TPi. -Proof. -exact (eq_refl). -Qed. - -Lemma congr_TSig : TSig = TSig. -Proof. -exact (eq_refl). -Qed. - Inductive Tm : Type := | VarTm : nat -> Tm - | Abs : Tm -> Tm -> Tm + | Abs : Tm -> Tm | App : Tm -> Tm -> Tm | Pair : Tm -> Tm -> Tm | Proj : PTag -> Tm -> Tm @@ -507,11 +539,9 @@ Inductive Tm : Type := | Bool : Tm | If : Tm -> Tm -> Tm -> Tm. -Lemma congr_Abs {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0) - (H1 : s1 = t1) : Abs s0 s1 = Abs t0 t1. +Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Abs x s1) H0)) - (ap (fun x => Abs t0 x) H1)). +exact (eq_trans eq_refl (ap (fun x => Abs x) H0)). Qed. Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0) @@ -576,7 +606,7 @@ Defined. Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm := match s with | VarTm s0 => VarTm (xi_Tm s0) - | Abs s0 s1 => Abs (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1) + | Abs s0 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0) | App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) | Pair s0 s1 => Pair (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) | Proj s0 s1 => Proj s0 (ren_Tm xi_Tm s1) @@ -596,7 +626,7 @@ Defined. Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm := match s with | VarTm s0 => sigma_Tm s0 - | Abs s0 s1 => Abs (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1) + | Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0) | App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) | Pair s0 s1 => Pair (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) | Proj s0 s1 => Proj s0 (subst_Tm sigma_Tm s1) @@ -624,9 +654,8 @@ Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm) subst_Tm sigma_Tm s = s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (idSubst_Tm sigma_Tm Eq_Tm s0) - (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1) + | Abs s0 => + congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0) | App s0 s1 => congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) | Pair s0 s1 => @@ -659,10 +688,10 @@ Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) ren_Tm xi_Tm s = ren_Tm zeta_Tm s := match s with | VarTm s0 => ap (VarTm) (Eq_Tm s0) - | Abs s0 s1 => - congr_Abs (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) - (upExtRen_Tm_Tm _ _ Eq_Tm) s1) + (upExtRen_Tm_Tm _ _ Eq_Tm) s0) | App s0 s1 => congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) @@ -698,10 +727,10 @@ Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) subst_Tm sigma_Tm s = subst_Tm tau_Tm s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) - s1) + s0) | App s0 s1 => congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) @@ -733,10 +762,10 @@ Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) (s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s := match s with | VarTm s0 => ap (VarTm) (Eq_Tm s0) - | Abs s0 s1 => - congr_Abs (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) - (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1) + (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0) | App s0 s1 => congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) @@ -775,10 +804,10 @@ Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm) - (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0) | App s0 s1 => congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) @@ -831,10 +860,10 @@ Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm) - (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0) | App s0 s1 => congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) @@ -887,10 +916,10 @@ Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) - (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0) | App s0 s1 => congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) @@ -984,10 +1013,10 @@ Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm) : ren_Tm xi_Tm s = subst_Tm sigma_Tm s := match s with | VarTm s0 => Eq_Tm s0 - | Abs s0 s1 => - congr_Abs (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + | Abs s0 => + congr_Abs (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) - (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1) + (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0) | App s0 s1 => congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) diff --git a/theories/compile.v b/theories/compile.v index 73da296..e481d71 100644 --- a/theories/compile.v +++ b/theories/compile.v @@ -1,47 +1,47 @@ -Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax fp_red. +Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red. Require Import ssreflect ssrbool. From Hammer Require Import Tactics. From stdpp Require Import relations (rtc(..)). Module Compile. - Definition compileTag p := if p is TPi then 0 else 1. - - Fixpoint F (a : Tm) : PTm := + Fixpoint F {n} (a : Tm n) : Tm n := match a with - | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B)) - | Univ i => PConst (3 + i) - | Abs _ a => PAbs (F a) - | App a b => PApp (F a) (F b) - | VarTm i => VarPTm i - | Pair a b => PPair (F a) (F b) - | Proj t a => PProj t (F a) - | If a b c => PApp (PApp (F a) (F b)) (F c) - | BVal b => if b then (PAbs (PAbs (VarPTm (shift var_zero)))) else (PAbs (PAbs (VarPTm var_zero))) - | Bool => PConst 2 + | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B)) + | Const k => Const k + | Univ i => Univ i + | Abs a => Abs (F a) + | App a b => App (F a) (F b) + | VarTm i => VarTm i + | Pair a b => Pair (F a) (F b) + | Proj t a => Proj t (F a) + | Bot => Bot + | If a b c => App (App (F a) (F b)) (F c) + | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero))) + | Bool => Bool end. - Lemma renaming (a : Tm) (ξ : nat -> nat) : - F (ren_Tm ξ a)= ren_PTm ξ (F a). - Proof. move : ξ. elim : a => //=; hauto lq:on. Qed. + Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) : + F (ren_Tm ξ a)= ren_Tm ξ (F a). + Proof. move : m ξ. elim : n / a => //=; hauto lq:on. Qed. #[local]Hint Rewrite Compile.renaming : compile. - Lemma morphing (a : Tm) ρ0 ρ1 : + Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) : (forall i, ρ0 i = F (ρ1 i)) -> - subst_PTm ρ0 (F a) = F (subst_Tm ρ1 a). + subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a). Proof. - move : ρ0 ρ1. elim : a =>//=. - - hauto lq:on inv:nat rew:db:compile unfold:funcomp. + move : m ρ0 ρ1. elim : n / a => n//=. + - hauto lq:on inv:option rew:db:compile unfold:funcomp. - hauto lq:on rew:off. - hauto lq:on rew:off. - hauto lq:on. - - hauto lq:on inv:nat rew:db:compile unfold:funcomp. + - hauto lq:on inv:option rew:db:compile unfold:funcomp. - hauto lq:on rew:off. - hauto lq:on rew:off. Qed. - Lemma substing b (a : Tm) : - subst_PTm (scons (F b) VarPTm) (F a) = F (subst_Tm (scons b VarTm) a). + Lemma substing n b (a : Tm (S n)) : + subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a). Proof. apply morphing. case => //=. @@ -53,55 +53,38 @@ End Compile. Module Join. - Definition R (a b : Tm) := join (Compile.F a) (Compile.F b). + Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b). - Lemma compileTagInj p0 p1 : - Compile.compileTag p0 = Compile.compileTag p1 -> p0 = p1. - Proof. - case : p0 ; case : p1 => //. - Qed. - - Lemma BindInj p0 p1 (A0 A1 : Tm) B0 B1 : + Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1 : R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1. Proof. rewrite /R /= !join_pair_inj. - move => [[/join_const_inj /compileTagInj h0 h1] h2]. + move => [[/join_const_inj h0 h1] h2]. apply abs_eq in h2. - evar (t : PTm ). - have : join (PApp (ren_PTm shift (PAbs (Compile.F B1))) (VarPTm var_zero)) t by + evar (t : Tm (S n)). + have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by apply Join.FromPar; apply Par.AppAbs; auto using Par.refl. - subst t. rewrite -/ren_PTm. - move : h2. move /join_transitive => /[apply]. asimpl; rewrite subst_id => h2. + subst t. rewrite -/ren_Tm. + move : h2. move /join_transitive => /[apply]. asimpl => h2. tauto. Qed. - Lemma BindCong p A0 A1 B0 B1 : - R A0 A1 -> - R B0 B1 -> - R (TBind p A0 B0) (TBind p A1 B1). - Proof. - move => h0 h1. rewrite /R /=. - apply join_pair_inj. - split. apply join_pair_inj. split. apply join_refl. done. - by apply Join.AbsCong. - Qed. + Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j. + Proof. hauto l:on use:join_univ_inj. Qed. - Lemma UnivInj i j : R (Univ i : Tm) (Univ j) -> i = j. - Proof. hauto l:on use:join_const_inj. Qed. - - Lemma transitive (a b c : Tm) : + Lemma transitive n (a b c : Tm n) : R a b -> R b c -> R a c. Proof. hauto l:on use:join_transitive unfold:R. Qed. - Lemma symmetric (a b : Tm) : + Lemma symmetric n (a b : Tm n) : R a b -> R b a. Proof. hauto l:on use:join_symmetric. Qed. - Lemma reflexive (a : Tm) : + Lemma reflexive n (a : Tm n) : R a a. Proof. hauto l:on use:join_refl. Qed. - Lemma substing (a b : Tm) (ρ : nat -> Tm) : + Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : R a b -> R (subst_Tm ρ a) (subst_Tm ρ b). Proof. rewrite /R. @@ -112,3 +95,92 @@ Module Join. Qed. End Join. + +Module Equiv. + Inductive R {n} : Tm n -> Tm n -> Prop := + (***************** Beta ***********************) + | AppAbs a b : + R (App (Abs a) b) (subst_Tm (scons b VarTm) a) + | ProjPair p a b : + R (Proj p (Pair a b)) (if p is PL then a else b) + + (****************** Eta ***********************) + | AppEta a : + R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) + | PairEta a : + R a (Pair (Proj PL a) (Proj PR a)) + + (*************** Congruence ********************) + | Var i : R (VarTm i) (VarTm i) + | AbsCong a b : + R a b -> + R (Abs a) (Abs b) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (App a0 b0) (App a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (Pair a0 b0) (Pair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (Proj p a0) (Proj p a1) + | BindCong p A0 A1 B0 B1: + R A0 A1 -> + R B0 B1 -> + R (TBind p A0 B0) (TBind p A1 B1) + | UnivCong i : + R (Univ i) (Univ i). +End Equiv. + +Module EquivJoin. + Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b. + Proof. + move => h. elim : n a b /h => n. + - move => a b. + rewrite /Join.R /join /=. + eexists. split. apply relations.rtc_once. + apply Par.AppAbs; auto using Par.refl. + rewrite Compile.substing. + apply relations.rtc_refl. + - move => p a b. + apply Join.FromPar. + simpl. apply : Par.ProjPair'; auto using Par.refl. + case : p => //=. + - move => a. apply Join.FromPar => /=. + apply : Par.AppEta'; auto using Par.refl. + by autorewrite with compile. + - move => a. apply Join.FromPar => /=. + apply : Par.PairEta; auto using Par.refl. + - hauto l:on use:Join.FromPar, Par.Var. + - hauto lq:on use:Join.AbsCong. + - qauto l:on use:Join.AppCong. + - qauto l:on use:Join.PairCong. + - qauto use:Join.ProjCong. + - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=. + sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong. + - hauto l:on. + Qed. +End EquivJoin. + +Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b). +Proof. + move => h. elim : n a b /h. + - move => n a0 a1 b0 b1 ha iha hb ihb /=. + rewrite -Compile.substing. + apply RPar'.AppAbs => //. + - hauto q:on use:RPar'.ProjPair'. + - qauto ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. + - hauto lq:on ctrs:RPar'.R. +Qed. + +Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b). +Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed. diff --git a/theories/fp_red.v b/theories/fp_red.v index 7bb5f2e..f9abc08 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -66,7 +66,11 @@ Module Par. R a0 a1 -> R (PProj p a0) (PProj p a1) | ConstCong k : - R (PConst k) (PConst k). + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. Lemma refl (a : PTm) : R a a. elim : a; hauto ctrs:R. @@ -126,6 +130,8 @@ Module Par. - qauto l:on ctrs:R. - qauto l:on ctrs:R. - hauto l:on inv:option ctrs:R use:renaming. + - qauto l:on ctrs:R. + - qauto l:on ctrs:R. Qed. Lemma substing (a b : PTm) (ρ : nat -> PTm) : @@ -198,24 +204,26 @@ Module Par. eexists. split. by apply ProjCong; eauto. done. - hauto q:on inv:PTm ctrs:R. + - hauto q:on inv:PTm ctrs:R. + - hauto q:on inv:PTm ctrs:R. Qed. End Par. Module Pars. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : rtc Par.R a b -> rtc Par.R (ren_PTm ξ a) (ren_PTm ξ b). Proof. induction 1; hauto lq:on ctrs:rtc use:Par.renaming. Qed. - Lemma substing (a b : PTm) (ρ : nat -> PTm) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc Par.R a b -> rtc Par.R (subst_PTm ρ a) (subst_PTm ρ b). induction 1; hauto l:on ctrs:rtc use:Par.substing. Qed. - Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) : + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : rtc Par.R (ren_PTm ξ a) b -> exists b0, rtc Par.R a b0 /\ ren_PTm ξ b0 = b. Proof. move E :(ren_PTm ξ a) => u h. @@ -235,33 +243,41 @@ Module Pars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc Par.R a0 a1 -> rtc Par.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc Par.R a0 a1 -> rtc Par.R b0 b1 -> rtc Par.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc Par.R a0 a1 -> rtc Par.R b0 b1 -> rtc Par.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma AbsCong (a b : PTm) : + Lemma AbsCong n (a b : PTm (S n)) : rtc Par.R a b -> rtc Par.R (PAbs a) (PAbs b). Proof. solve_s. Qed. End Pars. +Definition var_or_const {n} (a : PTm n) := + match a with + | VarPTm _ => true + | PBot => true + | _ => false + end. + + (***************** Beta rules only ***********************) Module RPar. - Inductive R : PTm -> PTm -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> @@ -298,60 +314,64 @@ Module RPar. R a0 a1 -> R (PProj p a0) (PProj p a1) | ConstCong k : - R (PConst k) (PConst k). + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. - Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma refl (a : PTm) : R a a. + Lemma refl n (a : PTm n) : R a a. Proof. induction a; hauto lq:on ctrs:R. Qed. - Lemma AppAbs' a0 a1 (b0 b1 t : PTm) : + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t : + Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : t = (if p is PL then a1 else b1) -> R a0 a1 -> R b0 b1 -> R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : ξ. - elim : a b /h. + move => h. move : m ξ. + elim : n a b /h. move => *; apply : AppAbs'; eauto; by asimpl. all : qauto ctrs:R use:ProjPair'. Qed. - Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) : + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). Proof. eauto using renaming. Qed. - Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) a b : + Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : R a b -> (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). Proof. hauto q:on inv:nat. Qed. - Lemma morphing_up (ρ0 ρ1 : nat -> PTm) : + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. - Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. - move => + h. move : ρ0 ρ1. - elim : a b /h. + move => + h. move : m ρ0 ρ1. + elim : n a b /h. - move => *. apply : AppAbs'; eauto using morphing_up. by asimpl. @@ -364,80 +384,144 @@ Module RPar. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. - Lemma substing (a b : PTm) (ρ : nat -> PTm) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma cong (a b : PTm) c d : + Lemma cong n (a b : PTm (S n)) c d : R a b -> R c d -> R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. - destruct i as [|i]. - - done. - - simpl. apply Var. + qauto l:on ctrs:R inv:nat. Qed. - - Ltac2 rec solve_anti_ren () := - let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in - intro $x; - lazy_match! Constr.type (Control.hyp x) with - | nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R)) - | nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R)) - | _ => solve_anti_ren () - end. - - Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). - - Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) : - R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b. + Lemma var_or_const_imp {n} (a b : PTm n) : + var_or_const a -> + a = b -> ~~ var_or_const b -> False. Proof. - move E : (ren_PTm ρ a) => u h. - move : ρ a E. elim : u b/h; try solve_anti_ren. - - move => a0 a1 b0 b1 ha iha hb ihb ρ []//=. + hauto lq:on inv:PTm. + Qed. + + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (forall i, var_or_const (up_PTm_PTm ρ i)). + Proof. + move => h /= [i|]. + - asimpl. + move /(_ i) in h. + rewrite /funcomp. + move : (ρ i) h. + case => //=. + - sfirstorder. + Qed. + + Local Ltac antiimp := qauto l:on use:var_or_const_imp. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E : (subst_PTm ρ a) => u hρ h. + move : n ρ hρ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. move => c c0 [+ ?]. subst. - case : c => //=. + case : c => //=; first by antiimp. move => c [?]. subst. spec_refl. + have /var_or_const_up hρ' := hρ. + move : iha hρ' => /[apply] iha. + move : ihb hρ => /[apply] ihb. + spec_refl. move : iha => [c1][ih0]?. subst. move : ihb => [c2][ih1]?. subst. eexists. split. apply AppAbs; eauto. by asimpl. - - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ. - move => []//=. - move => []//=. - move => p p0 p1 [*]. subst. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ. + move => []//=; + first by antiimp. + move => []//=; first by antiimp. + move => t t0 t1 [*]. subst. + have {}/iha := hρ => iha. + have {}/ihb := hρ => ihb. + have {}/ihc := hρ => ihc. spec_refl. move : iha => [? [*]]. move : ihb => [? [*]]. - move : ihc => [? [*]]. subst. + move : ihc => [? [*]]. eexists. split. - apply AppPair; hauto. + apply AppPair; hauto. subst. by asimpl. - - move => p a0 a1 ha iha ρ []//=. - move => p0 []//= t [*]. subst. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 []//= t [*]; first by antiimp. subst. + have /var_or_const_up {}/iha := hρ => iha. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjAbs; eauto. by asimpl. - - move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=. - move => p0 []//=. move => t t0[*]. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => p0 []//=; first by antiimp. move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. spec_refl. move : iha => [b0 [? ?]]. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n i m ρ hρ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. + move => t [*]. subst. + have /var_or_const_up {}/iha := hρ => iha. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + by asimpl. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply PairCong; eauto. + by asimpl. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 t [*]. subst. + have {}/iha := (hρ) => iha. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjCong; eauto. reflexivity. + - hauto q:on ctrs:R inv:PTm. + - hauto q:on ctrs:R inv:PTm. + - hauto q:on ctrs:R inv:PTm. Qed. End RPar. (***************** Beta rules only ***********************) Module RPar'. - Inductive R : PTm -> PTm -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> @@ -466,60 +550,64 @@ Module RPar'. R a0 a1 -> R (PProj p a0) (PProj p a1) | ConstCong k : - R (PConst k) (PConst k). + R (PConst k) (PConst k) + | UnivCong i : + R (PUniv i) (PUniv i) + | BotCong : + R PBot PBot. - Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma refl (a : PTm) : R a a. + Lemma refl n (a : PTm n) : R a a. Proof. induction a; hauto lq:on ctrs:R. Qed. - Lemma AppAbs' a0 a1 (b0 b1 t : PTm) : + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t : + Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : t = (if p is PL then a1 else b1) -> R a0 a1 -> R b0 b1 -> R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : ξ. - elim : a b /h. + move => h. move : m ξ. + elim : n a b /h. move => *; apply : AppAbs'; eauto; by asimpl. all : qauto ctrs:R use:ProjPair'. Qed. - Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) : + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). Proof. eauto using renaming. Qed. - Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) a b : + Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : R a b -> (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). Proof. hauto q:on inv:nat. Qed. - Lemma morphing_up (ρ0 ρ1 : nat -> PTm) : + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. - Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. - move => + h. move : ρ0 ρ1. - elim : a b /h. + move => + h. move : m ρ0 ρ1. + elim : n a b /h. - move => *. apply : AppAbs'; eauto using morphing_up. by asimpl. @@ -530,60 +618,123 @@ Module RPar'. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - hauto l:on ctrs:R use:morphing_up. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. - Lemma substing (a b : PTm) (ρ : nat -> PTm) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma cong (a b : PTm) c d : + Lemma cong n (a b : PTm (S n)) c d : R a b -> R c d -> R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. - hauto l:on ctrs:R inv:nat. + qauto l:on ctrs:R inv:nat. Qed. - Ltac2 rec solve_anti_ren () := - let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in - intro $x; - lazy_match! Constr.type (Control.hyp x) with - | nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R)) - | nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R)) - | _ => solve_anti_ren () - end. - - Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). - - Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) : - R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b. + Lemma var_or_const_imp {n} (a b : PTm n) : + var_or_const a -> + a = b -> ~~ var_or_const b -> False. Proof. - move E : (ren_PTm ρ a) => u h. - move : ρ a E. elim : u b/h; try solve_anti_ren. - - move => a0 a1 b0 b1 ha iha hb ihb ρ []//=. - move => []//=. - move => p p0 [*]. subst. + hauto lq:on inv:PTm. + Qed. + + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (forall i, var_or_const (up_PTm_PTm ρ i)). + Proof. + move => h /= [i|]. + - asimpl. + move /(_ i) in h. + rewrite /funcomp. + move : (ρ i) h. + case => //=. + - sfirstorder. + Qed. + + Local Ltac antiimp := qauto l:on use:var_or_const_imp. + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. + Proof. + move E : (subst_PTm ρ a) => u hρ h. + move : n ρ hρ a E. elim : m u b/h. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => c c0 [+ ?]. subst. + case : c => //=; first by antiimp. + move => c [?]. subst. + spec_refl. + have /var_or_const_up hρ' := hρ. + move : iha hρ' => /[apply] iha. + move : ihb hρ => /[apply] ihb. spec_refl. move : iha => [c1][ih0]?. subst. move : ihb => [c2][ih1]?. subst. eexists. split. apply AppAbs; eauto. by asimpl. - - move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=. - move => p0 []//=. move => t t0[*]. + - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => p0 []//=; first by antiimp. move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. spec_refl. move : iha => [b0 [? ?]]. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n i m ρ hρ []//=. + hauto l:on. + - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. + move => t [*]. subst. + have /var_or_const_up {}/iha := hρ => iha. + spec_refl. + move :iha => [b0 [? ?]]. subst. + eexists. split. by apply AbsCong; eauto. + by asimpl. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply AppCong; eauto. + done. + - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; + first by antiimp. + move => t t0[*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + spec_refl. + move : iha => [b0 [? ?]]. subst. + move : ihb => [c0 [? ?]]. subst. + eexists. split. by apply PairCong; eauto. + by asimpl. + - move => n p a0 a1 ha iha m ρ hρ []//=; + first by antiimp. + move => p0 t [*]. subst. + have {}/iha := (hρ) => iha. + spec_refl. + move : iha => [b0 [? ?]]. subst. + eexists. split. apply ProjCong; eauto. reflexivity. + - hauto q:on ctrs:R inv:PTm. + - move => n i n0 ρ hρ []//=; first by antiimp. + hauto l:on. + - hauto q:on inv:PTm ctrs:R. Qed. End RPar'. Module ERed. - Inductive R : PTm -> PTm -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a : R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) @@ -610,30 +761,30 @@ Module ERed. R a0 a1 -> R (PProj p a0) (PProj p a1). - Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma AppEta' a (u : PTm) : + Lemma AppEta' n a (u : PTm n) : u = (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) -> R a u. Proof. move => ->. apply AppEta. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : ξ. - elim : a b /h. + move => h. move : m ξ. + elim : n a b /h. - move => a ξ. + move => n a m ξ. apply AppEta'. by asimpl. all : qauto ctrs:R. Qed. - Lemma substing (a : PTm) b (ρ : nat -> PTm) : + Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. - move => h. move : ρ. elim : a b / h. - move => a ρ /=. + move => h. move : m ρ. elim : n a b / h => n. + move => a m ρ /=. apply : AppEta'; eauto. by asimpl. all : hauto ctrs:R inv:nat use:renaming. Qed. @@ -649,31 +800,31 @@ Module EReds. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong (a b : PTm) : + Lemma AbsCong n (a b : PTm (S n)) : rtc ERed.R a b -> rtc ERed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc ERed.R a0 a1 -> rtc ERed.R b0 b1 -> rtc ERed.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc ERed.R a0 a1 -> rtc ERed.R b0 b1 -> rtc ERed.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc ERed.R a0 a1 -> rtc ERed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. End EReds. Module EPar. - Inductive R : PTm -> PTm -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> @@ -699,41 +850,45 @@ Module EPar. R a0 a1 -> R (PProj p a0) (PProj p a1) | ConstCong k : - R (PConst k) (PConst k). + R (PConst k) (PConst k) + | UnivCong i : + R (PUniv i) (PUniv i) + | BotCong : + R PBot PBot. - Lemma refl (a : PTm) : EPar.R a a. + Lemma refl n (a : PTm n) : EPar.R a a. Proof. induction a; hauto lq:on ctrs:EPar.R. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : ξ. - elim : a b /h. + move => h. move : m ξ. + elim : n a b /h. - move => a0 a1 ha iha ξ /=. - move /(_ ξ) /AppEta : iha. + move => n a0 a1 ha iha m ξ /=. + move /(_ _ ξ) /AppEta : iha. by asimpl. all : qauto ctrs:R. Qed. - Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma AppEta' (a0 a1 b : PTm) : + Lemma AppEta' n (a0 a1 b : PTm n) : b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) -> R a0 a1 -> R a0 b. Proof. move => ->; apply AppEta. Qed. - Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : R a b -> (forall i, R (ρ0 i) (ρ1 i)) -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. - move => h. move : ρ0 ρ1. elim : a b / h. - - move => a0 a1 ha iha ρ0 ρ1 hρ /=. + move => h. move : m ρ0 ρ1. elim : n a b / h => n. + - move => a0 a1 ha iha m ρ0 ρ1 hρ /=. apply : AppEta'; eauto. by asimpl. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. @@ -742,9 +897,11 @@ Module EPar. - hauto q:on ctrs:R. - hauto q:on ctrs:R. - hauto l:on ctrs:R use:renaming inv:nat. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. - Lemma substing a0 a1 (b0 b1 : PTm) : + Lemma substing n a0 a1 (b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1). @@ -757,14 +914,14 @@ End EPar. Module OExp. - Inductive R : PTm -> PTm -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a : R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) | PairEta a : R a (PPair (PProj PL a) (PProj PR a)). - Lemma merge (t a b : PTm) : + Lemma merge n (t a b : PTm n) : rtc R a b -> EPar.R t a -> EPar.R t b. @@ -774,7 +931,7 @@ Module OExp. - hauto q:on ctrs:EPar.R inv:R. Qed. - Lemma commutativity (a b c : PTm) : + Lemma commutativity n (a b c : PTm n) : EPar.R a b -> R a c -> exists d, R b d /\ EPar.R c d. Proof. move => h. @@ -783,7 +940,7 @@ Module OExp. - hauto lq:on ctrs:EPar.R, R. Qed. - Lemma commutativity0 (a b c : PTm) : + Lemma commutativity0 n (a b c : PTm n) : EPar.R a b -> rtc R a c -> exists d, rtc R b d /\ EPar.R c d. Proof. move => + h. move : b. @@ -808,29 +965,29 @@ Module RPars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong (a b : PTm) : + Lemma AbsCong n (a b : PTm (S n)) : rtc RPar.R a b -> rtc RPar.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> rtc RPar.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> rtc RPar.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) : + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc RPar.R a0 a1 -> rtc RPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. @@ -839,12 +996,12 @@ Module RPars. - eauto using RPar.renaming, rtc_l. Qed. - Lemma weakening (a0 a1 : PTm) : + Lemma weakening n (a0 a1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R (ren_PTm shift a0) (ren_PTm shift a1). Proof. apply renaming. Qed. - Lemma Abs_inv (a : PTm) b : + Lemma Abs_inv n (a : PTm (S n)) b : rtc RPar.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar.R a a'. Proof. move E : (PAbs a) => b0 h. move : a E. @@ -853,25 +1010,27 @@ Module RPars. - hauto lq:on ctrs:rtc inv:RPar.R, rtc. Qed. - Lemma morphing (a b : PTm) (ρ : nat -> PTm) : + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc RPar.R a b -> rtc RPar.R (subst_PTm ρ a) (subst_PTm ρ b). Proof. induction 1; qauto l:on ctrs:rtc use:RPar.substing. Qed. - Lemma substing (a b : PTm) c : + Lemma substing n (a b : PTm (S n)) c : rtc RPar.R a b -> rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). Proof. hauto lq:on use:morphing inv:nat. Qed. - Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) : - rtc RPar.R (ren_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ ren_PTm ρ b0 = b. + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + rtc RPar.R (subst_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E :(ren_PTm ρ a) => u h. + move E :(subst_PTm ρ a) => u hρ h. move : a E. elim : u b /h. - sfirstorder. - move => a b c h0 h1 ih1 a0 ?. subst. move /RPar.antirenaming : h0. + move /(_ hρ). move => [b0 [h2 ?]]. subst. hauto lq:on rew:off ctrs:rtc. Qed. @@ -887,29 +1046,29 @@ Module RPars'. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong (a b : PTm) : + Lemma AbsCong n (a b : PTm (S n)) : rtc RPar'.R a b -> rtc RPar'.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R b0 b1 -> rtc RPar'.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R b0 b1 -> rtc RPar'.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) : + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc RPar'.R a0 a1 -> rtc RPar'.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. @@ -918,12 +1077,12 @@ Module RPars'. - eauto using RPar'.renaming, rtc_l. Qed. - Lemma weakening (a0 a1 : PTm) : + Lemma weakening n (a0 a1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R (ren_PTm shift a0) (ren_PTm shift a1). Proof. apply renaming. Qed. - Lemma Abs_inv (a : PTm) b : + Lemma Abs_inv n (a : PTm (S n)) b : rtc RPar'.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar'.R a a'. Proof. move E : (PAbs a) => b0 h. move : a E. @@ -932,41 +1091,34 @@ Module RPars'. - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. Qed. - Lemma morphing (a b : PTm) (ρ : nat -> PTm) : + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc RPar'.R a b -> rtc RPar'.R (subst_PTm ρ a) (subst_PTm ρ b). Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. - Lemma substing (a b : PTm ) c : + Lemma substing n (a b : PTm (S n)) c : rtc RPar'.R a b -> rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). Proof. hauto lq:on use:morphing inv:nat. Qed. - Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) : - rtc RPar'.R (ren_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ ren_PTm ρ b0 = b. + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + rtc RPar'.R (subst_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E :(ren_PTm ρ a) => u h. + move E :(subst_PTm ρ a) => u hρ h. move : a E. elim : u b /h. - sfirstorder. - move => a b c h0 h1 ih1 a0 ?. subst. move /RPar'.antirenaming : h0. + move /(_ hρ). move => [b0 [h2 ?]]. subst. hauto lq:on rew:off ctrs:rtc. Qed. End RPars'. -Lemma subst_id: forall d : PTm, subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) d = d. -Proof. - intros d. - have h : d = subst_PTm VarPTm d by asimpl. - rewrite {2}h. - apply ext_PTm. - destruct x => //=. -Qed. - -Lemma Abs_EPar a (b : PTm) : +Lemma Abs_EPar n a (b : PTm n) : EPar.R (PAbs a) b -> (exists d, EPar.R a d /\ rtc RPar.R (PApp (ren_PTm shift b) (VarPTm var_zero)) d) /\ @@ -976,8 +1128,8 @@ Lemma Abs_EPar a (b : PTm) : Proof. move E : (PAbs a) => u h. move : a E. - elim : u b /h => //=. - - move => a0 a1 ha iha b ?. subst. + elim : n u b /h => //=. + - move => n a0 a1 ha iha b ?. subst. specialize iha with (1 := eq_refl). move : iha => [[d [ih0 ih1]] _]. split; exists d. @@ -992,7 +1144,7 @@ Proof. apply : RPar.ProjAbs. by apply RPar.refl. eauto using RPars.ProjCong, RPars.AbsCong. - - move => ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl). + - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl). move : iha => [_ [d [ih0 ih1]]]. split. + exists (PPair (PProj PL d) (PProj PR d)). @@ -1006,20 +1158,19 @@ Proof. by eauto using RPars.AppCong, rtc_refl. apply relations.rtc_once => /=. apply : RPar.AppAbs'; eauto using RPar.refl. - simpl. f_equal. asimpl. clear. - by rewrite subst_id. + by asimpl. + exists d. repeat split => //. move => p. apply : rtc_l; eauto. hauto q:on use:RPar.ProjPair', RPar.refl. - - move => a0 a1 ha _ ? [*]. subst. + - move => n a0 a1 ha _ ? [*]. subst. split. + exists a1. split => //. - apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl; rewrite subst_id. + apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl. + exists a1. split => // p. apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl. Qed. -Lemma Pair_EPar (a b c : PTm) : +Lemma Pair_EPar n (a b c : PTm n) : EPar.R (PPair a b) c -> (forall p, exists d, rtc RPar.R (PProj p c) d /\ EPar.R (if p is PL then a else b) d) /\ (exists d0 d1, rtc RPar.R (PApp (ren_PTm shift c) (VarPTm var_zero)) @@ -1027,8 +1178,8 @@ Lemma Pair_EPar (a b c : PTm) : EPar.R a d0 /\ EPar.R b d1). Proof. move E : (PPair a b) => u h. move : a b E. - elim : u c /h => //=. - - move => a0 a1 ha iha a b ?. subst. + elim : n u c /h => //=. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). move : iha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. split. @@ -1045,7 +1196,7 @@ Proof. repeat split => //. apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=. by asimpl; renamify. - - move => a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). split => [p|]. + move : iha => [/(_ p) [d [ih0 ih1]] _]. exists d. split=>//. @@ -1060,7 +1211,7 @@ Proof. repeat split => //=. apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl. apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl. - - move => a0 a1 b0 b1 ha _ hb _ a b [*]. subst. + - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst. split. + move => p. exists (if p is PL then a1 else b1). @@ -1072,30 +1223,30 @@ Proof. split => //. Qed. -Lemma commutativity0 (a b0 b1 : PTm) : +Lemma commutativity0 n (a b0 b1 : PTm n) : EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. Proof. move => h. move : b1. - elim : a b0 / h. - - move => a b0 ha iha b1 hb. + elim : n a b0 / h. + - move => n a b0 ha iha b1 hb. move : iha (hb) => /[apply]. move => [c [ih0 ih1]]. exists (PAbs (PApp (ren_PTm shift c) (VarPTm var_zero))). split. + hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. - - move => a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. + - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. move => [c [ih0 ih1]]. exists (PPair (PProj PL c) (PProj PR c)). split. + apply RPars.PairCong; by apply RPars.ProjCong. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. - hauto l:on ctrs:rtc inv:RPar.R. - - move => a0 a1 h ih b1. + - move => n a0 a1 h ih b1. elim /RPar.inv => //= _. move => a2 a3 ? [*]. subst. hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong. - - move => a0 a1 b0 b1 ha iha hb ihb b2. + - move => n a0 a1 b0 b1 ha iha hb ihb b2. elim /RPar.inv => //= _. + move => a2 a3 b3 b4 h0 h1 [*]. subst. move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]]. @@ -1123,7 +1274,7 @@ Proof. apply EPar.PairCong; by apply EPar.AppCong. + hauto lq:on ctrs:EPar.R use:RPars.AppCong. - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. - - move => p a b0 h0 ih0 b1. + - move => n p a b0 h0 ih0 b1. elim /RPar.inv => //= _. + move => ? a0 a1 h [*]. subst. move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]]. @@ -1137,9 +1288,11 @@ Proof. hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - hauto l:on ctrs:EPar.R inv:RPar.R. + - hauto l:on ctrs:EPar.R inv:RPar.R. + - hauto l:on ctrs:EPar.R inv:RPar.R. Qed. -Lemma commutativity1 (a b0 b1 : PTm) : +Lemma commutativity1 n (a b0 b1 : PTm n) : EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. Proof. move => + h. move : b0. @@ -1148,7 +1301,7 @@ Proof. - qauto l:on use:relations.rtc_transitive, commutativity0. Qed. -Lemma commutativity (a b0 b1 : PTm) : +Lemma commutativity n (a b0 b1 : PTm n) : rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c. move => h. move : b1. elim : a b0 /h. - sfirstorder. @@ -1157,96 +1310,124 @@ Lemma commutativity (a b0 b1 : PTm) : hauto q:on ctrs:rtc. Qed. -Lemma Abs_EPar' a (b : PTm) : +Lemma Abs_EPar' n a (b : PTm n) : EPar.R (PAbs a) b -> (exists d, EPar.R a d /\ rtc OExp.R (PAbs d) b). Proof. move E : (PAbs a) => u h. move : a E. - elim : u b /h => //=. - - move => a0 a1 ha iha a ?. subst. + elim : n u b /h => //=. + - move => n a0 a1 ha iha a ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - - move => a0 a1 ha iha a ?. subst. + - move => n a0 a1 ha iha a ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - hauto l:on ctrs:OExp.R. Qed. -Lemma Proj_EPar' p a (b : PTm) : +Lemma Proj_EPar' n p a (b : PTm n) : EPar.R (PProj p a) b -> (exists d, EPar.R a d /\ rtc OExp.R (PProj p d) b). Proof. move E : (PProj p a) => u h. move : p a E. - elim : u b /h => //=. - - move => a0 a1 ha iha a p ?. subst. + elim : n u b /h => //=. + - move => n a0 a1 ha iha a p ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - - move => a0 a1 ha iha a p ?. subst. + - move => n a0 a1 ha iha a p ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - hauto l:on ctrs:OExp.R. Qed. -Lemma App_EPar' (a b u : PTm) : +Lemma App_EPar' n (a b u : PTm n) : EPar.R (PApp a b) u -> (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PApp a0 b0) u). Proof. move E : (PApp a b) => t h. - move : a b E. elim : t u /h => //=. - - move => a0 a1 ha iha a b ?. subst. + move : a b E. elim : n t u /h => //=. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - - move => a0 a1 ha iha a b ?. subst. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - hauto l:on ctrs:OExp.R. Qed. -Lemma Pair_EPar' (a b u : PTm) : +Lemma Pair_EPar' n (a b u : PTm n) : EPar.R (PPair a b) u -> exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PPair a0 b0) u. Proof. move E : (PPair a b) => t h. - move : a b E. elim : t u /h => //=. - - move => a0 a1 ha iha a b ?. subst. + move : a b E. elim : n t u /h => //=. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - - move => a0 a1 ha iha a b ?. subst. + - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - hauto l:on ctrs:OExp.R. Qed. -Lemma Const_EPar' k (u : PTm) : +Lemma Const_EPar' n k (u : PTm n) : EPar.R (PConst k) u -> rtc OExp.R (PConst k) u. move E : (PConst k) => t h. - move : k E. elim : t u /h => //=. - - move => a0 a1 h ih k ?. subst. + move : k E. elim : n t u /h => //=. + - move => n a0 a1 h ih k ?. subst. specialize ih with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - - move => a0 a1 h ih k ?. subst. + - move => n a0 a1 h ih k ?. subst. specialize ih with (1 := eq_refl). hauto lq:on ctrs:OExp.R use:rtc_r. - hauto l:on ctrs:OExp.R. Qed. -Lemma EPar_diamond (c a1 b1 : PTm) : +Lemma Bot_EPar' n (u : PTm n) : + EPar.R (PBot) u -> + rtc OExp.R (PBot) u. + move E : (PBot) => t h. + move : E. elim : n t u /h => //=. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma Univ_EPar' n i (u : PTm n) : + EPar.R (PUniv i) u -> + rtc OExp.R (PUniv i) u. + move E : (PUniv i) => t h. + move : E. elim : n t u /h => //=. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma EPar_diamond n (c a1 b1 : PTm n) : EPar.R c a1 -> EPar.R c b1 -> exists d2, EPar.R a1 d2 /\ EPar.R b1 d2. Proof. - move => h. move : b1. elim : c a1 / h. - - move => c a1 ha iha b1 /iha [d2 [hd0 hd1]]. + move => h. move : b1. elim : n c a1 / h. + - move => n c a1 ha iha b1 /iha [d2 [hd0 hd1]]. exists(PAbs (PApp (ren_PTm shift d2) (VarPTm var_zero))). hauto lq:on ctrs:EPar.R use:EPar.renaming. - hauto lq:on rew:off ctrs:EPar.R. - hauto lq:on use:EPar.refl. - - move => a0 a1 ha iha a2. + - move => n a0 a1 ha iha a2. move /Abs_EPar' => [d [hd0 hd1]]. move : iha hd0; repeat move/[apply]. move => [d2 [h0 h1]]. @@ -1254,21 +1435,21 @@ Proof. move : OExp.commutativity0 hd1; repeat move/[apply]. move => [d1 [hd1 hd2]]. exists d1. hauto lq:on ctrs:EPar.R use:OExp.merge. - - move => a0 a1 b0 b1 ha iha hb ihb c. + - move => n a0 a1 b0 b1 ha iha hb ihb c. move /App_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. have : EPar.R (PApp a2 b2)(PApp a3 b3) by hauto l:on use:EPar.AppCong. move : OExp.commutativity0 h2; repeat move/[apply]. move => [d h]. exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - - move => a0 a1 b0 b1 ha iha hb ihb c. + - move => n a0 a1 b0 b1 ha iha hb ihb c. move /Pair_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. have : EPar.R (PPair a2 b2)(PPair a3 b3) by hauto l:on use:EPar.PairCong. move : OExp.commutativity0 h2; repeat move/[apply]. move => [d h]. exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - - move => p a0 a1 ha iha b. + - move => n p a0 a1 ha iha b. move /Proj_EPar' => [d [/iha [d2 h] h1]] {iha}. have : EPar.R (PProj p d) (PProj p d2) by hauto l:on use:EPar.ProjCong. @@ -1276,9 +1457,11 @@ Proof. move => [d1 h1]. exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - qauto use:Const_EPar', EPar.refl. + - qauto use:Univ_EPar', EPar.refl. + - qauto use:Bot_EPar', EPar.refl. Qed. -Function tstar (a : PTm) := +Function tstar {n} (a : PTm n) := match a with | VarPTm i => a | PAbs a => PAbs (tstar a) @@ -1291,11 +1474,13 @@ Function tstar (a : PTm) := | PProj p (PAbs a) => (PAbs (PProj p (tstar a))) | PProj p a => PProj p (tstar a) | PConst k => PConst k + | PUniv i => PUniv i + | PBot => PBot end. -Lemma RPar_triangle (a : PTm) : forall b, RPar.R a b -> RPar.R b (tstar a). +Lemma RPar_triangle n (a : PTm n) : forall b, RPar.R a b -> RPar.R b (tstar a). Proof. - apply tstar_ind => {a}. + apply tstar_ind => {n a}. - hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R. @@ -1307,9 +1492,11 @@ Proof. - hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. Qed. -Function tstar' (a : PTm) := +Function tstar' {n} (a : PTm n) := match a with | VarPTm i => a | PAbs a => PAbs (tstar' a) @@ -1319,11 +1506,13 @@ Function tstar' (a : PTm) := | PProj p (PPair a b) => if p is PL then (tstar' a) else (tstar' b) | PProj p a => PProj p (tstar' a) | PConst k => PConst k + | PUniv i => PUniv i + | PBot => PBot end. -Lemma RPar'_triangle (a : PTm) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). +Lemma RPar'_triangle n (a : PTm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). Proof. - apply tstar'_ind => {a}. + apply tstar'_ind => {n a}. - hauto lq:on inv:RPar'.R ctrs:RPar'.R. - hauto lq:on inv:RPar'.R ctrs:RPar'.R. - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R. @@ -1333,21 +1522,23 @@ Proof. - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. - hauto lq:on inv:RPar'.R ctrs:RPar'.R. - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. + - hauto lq:on inv:RPar'.R ctrs:RPar'.R. Qed. -Lemma RPar_diamond (c a1 b1 : PTm) : +Lemma RPar_diamond n (c a1 b1 : PTm n) : RPar.R c a1 -> RPar.R c b1 -> exists d2, RPar.R a1 d2 /\ RPar.R b1 d2. Proof. hauto l:on use:RPar_triangle. Qed. -Lemma RPar'_diamond (c a1 b1 : PTm) : +Lemma RPar'_diamond n (c a1 b1 : PTm n) : RPar'.R c a1 -> RPar'.R c b1 -> exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2. Proof. hauto l:on use:RPar'_triangle. Qed. -Lemma RPar_confluent (c a1 b1 : PTm) : +Lemma RPar_confluent n (c a1 b1 : PTm n) : rtc RPar.R c a1 -> rtc RPar.R c b1 -> exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2. @@ -1355,7 +1546,7 @@ Proof. sfirstorder use:relations.diamond_confluent, RPar_diamond. Qed. -Lemma EPar_confluent (c a1 b1 : PTm) : +Lemma EPar_confluent n (c a1 b1 : PTm n) : rtc EPar.R c a1 -> rtc EPar.R c b1 -> exists d2, rtc EPar.R a1 d2 /\ rtc EPar.R b1 d2. @@ -1363,7 +1554,7 @@ Proof. sfirstorder use:relations.diamond_confluent, EPar_diamond. Qed. -Inductive prov : PTm -> PTm -> Prop := +Inductive prov {n} : PTm n -> PTm n -> Prop := | P_Abs h a : (forall b, prov h (subst_PTm (scons b VarPTm) a)) -> prov h (PAbs a) @@ -1380,16 +1571,20 @@ Inductive prov : PTm -> PTm -> Prop := | P_Const k : prov (PConst k) (PConst k) | P_Var i : - prov (VarPTm i) (VarPTm i). + prov (VarPTm i) (VarPTm i) +| P_Univ i : + prov (PUniv i) (PUniv i) +| P_Bot : + prov PBot PBot. -Lemma ERed_EPar (a b : PTm) : ERed.R a b -> EPar.R a b. +Lemma ERed_EPar n (a b : PTm n) : ERed.R a b -> EPar.R a b. Proof. induction 1; hauto lq:on ctrs:EPar.R use:EPar.refl. Qed. -Lemma EPar_ERed (a b : PTm) : EPar.R a b -> rtc ERed.R a b. +Lemma EPar_ERed n (a b : PTm n) : EPar.R a b -> rtc ERed.R a b. Proof. - move => h. elim : a b /h. + move => h. elim : n a b /h. - eauto using rtc_r, ERed.AppEta. - eauto using rtc_r, ERed.PairEta. - auto using rtc_refl. @@ -1398,29 +1593,31 @@ Proof. - eauto using EReds.PairCong. - eauto using EReds.ProjCong. - auto using rtc_refl. + - auto using rtc_refl. + - auto using rtc_refl. Qed. -Lemma EPar_Par (a b : PTm) : EPar.R a b -> Par.R a b. +Lemma EPar_Par n (a b : PTm n) : EPar.R a b -> Par.R a b. Proof. - move => h. elim : a b /h; qauto ctrs:Par.R. + move => h. elim : n a b /h; qauto ctrs:Par.R. Qed. -Lemma RPar_Par (a b : PTm) : RPar.R a b -> Par.R a b. +Lemma RPar_Par n (a b : PTm n) : RPar.R a b -> Par.R a b. Proof. - move => h. elim : a b /h; hauto lq:on ctrs:Par.R. + move => h. elim : n a b /h; hauto lq:on ctrs:Par.R. Qed. -Lemma rtc_idem (R : PTm -> PTm -> Prop) (a b : PTm) : rtc (rtc R) a b -> rtc R a b. +Lemma rtc_idem n (R : PTm n -> PTm n -> Prop) (a b : PTm n) : rtc (rtc R) a b -> rtc R a b. Proof. induction 1; hauto l:on use:@relations.rtc_transitive, @rtc_r. Qed. -Lemma EPars_EReds (a b : PTm) : rtc EPar.R a b <-> rtc ERed.R a b. +Lemma EPars_EReds {n} (a b : PTm n) : rtc EPar.R a b <-> rtc ERed.R a b. Proof. sfirstorder use:@relations.rtc_subrel, EPar_ERed, rtc_idem, ERed_EPar. Qed. -Lemma prov_rpar (u : PTm) a b : prov u a -> RPar.R a b -> prov u b. +Lemma prov_rpar n (u : PTm n) a b : prov u a -> RPar.R a b -> prov u b. Proof. move => h. move : b. @@ -1449,22 +1646,24 @@ Proof. + hauto lq:on ctrs:prov. - hauto lq:on ctrs:prov inv:RPar.R. - hauto l:on ctrs:RPar.R inv:RPar.R. + - hauto l:on ctrs:RPar.R inv:RPar.R. + - hauto l:on ctrs:RPar.R inv:RPar.R. Qed. -Lemma prov_lam (u : PTm) a : prov u a <-> prov u (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))). +Lemma prov_lam n (u : PTm n) a : prov u a <-> prov u (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))). Proof. split. move => h. constructor. move => b. asimpl. by constructor. inversion 1; subst. - specialize H2 with (b := (VarPTm var_zero)). + specialize H2 with (b := PBot). move : H2. asimpl. inversion 1; subst. done. Qed. -Lemma prov_pair (u : PTm) a : prov u a <-> prov u (PPair (PProj PL a) (PProj PR a)). +Lemma prov_pair n (u : PTm n) a : prov u a <-> prov u (PPair (PProj PL a) (PProj PR a)). Proof. hauto lq:on inv:prov ctrs:prov. Qed. -Lemma prov_ered (u : PTm) a b : prov u a -> ERed.R a b -> prov u b. +Lemma prov_ered n (u : PTm n) a b : prov u a -> ERed.R a b -> prov u b. Proof. move => h. move : b. @@ -1492,66 +1691,74 @@ Proof. - hauto lq:on inv:ERed.R, prov ctrs:prov. - hauto lq:on inv:ERed.R, prov ctrs:prov. - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. + - hauto lq:on inv:ERed.R, prov ctrs:prov. Qed. -Lemma prov_ereds (u : PTm) a b : prov u a -> rtc ERed.R a b -> prov u b. +Lemma prov_ereds n (u : PTm n) a b : prov u a -> rtc ERed.R a b -> prov u b. Proof. induction 2; sfirstorder use:prov_ered. Qed. -Fixpoint extract (a : PTm) : PTm := +Fixpoint extract {n} (a : PTm n) : PTm n := match a with - | PAbs a => subst_PTm (scons (PConst 0) VarPTm) (extract a) + | PAbs a => subst_PTm (scons PBot VarPTm) (extract a) | PApp a b => extract a | PPair a b => extract a | PProj p a => extract a | PConst k => PConst k | VarPTm i => VarPTm i + | PUniv i => PUniv i + | PBot => PBot end. -Lemma ren_extract (a : PTm) (ξ : nat -> nat) : +Lemma ren_extract n m (a : PTm n) (ξ : fin n -> fin m) : extract (ren_PTm ξ a) = ren_PTm ξ (extract a). Proof. - move : ξ. elim : a. + move : m ξ. elim : n/a. - sfirstorder. - - move => a ih ξ /=. + - move => n a ih m ξ /=. rewrite ih. by asimpl. - hauto q:on. - hauto q:on. - hauto q:on. - hauto q:on. + - sfirstorder. + - sfirstorder. Qed. -Lemma ren_morphing (a : PTm) (ρ : nat -> PTm) : +Lemma ren_morphing n m (a : PTm n) (ρ : fin n -> PTm m) : (forall i, ρ i = extract (ρ i)) -> extract (subst_PTm ρ a) = subst_PTm ρ (extract a). Proof. - move : ρ. - elim : a => //=. - move => a ha ρ hi. + move : m ρ. + elim : n /a => n //=. + move => a ha m ρ hi. rewrite ha. - - destruct i as [|i] => //. + - destruct i as [i|] => //. rewrite ren_extract. rewrite -hi. by asimpl. - by asimpl. Qed. -Lemma ren_subst_bot (a : PTm) : - extract (subst_PTm (scons (PConst 0) VarPTm) a) = subst_PTm (scons (PConst 0) VarPTm) (extract a). +Lemma ren_subst_bot n (a : PTm (S n)) : + extract (subst_PTm (scons PBot VarPTm) a) = subst_PTm (scons PBot VarPTm) (extract a). Proof. - apply ren_morphing. destruct i => //=. + apply ren_morphing. destruct i as [i|] => //=. Qed. -Definition prov_extract_spec u (a : PTm) := +Definition prov_extract_spec {n} u (a : PTm n) := match u with + | PUniv i => extract a = PUniv i | VarPTm i => extract a = VarPTm i | (PConst i) => extract a = (PConst i) + | PBot => extract a = PBot | _ => True end. -Lemma prov_extract u (a : PTm) : +Lemma prov_extract n u (a : PTm n) : prov u a -> prov_extract_spec u a. Proof. move => h. @@ -1559,35 +1766,42 @@ Proof. - move => h a ha ih. case : h ha ih => //=. + move => i ha ih. - move /(_ (PConst 0)) in ih. + move /(_ PBot) in ih. rewrite -ih. by rewrite ren_subst_bot. - + move => p _ /(_ (PConst 0)). + + move => p _ /(_ PBot). + by rewrite ren_subst_bot. + + move => i h /(_ PBot). + by rewrite ren_subst_bot => ->. + + move /(_ PBot). + move => h /(_ PBot). by rewrite ren_subst_bot. - hauto lq:on. - hauto lq:on. - hauto lq:on. - case => //=. - sfirstorder. + - sfirstorder. + - sfirstorder. Qed. Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b := R0 a b \/ R1 a b. Module ERPar. - Definition R (a b : PTm) := union RPar.R EPar.R a b. - Lemma RPar (a b : PTm) : RPar.R a b -> R a b. + Definition R {n} (a b : PTm n) := union RPar.R EPar.R a b. + Lemma RPar {n} (a b : PTm n) : RPar.R a b -> R a b. Proof. sfirstorder. Qed. - Lemma EPar (a b : PTm) : EPar.R a b -> R a b. + Lemma EPar {n} (a b : PTm n) : EPar.R a b -> R a b. Proof. sfirstorder. Qed. - Lemma refl ( a : PTm) : ERPar.R a a. + Lemma refl {n} ( a : PTm n) : ERPar.R a a. Proof. sfirstorder use:RPar.refl, EPar.refl. Qed. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : R a0 a1 -> rtc R (PProj p a0) (PProj p a1). Proof. @@ -1602,7 +1816,7 @@ Module ERPar. by apply EPar.ProjCong. Qed. - Lemma AbsCong (a0 a1 : PTm) : + Lemma AbsCong n (a0 a1 : PTm (S n)) : R a0 a1 -> rtc R (PAbs a0) (PAbs a1). Proof. @@ -1617,7 +1831,7 @@ Module ERPar. by apply EPar.AbsCong. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> rtc R (PApp a0 b0) (PApp a1 b1). @@ -1637,7 +1851,7 @@ Module ERPar. - sfirstorder use:EPar.AppCong, @rtc_once. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> rtc R (PPair a0 b0) (PPair a1 b1). @@ -1657,7 +1871,7 @@ Module ERPar. - sfirstorder use:EPar.PairCong, @rtc_once. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. sfirstorder use:EPar.renaming, RPar.renaming. @@ -1674,29 +1888,29 @@ Module ERPars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc ERPar.R a0 a1 -> rtc ERPar.R b0 b1 -> rtc ERPar.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma AbsCong (a0 a1 : PTm) : + Lemma AbsCong n (a0 a1 : PTm (S n)) : rtc ERPar.R a0 a1 -> rtc ERPar.R (PAbs a0) (PAbs a1). Proof. solve_s. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc ERPar.R a0 a1 -> rtc ERPar.R b0 b1 -> rtc ERPar.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc ERPar.R a0 a1 -> rtc ERPar.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) : + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc ERPar.R a0 a1 -> rtc ERPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. @@ -1707,35 +1921,35 @@ Module ERPars. End ERPars. -Lemma ERPar_Par (a b : PTm) : ERPar.R a b -> Par.R a b. +Lemma ERPar_Par n (a b : PTm n) : ERPar.R a b -> Par.R a b. Proof. sfirstorder use:EPar_Par, RPar_Par. Qed. -Lemma Par_ERPar (a b : PTm) : Par.R a b -> rtc ERPar.R a b. +Lemma Par_ERPar n (a b : PTm n) : Par.R a b -> rtc ERPar.R a b. Proof. - move => h. elim : a b /h. - - move => a0 a1 b0 b1 ha iha hb ihb. + move => h. elim : n a b /h. + - move => n a0 a1 b0 b1 ha iha hb ihb. suff ? : rtc ERPar.R (PApp (PAbs a0) b0) (PApp (PAbs a1) b1). apply : relations.rtc_transitive; eauto. apply rtc_once. apply ERPar.RPar. by apply RPar.AppAbs; eauto using RPar.refl. eauto using ERPars.AppCong,ERPars.AbsCong. - - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc. apply : rtc_l. apply ERPar.RPar. apply RPar.AppPair; eauto using RPar.refl. sfirstorder use:ERPars.AppCong, ERPars.PairCong. - - move => p a0 a1 ha iha. + - move => n p a0 a1 ha iha. apply : rtc_l. apply ERPar.RPar. apply RPar.ProjAbs; eauto using RPar.refl. sfirstorder use:ERPars.AbsCong, ERPars.ProjCong. - - move => p a0 a1 b0 b1 ha iha hb ihb. + - move => n p a0 a1 b0 b1 ha iha hb ihb. apply : rtc_l. apply ERPar.RPar. apply RPar.ProjPair; eauto using RPar.refl. hauto lq:on. - - move => a0 a1 ha iha. + - move => n a0 a1 ha iha. apply : rtc_l. apply ERPar.EPar. apply EPar.AppEta; eauto using EPar.refl. hauto lq:on ctrs:rtc use:ERPars.AppCong, ERPars.AbsCong, ERPars.renaming. - - move => a0 a1 ha iha. + - move => n a0 a1 ha iha. apply : rtc_l. apply ERPar.EPar. apply EPar.PairEta; eauto using EPar.refl. sfirstorder use:ERPars.PairCong, ERPars.ProjCong. - sfirstorder. @@ -1744,46 +1958,48 @@ Proof. - sfirstorder use:ERPars.PairCong. - sfirstorder use:ERPars.ProjCong. - sfirstorder. + - sfirstorder. + - sfirstorder. Qed. -Lemma Pars_ERPar (a b : PTm) : rtc Par.R a b -> rtc ERPar.R a b. +Lemma Pars_ERPar n (a b : PTm n) : rtc Par.R a b -> rtc ERPar.R a b. Proof. induction 1; hauto l:on use:Par_ERPar, @relations.rtc_transitive. Qed. -Lemma Par_ERPar_iff (a b : PTm) : rtc Par.R a b <-> rtc ERPar.R a b. +Lemma Par_ERPar_iff n (a b : PTm n) : rtc Par.R a b <-> rtc ERPar.R a b. Proof. split. sfirstorder use:Pars_ERPar, @relations.rtc_subrel. sfirstorder use:ERPar_Par, @relations.rtc_subrel. Qed. -Lemma RPar_ERPar (a b : PTm) : rtc RPar.R a b -> rtc ERPar.R a b. +Lemma RPar_ERPar n (a b : PTm n) : rtc RPar.R a b -> rtc ERPar.R a b. Proof. sfirstorder use:@relations.rtc_subrel. Qed. -Lemma EPar_ERPar (a b : PTm) : rtc EPar.R a b -> rtc ERPar.R a b. +Lemma EPar_ERPar n (a b : PTm n) : rtc EPar.R a b -> rtc ERPar.R a b. Proof. sfirstorder use:@relations.rtc_subrel. Qed. Module Type HindleyRosen. - Parameter A : Type. - Parameter R0 R1 : A -> A -> Prop. - Axiom diamond_R0 : relations.diamond R0. - Axiom diamond_R1 : relations.diamond R1. - Axiom commutativity : - forall a b c, R0 a b -> R1 a c -> exists d, R1 b d /\ R0 c d. + Parameter A : nat -> Type. + Parameter R0 R1 : forall n, A n -> A n -> Prop. + Axiom diamond_R0 : forall n, relations.diamond (R0 n). + Axiom diamond_R1 : forall n, relations.diamond (R1 n). + Axiom commutativity : forall n, + forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d. End HindleyRosen. Module HindleyRosenFacts (M : HindleyRosen). Import M. Lemma R0_comm : - forall a b c, R0 a b -> rtc (union R0 R1) a c -> - exists d, rtc (union R0 R1) b d /\ R0 c d. + forall n a b c, R0 n a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ R0 n c d. Proof. - move => a + c + h. + move => n a + c + h. elim : a c /h. - sfirstorder. - move => a0 a1 a2 ha ha0 ih b h. @@ -1795,10 +2011,10 @@ Module HindleyRosenFacts (M : HindleyRosen). Qed. Lemma R1_comm : - forall a b c, R1 a b -> rtc (union (R0) (R1)) a c -> - exists d, rtc (union (R0) (R1)) b d /\ R1 c d. + forall n a b c, R1 n a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ R1 n c d. Proof. - move => a + c + h. + move => n a + c + h. elim : a c /h. - sfirstorder. - move => a0 a1 a2 ha ha0 ih b h. @@ -1810,17 +2026,17 @@ Module HindleyRosenFacts (M : HindleyRosen). Qed. Lemma U_comm : - forall a b c, (union R0 R1) a b -> rtc (union R0 R1) a c -> - exists d, rtc (union R0 R1) b d /\ (union R0 R1) c d. + forall n a b c, (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ (union (R0 n) (R1 n)) c d. Proof. hauto lq:on use:R0_comm, R1_comm. Qed. Lemma U_comms : - forall a b c, rtc (union R0 R1) a b -> rtc (union R0 R1) a c -> - exists d, rtc (union R0 R1) b d /\ rtc (union R0 R1) c d. + forall n a b c, rtc (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c -> + exists d, rtc (union (R0 n) (R1 n)) b d /\ rtc (union (R0 n) (R1 n)) c d. Proof. - move => a b + h. + move => n a b + h. elim : a b /h. - sfirstorder. - hecrush ctrs:rtc use:U_comm. @@ -1830,15 +2046,16 @@ End HindleyRosenFacts. Module HindleyRosenER <: HindleyRosen. Definition A := PTm. - Definition R0 := rtc (@RPar.R ). - Definition R1 := rtc (@EPar.R ). - Lemma diamond_R0 : relations.diamond (R0). + Definition R0 n := rtc (@RPar.R n). + Definition R1 n := rtc (@EPar.R n). + Lemma diamond_R0 : forall n, relations.diamond (R0 n). sfirstorder use:RPar_confluent. Qed. - Lemma diamond_R1 : relations.diamond (R1). + Lemma diamond_R1 : forall n, relations.diamond (R1 n). sfirstorder use:EPar_confluent. Qed. - Lemma commutativity : forall a b c, R0 a b -> R1 a c -> exists d, R1 b d /\ R0 c d. + Lemma commutativity : forall n, + forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d. Proof. hauto l:on use:commutativity. Qed. @@ -1846,7 +2063,7 @@ End HindleyRosenER. Module ERFacts := HindleyRosenFacts HindleyRosenER. -Lemma rtc_union (a b : PTm) : +Lemma rtc_union n (a b : PTm n) : rtc (union RPar.R EPar.R) a b <-> rtc (union (rtc RPar.R) (rtc EPar.R)) a b. Proof. @@ -1868,7 +2085,7 @@ Proof. sfirstorder. Qed. -Lemma prov_erpar (u : PTm) a b : prov u a -> ERPar.R a b -> prov u b. +Lemma prov_erpar n (u : PTm n) a b : prov u a -> ERPar.R a b -> prov u b. Proof. move => h []. - sfirstorder use:prov_rpar. @@ -1876,7 +2093,7 @@ Proof. sfirstorder use:prov_ereds. Qed. -Lemma prov_pars (u : PTm) a b : prov u a -> rtc Par.R a b -> prov u b. +Lemma prov_pars n (u : PTm n) a b : prov u a -> rtc Par.R a b -> prov u b. Proof. move => h /Pars_ERPar. move => h0. @@ -1886,41 +2103,51 @@ Proof. - hauto lq:on use:prov_erpar. Qed. -Lemma Par_confluent (a b c : PTm) : +Lemma Par_confluent n (a b c : PTm n) : rtc Par.R a b -> rtc Par.R a c -> exists d, rtc Par.R b d /\ rtc Par.R c d. Proof. - move : a b c. - suff : forall (a b c : PTm), + move : n a b c. + suff : forall (n : nat) (a b c : PTm n), rtc ERPar.R a b -> - rtc ERPar.R a c -> exists d : PTm, rtc ERPar.R b d /\ rtc ERPar.R c d. - move => h a b c h0 h1. + rtc ERPar.R a c -> exists d : PTm n, rtc ERPar.R b d /\ rtc ERPar.R c d. + move => h n a b c h0 h1. apply Par_ERPar_iff in h0, h1. move : h h0 h1; repeat move/[apply]. hauto lq:on use:Par_ERPar_iff. have h := ERFacts.U_comms. - move => a b c. + move => n a b c. rewrite /HindleyRosenER.R0 /HindleyRosenER.R1 in h. + specialize h with (n := n). rewrite /HindleyRosenER.A in h. rewrite /ERPar.R. - have eq : (fun a0 b0 : PTm => union RPar.R EPar.R a0 b0) = union RPar.R EPar.R by reflexivity. + have eq : (fun a0 b0 : PTm n => union RPar.R EPar.R a0 b0) = union RPar.R EPar.R by reflexivity. rewrite !{}eq. move /rtc_union => + /rtc_union. move : h; repeat move/[apply]. hauto lq:on use:rtc_union. Qed. -Lemma pars_const_inv i (c : PTm) : - rtc Par.R (PConst i) c -> - extract c = PConst i. +Lemma pars_univ_inv n i (c : PTm n) : + rtc Par.R (PUniv i) c -> + extract c = PUniv i. Proof. - have : prov (PConst i) (PConst i : PTm) by sfirstorder. + have : prov (PUniv i) (PUniv i : PTm n) by sfirstorder. move : prov_pars. repeat move/[apply]. apply prov_extract. Qed. -Lemma pars_var_inv (i : nat) C : +Lemma pars_const_inv n i (c : PTm n) : + rtc Par.R (PConst i) c -> + extract c = PConst i. +Proof. + have : prov (PConst i) (PConst i : PTm n) by sfirstorder. + move : prov_pars. repeat move/[apply]. + apply prov_extract. +Qed. + +Lemma pars_var_inv n (i : fin n) C : rtc Par.R (VarPTm i) C -> extract C = VarPTm i. Proof. @@ -1929,7 +2156,15 @@ Proof. apply prov_extract. Qed. -Lemma pars_const_inj i j (C : PTm) : +Lemma pars_univ_inj n i j (C : PTm n) : + rtc Par.R (PUniv i) C -> + rtc Par.R (PUniv j) C -> + i = j. +Proof. + sauto l:on use:pars_univ_inv. +Qed. + +Lemma pars_const_inj n i j (C : PTm n) : rtc Par.R (PConst i) C -> rtc Par.R (PConst j) C -> i = j. @@ -1937,10 +2172,10 @@ Proof. sauto l:on use:pars_const_inv. Qed. -Definition join (a b : PTm) := +Definition join {n} (a b : PTm n) := exists c, rtc Par.R a c /\ rtc Par.R b c. -Lemma join_transitive (a b c : PTm) : +Lemma join_transitive n (a b c : PTm n) : join a b -> join b c -> join a c. Proof. rewrite /join. @@ -1950,90 +2185,100 @@ Proof. eauto using relations.rtc_transitive. Qed. -Lemma join_symmetric (a b : PTm) : +Lemma join_symmetric n (a b : PTm n) : join a b -> join b a. Proof. sfirstorder unfold:join. Qed. -Lemma join_refl (a : PTm) : join a a. +Lemma join_refl n (a : PTm n) : join a a. Proof. hauto lq:on ctrs:rtc unfold:join. Qed. -Lemma join_const_inj i j : - join (PConst i : PTm) (PConst j) -> i = j. +Lemma join_univ_inj n i j : + join (PUniv i : PTm n) (PUniv j) -> i = j. +Proof. + sfirstorder use:pars_univ_inj. +Qed. + +Lemma join_const_inj n i j : + join (PConst i : PTm n) (PConst j) -> i = j. Proof. sfirstorder use:pars_const_inj. Qed. -Lemma join_substing (a b : PTm) (ρ : nat -> PTm) : +Lemma join_substing n m (a b : PTm n) (ρ : fin n -> PTm m) : join a b -> join (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto lq:on unfold:join use:Pars.substing. Qed. -Fixpoint ne (a : PTm) := +Fixpoint ne {n} (a : PTm n) := match a with | VarPTm i => true | PApp a b => ne a && nf b | PAbs a => false + | PUniv _ => false | PProj _ a => ne a | PPair _ _ => false | PConst _ => false + | PBot => true end -with nf (a : PTm) := +with nf {n} (a : PTm n) := match a with | VarPTm i => true | PApp a b => ne a && nf b | PAbs a => nf a + | PUniv _ => true | PProj _ a => ne a | PPair a b => nf a && nf b | PConst _ => true + | PBot => true end. -Lemma ne_nf a : ne a -> nf a. +Lemma ne_nf n a : @ne n a -> nf a. Proof. elim : a => //=. Qed. -Definition wn (a : PTm) := exists b, rtc RPar'.R a b /\ nf b. -Definition wne (a : PTm) := exists b, rtc RPar'.R a b /\ ne b. +Definition wn {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ nf b. +Definition wne {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ ne b. (* Weakly neutral implies weakly normal *) -Lemma wne_wn a : @wne a -> wn a. +Lemma wne_wn n a : @wne n a -> wn a. Proof. sfirstorder use:ne_nf. Qed. (* Normal implies weakly normal *) -Lemma nf_wn v : @nf v -> wn v. +Lemma nf_wn n v : @nf n v -> wn v. Proof. sfirstorder ctrs:rtc. Qed. -Lemma nf_refl (a b : PTm) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a). +Lemma nf_refl n (a b : PTm n) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a). Proof. elim : a b /h => //=; solve [hauto b:on]. Qed. -Lemma ne_nf_ren (a : PTm) (ξ : nat -> nat) : +Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) : (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)). Proof. - move : ξ. elim : a => //=; solve [hauto b:on]. + move : m ξ. elim : n / a => //=; solve [hauto b:on]. Qed. -Lemma wne_app (a b : PTm) : +Lemma wne_app n (a b : PTm n) : wne a -> wn b -> wne (PApp a b). Proof. move => [a0 [? ?]] [b0 [? ?]]. exists (PApp a0 b0). hauto b:on drew:off use:RPars'.AppCong. Qed. -Lemma wn_abs a (h : wn a) : @wn (PAbs a). +Lemma wn_abs n a (h : wn a) : @wn n (PAbs a). Proof. move : h => [v [? ?]]. exists (PAbs v). eauto using RPars'.AbsCong. Qed. -Lemma wn_pair (a b : PTm) : wn a -> wn b -> wn (PPair a b). +Lemma wn_pair n (a b : PTm n) : wn a -> wn b -> wn (PPair a b). Proof. move => [a0 [? ?]] [b0 [? ?]]. exists (PPair a0 b0). hauto lqb:on use:RPars'.PairCong. Qed. -Lemma wne_proj p (a : PTm) : wne a -> wne (PProj p a). +Lemma wne_proj n p (a : PTm n) : wne a -> wne (PProj p a). Proof. move => [a0 [? ?]]. exists (PProj p a0). hauto lqb:on use:RPars'.ProjCong. @@ -2042,30 +2287,31 @@ Qed. Create HintDb nfne. #[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne. -Lemma ne_nf_antiren (a : PTm) (ρ : nat -> nat) : - (ne (ren_PTm ρ a) -> ne a) /\ (nf (ren_PTm ρ a) -> nf a). +Lemma ne_nf_antiren n m (a : PTm n) (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + (ne (subst_PTm ρ a) -> ne a) /\ (nf (subst_PTm ρ a) -> nf a). Proof. - move : ρ. elim : a => //; - hauto b:on drew:off . + move : m ρ. elim : n / a => //; + hauto b:on drew:off use:RPar.var_or_const_up. Qed. -Lemma wn_antirenaming a (ρ : nat -> nat) : - wn (ren_PTm ρ a) -> wn a. +Lemma wn_antirenaming n m a (ρ : fin n -> PTm m) : + (forall i, var_or_const (ρ i)) -> + wn (subst_PTm ρ a) -> wn a. Proof. - rewrite /wn. + rewrite /wn => hρ. move => [v [rv nfv]]. move /RPars'.antirenaming : rv. - move => [b [hb ?]]. subst. + move /(_ hρ) => [b [hb ?]]. subst. exists b. split => //=. move : nfv. by eapply ne_nf_antiren. Qed. -Lemma ext_wn (a : PTm) : - wn (PApp a (VarPTm var_zero)) -> +Lemma ext_wn n (a : PTm n) : + wn (PApp a PBot) -> wn a. Proof. - set PBot := VarPTm var_zero. move E : (PApp a (PBot)) => a0 [v [hr hv]]. move : a E. move : hv. @@ -2079,51 +2325,49 @@ Proof. + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst. have ? : b3 = (PBot) by hauto lq:on inv:RPar'.R. subst. suff : wn (PAbs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn. - have : wn (subst_PTm (scons (VarPTm var_zero) VarPTm) a3) by sfirstorder. - asimpl. + have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder. move => h. apply wn_abs. - move : h. - have -> : subst_PTm (scons (VarPTm var_zero) VarPTm) a3 = ren_PTm (scons var_zero id) a3 by substify; asimpl. - apply wn_antirenaming. + move : h. apply wn_antirenaming. + hauto lq:on rew:off inv:nat. + hauto q:on inv:RPar'.R ctrs:rtc b:on. Qed. Module Join. - Lemma ProjCong p (a0 a1 : PTm) : + Lemma ProjCong p n (a0 a1 : PTm n) : join a0 a1 -> join (PProj p a0) (PProj p a1). Proof. hauto lq:on use:Pars.ProjCong unfold:join. Qed. - Lemma PairCong (a0 a1 b0 b1 : PTm) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : join a0 a1 -> join b0 b1 -> join (PPair a0 b0) (PPair a1 b1). Proof. hauto lq:on use:Pars.PairCong unfold:join. Qed. - Lemma AppCong (a0 a1 b0 b1 : PTm) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : join a0 a1 -> join b0 b1 -> join (PApp a0 b0) (PApp a1 b1). Proof. hauto lq:on use:Pars.AppCong. Qed. - Lemma AbsCong (a b : PTm) : + Lemma AbsCong n (a b : PTm (S n)) : join a b -> join (PAbs a) (PAbs b). Proof. hauto lq:on use:Pars.AbsCong. Qed. - Lemma renaming (a b : PTm) (ξ : nat -> nat) : + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : join a b -> join (ren_PTm ξ a) (ren_PTm ξ b). Proof. induction 1; hauto lq:on use:Pars.renaming. Qed. - Lemma weakening (a b : PTm) : + Lemma weakening n (a b : PTm n) : join a b -> join (ren_PTm shift a) (ren_PTm shift b). Proof. apply renaming. Qed. - Lemma FromPar (a b : PTm) : + Lemma FromPar n (a b : PTm n) : Par.R a b -> join a b. Proof. @@ -2131,7 +2375,7 @@ Module Join. Qed. End Join. -Lemma abs_eq a (b : PTm) : +Lemma abs_eq n a (b : PTm n) : join (PAbs a) b <-> join a (PApp (ren_PTm shift b) (VarPTm var_zero)). Proof. split. @@ -2141,27 +2385,13 @@ Proof. simpl. move => ?. apply : join_transitive; eauto. apply join_symmetric. apply Join.FromPar. - apply : Par.AppAbs'; eauto using Par.refl. by asimpl; rewrite subst_id. + apply : Par.AppAbs'; eauto using Par.refl. by asimpl. - move /Join.AbsCong. move /join_transitive. apply. apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl. Qed. -(* Lemma abs_inj a b : *) -(* join a b <-> join (PAbs a) (PAbs b). *) -(* Proof. *) -(* split. *) - -(* transitivity (join a (PApp (ren_PTm shift (PAbs b)) (VarPTm var_zero))); last by rewrite abs_eq. *) -(* have h : RPar.R (PApp (ren_PTm shift (PAbs b)) (VarPTm var_zero)) (subst_PTm (scons (VarPTm var_zero) VarPTm) (ren_PTm (upRen_PTm_PTm shift) b)). *) -(* apply RPar.AppAbs. rewrite -/ren_PTm. asimpl. substify. asimpl. apply RPar.refl. apply RPar.refl. *) -(* split. *) -(* move => h1. apply : join_transitive; eauto. *) -(* apply join_symmetric. *) -(* apply *) - - -Lemma pair_eq (a0 a1 b : PTm) : +Lemma pair_eq n (a0 a1 b : PTm n) : join (PPair a0 a1) b <-> join a0 (PProj PL b) /\ join a1 (PProj PR b). Proof. split. @@ -2177,7 +2407,7 @@ Proof. apply Join.FromPar. hauto lq:on ctrs:Par.R use:Par.refl. Qed. -Lemma join_pair_inj (a0 a1 b0 b1 : PTm) : +Lemma join_pair_inj n (a0 a1 b0 b1 : PTm n) : join (PPair a0 a1) (PPair b0 b1) <-> join a0 b0 /\ join a1 b1. Proof. split; last by hauto lq:on use:Join.PairCong. diff --git a/theories/typing.v b/theories/typing.v index ac3ed0f..d41facd 100644 --- a/theories/typing.v +++ b/theories/typing.v @@ -1,93 +1,251 @@ -Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect. -From Hammer Require Import Tactics. +Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. Reserved Notation "Γ ⊢ a ∈ A" (at level 70). +Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70). +Reserved Notation "Γ ⊢ A ≲ B" (at level 70). Reserved Notation "⊢ Γ" (at level 70). -Inductive lookup : nat -> list Tm -> Tm -> Prop := -| here A Γ : lookup 0 (cons A Γ) (ren_Tm shift A) -| there i Γ A B : - lookup i Γ A -> - lookup (S i) (cons B Γ) (ren_Tm shift A). - -Lemma lookup_deter i Γ A B : - lookup i Γ A -> - lookup i Γ B -> - A = B. -Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed. - -Lemma here' A Γ U : U = ren_Tm shift A -> lookup 0 (A :: Γ) U. -Proof. move => ->. apply here. Qed. - -Lemma there' i Γ A B U : U = ren_Tm shift A -> lookup i Γ A -> - lookup (S i) (cons B Γ) U. -Proof. move => ->. apply there. Qed. - -Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A). - - -Inductive Wt : list Tm -> Tm -> Tm -> Prop := +Inductive Wt : list PTm -> PTm -> PTm -> Prop := | T_Var i Γ A : ⊢ Γ -> lookup i Γ A -> - Γ ⊢ VarTm i ∈ A + Γ ⊢ VarPTm i ∈ A -| T_Bind Γ i p A B : - Γ ⊢ A ∈ Univ i -> - cons A Γ ⊢ B ∈ Univ i -> - Γ ⊢ TBind p A B ∈ Univ i +| T_Bind Γ i p (A : PTm) (B : PTm) : + Γ ⊢ A ∈ PUniv i -> + cons A Γ ⊢ B ∈ PUniv i -> + Γ ⊢ PBind p A B ∈ PUniv i -| T_Abs Γ a A B i : - Γ ⊢ TBind TPi A B ∈ (Univ i) -> +| T_Abs Γ (a : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> (cons A Γ) ⊢ a ∈ B -> - Γ ⊢ Abs A a ∈ TBind TPi A B + Γ ⊢ PAbs a ∈ PBind PPi A B -| T_App Γ b a A B : - Γ ⊢ b ∈ TBind TPi A B -> +| T_App Γ (b a : PTm) A B : + Γ ⊢ b ∈ PBind PPi A B -> Γ ⊢ a ∈ A -> - Γ ⊢ App b a ∈ subst_Tm (scons a VarTm) B + Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B -| T_Pair Γ (a b : Tm) A B i : - Γ ⊢ TBind TSig A B ∈ (Univ i) -> +| T_Pair Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> Γ ⊢ a ∈ A -> - Γ ⊢ b ∈ subst_Tm (scons a VarTm) B -> - Γ ⊢ Pair a b ∈ TBind TSig A B + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PPair a b ∈ PBind PSig A B -| T_Proj1 Γ (a : Tm) A B : - Γ ⊢ a ∈ TBind TSig A B -> - Γ ⊢ Proj PL a ∈ A +| T_Proj1 Γ (a : PTm) A B : + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ PProj PL a ∈ A -| T_Proj2 Γ (a : Tm) A B : - Γ ⊢ a ∈ TBind TSig A B -> - Γ ⊢ Proj PR a ∈ subst_Tm (scons (Proj PL a) VarTm) B +| T_Proj2 Γ (a : PTm) A B : + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B | T_Univ Γ i : ⊢ Γ -> - Γ ⊢ Univ i ∈ Univ (S i) + Γ ⊢ PUniv i ∈ PUniv (S i) -| T_Conv Γ (a : Tm) A B i : +| T_Nat Γ i : + ⊢ Γ -> + Γ ⊢ PNat ∈ PUniv i + +| T_Zero Γ : + ⊢ Γ -> + Γ ⊢ PZero ∈ PNat + +| T_Suc Γ (a : PTm) : + Γ ⊢ a ∈ PNat -> + Γ ⊢ PSuc a ∈ PNat + +| T_Ind Γ P (a : PTm) b c i : + cons PNat Γ ⊢ P ∈ PUniv i -> + Γ ⊢ a ∈ PNat -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P + +| T_Conv Γ (a : PTm) A B : Γ ⊢ a ∈ A -> - Γ ⊢ B ∈ Univ i -> - Join.R A B -> + Γ ⊢ A ≲ B -> Γ ⊢ a ∈ B -with Wff : list Tm -> Prop := +with Eq : list PTm -> PTm -> PTm -> PTm -> Prop := +(* Structural *) +| E_Refl Γ (a : PTm ) A : + Γ ⊢ a ∈ A -> + Γ ⊢ a ≡ a ∈ A + +| E_Symmetric Γ (a b : PTm) A : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ b ≡ a ∈ A + +| E_Transitive Γ (a b c : PTm) A : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ b ≡ c ∈ A -> + Γ ⊢ a ≡ c ∈ A + +(* Congruence *) +| E_Bind Γ i p (A0 A1 : PTm) B0 B1 : + Γ ⊢ A0 ∈ PUniv i -> + Γ ⊢ A0 ≡ A1 ∈ PUniv i -> + (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> + Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i + +| E_Abs Γ (a b : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + (cons A Γ) ⊢ a ≡ b ∈ B -> + Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B + +| E_App Γ i (b0 b1 a0 a1 : PTm) A B : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B -> + Γ ⊢ a0 ≡ a1 ∈ A -> + Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B + +| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a0 ≡ a1 ∈ A -> + Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B -> + Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B + +| E_Proj1 Γ (a b : PTm) A B : + Γ ⊢ a ≡ b ∈ PBind PSig A B -> + Γ ⊢ PProj PL a ≡ PProj PL b ∈ A + +| E_Proj2 Γ i (a b : PTm) A B : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ≡ b ∈ PBind PSig A B -> + Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B + +| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i : + (cons PNat Γ) ⊢ P0 ∈ PUniv i -> + (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i -> + Γ ⊢ a0 ≡ a1 ∈ PNat -> + Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 -> + (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) -> + Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0 + +| E_SucCong Γ (a b : PTm) : + Γ ⊢ a ≡ b ∈ PNat -> + Γ ⊢ PSuc a ≡ PSuc b ∈ PNat + +| E_Conv Γ (a b : PTm) A B : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ A ≲ B -> + Γ ⊢ a ≡ b ∈ B + +(* Beta *) +| E_AppAbs Γ (a : PTm) b A B i: + Γ ⊢ PBind PPi A B ∈ PUniv i -> + Γ ⊢ b ∈ A -> + (cons A Γ) ⊢ a ∈ B -> + Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B + +| E_ProjPair1 Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ A -> + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A + +| E_ProjPair2 Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ A -> + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B + +| E_IndZero Γ P i (b : PTm) c : + (cons PNat Γ) ⊢ P ∈ PUniv i -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P + +| E_IndSuc Γ P (a : PTm) b c i : + (cons PNat Γ) ⊢ P ∈ PUniv i -> + Γ ⊢ a ∈ PNat -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P + +(* Eta *) +| E_AppEta Γ (b : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + Γ ⊢ b ∈ PBind PPi A B -> + Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B + +| E_PairEta Γ (a : PTm ) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B + +with LEq : list PTm -> PTm -> PTm -> Prop := +(* Structural *) +| Su_Transitive Γ (A B C : PTm) : + Γ ⊢ A ≲ B -> + Γ ⊢ B ≲ C -> + Γ ⊢ A ≲ C + +(* Congruence *) +| Su_Univ Γ i j : + ⊢ Γ -> + i <= j -> + Γ ⊢ PUniv i ≲ PUniv j + +| Su_Pi Γ (A0 A1 : PTm) B0 B1 i : + Γ ⊢ A0 ∈ PUniv i -> + Γ ⊢ A1 ≲ A0 -> + (cons A0 Γ) ⊢ B0 ≲ B1 -> + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 + +| Su_Sig Γ (A0 A1 : PTm) B0 B1 i : + Γ ⊢ A1 ∈ PUniv i -> + Γ ⊢ A0 ≲ A1 -> + (cons A1 Γ) ⊢ B0 ≲ B1 -> + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 + +(* Injecting from equalities *) +| Su_Eq Γ (A : PTm) B i : + Γ ⊢ A ≡ B ∈ PUniv i -> + Γ ⊢ A ≲ B + +(* Projection axioms *) +| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> + Γ ⊢ A1 ≲ A0 + +| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> + Γ ⊢ A0 ≲ A1 + +| Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 : + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> + Γ ⊢ a0 ≡ a1 ∈ A1 -> + Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 + +| Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> + Γ ⊢ a0 ≡ a1 ∈ A0 -> + Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 + +with Wff : list PTm -> Prop := | Wff_Nil : ⊢ nil -| Wff_Cons Γ (A : Tm) i : +| Wff_Cons Γ (A : PTm) i : ⊢ Γ -> - Γ ⊢ A ∈ Univ i -> + Γ ⊢ A ∈ PUniv i -> (* -------------------------------- *) ⊢ (cons A Γ) where -"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ). +"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B). Scheme wf_ind := Induction for Wff Sort Prop - with wt_ind := Induction for Wt Sort Prop. + with wt_ind := Induction for Wt Sort Prop + with eq_ind := Induction for Eq Sort Prop + with le_ind := Induction for LEq Sort Prop. -Combined Scheme wt_mutual from wf_ind, wt_ind. +Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind. (* Lemma lem : *) -(* (forall n (Γ : fin n -> Tm n), ⊢ Γ -> ...) /\ *) -(* (forall n Γ (a A : Tm n), Γ ⊢ a ∈ A -> ...) /\ *) +(* (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *) +(* (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...) /\ *) +(* (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *) +(* (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *) (* Proof. apply wt_mutual. ... *) diff --git a/theories/typing_properties.v b/theories/typing_properties.v deleted file mode 100644 index b8defe3..0000000 --- a/theories/typing_properties.v +++ /dev/null @@ -1,134 +0,0 @@ -Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect typing. -From Hammer Require Import Tactics. - -Lemma Bind_Inv Γ p A B U : - Γ ⊢ TBind p A B ∈ U -> - exists i, Γ ⊢ A ∈ Univ i /\ cons A Γ ⊢ B ∈ Univ i /\ Join.R (Univ i) U. -Proof. - move E : (TBind p A B) => u hu. - move : p A B E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma Univ_Inv Γ i U : - Γ ⊢ Univ i ∈ U -> - Γ ⊢ Univ i ∈ Univ (S i) /\ Join.R (Univ (S i)) U. -Proof. - move E : (Univ i) => u hu. - move : i E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma App_Inv Γ b a U : - Γ ⊢ App b a ∈ U -> - exists A B, Γ ⊢ b ∈ TBind TPi A B /\ Γ ⊢ a ∈ A /\ Join.R (subst_Tm (scons a VarTm) B) U. -Proof. - move E : (App b a) => u hu. - move : b a E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma Abs_Inv Γ A a U : - Γ ⊢ Abs A a ∈ U -> - exists B, cons A Γ ⊢ a ∈ B /\ Join.R (TBind TPi A B) U. -Proof. - move E : (Abs A a) => u hu. - move : A a E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma Var_Inv Γ i U : - Γ ⊢ VarTm i ∈ U -> - exists A, lookup i Γ A /\ Join.R A U. -Proof. - move E : (VarTm i) => u hu. - move : i E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma Pair_Inv Γ a b U : - Γ ⊢ Pair a b ∈ U -> - exists A B, Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_Tm (scons a VarTm) B /\ Join.R (TBind TSig A B) U. -Proof. - move E : (Pair a b ) => u hu. - move : a b E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma ProjL_Inv Γ a U : - Γ ⊢ Proj PL a ∈ U -> - exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R A U. -Proof. - move E : (Proj PL a) => u hu. - move : a E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma ProjR_Inv Γ a U : - Γ ⊢ Proj PR a ∈ U -> - exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R (subst_Tm (scons (Proj PL a) VarTm) B) U. -Proof. - move E : (Proj PR a) => u hu. - move : a E. - elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive. -Qed. - -Lemma ctx_wff_mutual : - (forall Γ, ⊢ Γ -> True) /\ - (forall Γ a A, Γ ⊢ a ∈ A -> ⊢ Γ). -Proof. apply wt_mutual => //=. Qed. - -Lemma lookup_deter i Γ A A0 : - lookup i Γ A -> - lookup i Γ A0 -> A = A0. -Proof. - move => h. move : A0. elim : i Γ A / h; hauto lq:on inv:lookup. -Qed. - -Lemma wt_unique : - (forall Γ, ⊢ Γ -> True) /\ - (forall Γ a A, Γ ⊢ a ∈ A -> forall B, Γ ⊢ a ∈ B -> Join.R A B). -Proof. - apply wt_mutual => //=. - - move => i Γ A hΓ _ hl B. - move /Var_Inv. - move => [A0 [h0 h1]]. - move : hl h0. - move : lookup_deter; repeat move/[apply]. move => ?. by subst. - - move => Γ i p A B hA ihA hB ihB U. - move /Bind_Inv => [j][ih0][ih1]ih2. - apply ihB in ih1. - move /Join.UnivInj in ih1. by subst. - - move => Γ a A B i hP ihP ha iha U. - move /Abs_Inv => [B0][ha']hJ. - move /iha in ha' => {iha}. - apply : Join.transitive; eauto. - apply Join.BindCong; eauto using Join.reflexive. - - move => Γ b a A B hb ihb ha iha U. - move /App_Inv. move => [A0][B0][hb'][ha']hU. - apply ihb in hb' => {ihb}. - move /Join.BindInj : hb'. - move => [_][hJ0]hJ1. - apply : Join.transitive; eauto. - by apply Join.substing. - - move => Γ a b A B i hS ihS ha iha hb ihb U. - move /Pair_Inv. - move => [A0][B0][{}/iha ha'][{}/ihb hb']hJ. - apply : Join.transitive; eauto. - apply Join.BindCong; eauto. - admit. - - move => Γ a A B ha iha U. - move /ProjL_Inv. - move => [A0][B0][{}/iha ha0]hU. - apply Join.BindInj in ha0. - decompose record ha0. - eauto using Join.transitive. - - move => Γ a A B ha iha U /ProjR_Inv [A0][B0][{}/iha /Join.BindInj ha']. - decompose record ha'. - move => h. apply : Join.transitive; eauto. - by apply Join.substing. - - move => Γ i hΓ _ B /Univ_Inv. tauto. - - move => Γ a A B i ha iha hb ihb. - move => h0 B0 {}/iha ha'. - eauto using Join.symmetric, Join.transitive. -Admitted.