diff --git a/syntax.sig b/syntax.sig index 9e04431..e63c3b4 100644 --- a/syntax.sig +++ b/syntax.sig @@ -1,4 +1,5 @@ nat : Type +PTm(VarPTm) : Type Tm(VarTm) : Type PTag : Type TTag : Type @@ -8,14 +9,21 @@ PL : PTag PR : PTag TPi : TTag TSig : TTag + +PAbs : (bind PTm in PTm) -> PTm +PApp : PTm -> PTm -> PTm +PPair : PTm -> PTm -> PTm +PProj : PTag -> PTm -> PTm +PConst : TTag -> PTm +PUniv : nat -> PTm +PBot : PTm + Abs : (bind Tm in Tm) -> Tm App : Tm -> Tm -> Tm Pair : Tm -> Tm -> Tm Proj : PTag -> Tm -> Tm TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm -Const : TTag -> Tm Univ : nat -> Tm -Bot : Tm BVal : bool -> Tm Bool : Tm If : Tm -> Tm -> Tm -> Tm diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 5b06281..75ef645 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -33,6 +33,674 @@ Proof. exact (eq_refl). Qed. +Inductive PTm (n_PTm : nat) : Type := + | VarPTm : fin n_PTm -> PTm n_PTm + | PAbs : PTm (S n_PTm) -> PTm n_PTm + | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm + | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm + | PProj : PTag -> PTm n_PTm -> PTm n_PTm + | PConst : TTag -> PTm n_PTm + | PUniv : nat -> PTm n_PTm + | PBot : PTm n_PTm. + +Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)} + (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)). +Qed. + +Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} + {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PApp m_PTm s0 s1 = PApp m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp m_PTm x s1) H0)) + (ap (fun x => PApp m_PTm t0 x) H1)). +Qed. + +Lemma congr_PPair {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} + {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PPair m_PTm s0 s1 = PPair m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair m_PTm x s1) H0)) + (ap (fun x => PPair m_PTm t0 x) H1)). +Qed. + +Lemma congr_PProj {m_PTm : nat} {s0 : PTag} {s1 : PTm m_PTm} {t0 : PTag} + {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : + PProj m_PTm s0 s1 = PProj m_PTm t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0)) + (ap (fun x => PProj m_PTm t0 x) H1)). +Qed. + +Lemma congr_PConst {m_PTm : nat} {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) : + PConst m_PTm s0 = PConst m_PTm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => PConst m_PTm x) H0)). +Qed. + +Lemma congr_PUniv {m_PTm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : + PUniv m_PTm s0 = PUniv m_PTm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)). +Qed. + +Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm. +Proof. +exact (eq_refl). +Qed. + +Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) : + fin (S m) -> fin (S n). +Proof. +exact (up_ren xi). +Defined. + +Lemma upRen_list_PTm_PTm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) + : fin (plus p m) -> fin (plus p n). +Proof. +exact (upRen_p p xi). +Defined. + +Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm := + match s with + | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0) + | PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) + | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1) + | PConst _ s0 => PConst n_PTm s0 + | PUniv _ s0 => PUniv n_PTm s0 + | PBot _ => PBot n_PTm + end. + +Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : + fin (S m) -> PTm (S n_PTm). +Proof. +exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)). +Defined. + +Lemma up_list_PTm_PTm (p : nat) {m : nat} {n_PTm : nat} + (sigma : fin m -> PTm n_PTm) : fin (plus p m) -> PTm (plus p n_PTm). +Proof. +exact (scons_p p (funcomp (VarPTm (plus p n_PTm)) (zero_p p)) + (funcomp (ren_PTm (shift_p p)) sigma)). +Defined. + +Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm +:= + match s with + | VarPTm _ s0 => sigma_PTm s0 + | PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) + | PApp _ s0 s1 => + PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PPair _ s0 s1 => + PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PProj _ s0 s1 => PProj n_PTm s0 (subst_PTm sigma_PTm s1) + | PConst _ s0 => PConst n_PTm s0 + | PUniv _ s0 => PUniv n_PTm s0 + | PBot _ => PBot n_PTm + end. + +Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm) + (Eq : forall x, sigma x = VarPTm m_PTm x) : + forall x, up_PTm_PTm sigma x = VarPTm (S m_PTm) x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upId_list_PTm_PTm {p : nat} {m_PTm : nat} + (sigma : fin m_PTm -> PTm m_PTm) (Eq : forall x, sigma x = VarPTm m_PTm x) + : forall x, up_list_PTm_PTm p sigma x = VarPTm (plus p m_PTm) x. +Proof. +exact (fun n => + scons_p_eta (VarPTm (plus p m_PTm)) + (fun n => ap (ren_PTm (shift_p p)) (Eq n)) (fun n => eq_refl)). +Qed. + +Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) +(Eq_PTm : forall x, sigma_PTm x = VarPTm m_PTm x) (s : PTm m_PTm) {struct s} + : subst_PTm sigma_PTm s = s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) + (idSubst_PTm sigma_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0) + (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 {m : nat} {n : nat} (xi : fin m -> fin n) + (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : + forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap shift (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upExtRen_list_PTm_PTm {p : nat} {m : nat} {n : nat} + (xi : fin m -> fin n) (zeta : fin m -> fin n) + (Eq : forall x, xi x = zeta x) : + forall x, upRen_list_PTm_PTm p xi x = upRen_list_PTm_PTm p zeta x. +Proof. +exact (fun n => + scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))). +Qed. + +Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (zeta_PTm : fin m_PTm -> fin n_PTm) +(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm m_PTm) {struct s} : +ren_PTm xi_PTm s = ren_PTm zeta_PTm s := + match s with + | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0) + | PAbs _ s0 => + congr_PAbs + (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) + (upExtRen_PTm_PTm _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) + | 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 {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) + (tau : fin m -> PTm n_PTm) (Eq : forall x, sigma x = tau x) : + forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma upExt_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} + (sigma : fin m -> PTm n_PTm) (tau : fin m -> PTm n_PTm) + (Eq : forall x, sigma x = tau x) : + forall x, up_list_PTm_PTm p sigma x = up_list_PTm_PTm p tau x. +Proof. +exact (fun n => + scons_p_congr (fun n => eq_refl) + (fun n => ap (ren_PTm (shift_p p)) (Eq n))). +Qed. + +Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm n_PTm) (tau_PTm : fin m_PTm -> PTm n_PTm) +(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm m_PTm) {struct s} : +subst_PTm sigma_PTm s = subst_PTm tau_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) + (upExt_PTm_PTm _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) + | 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 {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) + (zeta : fin l -> fin m) (rho : fin k -> fin m) + (Eq : forall x, funcomp zeta xi x = rho x) : + forall x, + funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x. +Proof. +exact (up_ren_ren xi zeta rho Eq). +Qed. + +Lemma up_ren_ren_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m : nat} + (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m) + (Eq : forall x, funcomp zeta xi x = rho x) : + forall x, + funcomp (upRen_list_PTm_PTm p zeta) (upRen_list_PTm_PTm p xi) x = + upRen_list_PTm_PTm p rho x. +Proof. +exact (up_ren_ren_p Eq). +Qed. + +Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) +(rho_PTm : fin m_PTm -> fin l_PTm) +(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm m_PTm) +{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := + match s with + | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0) + | PAbs _ s0 => + congr_PAbs + (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) + (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) + | PProj _ s0 s1 => + 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 {k : nat} {l : nat} {m_PTm : nat} + (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : + forall x, + funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma up_ren_subst_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m_PTm : nat} + (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : + forall x, + funcomp (up_list_PTm_PTm p tau) (upRen_list_PTm_PTm p xi) x = + up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ _ n) + (scons_p_congr (fun z => scons_p_head' _ _ z) + (fun z => + eq_trans (scons_p_tail' _ _ (xi z)) + (ap (ren_PTm (shift_p p)) (Eq z))))). +Qed. + +Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm m_PTm) +{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) + (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) + (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) + (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + 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 {k : nat} {l_PTm : nat} {m_PTm : nat} + (sigma : fin k -> PTm l_PTm) (zeta_PTm : fin l_PTm -> fin m_PTm) + (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : + forall x, + funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x = + up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => + eq_trans + (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm) + (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n)) + (eq_trans + (eq_sym + (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm) + (fun x => eq_refl) (sigma fin_n))) + (ap (ren_PTm shift) (Eq fin_n))) + | None => eq_refl + end). +Qed. + +Lemma up_subst_ren_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} + {m_PTm : nat} (sigma : fin k -> PTm l_PTm) + (zeta_PTm : fin l_PTm -> fin m_PTm) (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : + forall x, + funcomp (ren_PTm (upRen_list_PTm_PTm p zeta_PTm)) (up_list_PTm_PTm p sigma) + x = up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ _ n) + (scons_p_congr + (fun x => ap (VarPTm (plus p m_PTm)) (scons_p_head' _ _ x)) + (fun n => + eq_trans + (compRenRen_PTm (shift_p p) (upRen_list_PTm_PTm p zeta_PTm) + (funcomp (shift_p p) zeta_PTm) + (fun x => scons_p_tail' _ _ x) (sigma n)) + (eq_trans + (eq_sym + (compRenRen_PTm zeta_PTm (shift_p p) + (funcomp (shift_p p) zeta_PTm) (fun x => eq_refl) + (sigma n))) (ap (ren_PTm (shift_p p)) (Eq n)))))). +Qed. + +Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x) +(s : PTm m_PTm) {struct s} : +ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) + (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) + (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) + (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + 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 {k : nat} {l_PTm : nat} {m_PTm : nat} + (sigma : fin k -> PTm l_PTm) (tau_PTm : fin l_PTm -> PTm m_PTm) + (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : + forall x, + funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x = + up_PTm_PTm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => + eq_trans + (compRenSubst_PTm shift (up_PTm_PTm tau_PTm) + (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl) + (sigma fin_n)) + (eq_trans + (eq_sym + (compSubstRen_PTm tau_PTm shift + (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl) + (sigma fin_n))) (ap (ren_PTm shift) (Eq fin_n))) + | None => eq_refl + end). +Qed. + +Lemma up_subst_subst_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} + {m_PTm : nat} (sigma : fin k -> PTm l_PTm) + (tau_PTm : fin l_PTm -> PTm m_PTm) (theta : fin k -> PTm m_PTm) + (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : + forall x, + funcomp (subst_PTm (up_list_PTm_PTm p tau_PTm)) (up_list_PTm_PTm p sigma) x = + up_list_PTm_PTm p theta x. +Proof. +exact (fun n => + eq_trans + (scons_p_comp' (funcomp (VarPTm (plus p l_PTm)) (zero_p p)) _ _ n) + (scons_p_congr + (fun x => scons_p_head' _ (fun z => ren_PTm (shift_p p) _) x) + (fun n => + eq_trans + (compRenSubst_PTm (shift_p p) (up_list_PTm_PTm p tau_PTm) + (funcomp (up_list_PTm_PTm p tau_PTm) (shift_p p)) + (fun x => eq_refl) (sigma n)) + (eq_trans + (eq_sym + (compSubstRen_PTm tau_PTm (shift_p p) _ + (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n))) + (ap (ren_PTm (shift_p p)) (Eq n)))))). +Qed. + +Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} +(sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) +(theta_PTm : fin m_PTm -> PTm l_PTm) +(Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x) +(s : PTm m_PTm) {struct s} : +subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) + (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) + (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) + (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) + | PProj _ s0 s1 => + 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 {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) + (s : PTm m_PTm) : + ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s. +Proof. +exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renRen'_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm)) + (ren_PTm (funcomp zeta_PTm xi_PTm)). +Proof. +exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) + (s : PTm m_PTm) : + subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s. +Proof. +exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma renSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm)) + (subst_PTm (funcomp tau_PTm xi_PTm)). +Proof. +exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) + (s : PTm m_PTm) : + ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = + subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s. +Proof. +exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substRen_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm)) + (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)). +Proof. +exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) + (s : PTm m_PTm) : + subst_PTm tau_PTm (subst_PTm sigma_PTm s) = + subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s. +Proof. +exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma substSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm)) + (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)). +Proof. +exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma rinstInst_up_PTm_PTm {m : nat} {n_PTm : nat} (xi : fin m -> fin n_PTm) + (sigma : fin m -> PTm n_PTm) + (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : + forall x, + funcomp (VarPTm (S n_PTm)) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_PTm shift) (Eq fin_n) + | None => eq_refl + end). +Qed. + +Lemma rinstInst_up_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} + (xi : fin m -> fin n_PTm) (sigma : fin m -> PTm n_PTm) + (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : + forall x, + funcomp (VarPTm (plus p n_PTm)) (upRen_list_PTm_PTm p xi) x = + up_list_PTm_PTm p sigma x. +Proof. +exact (fun n => + eq_trans (scons_p_comp' _ _ (VarPTm (plus p n_PTm)) n) + (scons_p_congr (fun z => eq_refl) + (fun n => ap (ren_PTm (shift_p p)) (Eq n)))). +Qed. + +Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} +(xi_PTm : fin m_PTm -> fin n_PTm) (sigma_PTm : fin m_PTm -> PTm n_PTm) +(Eq_PTm : forall x, funcomp (VarPTm n_PTm) xi_PTm x = sigma_PTm x) +(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := + match s with + | VarPTm _ s0 => Eq_PTm s0 + | PAbs _ s0 => + congr_PAbs + (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) + (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) + | PApp _ s0 s1 => + congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) + | PPair _ s0 s1 => + congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) + | 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 {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) : + ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm n_PTm) xi_PTm) s. +Proof. +exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma rinstInst'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) : + pointwise_relation _ eq (ren_PTm xi_PTm) + (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)). +Proof. +exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). +Qed. + +Lemma instId'_PTm {m_PTm : nat} (s : PTm m_PTm) : + subst_PTm (VarPTm m_PTm) s = s. +Proof. +exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +Qed. + +Lemma instId'_PTm_pointwise {m_PTm : nat} : + pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id. +Proof. +exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +Qed. + +Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s. +Proof. +exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). +Qed. + +Lemma rinstId'_PTm_pointwise {m_PTm : nat} : + pointwise_relation _ eq (@ren_PTm m_PTm m_PTm id) id. +Proof. +exact (fun s => + eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). +Qed. + +Lemma varL'_PTm {m_PTm : nat} {n_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm n_PTm) (x : fin m_PTm) : + subst_PTm sigma_PTm (VarPTm m_PTm x) = sigma_PTm x. +Proof. +exact (eq_refl). +Qed. + +Lemma varL'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (sigma_PTm : fin m_PTm -> PTm n_PTm) : + pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm m_PTm)) + sigma_PTm. +Proof. +exact (fun x => eq_refl). +Qed. + +Lemma varLRen'_PTm {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) (x : fin m_PTm) : + ren_PTm xi_PTm (VarPTm m_PTm x) = VarPTm n_PTm (xi_PTm x). +Proof. +exact (eq_refl). +Qed. + +Lemma varLRen'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} + (xi_PTm : fin m_PTm -> fin n_PTm) : + pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm m_PTm)) + (funcomp (VarPTm n_PTm) xi_PTm). +Proof. +exact (fun x => eq_refl). +Qed. + Inductive Tm (n_Tm : nat) : Type := | VarTm : fin n_Tm -> Tm n_Tm | Abs : Tm (S n_Tm) -> Tm n_Tm @@ -40,9 +708,7 @@ Inductive Tm (n_Tm : nat) : Type := | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm | Proj : PTag -> Tm n_Tm -> Tm n_Tm | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm - | Const : TTag -> Tm n_Tm | Univ : nat -> Tm n_Tm - | Bot : Tm n_Tm | BVal : bool -> Tm n_Tm | Bool : Tm n_Tm | If : Tm n_Tm -> Tm n_Tm -> Tm n_Tm -> Tm n_Tm. @@ -87,23 +753,12 @@ exact (eq_trans (ap (fun x => TBind m_Tm t0 t1 x) H2)). Qed. -Lemma congr_Const {m_Tm : nat} {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) : - Const m_Tm s0 = Const m_Tm t0. -Proof. -exact (eq_trans eq_refl (ap (fun x => Const m_Tm x) H0)). -Qed. - Lemma congr_Univ {m_Tm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : Univ m_Tm s0 = Univ m_Tm t0. Proof. exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)). Qed. -Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm. -Proof. -exact (eq_refl). -Qed. - Lemma congr_BVal {m_Tm : nat} {s0 : bool} {t0 : bool} (H0 : s0 = t0) : BVal m_Tm s0 = BVal m_Tm t0. Proof. @@ -147,9 +802,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1) | TBind _ s0 s1 s2 => TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2) - | Const _ s0 => Const n_Tm s0 | Univ _ s0 => Univ n_Tm s0 - | Bot _ => Bot n_Tm | BVal _ s0 => BVal n_Tm s0 | Bool _ => Bool n_Tm | If _ s0 s1 s2 => @@ -179,9 +832,7 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1) | TBind _ s0 s1 s2 => TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2) - | Const _ s0 => Const n_Tm s0 | Univ _ s0 => Univ n_Tm s0 - | Bot _ => Bot n_Tm | BVal _ s0 => BVal n_Tm s0 | Bool _ => Bool n_Tm | If _ s0 s1 s2 => @@ -225,9 +876,7 @@ subst_Tm sigma_Tm s = s := | TBind _ s0 s1 s2 => congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -275,9 +924,7 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) congr_TBind (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upExtRen_Tm_Tm _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -326,9 +973,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) congr_TBind (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -377,9 +1022,7 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} congr_TBind (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -440,9 +1083,7 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -524,9 +1165,7 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm) (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -609,9 +1248,7 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -732,9 +1369,7 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat} congr_TBind (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2) - | Const _ s0 => congr_Const (eq_refl s0) | Univ _ s0 => congr_Univ (eq_refl s0) - | Bot _ => congr_Bot | BVal _ s0 => congr_BVal (eq_refl s0) | Bool _ => congr_Bool | If _ s0 s1 s2 => @@ -809,6 +1444,9 @@ Qed. Class Up_Tm X Y := up_Tm : X -> Y. +Class Up_PTm X Y := + up_PTm : X -> Y. + #[global] Instance Subst_Tm {m_Tm n_Tm : nat}: (Subst1 _ _ _) := (@subst_Tm m_Tm n_Tm). @@ -821,6 +1459,19 @@ Instance Ren_Tm {m_Tm n_Tm : nat}: (Ren1 _ _ _) := (@ren_Tm m_Tm n_Tm). #[global] Instance VarInstance_Tm {n_Tm : nat}: (Var _ _) := (@VarTm n_Tm). +#[global] +Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := + (@subst_PTm m_PTm n_PTm). + +#[global] +Instance Up_PTm_PTm {m n_PTm : nat}: (Up_PTm _ _) := (@up_PTm_PTm m n_PTm). + +#[global] +Instance Ren_PTm {m_PTm n_PTm : nat}: (Ren1 _ _ _) := (@ren_PTm m_PTm n_PTm). + +#[global] +Instance VarInstance_PTm {n_PTm : nat}: (Var _ _) := (@VarPTm n_PTm). + Notation "[ sigma_Tm ]" := (subst_Tm sigma_Tm) ( at level 1, left associativity, only printing) : fscope. @@ -845,6 +1496,30 @@ Notation "x '__Tm'" := (@ids _ _ VarInstance_Tm x) Notation "x '__Tm'" := (VarTm x) ( at level 5, format "x __Tm") : subst_scope. +Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s [ sigma_PTm ]" := (subst_PTm sigma_PTm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "↑__PTm" := up_PTm (only printing) : subst_scope. + +Notation "↑__PTm" := up_PTm_PTm (only printing) : subst_scope. + +Notation "⟨ xi_PTm ⟩" := (ren_PTm xi_PTm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s ⟨ xi_PTm ⟩" := (ren_PTm xi_PTm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "'var'" := VarPTm ( at level 1, only printing) : subst_scope. + +Notation "x '__PTm'" := (@ids _ _ VarInstance_PTm x) +( at level 5, format "x __PTm", only printing) : subst_scope. + +Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : +subst_scope. + #[global] Instance subst_Tm_morphism {m_Tm : nat} {n_Tm : nat}: (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) @@ -881,15 +1556,56 @@ Proof. exact (fun f_Tm g_Tm Eq_Tm s => extRen_Tm f_Tm g_Tm Eq_Tm s). Qed. +#[global] +Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) + (@subst_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => + eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t') + (ext_PTm f_PTm g_PTm Eq_PTm s) t Eq_st). +Qed. + +#[global] +Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@subst_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s). +Qed. + +#[global] +Instance ren_PTm_morphism {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) + (@ren_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => + eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t') + (extRen_PTm f_PTm g_PTm Eq_PTm s) t Eq_st). +Qed. + +#[global] +Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@ren_PTm m_PTm n_PTm)). +Proof. +exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s). +Qed. + Ltac auto_unfold := repeat - unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, - Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1. + unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1, + Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1, + VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, Up_Tm_Tm, + Up_Tm, up_Tm, Subst_Tm, Subst1, subst1. Tactic Notation "auto_unfold" "in" "*" := repeat - unfold VarInstance_Tm, Var, ids, - Ren_Tm, Ren1, ren1, Up_Tm_Tm, - Up_Tm, up_Tm, Subst_Tm, Subst1, - subst1 in *. + unfold VarInstance_PTm, Var, ids, + Ren_PTm, Ren1, ren1, Up_PTm_PTm, + Up_PTm, up_PTm, Subst_PTm, + Subst1, subst1, VarInstance_Tm, + Var, ids, Ren_Tm, Ren1, ren1, + Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, + Subst1, subst1 in *. Ltac asimpl' := repeat (first [ progress setoid_rewrite substSubst_Tm_pointwise @@ -900,6 +1616,14 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite renSubst_Tm | progress setoid_rewrite renRen'_Tm_pointwise | progress setoid_rewrite renRen_Tm + | progress setoid_rewrite substSubst_PTm_pointwise + | progress setoid_rewrite substSubst_PTm + | progress setoid_rewrite substRen_PTm_pointwise + | progress setoid_rewrite substRen_PTm + | progress setoid_rewrite renSubst_PTm_pointwise + | progress setoid_rewrite renSubst_PTm + | progress setoid_rewrite renRen'_PTm_pointwise + | progress setoid_rewrite renRen_PTm | progress setoid_rewrite varLRen'_Tm_pointwise | progress setoid_rewrite varLRen'_Tm | progress setoid_rewrite varL'_Tm_pointwise @@ -908,27 +1632,42 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite rinstId'_Tm | progress setoid_rewrite instId'_Tm_pointwise | progress setoid_rewrite instId'_Tm + | progress setoid_rewrite varLRen'_PTm_pointwise + | progress setoid_rewrite varLRen'_PTm + | progress setoid_rewrite varL'_PTm_pointwise + | progress setoid_rewrite varL'_PTm + | progress setoid_rewrite rinstId'_PTm_pointwise + | progress setoid_rewrite rinstId'_PTm + | progress setoid_rewrite instId'_PTm_pointwise + | progress setoid_rewrite instId'_PTm | progress unfold up_list_Tm_Tm, up_Tm_Tm, upRen_list_Tm_Tm, - upRen_Tm_Tm, up_ren - | progress cbn[subst_Tm ren_Tm] + upRen_Tm_Tm, up_list_PTm_PTm, up_PTm_PTm, + upRen_list_PTm_PTm, upRen_PTm_PTm, up_ren + | progress cbn[subst_Tm ren_Tm subst_PTm ren_PTm] | progress fsimpl ]). Ltac asimpl := check_no_evars; repeat - unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, - Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1 in *; - asimpl'; minimize. + unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1, + Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1, + VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, Up_Tm_Tm, + Up_Tm, up_Tm, Subst_Tm, Subst1, subst1 in *; asimpl'; + minimize. Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J. Tactic Notation "auto_case" := auto_case ltac:(asimpl; cbn; eauto). Ltac substify := auto_unfold; try setoid_rewrite rinstInst'_Tm_pointwise; - try setoid_rewrite rinstInst'_Tm. + try setoid_rewrite rinstInst'_Tm; + try setoid_rewrite rinstInst'_PTm_pointwise; + try setoid_rewrite rinstInst'_PTm. Ltac renamify := auto_unfold; try setoid_rewrite_left rinstInst'_Tm_pointwise; - try setoid_rewrite_left rinstInst'_Tm. + try setoid_rewrite_left rinstInst'_Tm; + try setoid_rewrite_left rinstInst'_PTm_pointwise; + try setoid_rewrite_left rinstInst'_PTm. End Core. @@ -945,12 +1684,8 @@ Arguments Bool {n_Tm}. Arguments BVal {n_Tm}. -Arguments Bot {n_Tm}. - Arguments Univ {n_Tm}. -Arguments Const {n_Tm}. - Arguments TBind {n_Tm}. Arguments Proj {n_Tm}. @@ -961,10 +1696,30 @@ Arguments App {n_Tm}. Arguments Abs {n_Tm}. +Arguments VarPTm {n_PTm}. + +Arguments PBot {n_PTm}. + +Arguments PUniv {n_PTm}. + +Arguments PConst {n_PTm}. + +Arguments PProj {n_PTm}. + +Arguments PPair {n_PTm}. + +Arguments PApp {n_PTm}. + +Arguments PAbs {n_PTm}. + #[global]Hint Opaque subst_Tm: rewrite. #[global]Hint Opaque ren_Tm: rewrite. +#[global]Hint Opaque subst_PTm: rewrite. + +#[global]Hint Opaque ren_PTm: rewrite. + End Extra. Module interface. diff --git a/theories/diagram.txt b/theories/diagram.txt index 2cf16e8..ab47f3d 100644 --- a/theories/diagram.txt +++ b/theories/diagram.txt @@ -18,3 +18,25 @@ a0 >> a1 | | v v b0 >> b1 + + +prov x (x, x) + +prov x b + + +a => b + +prov x a + +prov y b + +prov x c +prov y c + +extract c = x +extract c = y + +prov x b + +pr diff --git a/theories/fp_red.v b/theories/fp_red.v index e9b5591..3482f45 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -22,86 +22,82 @@ Ltac spec_refl := ltac2:(spec_refl ()). (* Trying my best to not write C style module_funcname *) Module Par. - Inductive R {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1) + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) | AppPair a0 a1 b0 b1 c0 c1: R a0 a1 -> R b0 b1 -> R c0 c1 -> - R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) + R (PApp (PPair a0 b0) c0) (PPair (PApp a1 c1) (PApp b1 c1)) | ProjAbs p a0 a1 : R a0 a1 -> - R (Proj p (Abs a0)) (Abs (Proj p a1)) + R (PProj p (PAbs a0)) (PAbs (PProj p a1)) | ProjPair p a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> - R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero))) + R a0 (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) | PairEta a0 a1 : R a0 a1 -> - R a0 (Pair (Proj PL a1) (Proj PR a1)) + R a0 (PPair (PProj PL a1) (PProj PR a1)) (*************** Congruence ********************) - | Var i : R (VarTm i) (VarTm i) + | Var i : R (VarPTm i) (VarPTm i) | AbsCong a0 a1 : R a0 a1 -> - R (Abs a0) (Abs a1) + R (PAbs a0) (PAbs a1) | AppCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App a0 b0) (App a1 b1) + R (PApp a0 b0) (PApp a1 b1) | PairCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Pair a0 b0) (Pair a1 b1) + R (PPair a0 b0) (PPair 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) + R (PProj p a0) (PProj p a1) | ConstCong k : - R (Const k) (Const k) - | UnivCong i : - R (Univ i) (Univ i) - | BotCong : - R Bot Bot. + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. - Lemma refl n (a : Tm n) : R a a. + Lemma refl n (a : PTm n) : R a a. elim : n /a; hauto ctrs:R. Qed. - Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : - t = subst_Tm (scons b1 VarTm) a1 -> + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) t. + R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) 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 (Proj p (Pair a0 b0)) t. + R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma AppEta' n (a0 a1 b : Tm n) : - b = (Abs (App (ren_Tm shift a1) (VarTm var_zero))) -> + 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 renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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 : m ξ. elim : n a b /h. @@ -113,13 +109,13 @@ Module Par. Qed. - Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : + 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_Tm ρ0 a) (subst_Tm ρ1 b). + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. move => + h. move : m ρ0 ρ1. elim : n a b/h. - move => n a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=. - eapply AppAbs' with (a1 := subst_Tm (up_Tm_Tm ρ1) a1); eauto. + eapply AppAbs' with (a1 := subst_PTm (up_PTm_PTm ρ1) a1); eauto. by asimpl. hauto l:on use:renaming inv:option. - hauto lq:on rew:off ctrs:R. @@ -134,19 +130,18 @@ Module Par. - qauto l:on ctrs:R. - qauto l:on ctrs:R. - hauto l:on inv:option ctrs:R use:renaming. - - sfirstorder. - - sfirstorder. - - sfirstorder. + - qauto l:on ctrs:R. + - qauto l:on ctrs:R. Qed. - Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : - R a b -> R (subst_Tm ρ a) (subst_Tm ρ b). + 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 antirenaming n m (a : Tm n) (b : Tm m) (ξ : fin n -> fin m) : - R (ren_Tm ξ a) b -> exists b0, R a b0 /\ ren_Tm ξ b0 = b. + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. Proof. - move E : (ren_Tm ξ a) => u h. + move E : (ren_PTm ξ a) => u h. move : n ξ a E. elim : m u b/h. - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=. move => c c0 [+ ?]. subst. @@ -190,7 +185,7 @@ Module Par. spec_refl. move :iha => [b0 [? ?]]. subst. eexists. split. by apply AbsCong; eauto. - by asimpl. + done. - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. @@ -201,43 +196,37 @@ Module Par. spec_refl. move : iha => [b0 [? ?]]. subst. move : ihb => [c0 [? ?]]. subst. - eexists. split. by apply PairCong; eauto. - by asimpl. + eexists. split=>/=. by apply PairCong; eauto. + done. - move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. by apply ProjCong; eauto. - by asimpl. - - move => n p A0 A1 B0 B1 ha iha hB ihB m ξ []//= ? t t0 [*]. subst. - spec_refl. - move : iha => [b0 [? ?]]. - move : ihB => [c0 [? ?]]. subst. - eexists. split. by apply BindCong; eauto. - by asimpl. - - move => n k m ξ []//=. hauto l:on. - - move => n i n0 ξ []//=. hauto l:on. - - hauto q:on inv:Tm ctrs:R. + 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 n m (a b : Tm n) (ξ : fin n -> fin m) : - rtc Par.R a b -> rtc Par.R (ren_Tm ξ a) (ren_Tm ξ b). + 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 n m (a b : Tm n) (ρ : fin n -> Tm m) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc Par.R a b -> - rtc Par.R (subst_Tm ρ a) (subst_Tm ρ b). + rtc Par.R (subst_PTm ρ a) (subst_PTm ρ b). induction 1; hauto l:on ctrs:rtc use:Par.substing. Qed. - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ξ : fin n -> fin m) : - rtc Par.R (ren_Tm ξ a) b -> exists b0, rtc Par.R a b0 /\ ren_Tm ξ b0 = b. + 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_Tm ξ a) => u h. + move E :(ren_PTm ξ a) => u h. move : a E. elim : u b /h. - sfirstorder. @@ -254,109 +243,106 @@ Module Pars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma ProjCong n p (a0 a1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc Par.R a0 a1 -> - rtc Par.R (Proj p a0) (Proj p a1). + rtc Par.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc Par.R a0 a1 -> rtc Par.R b0 b1 -> - rtc Par.R (Pair a0 b0) (Pair a1 b1). + rtc Par.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc Par.R a0 a1 -> rtc Par.R b0 b1 -> - rtc Par.R (App a0 b0) (App a1 b1). + rtc Par.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma AbsCong n (a b : Tm (S n)) : + Lemma AbsCong n (a b : PTm (S n)) : rtc Par.R a b -> - rtc Par.R (Abs a) (Abs b). + rtc Par.R (PAbs a) (PAbs b). Proof. solve_s. Qed. End Pars. -Definition var_or_const {n} (a : Tm n) := +Definition var_or_const {n} (a : PTm n) := match a with - | VarTm _ => true - | Bot => true + | VarPTm _ => true + | PBot => true | _ => false end. + (***************** Beta rules only ***********************) Module RPar. - Inductive R {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1) + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) | AppPair a0 a1 b0 b1 c0 c1: R a0 a1 -> R b0 b1 -> R c0 c1 -> - R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) + R (PApp (PPair a0 b0) c0) (PPair (PApp a1 c1) (PApp b1 c1)) | ProjAbs p a0 a1 : R a0 a1 -> - R (Proj p (Abs a0)) (Abs (Proj p a1)) + R (PProj p (PAbs a0)) (PAbs (PProj p a1)) | ProjPair p a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) (*************** Congruence ********************) - | Var i : R (VarTm i) (VarTm i) + | Var i : R (VarPTm i) (VarPTm i) | AbsCong a0 a1 : R a0 a1 -> - R (Abs a0) (Abs a1) + R (PAbs a0) (PAbs a1) | AppCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App a0 b0) (App a1 b1) + R (PApp a0 b0) (PApp a1 b1) | PairCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Pair a0 b0) (Pair a1 b1) + R (PPair a0 b0) (PPair 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) + R (PProj p a0) (PProj p a1) | ConstCong k : - R (Const k) (Const k) - | UnivCong i : - R (Univ i) (Univ i) - | BotCong : - R Bot Bot. + R (PConst k) (PConst k) + | Univ i : + R (PUniv i) (PUniv i) + | Bot : + R PBot PBot. - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma refl n (a : Tm n) : R a a. + Lemma refl n (a : PTm n) : R a a. Proof. induction a; hauto lq:on ctrs:R. Qed. - Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : - t = subst_Tm (scons b1 VarTm) a1 -> + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) t. + R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) 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 (Proj p (Pair a0 b0)) t. + R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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 : m ξ. elim : n a b /h. @@ -364,25 +350,25 @@ Module RPar. all : qauto ctrs:R use:ProjPair'. Qed. - Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : + 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_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)). + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). Proof. eauto using renaming. Qed. - Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm m) 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:option. Qed. - Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) : + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> - (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)). - Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed. + (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 n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : + 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_Tm ρ0 a) (subst_Tm ρ1 b). + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. move => + h. move : m ρ0 ρ1. elim : n a b /h. @@ -400,33 +386,32 @@ Module RPar. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. Qed. - Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : R a b -> - R (subst_Tm ρ a) (subst_Tm ρ b). + R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma cong n (a b : Tm (S n)) c d : + Lemma cong n (a b : PTm (S n)) c d : R a b -> R c d -> - R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). + R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. qauto l:on ctrs:R inv:option. Qed. - Lemma var_or_const_imp {n} (a b : Tm n) : + Lemma var_or_const_imp {n} (a b : PTm n) : var_or_const a -> a = b -> ~~ var_or_const b -> False. Proof. - hauto lq:on inv:Tm. + hauto lq:on inv:PTm. Qed. - Lemma var_or_const_up n m (ρ : fin n -> Tm m) : + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - (forall i, var_or_const (up_Tm_Tm ρ i)). + (forall i, var_or_const (up_PTm_PTm ρ i)). Proof. move => h /= [i|]. - asimpl. @@ -439,11 +424,11 @@ Module RPar. Local Ltac antiimp := qauto l:on use:var_or_const_imp. - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E : (subst_Tm ρ a) => u hρ h. + 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. @@ -460,7 +445,8 @@ Module RPar. eexists. split. apply AppAbs; eauto. by asimpl. - - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; + - 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. @@ -527,87 +513,72 @@ Module RPar. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjCong; eauto. reflexivity. - - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; - first by antiimp. - move => ? t t0 [*]. subst. - have {}/iha := (hρ) => iha. - have /var_or_const_up {}/ihB := (hρ) => ihB. - spec_refl. - move : iha => [b0 [? ?]]. - move : ihB => [c0 [? ?]]. subst. - eexists. split. by apply BindCong; eauto. - by asimpl. - - hauto q:on ctrs:R inv:Tm. - - move => n i n0 ρ hρ []//=; first by antiimp. - hauto l:on. - - move => n m ρ hρ []//=; hauto lq:on ctrs:R. + - 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 {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1) + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) | ProjPair p a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) (*************** Congruence ********************) - | Var i : R (VarTm i) (VarTm i) + | Var i : R (VarPTm i) (VarPTm i) | AbsCong a0 a1 : R a0 a1 -> - R (Abs a0) (Abs a1) + R (PAbs a0) (PAbs a1) | AppCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App a0 b0) (App a1 b1) + R (PApp a0 b0) (PApp a1 b1) | PairCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Pair a0 b0) (Pair a1 b1) + R (PPair a0 b0) (PPair 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) + R (PProj p a0) (PProj p a1) | ConstCong k : - R (Const k) (Const k) + R (PConst k) (PConst k) | UnivCong i : - R (Univ i) (Univ i) + R (PUniv i) (PUniv i) | BotCong : - R Bot Bot. + R PBot PBot. - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma refl n (a : Tm n) : R a a. + Lemma refl n (a : PTm n) : R a a. Proof. induction a; hauto lq:on ctrs:R. Qed. - Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : - t = subst_Tm (scons b1 VarTm) a1 -> + Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> - R (App (Abs a0) b0) t. + R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) 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 (Proj p (Pair a0 b0)) t. + R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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 : m ξ. elim : n a b /h. @@ -615,25 +586,25 @@ Module RPar'. all : qauto ctrs:R use:ProjPair'. Qed. - Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : + 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_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)). + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). Proof. eauto using renaming. Qed. - Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm m) 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:option. Qed. - Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) : + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> - (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)). - Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed. + (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 n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : + 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_Tm ρ0 a) (subst_Tm ρ1 b). + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. move => + h. move : m ρ0 ρ1. elim : n a b /h. @@ -646,36 +617,35 @@ Module RPar'. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R use:morphing_up. - - 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 n m (a b : Tm n) (ρ : fin n -> Tm m) : + Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : R a b -> - R (subst_Tm ρ a) (subst_Tm ρ b). + R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma cong n (a b : Tm (S n)) c d : + Lemma cong n (a b : PTm (S n)) c d : R a b -> R c d -> - R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). + R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. qauto l:on ctrs:R inv:option. Qed. - Lemma var_or_const_imp {n} (a b : Tm n) : + Lemma var_or_const_imp {n} (a b : PTm n) : var_or_const a -> a = b -> ~~ var_or_const b -> False. Proof. - hauto lq:on inv:Tm. + hauto lq:on inv:PTm. Qed. - Lemma var_or_const_up n m (ρ : fin n -> Tm m) : + Lemma var_or_const_up n m (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - (forall i, var_or_const (up_Tm_Tm ρ i)). + (forall i, var_or_const (up_PTm_PTm ρ i)). Proof. move => h /= [i|]. - asimpl. @@ -688,11 +658,11 @@ Module RPar'. Local Ltac antiimp := qauto l:on use:var_or_const_imp. - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. + R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E : (subst_Tm ρ a) => u hρ h. + 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. @@ -756,66 +726,50 @@ Module RPar'. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjCong; eauto. reflexivity. - - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; - first by antiimp. - move => ? t t0 [*]. subst. - have {}/iha := (hρ) => iha. - have /var_or_const_up {}/ihB := (hρ) => ihB. - spec_refl. - move : iha => [b0 [? ?]]. - move : ihB => [c0 [? ?]]. subst. - eexists. split. by apply BindCong; eauto. - by asimpl. - - hauto q:on ctrs:R inv:Tm. + - hauto q:on ctrs:R inv:PTm. - move => n i n0 ρ hρ []//=; first by antiimp. hauto l:on. - - hauto q:on inv:Tm ctrs:R. + - hauto q:on inv:PTm ctrs:R. Qed. End RPar'. Module ERed. - Inductive R {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a : - R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) + R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) | PairEta a : - R a (Pair (Proj PL a) (Proj PR a)) + R a (PPair (PProj PL a) (PProj PR a)) (*************** Congruence ********************) | AbsCong a0 a1 : R a0 a1 -> - R (Abs a0) (Abs a1) + R (PAbs a0) (PAbs a1) | AppCong0 a0 a1 b : R a0 a1 -> - R (App a0 b) (App a1 b) + R (PApp a0 b) (PApp a1 b) | AppCong1 a b0 b1 : R b0 b1 -> - R (App a b0) (App a b1) + R (PApp a b0) (PApp a b1) | PairCong0 a0 a1 b : R a0 a1 -> - R (Pair a0 b) (Pair a1 b) + R (PPair a0 b) (PPair a1 b) | PairCong1 a b0 b1 : R b0 b1 -> - R (Pair a b0) (Pair a b1) + R (PPair a b0) (PPair a b1) | ProjCong p a0 a1 : R a0 a1 -> - R (Proj p a0) (Proj p a1) - | BindCong0 p A0 A1 B: - R A0 A1 -> - R (TBind p A0 B) (TBind p A1 B) - | BindCong1 p A B0 B1: - R B0 B1 -> - R (TBind p A B0) (TBind p A B1). + R (PProj p a0) (PProj p a1). - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma AppEta' n a (u : Tm n) : - u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) -> + 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 n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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 : m ξ. elim : n a b /h. @@ -825,9 +779,9 @@ Module ERed. all : qauto ctrs:R. Qed. - Lemma substing n m (a : Tm n) b (ρ : fin n -> Tm m) : + Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : R a b -> - R (subst_Tm ρ a) (subst_Tm ρ b). + R (subst_PTm ρ a) (subst_PTm ρ b). Proof. move => h. move : m ρ. elim : n a b / h => n. move => a m ρ /=. @@ -846,79 +800,69 @@ Module EReds. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong n (a b : Tm (S n)) : + Lemma AbsCong n (a b : PTm (S n)) : rtc ERed.R a b -> - rtc ERed.R (Abs a) (Abs b). + rtc ERed.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc ERed.R a0 a1 -> rtc ERed.R b0 b1 -> - rtc ERed.R (App a0 b0) (App a1 b1). + rtc ERed.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc ERed.R a0 a1 -> rtc ERed.R b0 b1 -> - rtc ERed.R (TBind p a0 b0) (TBind p a1 b1). + rtc ERed.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (Pair a0 b0) (Pair a1 b1). - Proof. solve_s. Qed. - - Lemma ProjCong n p (a0 a1 : Tm n) : - rtc ERed.R a0 a1 -> - rtc ERed.R (Proj p a0) (Proj p a1). + rtc ERed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. End EReds. Module EPar. - Inductive R {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> - R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero))) + R a0 (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) | PairEta a0 a1 : R a0 a1 -> - R a0 (Pair (Proj PL a1) (Proj PR a1)) + R a0 (PPair (PProj PL a1) (PProj PR a1)) (*************** Congruence ********************) - | Var i : R (VarTm i) (VarTm i) + | Var i : R (VarPTm i) (VarPTm i) | AbsCong a0 a1 : R a0 a1 -> - R (Abs a0) (Abs a1) + R (PAbs a0) (PAbs a1) | AppCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (App a0 b0) (App a1 b1) + R (PApp a0 b0) (PApp a1 b1) | PairCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> - R (Pair a0 b0) (Pair a1 b1) + R (PPair a0 b0) (PPair 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) + R (PProj p a0) (PProj p a1) | ConstCong k : - R (Const k) (Const k) + R (PConst k) (PConst k) | UnivCong i : - R (Univ i) (Univ i) + R (PUniv i) (PUniv i) | BotCong : - R Bot Bot. + R PBot PBot. - Lemma refl n (a : Tm n) : 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 n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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 : m ξ. elim : n a b /h. @@ -930,18 +874,18 @@ Module EPar. all : qauto ctrs:R. Qed. - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma AppEta' n (a0 a1 b : Tm n) : - b = (Abs (App (ren_Tm shift a1) (VarTm var_zero))) -> + 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 n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : + 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_Tm ρ0 a) (subst_Tm ρ1 b). + R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. move => h. move : m ρ0 ρ1. elim : n a b / h => n. - move => a0 a1 ha iha m ρ0 ρ1 hρ /=. @@ -955,13 +899,12 @@ Module EPar. - hauto l:on ctrs:R use:renaming inv:option. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. Qed. - Lemma substing n a0 a1 (b0 b1 : Tm n) : + Lemma substing n a0 a1 (b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> - R (subst_Tm (scons b0 VarTm) a0) (subst_Tm (scons b1 VarTm) a1). + R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1). Proof. move => h0 h1. apply morphing => //. hauto lq:on ctrs:R inv:option. @@ -971,14 +914,14 @@ End EPar. Module OExp. - Inductive R {n} : Tm n -> Tm n -> Prop := + Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) | AppEta a : - R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) + R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) | PairEta a : - R a (Pair (Proj PL a) (Proj PR a)). + R a (PPair (PProj PL a) (PProj PR a)). - Lemma merge n (t a b : Tm n) : + Lemma merge n (t a b : PTm n) : rtc R a b -> EPar.R t a -> EPar.R t b. @@ -988,7 +931,7 @@ Module OExp. - hauto q:on ctrs:EPar.R inv:R. Qed. - Lemma commutativity n (a b c : Tm n) : + 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. @@ -997,7 +940,7 @@ Module OExp. - hauto lq:on ctrs:EPar.R, R. Qed. - Lemma commutativity0 n (a b c : Tm n) : + 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. @@ -1022,72 +965,66 @@ Module RPars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong n (a b : Tm (S n)) : + Lemma AbsCong n (a b : PTm (S n)) : rtc RPar.R a b -> - rtc RPar.R (Abs a) (Abs b). + rtc RPar.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> - rtc RPar.R (App a0 b0) (App a1 b1). + rtc RPar.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> - rtc RPar.R (TBind p a0 b0) (TBind p a1 b1). + rtc RPar.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc RPar.R a0 a1 -> - rtc RPar.R b0 b1 -> - rtc RPar.R (Pair a0 b0) (Pair a1 b1). + rtc RPar.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : Tm n) : + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc RPar.R a0 a1 -> - rtc RPar.R (Proj p a0) (Proj p a1). - Proof. solve_s. Qed. - - Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : - rtc RPar.R a0 a1 -> - rtc RPar.R (ren_Tm ξ a0) (ren_Tm ξ a1). + rtc RPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. induction 1. - apply rtc_refl. - eauto using RPar.renaming, rtc_l. Qed. - Lemma weakening n (a0 a1 : Tm n) : + Lemma weakening n (a0 a1 : PTm n) : rtc RPar.R a0 a1 -> - rtc RPar.R (ren_Tm shift a0) (ren_Tm shift a1). + rtc RPar.R (ren_PTm shift a0) (ren_PTm shift a1). Proof. apply renaming. Qed. - Lemma Abs_inv n (a : Tm (S n)) b : - rtc RPar.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar.R a a'. + 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 : (Abs a) => b0 h. move : a E. + move E : (PAbs a) => b0 h. move : a E. elim : b0 b / h. - hauto lq:on ctrs:rtc. - hauto lq:on ctrs:rtc inv:RPar.R, rtc. Qed. - Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) : + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc RPar.R a b -> - rtc RPar.R (subst_Tm ρ a) (subst_Tm ρ b). + rtc RPar.R (subst_PTm ρ a) (subst_PTm ρ b). Proof. induction 1; qauto l:on ctrs:rtc use:RPar.substing. Qed. - Lemma substing n (a b : Tm (S n)) c : + Lemma substing n (a b : PTm (S n)) c : rtc RPar.R a b -> - rtc RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). + rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). Proof. hauto lq:on use:morphing inv:option. Qed. - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - rtc RPar.R (subst_Tm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_Tm ρ b0 = b. + rtc RPar.R (subst_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E :(subst_Tm ρ a) => u hρ h. + move E :(subst_PTm ρ a) => u hρ h. move : a E. elim : u b /h. - sfirstorder. @@ -1109,72 +1046,66 @@ Module RPars'. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AbsCong n (a b : Tm (S n)) : + Lemma AbsCong n (a b : PTm (S n)) : rtc RPar'.R a b -> - rtc RPar'.R (Abs a) (Abs b). + rtc RPar'.R (PAbs a) (PAbs b). Proof. solve_s. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R b0 b1 -> - rtc RPar'.R (App a0 b0) (App a1 b1). + rtc RPar'.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc RPar'.R a0 a1 -> rtc RPar'.R b0 b1 -> - rtc RPar'.R (TBind p a0 b0) (TBind p a1 b1). + rtc RPar'.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc RPar'.R a0 a1 -> - rtc RPar'.R b0 b1 -> - rtc RPar'.R (Pair a0 b0) (Pair a1 b1). + rtc RPar'.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : Tm n) : + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc RPar'.R a0 a1 -> - rtc RPar'.R (Proj p a0) (Proj p a1). - Proof. solve_s. Qed. - - Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : - rtc RPar'.R a0 a1 -> - rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1). + rtc RPar'.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. induction 1. - apply rtc_refl. - eauto using RPar'.renaming, rtc_l. Qed. - Lemma weakening n (a0 a1 : Tm n) : + Lemma weakening n (a0 a1 : PTm n) : rtc RPar'.R a0 a1 -> - rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1). + rtc RPar'.R (ren_PTm shift a0) (ren_PTm shift a1). Proof. apply renaming. Qed. - Lemma Abs_inv n (a : Tm (S n)) b : - rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'. + 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 : (Abs a) => b0 h. move : a E. + move E : (PAbs a) => b0 h. move : a E. elim : b0 b / h. - hauto lq:on ctrs:rtc. - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. Qed. - Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) : + Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) : rtc RPar'.R a b -> - rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b). + rtc RPar'.R (subst_PTm ρ a) (subst_PTm ρ b). Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. - Lemma substing n (a b : Tm (S n)) c : + Lemma substing n (a b : PTm (S n)) c : rtc RPar'.R a b -> - rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). + rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). Proof. hauto lq:on use:morphing inv:option. Qed. - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b. + rtc RPar'.R (subst_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_PTm ρ b0 = b. Proof. - move E :(subst_Tm ρ a) => u hρ h. + move E :(subst_PTm ρ a) => u hρ h. move : a E. elim : u b /h. - sfirstorder. @@ -1187,15 +1118,15 @@ Module RPars'. End RPars'. -Lemma Abs_EPar n a (b : Tm n) : - EPar.R (Abs a) b -> +Lemma Abs_EPar n a (b : PTm n) : + EPar.R (PAbs a) b -> (exists d, EPar.R a d /\ - rtc RPar.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\ + rtc RPar.R (PApp (ren_PTm shift b) (VarPTm var_zero)) d) /\ (exists d, EPar.R a d /\ forall p, - rtc RPar.R (Proj p b) (Abs (Proj p d))). + rtc RPar.R (PProj p b) (PAbs (PProj p d))). Proof. - move E : (Abs a) => u h. + move E : (PAbs a) => u h. move : a E. elim : n u b /h => //=. - move => n a0 a1 ha iha b ?. subst. @@ -1216,14 +1147,14 @@ Proof. - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl). move : iha => [_ [d [ih0 ih1]]]. split. - + exists (Pair (Proj PL d) (Proj PR d)). + + exists (PPair (PProj PL d) (PProj PR d)). split; first by apply EPar.PairEta. apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl. - suff h : forall p, rtc RPar.R (App (Proj p (ren_Tm shift a1)) (VarTm var_zero)) (Proj p d) by + suff h : forall p, rtc RPar.R (PApp (PProj p (ren_PTm shift a1)) (VarPTm var_zero)) (PProj p d) by sfirstorder use:RPars.PairCong. move => p. move /(_ p) /RPars.weakening in ih1. - apply relations.rtc_transitive with (y := App (ren_Tm shift (Abs (Proj p d))) (VarTm var_zero)). + apply relations.rtc_transitive with (y := PApp (ren_PTm shift (PAbs (PProj p d))) (VarPTm var_zero)). by eauto using RPars.AppCong, rtc_refl. apply relations.rtc_once => /=. apply : RPar.AppAbs'; eauto using RPar.refl. @@ -1239,21 +1170,21 @@ Proof. apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl. Qed. -Lemma Pair_EPar n (a b c : Tm n) : - EPar.R (Pair a b) c -> - (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\ - (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero)) - (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\ +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)) + (PPair (PApp (ren_PTm shift d0) (VarPTm var_zero))(PApp (ren_PTm shift d1) (VarPTm var_zero))) /\ EPar.R a d0 /\ EPar.R b d1). Proof. - move E : (Pair a b) => u h. move : a b E. + move E : (PPair a b) => u h. move : a b E. 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. + move => p. - exists (Abs (App (ren_Tm shift (if p is PL then d0 else d1)) (VarTm var_zero))). + exists (PAbs (PApp (ren_PTm shift (if p is PL then d0 else d1)) (VarPTm var_zero))). split. * apply : relations.rtc_transitive. ** apply RPars.ProjCong. apply RPars.AbsCong. eassumption. @@ -1271,7 +1202,7 @@ Proof. exists d. split=>//. apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. set q := (X in rtc RPar.R X d). - by have -> : q = Proj p a1 by hauto lq:on. + by have -> : q = PProj p a1 by hauto lq:on. + move :iha => [iha _]. move : (iha PL) => [d0 [ih0 ih0']]. move : (iha PR) => [d1 [ih1 ih1']] {iha}. @@ -1292,7 +1223,7 @@ Proof. split => //. Qed. -Lemma commutativity0 n (a b0 b1 : Tm n) : +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. @@ -1300,13 +1231,13 @@ Proof. - move => n a b0 ha iha b1 hb. move : iha (hb) => /[apply]. move => [c [ih0 ih1]]. - exists (Abs (App (ren_Tm shift c) (VarTm var_zero))). + 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 => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. move => [c [ih0 ih1]]. - exists (Pair (Proj PL c) (Proj PR c)). split. + 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. @@ -1319,9 +1250,9 @@ Proof. elim /RPar.inv => //= _. + move => a2 a3 b3 b4 h0 h1 [*]. subst. move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]]. - have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R. + have {}/iha : RPar.R (PAbs a2) (PAbs a3) by hauto lq:on ctrs:RPar.R. move => [c [ih0 /Abs_EPar [[d [ih1 ih2]] _]]]. - exists (subst_Tm (scons b VarTm) d). + exists (subst_PTm (scons b VarPTm) d). split. (* By substitution *) * move /RPars.substing : ih2. @@ -1337,7 +1268,7 @@ Proof. move /Pair_EPar : ihc1 => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. move /RPars.substing : ih0. move /(_ d). asimpl => h. - exists (Pair (App d0 d) (App d1 d)). + exists (PPair (PApp d0 d) (PApp d1 d)). split. hauto lq:on use:relations.rtc_transitive, RPars.AppCong. apply EPar.PairCong; by apply EPar.AppCong. @@ -1348,7 +1279,7 @@ Proof. + move => ? a0 a1 h [*]. subst. move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]]. move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]]. - exists (Abs (Proj p d)). + exists (PAbs (PProj p d)). qauto l:on ctrs:EPar.R use:RPars.ProjCong, @relations.rtc_transitive. + move => p0 a0 a1 b2 b3 h1 h2 [*]. subst. move /(_ _ ltac:(by eauto using RPar.PairCong)) : ih0 => [c [ih0 ih1]]. @@ -1356,13 +1287,12 @@ Proof. exists d. split => //. hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - 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 n (a b0 b1 : Tm n) : +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. @@ -1371,7 +1301,7 @@ Proof. - qauto l:on use:relations.rtc_transitive, commutativity0. Qed. -Lemma commutativity n (a b0 b1 : Tm n) : +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. @@ -1380,12 +1310,12 @@ Lemma commutativity n (a b0 b1 : Tm n) : hauto q:on ctrs:rtc. Qed. -Lemma Abs_EPar' n a (b : Tm n) : - EPar.R (Abs a) b -> +Lemma Abs_EPar' n a (b : PTm n) : + EPar.R (PAbs a) b -> (exists d, EPar.R a d /\ - rtc OExp.R (Abs d) b). + rtc OExp.R (PAbs d) b). Proof. - move E : (Abs a) => u h. + move E : (PAbs a) => u h. move : a E. elim : n u b /h => //=. - move => n a0 a1 ha iha a ?. subst. @@ -1397,12 +1327,12 @@ Proof. - hauto l:on ctrs:OExp.R. Qed. -Lemma Proj_EPar' n p a (b : Tm n) : - EPar.R (Proj p a) b -> +Lemma Proj_EPar' n p a (b : PTm n) : + EPar.R (PProj p a) b -> (exists d, EPar.R a d /\ - rtc OExp.R (Proj p d) b). + rtc OExp.R (PProj p d) b). Proof. - move E : (Proj p a) => u h. + move E : (PProj p a) => u h. move : p a E. elim : n u b /h => //=. - move => n a0 a1 ha iha a p ?. subst. @@ -1414,11 +1344,11 @@ Proof. - hauto l:on ctrs:OExp.R. Qed. -Lemma App_EPar' n (a b u : Tm n) : - EPar.R (App a b) u -> - (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (App a0 b0) u). +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 : (App a b) => t h. + move E : (PApp a b) => t h. move : a b E. elim : n t u /h => //=. - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). @@ -1429,11 +1359,11 @@ Proof. - hauto l:on ctrs:OExp.R. Qed. -Lemma Bind_EPar' n p (a : Tm n) b u : - EPar.R (TBind p a b) u -> - (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (TBind p a0 b0) u). +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 : (TBind p a b) => t h. + move E : (PPair a b) => t h. move : a b E. elim : n t u /h => //=. - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). @@ -1444,25 +1374,10 @@ Proof. - hauto l:on ctrs:OExp.R. Qed. -Lemma Pair_EPar' n (a b u : Tm n) : - EPar.R (Pair a b) u -> - exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (Pair a0 b0) u. -Proof. - move E : (Pair a b) => t h. - 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 => 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' n k (u : Tm n) : - EPar.R (Const k) u -> - rtc OExp.R (Const k) u. - move E : (Const k) => t h. +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 : n t u /h => //=. - move => n a0 a1 h ih k ?. subst. specialize ih with (1 := eq_refl). @@ -1473,10 +1388,10 @@ Lemma Const_EPar' n k (u : Tm n) : - hauto l:on ctrs:OExp.R. Qed. -Lemma Bot_EPar' n (u : Tm n) : - EPar.R (Bot) u -> - rtc OExp.R (Bot) u. - move E : (Bot) => t h. +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). @@ -1487,10 +1402,10 @@ Lemma Bot_EPar' n (u : Tm n) : - hauto l:on ctrs:OExp.R. Qed. -Lemma Univ_EPar' n i (u : Tm n) : - EPar.R (Univ i) u -> - rtc OExp.R (Univ i) u. - move E : (Univ i) => t h. +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). @@ -1501,14 +1416,14 @@ Lemma Univ_EPar' n i (u : Tm n) : - hauto l:on ctrs:OExp.R. Qed. -Lemma EPar_diamond n (c a1 b1 : Tm n) : +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 : n c a1 / h. - move => n c a1 ha iha b1 /iha [d2 [hd0 hd1]]. - exists(Abs (App (ren_Tm shift d2) (VarTm var_zero))). + 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. @@ -1516,62 +1431,54 @@ Proof. move /Abs_EPar' => [d [hd0 hd1]]. move : iha hd0; repeat move/[apply]. move => [d2 [h0 h1]]. - have : EPar.R (Abs d) (Abs d2) by eauto using EPar.AbsCong. + have : EPar.R (PAbs d) (PAbs d2) by eauto using EPar.AbsCong. move : OExp.commutativity0 hd1; repeat move/[apply]. move => [d1 [hd1 hd2]]. exists d1. hauto lq:on ctrs:EPar.R use:OExp.merge. - 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 (App a2 b2)(App a3 b3) + 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 => 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 (Pair a2 b2)(Pair a3 b3) + 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 => n p a0 a1 ha iha b. move /Proj_EPar' => [d [/iha [d2 h] h1]] {iha}. - have : EPar.R (Proj p d) (Proj p d2) + have : EPar.R (PProj p d) (PProj p d2) by hauto l:on use:EPar.ProjCong. move : OExp.commutativity0 h1; repeat move/[apply]. move => [d1 h1]. exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - - move => n p a0 a1 b0 b1 ha iha hb ihb c. - move /Bind_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. - have : EPar.R (TBind p a2 b2)(TBind p a3 b3) - by hauto l:on use:EPar.BindCong. - move : OExp.commutativity0 h2; repeat move/[apply]. - move => [d h]. - exists d. 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 {n} (a : Tm n) := +Function tstar {n} (a : PTm n) := match a with - | VarTm i => a - | Abs a => Abs (tstar a) - | App (Abs a) b => subst_Tm (scons (tstar b) VarTm) (tstar a) - | App (Pair a b) c => - Pair (App (tstar a) (tstar c)) (App (tstar b) (tstar c)) - | App a b => App (tstar a) (tstar b) - | Pair a b => Pair (tstar a) (tstar b) - | Proj p (Pair a b) => if p is PL then (tstar a) else (tstar b) - | Proj p (Abs a) => (Abs (Proj p (tstar a))) - | Proj p a => Proj p (tstar a) - | TBind p a b => TBind p (tstar a) (tstar b) - | Const k => Const k - | Univ i => Univ i - | Bot => Bot + | VarPTm i => a + | PAbs a => PAbs (tstar a) + | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a) + | PApp (PPair a b) c => + PPair (PApp (tstar a) (tstar c)) (PApp (tstar b) (tstar c)) + | PApp a b => PApp (tstar a) (tstar b) + | PPair a b => PPair (tstar a) (tstar b) + | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b) + | 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 n (a : Tm n) : 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 => {n a}. - hauto lq:on inv:RPar.R ctrs:RPar.R. @@ -1587,25 +1494,23 @@ 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. Qed. -Function tstar' {n} (a : Tm n) := +Function tstar' {n} (a : PTm n) := match a with - | VarTm i => a - | Abs a => Abs (tstar' a) - | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a) - | App a b => App (tstar' a) (tstar' b) - | Pair a b => Pair (tstar' a) (tstar' b) - | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b) - | Proj p a => Proj p (tstar' a) - | TBind p a b => TBind p (tstar' a) (tstar' b) - | Const k => Const k - | Univ i => Univ i - | Bot => Bot + | VarPTm i => a + | PAbs a => PAbs (tstar' a) + | PApp (PAbs a) b => subst_PTm (scons (tstar' b) VarPTm) (tstar' a) + | PApp a b => PApp (tstar' a) (tstar' b) + | PPair a b => PPair (tstar' a) (tstar' b) + | 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 n (a : Tm n) : 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 => {n a}. - hauto lq:on inv:RPar'.R ctrs:RPar'.R. @@ -1619,22 +1524,21 @@ 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. Qed. -Lemma RPar_diamond n (c a1 b1 : Tm n) : +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 n (c a1 b1 : Tm n) : +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 n (c a1 b1 : Tm n) : +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. @@ -1642,7 +1546,7 @@ Proof. sfirstorder use:relations.diamond_confluent, RPar_diamond. Qed. -Lemma EPar_confluent n (c a1 b1 : Tm n) : +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. @@ -1650,52 +1554,35 @@ Proof. sfirstorder use:relations.diamond_confluent, EPar_diamond. Qed. -Definition prov_bind {n} p0 A0 B0 (a : Tm n) := - match a with - | TBind p A B => p = p0 /\ rtc Par.R A A0 /\ rtc Par.R B B0 - | _ => False - end. - -Definition prov_univ {n} i0 (a : Tm n) := - match a with - | Univ i => i = i0 - | _ => False - end. - - -Inductive prov {n} : Tm n -> Tm n -> Prop := -| P_Bind p A A0 B B0 : - rtc Par.R A A0 -> - rtc Par.R B B0 -> - prov (TBind p A B) (TBind p A0 B0) +Inductive prov {n} : PTm n -> PTm n -> Prop := | P_Abs h a : - (forall b, prov h (subst_Tm (scons b VarTm) a)) -> - prov h (Abs a) + (forall b, prov h (subst_PTm (scons b VarPTm) a)) -> + prov h (PAbs a) | P_App h a b : prov h a -> - prov h (App a b) + prov h (PApp a b) | P_Pair h a b : prov h a -> prov h b -> - prov h (Pair a b) + prov h (PPair a b) | P_Proj h p a : prov h a -> - prov h (Proj p a) + prov h (PProj p a) | P_Const k : - prov (Const k) (Const k) + prov (PConst k) (PConst k) | P_Var i : - prov (VarTm i) (VarTm i) + prov (VarPTm i) (VarPTm i) | P_Univ i : - prov (Univ i) (Univ i) + prov (PUniv i) (PUniv i) | P_Bot : - prov Bot Bot. + prov PBot PBot. -Lemma ERed_EPar n (a b : Tm n) : 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 n (a b : Tm n) : 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 : n a b /h. - eauto using rtc_r, ERed.AppEta. @@ -1705,57 +1592,56 @@ Proof. - eauto using EReds.AppCong. - eauto using EReds.PairCong. - eauto using EReds.ProjCong. - - eauto using EReds.BindCong. - auto using rtc_refl. - auto using rtc_refl. - auto using rtc_refl. Qed. -Lemma EPar_Par n (a b : Tm n) : 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 : n a b /h; qauto ctrs:Par.R. Qed. -Lemma RPar_Par n (a b : Tm n) : 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 : n a b /h; hauto lq:on ctrs:Par.R. Qed. -Lemma rtc_idem n (R : Tm n -> Tm n -> Prop) (a b : Tm n) : 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 {n} (a b : Tm n) : 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 n (u : Tm n) 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. elim : u a / h. - - qauto l:on ctrs:prov inv:RPar.R use:@rtc_r, RPar_Par. + (* - qauto l:on ctrs:prov inv:RPar.R use:@rtc_r, RPar_Par. *) - hauto lq:on ctrs:prov inv:RPar.R use:RPar.substing. - move => h a b ha iha b0. elim /RPar.inv => //= _. + move => a0 a1 b1 b2 h0 h1 [*]. subst. - have {}iha : prov h (Abs a1) by hauto lq:on ctrs:RPar.R. + have {}iha : prov h (PAbs a1) by hauto lq:on ctrs:RPar.R. hauto lq:on inv:prov use:RPar.substing. + move => a0 a1 b1 b2 c0 c1. move => h0 h1 h2 [*]. subst. - have {}iha : prov h (Pair a1 b2) by hauto lq:on ctrs:RPar.R. + have {}iha : prov h (PPair a1 b2) by hauto lq:on ctrs:RPar.R. hauto lq:on inv:prov ctrs:prov. + hauto lq:on ctrs:prov. - hauto lq:on ctrs:prov inv:RPar.R. - move => h p a ha iha b. elim /RPar.inv => //= _. + move => p0 a0 a1 h0 [*]. subst. - have {iha} : prov h (Abs a1) by hauto lq:on ctrs:RPar.R. + have {iha} : prov h (PAbs a1) by hauto lq:on ctrs:RPar.R. hauto lq:on ctrs:prov inv:prov use:RPar.substing. + move => p0 a0 a1 b0 b1 h0 h1 [*]. subst. - have {iha} : prov h (Pair a1 b1) by hauto lq:on ctrs:RPar.R. + have {iha} : prov h (PPair a1 b1) by hauto lq:on ctrs:RPar.R. qauto l:on inv:prov. + hauto lq:on ctrs:prov. - hauto lq:on ctrs:prov inv:RPar.R. @@ -1765,33 +1651,23 @@ Proof. Qed. -Lemma prov_lam n (u : Tm n) a : prov u a <-> prov u (Abs (App (ren_Tm shift a) (VarTm 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 := Const TPi). + specialize H2 with (b := PBot). move : H2. asimpl. inversion 1; subst. done. Qed. -Lemma prov_pair n (u : Tm n) a : prov u a <-> prov u (Pair (Proj PL a) (Proj 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 n (u : Tm n) 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. elim : u a / h. - - move => p A A0 B B0 hA hB b. - elim /ERed.inv => // _. - + move => a0 *. subst. - rewrite -prov_lam. - by constructor. - + move => a0 *. subst. - rewrite -prov_pair. - by constructor. - + qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par. - + qauto l:on ctrs:prov use:@rtc_r, ERed_EPar, EPar_Par. - move => h a ha iha b. elim /ERed.inv => // _. + move => a0 *. subst. @@ -1819,26 +1695,25 @@ Proof. - hauto lq:on inv:ERed.R, prov ctrs:prov. Qed. -Lemma prov_ereds n (u : Tm n) 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 {n} (a : Tm n) : Tm n := +Fixpoint extract {n} (a : PTm n) : PTm n := match a with - | TBind p A B => TBind p A B - | Abs a => subst_Tm (scons Bot VarTm) (extract a) - | App a b => extract a - | Pair a b => extract a - | Proj p a => extract a - | Const k => Const k - | VarTm i => VarTm i - | Univ i => Univ i - | Bot => Bot + | 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 n m (a : Tm n) (ξ : fin n -> fin m) : - extract (ren_Tm ξ a) = ren_Tm ξ (extract a). +Lemma ren_extract n m (a : PTm n) (ξ : fin n -> fin m) : + extract (ren_PTm ξ a) = ren_PTm ξ (extract a). Proof. move : m ξ. elim : n/a. - sfirstorder. @@ -1851,12 +1726,11 @@ Proof. - hauto q:on. - sfirstorder. - sfirstorder. - - sfirstorder. Qed. -Lemma ren_morphing n m (a : Tm n) (ρ : fin n -> Tm m) : +Lemma ren_morphing n m (a : PTm n) (ρ : fin n -> PTm m) : (forall i, ρ i = extract (ρ i)) -> - extract (subst_Tm ρ a) = subst_Tm ρ (extract a). + extract (subst_PTm ρ a) = subst_PTm ρ (extract a). Proof. move : m ρ. elim : n /a => n //=. @@ -1869,45 +1743,38 @@ Proof. - by asimpl. Qed. -Lemma ren_subst_bot n (a : Tm (S n)) : - extract (subst_Tm (scons Bot VarTm) a) = subst_Tm (scons Bot VarTm) (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 as [i|] => //=. Qed. -Definition prov_extract_spec {n} u (a : Tm n) := +Definition prov_extract_spec {n} u (a : PTm n) := match u with - | TBind p A B => exists A0 B0, extract a = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0 - | Univ i => extract a = Univ i - | VarTm i => extract a = VarTm i - | (Const i) => extract a = (Const i) - | Bot => extract a = Bot + | 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 n u (a : Tm n) : +Lemma prov_extract n u (a : PTm n) : prov u a -> prov_extract_spec u a. Proof. move => h. elim : u a /h. - - sfirstorder. - move => h a ha ih. case : h ha ih => //=. + move => i ha ih. - move /(_ Bot) in ih. + move /(_ PBot) in ih. rewrite -ih. by rewrite ren_subst_bot. - + move => p A B h ih. - move /(_ Bot) : ih => [A0][B0][h0][h1]h2. - rewrite ren_subst_bot in h0. - rewrite h0. - eauto. - + move => p _ /(_ Bot). + + move => p _ /(_ PBot). by rewrite ren_subst_bot. - + move => i h /(_ Bot). + + move => i h /(_ PBot). by rewrite ren_subst_bot => ->. - + move /(_ Bot). - move => h /(_ Bot). + + move /(_ PBot). + move => h /(_ PBot). by rewrite ren_subst_bot. - hauto lq:on. - hauto lq:on. @@ -1922,21 +1789,21 @@ Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b := R0 a b \/ R1 a b. Module ERPar. - Definition R {n} (a b : Tm n) := union RPar.R EPar.R a b. - Lemma RPar {n} (a b : Tm n) : 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 {n} (a b : Tm n) : 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 {n} ( a : Tm n) : ERPar.R a a. + Lemma refl {n} ( a : PTm n) : ERPar.R a a. Proof. sfirstorder use:RPar.refl, EPar.refl. Qed. - Lemma ProjCong n p (a0 a1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : R a0 a1 -> - rtc R (Proj p a0) (Proj p a1). + rtc R (PProj p a0) (PProj p a1). Proof. move => []. - move => h. @@ -1949,9 +1816,9 @@ Module ERPar. by apply EPar.ProjCong. Qed. - Lemma AbsCong n (a0 a1 : Tm (S n)) : + Lemma AbsCong n (a0 a1 : PTm (S n)) : R a0 a1 -> - rtc R (Abs a0) (Abs a1). + rtc R (PAbs a0) (PAbs a1). Proof. move => []. - move => h. @@ -1964,10 +1831,10 @@ Module ERPar. by apply EPar.AbsCong. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> - rtc R (App a0 b0) (App a1 b1). + rtc R (PApp a0 b0) (PApp a1 b1). Proof. move => [] + []. - sfirstorder use:RPar.AppCong, @rtc_once. @@ -1984,30 +1851,10 @@ Module ERPar. - sfirstorder use:EPar.AppCong, @rtc_once. Qed. - Lemma BindCong n p (a0 a1 : Tm n) b0 b1: + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : R a0 a1 -> R b0 b1 -> - rtc R (TBind p a0 b0) (TBind p a1 b1). - Proof. - move => [] + []. - - sfirstorder use:RPar.BindCong, @rtc_once. - - move => h0 h1. - apply : rtc_l. - left. apply RPar.BindCong; eauto; apply RPar.refl. - apply rtc_once. - hauto l:on use:EPar.BindCong, EPar.refl. - - move => h0 h1. - apply : rtc_l. - left. apply RPar.BindCong; eauto; apply RPar.refl. - apply rtc_once. - hauto l:on use:EPar.BindCong, EPar.refl. - - sfirstorder use:EPar.BindCong, @rtc_once. - Qed. - - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : - R a0 a1 -> - R b0 b1 -> - rtc R (Pair a0 b0) (Pair a1 b1). + rtc R (PPair a0 b0) (PPair a1 b1). Proof. move => [] + []. - sfirstorder use:RPar.PairCong, @rtc_once. @@ -2024,15 +1871,15 @@ Module ERPar. - sfirstorder use:EPar.PairCong, @rtc_once. Qed. - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + 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. Qed. End ERPar. -Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong ERPar.BindCong : erpar. +Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong : erpar. Module ERPars. #[local]Ltac solve_s_rec := @@ -2041,37 +1888,31 @@ Module ERPars. #[local]Ltac solve_s := repeat (induction 1; last by solve_s_rec); apply rtc_refl. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : rtc ERPar.R a0 a1 -> rtc ERPar.R b0 b1 -> - rtc ERPar.R (App a0 b0) (App a1 b1). + rtc ERPar.R (PApp a0 b0) (PApp a1 b1). Proof. solve_s. Qed. - Lemma AbsCong n (a0 a1 : Tm (S n)) : + Lemma AbsCong n (a0 a1 : PTm (S n)) : rtc ERPar.R a0 a1 -> - rtc ERPar.R (Abs a0) (Abs a1). + rtc ERPar.R (PAbs a0) (PAbs a1). Proof. solve_s. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : rtc ERPar.R a0 a1 -> rtc ERPar.R b0 b1 -> - rtc ERPar.R (Pair a0 b0) (Pair a1 b1). + rtc ERPar.R (PPair a0 b0) (PPair a1 b1). Proof. solve_s. Qed. - Lemma ProjCong n p (a0 a1 : Tm n) : + Lemma ProjCong n p (a0 a1 : PTm n) : rtc ERPar.R a0 a1 -> - rtc ERPar.R (Proj p a0) (Proj p a1). + rtc ERPar.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. - Lemma BindCong n p (a0 a1 : Tm n) b0 b1: + Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) : rtc ERPar.R a0 a1 -> - rtc ERPar.R b0 b1 -> - rtc ERPar.R (TBind p a0 b0) (TBind p a1 b1). - Proof. solve_s. Qed. - - Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : - rtc ERPar.R a0 a1 -> - rtc ERPar.R (ren_Tm ξ a0) (ren_Tm ξ a1). + rtc ERPar.R (ren_PTm ξ a0) (ren_PTm ξ a1). Proof. induction 1. - apply rtc_refl. @@ -2080,16 +1921,16 @@ Module ERPars. End ERPars. -Lemma ERPar_Par n (a b : Tm n) : 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 n (a b : Tm n) : 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 : n a b /h. - move => n a0 a1 b0 b1 ha iha hb ihb. - suff ? : rtc ERPar.R (App (Abs a0) b0) (App (Abs a1) b1). + 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. @@ -2116,30 +1957,29 @@ Proof. - sfirstorder use:ERPars.AppCong. - sfirstorder use:ERPars.PairCong. - sfirstorder use:ERPars.ProjCong. - - sfirstorder use:ERPars.BindCong. - sfirstorder. - sfirstorder. - sfirstorder. Qed. -Lemma Pars_ERPar n (a b : Tm n) : 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 n (a b : Tm n) : 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 n (a b : Tm n) : 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 n (a b : Tm n) : 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. @@ -2205,7 +2045,7 @@ Module HindleyRosenFacts (M : HindleyRosen). End HindleyRosenFacts. Module HindleyRosenER <: HindleyRosen. - Definition A := Tm. + Definition A := PTm. Definition R0 n := rtc (@RPar.R n). Definition R1 n := rtc (@EPar.R n). Lemma diamond_R0 : forall n, relations.diamond (R0 n). @@ -2223,7 +2063,7 @@ End HindleyRosenER. Module ERFacts := HindleyRosenFacts HindleyRosenER. -Lemma rtc_union n (a b : Tm n) : +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. @@ -2245,7 +2085,7 @@ Proof. sfirstorder. Qed. -Lemma prov_erpar n (u : Tm n) 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. @@ -2253,7 +2093,7 @@ Proof. sfirstorder use:prov_ereds. Qed. -Lemma prov_pars n (u : Tm n) 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. @@ -2263,15 +2103,15 @@ Proof. - hauto lq:on use:prov_erpar. Qed. -Lemma Par_confluent n (a b c : Tm n) : +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 : n a b c. - suff : forall (n : nat) (a b c : Tm n), + suff : forall (n : nat) (a b c : PTm n), rtc ERPar.R a b -> - rtc ERPar.R a c -> exists d : Tm n, rtc ERPar.R b d /\ rtc ERPar.R c d. + 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]. @@ -2282,32 +2122,32 @@ Proof. specialize h with (n := n). rewrite /HindleyRosenER.A in h. rewrite /ERPar.R. - have eq : (fun a0 b0 : Tm n => 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_univ_inv n i (c : Tm n) : - rtc Par.R (Univ i) c -> - extract c = Univ i. +Lemma pars_univ_inv n i (c : PTm n) : + rtc Par.R (PUniv i) c -> + extract c = PUniv i. Proof. - have : prov (Univ i) (Univ i : Tm n) by sfirstorder. + have : prov (PUniv i) (Univ i : PTm n) by sfirstorder. move : prov_pars. repeat move/[apply]. apply prov_extract. Qed. -Lemma pars_const_inv n i (c : Tm n) : +Lemma pars_const_inv n i (c : PTm n) : rtc Par.R (Const i) c -> extract c = Const i. Proof. - have : prov (Const i) (Const i : Tm n) by sfirstorder. + have : prov (Const i) (Const i : PTm n) by sfirstorder. move : prov_pars. repeat move/[apply]. apply prov_extract. Qed. -Lemma pars_pi_inv n p (A : Tm n) B C : +Lemma pars_pi_inv n p (A : PTm n) B C : rtc Par.R (TBind p A B) C -> exists A0 B0, extract C = TBind p A0 B0 /\ rtc Par.R A A0 /\ rtc Par.R B B0. @@ -2318,15 +2158,15 @@ Proof. Qed. Lemma pars_var_inv n (i : fin n) C : - rtc Par.R (VarTm i) C -> - extract C = VarTm i. + rtc Par.R (VarPTm i) C -> + extract C = VarPTm i. Proof. - have : prov (VarTm i) (VarTm i) by hauto lq:on ctrs:prov, rtc. + have : prov (VarPTm i) (VarPTm i) by hauto lq:on ctrs:prov, rtc. move : prov_pars. repeat move/[apply]. apply prov_extract. Qed. -Lemma pars_univ_inj n i j (C : Tm n) : +Lemma pars_univ_inj n i j (C : PTm n) : rtc Par.R (Univ i) C -> rtc Par.R (Univ j) C -> i = j. @@ -2334,7 +2174,7 @@ Proof. sauto l:on use:pars_univ_inv. Qed. -Lemma pars_const_inj n i j (C : Tm n) : +Lemma pars_const_inj n i j (C : PTm n) : rtc Par.R (Const i) C -> rtc Par.R (Const j) C -> i = j. @@ -2342,7 +2182,7 @@ Proof. sauto l:on use:pars_const_inv. Qed. -Lemma pars_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 C : +Lemma pars_pi_inj n p0 p1 (A0 A1 : PTm n) B0 B1 C : rtc Par.R (TBind p0 A0 B0) C -> rtc Par.R (TBind p1 A1 B1) C -> exists A2 B2, p1 = p0 /\ rtc Par.R A0 A2 /\ rtc Par.R A1 A2 /\ @@ -2353,10 +2193,10 @@ Proof. exists A2, B2. hauto l:on. Qed. -Definition join {n} (a b : Tm n) := +Definition join {n} (a b : PTm n) := exists c, rtc Par.R a c /\ rtc Par.R b c. -Lemma join_transitive n (a b c : Tm n) : +Lemma join_transitive n (a b c : PTm n) : join a b -> join b c -> join a c. Proof. rewrite /join. @@ -2366,26 +2206,26 @@ Proof. eauto using relations.rtc_transitive. Qed. -Lemma join_symmetric n (a b : Tm n) : +Lemma join_symmetric n (a b : PTm n) : join a b -> join b a. Proof. sfirstorder unfold:join. Qed. -Lemma join_refl n (a : Tm n) : join a a. +Lemma join_refl n (a : PTm n) : join a a. Proof. hauto lq:on ctrs:rtc unfold:join. Qed. Lemma join_univ_inj n i j : - join (Univ i : Tm n) (Univ j) -> i = j. + join (Univ i : PTm n) (Univ j) -> i = j. Proof. sfirstorder use:pars_univ_inj. Qed. Lemma join_const_inj n i j : - join (Const i : Tm n) (Const j) -> i = j. + join (Const i : PTm n) (Const j) -> i = j. Proof. sfirstorder use:pars_const_inj. Qed. -Lemma join_pi_inj n p0 p1 (A0 A1 : Tm n) B0 B1 : +Lemma join_pi_inj n p0 p1 (A0 A1 : PTm n) B0 B1 : join (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ join A0 A1 /\ join B0 B1. Proof. @@ -2394,14 +2234,14 @@ Proof. sfirstorder unfold:join. Qed. -Lemma join_substing n m (a b : Tm n) (ρ : fin n -> Tm m) : +Lemma join_substing n m (a b : PTm n) (ρ : fin n -> PTm m) : join a b -> - join (subst_Tm ρ a) (subst_Tm ρ b). + join (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto lq:on unfold:join use:Pars.substing. Qed. -Fixpoint ne {n} (a : Tm n) := +Fixpoint ne {n} (a : PTm n) := match a with - | VarTm i => true + | VarPTm i => true | TBind _ A B => false | App a b => ne a && nf b | Abs a => false @@ -2411,9 +2251,9 @@ Fixpoint ne {n} (a : Tm n) := | Const _ => false | Bot => true end -with nf {n} (a : Tm n) := +with nf {n} (a : PTm n) := match a with - | VarTm i => true + | VarPTm i => true | TBind _ A B => nf A && nf B | App a b => ne a && nf b | Abs a => nf a @@ -2427,8 +2267,8 @@ end. Lemma ne_nf n a : @ne n a -> nf a. Proof. elim : a => //=. Qed. -Definition wn {n} (a : Tm n) := exists b, rtc RPar'.R a b /\ nf b. -Definition wne {n} (a : Tm n) := 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 n a : @wne n a -> wn a. @@ -2438,18 +2278,18 @@ Proof. sfirstorder use:ne_nf. Qed. Lemma nf_wn n v : @nf n v -> wn v. Proof. sfirstorder ctrs:rtc. Qed. -Lemma nf_refl n (a b : Tm n) (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 n m (a : Tm n) (ξ : fin n -> fin m) : - (ne a <-> ne (ren_Tm ξ a)) /\ (nf a <-> nf (ren_Tm ξ a)). +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 : m ξ. elim : n / a => //=; solve [hauto b:on]. Qed. -Lemma wne_app n (a b : Tm n) : +Lemma wne_app n (a b : PTm n) : wne a -> wn b -> wne (App a b). Proof. move => [a0 [? ?]] [b0 [? ?]]. @@ -2470,14 +2310,14 @@ Proof. hauto lqb:on use:RPars'.BindCong. Qed. -Lemma wn_pair n (a b : Tm n) : wn a -> wn b -> wn (Pair a b). +Lemma wn_pair n (a b : PTm n) : wn a -> wn b -> wn (Pair a b). Proof. move => [a0 [? ?]] [b0 [? ?]]. exists (Pair a0 b0). hauto lqb:on use:RPars'.PairCong. Qed. -Lemma wne_proj n p (a : Tm n) : wne a -> wne (Proj p a). +Lemma wne_proj n p (a : PTm n) : wne a -> wne (Proj p a). Proof. move => [a0 [? ?]]. exists (Proj p a0). hauto lqb:on use:RPars'.ProjCong. @@ -2486,17 +2326,17 @@ Qed. Create HintDb nfne. #[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne. -Lemma ne_nf_antiren n m (a : Tm n) (ρ : fin n -> Tm m) : +Lemma ne_nf_antiren n m (a : PTm n) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - (ne (subst_Tm ρ a) -> ne a) /\ (nf (subst_Tm ρ a) -> nf a). + (ne (subst_PTm ρ a) -> ne a) /\ (nf (subst_PTm ρ a) -> nf a). Proof. move : m ρ. elim : n / a => //; hauto b:on drew:off use:RPar.var_or_const_up. Qed. -Lemma wn_antirenaming n m a (ρ : fin n -> Tm m) : +Lemma wn_antirenaming n m a (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> - wn (subst_Tm ρ a) -> wn a. + wn (subst_PTm ρ a) -> wn a. Proof. rewrite /wn => hρ. move => [v [rv nfv]]. @@ -2507,7 +2347,7 @@ Proof. by eapply ne_nf_antiren. Qed. -Lemma ext_wn n (a : Tm n) : +Lemma ext_wn n (a : PTm n) : wn (App a Bot) -> wn a. Proof. @@ -2515,7 +2355,7 @@ Proof. move : a E. move : hv. elim : a0 v / hr. - - hauto q:on inv:Tm ctrs:rtc b:on db: nfne. + - hauto q:on inv:PTm ctrs:rtc b:on db: nfne. - move => a0 a1 a2 hr0 hr1 ih hnfa2. move /(_ hnfa2) in ih. move => a. @@ -2524,7 +2364,7 @@ Proof. + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst. have ? : b3 = (Bot) by hauto lq:on inv:RPar'.R. subst. suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn. - have : wn (subst_Tm (scons (Bot) VarTm) a3) by sfirstorder. + have : wn (subst_PTm (scons (Bot) VarPTm) a3) by sfirstorder. move => h. apply wn_abs. move : h. apply wn_antirenaming. hauto lq:on rew:off inv:option. @@ -2532,41 +2372,41 @@ Proof. Qed. Module Join. - Lemma ProjCong p n (a0 a1 : Tm n) : + Lemma ProjCong p n (a0 a1 : PTm n) : join a0 a1 -> join (Proj p a0) (Proj p a1). Proof. hauto lq:on use:Pars.ProjCong unfold:join. Qed. - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : join a0 a1 -> join b0 b1 -> join (Pair a0 b0) (Pair a1 b1). Proof. hauto lq:on use:Pars.PairCong unfold:join. Qed. - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : join a0 a1 -> join b0 b1 -> join (App a0 b0) (App a1 b1). Proof. hauto lq:on use:Pars.AppCong. Qed. - Lemma AbsCong n (a b : Tm (S n)) : + Lemma AbsCong n (a b : PTm (S n)) : join a b -> join (Abs a) (Abs b). Proof. hauto lq:on use:Pars.AbsCong. Qed. - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - join a b -> join (ren_Tm ξ a) (ren_Tm ξ b). + 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 n (a b : Tm n) : - join a b -> join (ren_Tm shift a) (ren_Tm shift b). + 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 n (a b : Tm n) : + Lemma FromPar n (a b : PTm n) : Par.R a b -> join a b. Proof. @@ -2574,12 +2414,12 @@ Module Join. Qed. End Join. -Lemma abs_eq n a (b : Tm n) : - join (Abs a) b <-> join a (App (ren_Tm shift b) (VarTm var_zero)). +Lemma abs_eq n a (b : PTm n) : + join (Abs a) b <-> join a (App (ren_PTm shift b) (VarPTm var_zero)). Proof. split. - move => /Join.weakening h. - have {h} : join (App (ren_Tm shift (Abs a)) (VarTm var_zero)) (App (ren_Tm shift b) (VarTm var_zero)) + have {h} : join (App (ren_PTm shift (Abs a)) (VarPTm var_zero)) (App (ren_PTm shift b) (VarPTm var_zero)) by hauto l:on use:Join.AppCong, join_refl. simpl. move => ?. apply : join_transitive; eauto. @@ -2590,7 +2430,7 @@ Proof. apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl. Qed. -Lemma pair_eq n (a0 a1 b : Tm n) : +Lemma pair_eq n (a0 a1 b : PTm n) : join (Pair a0 a1) b <-> join a0 (Proj PL b) /\ join a1 (Proj PR b). Proof. split. @@ -2606,7 +2446,7 @@ Proof. apply Join.FromPar. hauto lq:on ctrs:Par.R use:Par.refl. Qed. -Lemma join_pair_inj n (a0 a1 b0 b1 : Tm n) : +Lemma join_pair_inj n (a0 a1 b0 b1 : PTm n) : join (Pair a0 a1) (Pair b0 b1) <-> join a0 b0 /\ join a1 b1. Proof. split; last by hauto lq:on use:Join.PairCong.