From 657c1325c99aa5891ba440af7ede8e3f656068c6 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 2 Mar 2025 16:40:39 -0500 Subject: [PATCH] Add unscoped syntax --- Makefile | 4 +- syntax.sig | 1 - theories/Autosubst2/syntax.v | 785 ++++++++++++--------------------- theories/Autosubst2/unscoped.v | 213 +++++++++ theories/common.v | 70 +-- 5 files changed, 532 insertions(+), 541 deletions(-) create mode 100644 theories/Autosubst2/unscoped.v diff --git a/Makefile b/Makefile index ef5b76f..79b3720 100644 --- a/Makefile +++ b/Makefile @@ -16,12 +16,12 @@ uninstall: $(COQMAKEFILE) $(MAKE) -f $(COQMAKEFILE) uninstall theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig - autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig + autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig .PHONY: clean FORCE clean: test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) ) - rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v FORCE: diff --git a/syntax.sig b/syntax.sig index a50911e..24931eb 100644 --- a/syntax.sig +++ b/syntax.sig @@ -16,7 +16,6 @@ PPair : PTm -> PTm -> PTm PProj : PTag -> PTm -> PTm PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm PUniv : nat -> PTm -PBot : PTm PNat : PTm PZero : PTm PSuc : PTm -> PTm diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 5d04c05..ee8b076 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -1,4 +1,4 @@ -Require Import core fintype. +Require Import core unscoped. Require Import Setoid Morphisms Relation_Definitions. @@ -33,221 +33,168 @@ 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 - | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm - | PUniv : nat -> PTm n_PTm - | PBot : PTm n_PTm - | PNat : PTm n_PTm - | PZero : PTm n_PTm - | PSuc : PTm n_PTm -> PTm n_PTm - | PInd : - PTm (S n_PTm) -> - PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm. +Inductive PTm : Type := + | VarPTm : nat -> PTm + | PAbs : PTm -> PTm + | PApp : PTm -> PTm -> PTm + | PPair : PTm -> PTm -> PTm + | PProj : PTag -> PTm -> PTm + | PBind : BTag -> PTm -> PTm -> PTm + | PUniv : nat -> PTm + | PNat : PTm + | PZero : PTm + | PSuc : PTm -> PTm + | PInd : PTm -> PTm -> PTm -> PTm -> 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. +Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PAbs 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. +Lemma congr_PApp {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PApp s0 s1 = PApp 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)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp x s1) H0)) + (ap (fun x => PApp 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. +Lemma congr_PPair {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PPair s0 s1 = PPair 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)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair x s1) H0)) + (ap (fun x => PPair 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. +Lemma congr_PProj {s0 : PTag} {s1 : PTm} {t0 : PTag} {t1 : PTm} + (H0 : s0 = t0) (H1 : s1 = t1) : PProj s0 s1 = PProj 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)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0)) + (ap (fun x => PProj t0 x) H1)). Qed. -Lemma congr_PBind {m_PTm : nat} {s0 : BTag} {s1 : PTm m_PTm} - {s2 : PTm (S m_PTm)} {t0 : BTag} {t1 : PTm m_PTm} {t2 : PTm (S m_PTm)} - (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : - PBind m_PTm s0 s1 s2 = PBind m_PTm t0 t1 t2. +Lemma congr_PBind {s0 : BTag} {s1 : PTm} {s2 : PTm} {t0 : BTag} {t1 : PTm} + {t2 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : + PBind s0 s1 s2 = PBind t0 t1 t2. Proof. exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => PBind m_PTm x s1 s2) H0)) - (ap (fun x => PBind m_PTm t0 x s2) H1)) - (ap (fun x => PBind m_PTm t0 t1 x) H2)). + (eq_trans (eq_trans eq_refl (ap (fun x => PBind x s1 s2) H0)) + (ap (fun x => PBind t0 x s2) H1)) + (ap (fun x => PBind t0 t1 x) H2)). Qed. -Lemma congr_PUniv {m_PTm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : - PUniv m_PTm s0 = PUniv m_PTm t0. +Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)). Qed. -Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm. +Lemma congr_PNat : PNat = PNat. Proof. exact (eq_refl). Qed. -Lemma congr_PNat {m_PTm : nat} : PNat m_PTm = PNat m_PTm. +Lemma congr_PZero : PZero = PZero. Proof. exact (eq_refl). Qed. -Lemma congr_PZero {m_PTm : nat} : PZero m_PTm = PZero m_PTm. +Lemma congr_PSuc {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PSuc s0 = PSuc t0. Proof. -exact (eq_refl). +exact (eq_trans eq_refl (ap (fun x => PSuc x) H0)). Qed. -Lemma congr_PSuc {m_PTm : nat} {s0 : PTm m_PTm} {t0 : PTm m_PTm} - (H0 : s0 = t0) : PSuc m_PTm s0 = PSuc m_PTm t0. -Proof. -exact (eq_trans eq_refl (ap (fun x => PSuc m_PTm x) H0)). -Qed. - -Lemma congr_PInd {m_PTm : nat} {s0 : PTm (S m_PTm)} {s1 : PTm m_PTm} - {s2 : PTm m_PTm} {s3 : PTm (S (S m_PTm))} {t0 : PTm (S m_PTm)} - {t1 : PTm m_PTm} {t2 : PTm m_PTm} {t3 : PTm (S (S m_PTm))} (H0 : s0 = t0) - (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) : - PInd m_PTm s0 s1 s2 s3 = PInd m_PTm t0 t1 t2 t3. +Lemma congr_PInd {s0 : PTm} {s1 : PTm} {s2 : PTm} {s3 : PTm} {t0 : PTm} + {t1 : PTm} {t2 : PTm} {t3 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) + (H2 : s2 = t2) (H3 : s3 = t3) : PInd s0 s1 s2 s3 = PInd t0 t1 t2 t3. Proof. exact (eq_trans (eq_trans - (eq_trans - (eq_trans eq_refl (ap (fun x => PInd m_PTm x s1 s2 s3) H0)) - (ap (fun x => PInd m_PTm t0 x s2 s3) H1)) - (ap (fun x => PInd m_PTm t0 t1 x s3) H2)) - (ap (fun x => PInd m_PTm t0 t1 t2 x) H3)). + (eq_trans (eq_trans eq_refl (ap (fun x => PInd x s1 s2 s3) H0)) + (ap (fun x => PInd t0 x s2 s3) H1)) + (ap (fun x => PInd t0 t1 x s3) H2)) + (ap (fun x => PInd t0 t1 t2 x) H3)). Qed. -Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) : - fin (S m) -> fin (S n). +Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat. 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 := +Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : 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) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (ren_PTm xi_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) + | VarPTm s0 => VarPTm (xi_PTm s0) + | PAbs s0 => PAbs (ren_PTm (upRen_PTm_PTm xi_PTm) s0) + | PApp s0 s1 => PApp (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1) + | PBind s0 s1 s2 => + PBind s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) + | PUniv s0 => PUniv s0 + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (ren_PTm xi_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) (ren_PTm xi_PTm s2) (ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm)) s3) end. -Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : - fin (S m) -> PTm (S n_PTm). +Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm. Proof. -exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)). +exact (scons (VarPTm 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 -:= +Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : 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) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (subst_PTm sigma_PTm s1) - (subst_PTm (up_PTm_PTm sigma_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (subst_PTm sigma_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) - (subst_PTm sigma_PTm s1) (subst_PTm sigma_PTm s2) + | VarPTm s0 => sigma_PTm s0 + | PAbs s0 => PAbs (subst_PTm (up_PTm_PTm sigma_PTm) s0) + | PApp s0 s1 => PApp (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1) + | PBind s0 s1 s2 => + PBind s0 (subst_PTm sigma_PTm s1) (subst_PTm (up_PTm_PTm sigma_PTm) s2) + | PUniv s0 => PUniv s0 + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (subst_PTm sigma_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (subst_PTm (up_PTm_PTm sigma_PTm) s0) (subst_PTm sigma_PTm s1) + (subst_PTm sigma_PTm s2) (subst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm)) s3) 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. +Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) : + forall x, up_PTm_PTm sigma x = VarPTm x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => 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 := +Fixpoint idSubst_PTm (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = VarPTm x) (s : PTm) {struct s} : +subst_PTm sigma_PTm s = s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | 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 => + | PApp s0 s1 => congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PPair _ s0 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) - | PBind _ s0 s1 s2 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s2) @@ -255,54 +202,42 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) (upId_PTm_PTm _ (upId_PTm_PTm _ Eq_PTm)) s3) 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) : +Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (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). +exact (fun n => match n with + | S n' => ap shift (Eq n') + | O => 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} : +Fixpoint extRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : 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 => + | VarPTm s0 => ap (VarPTm) (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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s0) @@ -313,55 +248,43 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s := (upExtRen_PTm_PTm _ _ (upExtRen_PTm_PTm _ _ Eq_PTm)) s3) 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) : +Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> 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 + | S n' => ap (ren_PTm shift) (Eq n') + | O => 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} : +Fixpoint ext_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm) {struct s} : subst_PTm sigma_PTm s = subst_PTm tau_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | 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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s0) @@ -372,57 +295,43 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s := (upExt_PTm_PTm _ _ (upExt_PTm_PTm _ _ Eq_PTm)) s3) 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) : +Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (rho : nat -> nat) (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 := +Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(rho_PTm : nat -> nat) +(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : 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 => + | VarPTm s0 => ap (VarPTm) (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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => - congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) @@ -434,66 +343,48 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_PTm)) s3) 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) : +Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm) + (theta : nat -> 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 + | S n' => ap (ren_PTm shift) (Eq n') + | O => 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 := +Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : 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 => + | 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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -506,9 +397,8 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} s3) 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) +Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat) + (theta : nat -> 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 = @@ -516,76 +406,50 @@ Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm) - (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n)) + (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma 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 + (fun x => eq_refl) (sigma n'))) + (ap (ren_PTm shift) (Eq n'))) + | O => 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) +Fixpoint compSubstRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : 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 => + | 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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -598,9 +462,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := s3) 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) +Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm) + (theta : nat -> 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 = @@ -608,78 +471,51 @@ Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S 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)) + (sigma 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 + (sigma n'))) (ap (ren_PTm shift) (Eq n'))) + | O => 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) +Fixpoint compSubstSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : 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 => + | 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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -692,126 +528,101 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := (up_subst_subst_PTm_PTm _ _ _ Eq_PTm)) s3) 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) : +Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : 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) : +Lemma renRen'_PTm_pointwise (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) : 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) : +Lemma renSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) (s : 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) : +Lemma renSubst_PTm_pointwise (xi_PTm : nat -> nat) (tau_PTm : nat -> 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) : +Lemma substRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) (s : 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) : +Lemma substRen_PTm_pointwise (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) + : 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) : +Lemma substSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) + (s : 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) : +Lemma substSubst_PTm_pointwise (sigma_PTm : nat -> PTm) + (tau_PTm : nat -> 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. +Lemma rinstInst_up_PTm_PTm (xi : nat -> nat) (sigma : nat -> PTm) + (Eq : forall x, funcomp (VarPTm) xi x = sigma x) : + forall x, funcomp (VarPTm) (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 + | S n' => ap (ren_PTm shift) (Eq n') + | O => 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 := +Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp (VarPTm) xi_PTm x = sigma_PTm x) (s : PTm) +{struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | 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 => + | 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 => + | 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 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) @@ -822,71 +633,61 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} (rinstInst_up_PTm_PTm _ _ (rinstInst_up_PTm_PTm _ _ Eq_PTm)) s3) 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. +Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) : + ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm) 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) : +Lemma rinstInst'_PTm_pointwise (xi_PTm : nat -> nat) : pointwise_relation _ eq (ren_PTm xi_PTm) - (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)). + (subst_PTm (funcomp (VarPTm) 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. +Lemma instId'_PTm (s : PTm) : subst_PTm (VarPTm) s = s. Proof. -exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma instId'_PTm_pointwise {m_PTm : nat} : - pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id. +Lemma instId'_PTm_pointwise : pointwise_relation _ eq (subst_PTm (VarPTm)) id. Proof. -exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (fun s => idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s. +Lemma rinstId'_PTm (s : 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. +Lemma rinstId'_PTm_pointwise : pointwise_relation _ eq (@ren_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. +Lemma varL'_PTm (sigma_PTm : nat -> PTm) (x : nat) : + subst_PTm sigma_PTm (VarPTm 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. +Lemma varL'_PTm_pointwise (sigma_PTm : nat -> PTm) : + pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm)) 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). +Lemma varLRen'_PTm (xi_PTm : nat -> nat) (x : nat) : + ren_PTm xi_PTm (VarPTm x) = VarPTm (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). +Lemma varLRen'_PTm_pointwise (xi_PTm : nat -> nat) : + pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm)) + (funcomp (VarPTm) xi_PTm). Proof. exact (fun x => eq_refl). Qed. @@ -894,18 +695,14 @@ Qed. Class Up_PTm X Y := up_PTm : X -> Y. -#[global] -Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := - (@subst_PTm m_PTm n_PTm). +#[global] Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. + +#[global] Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. + +#[global] Instance Ren_PTm : (Ren1 _ _ _) := @ren_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). +Instance VarInstance_PTm : (Var _ _) := @VarPTm. Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm) ( at level 1, left associativity, only printing) : fscope. @@ -932,9 +729,9 @@ Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : subst_scope. #[global] -Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_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') @@ -942,17 +739,16 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_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)). +Instance ren_PTm_morphism : + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_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') @@ -960,9 +756,9 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance ren_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@ren_PTm m_PTm n_PTm)). + (@ren_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s). Qed. @@ -994,9 +790,7 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite rinstId'_PTm | progress setoid_rewrite instId'_PTm_pointwise | progress setoid_rewrite instId'_PTm - | progress - unfold up_list_PTm_PTm, up_PTm_PTm, upRen_list_PTm_PTm, - upRen_PTm_PTm, up_ren + | progress unfold up_PTm_PTm, upRen_PTm_PTm, up_ren | progress cbn[subst_PTm ren_PTm] | progress fsimpl ]). @@ -1021,36 +815,11 @@ End Core. Module Extra. -Import -Core. +Import Core. -Arguments VarPTm {n_PTm}. +#[global] Hint Opaque subst_PTm: rewrite. -Arguments PInd {n_PTm}. - -Arguments PSuc {n_PTm}. - -Arguments PZero {n_PTm}. - -Arguments PNat {n_PTm}. - -Arguments PBot {n_PTm}. - -Arguments PUniv {n_PTm}. - -Arguments PBind {n_PTm}. - -Arguments PProj {n_PTm}. - -Arguments PPair {n_PTm}. - -Arguments PApp {n_PTm}. - -Arguments PAbs {n_PTm}. - -#[global]Hint Opaque subst_PTm: rewrite. - -#[global]Hint Opaque ren_PTm: rewrite. +#[global] Hint Opaque ren_PTm: rewrite. End Extra. diff --git a/theories/Autosubst2/unscoped.v b/theories/Autosubst2/unscoped.v new file mode 100644 index 0000000..55f8172 --- /dev/null +++ b/theories/Autosubst2/unscoped.v @@ -0,0 +1,213 @@ +(** * Autosubst Header for Unnamed Syntax + +Version: December 11, 2019. + *) + +(* Adrian: + I changed this library a bit to work better with my generated code. + 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O + 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*) +Require Import core. +Require Import Setoid Morphisms Relation_Definitions. + +Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := + match p with eq_refl => eq_refl end. + +Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := + match q with eq_refl => match p with eq_refl => eq_refl end end. + +(** ** Primitives of the Sigma Calculus. *) + +Definition shift := S. + +Definition var_zero := 0. + +Definition id {X} := @Datatypes.id X. + +Definition scons {X: Type} (x : X) (xi : nat -> X) := + fun n => match n with + | 0 => x + | S n => xi n + end. + +#[ export ] +Hint Opaque scons : rewrite. + +(** ** Type Class Instances for Notation +Required to make notation work. *) + +(** *** Type classes for renamings. *) + +Class Ren1 (X1 : Type) (Y Z : Type) := + ren1 : X1 -> Y -> Z. + +Class Ren2 (X1 X2 : Type) (Y Z : Type) := + ren2 : X1 -> X2 -> Y -> Z. + +Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := + ren3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := + ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := + ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module RenNotations. + Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. + + Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. + + Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. +End RenNotations. + +(** *** Type Classes for Substiution *) + +Class Subst1 (X1 : Type) (Y Z: Type) := + subst1 : X1 -> Y -> Z. + +Class Subst2 (X1 X2 : Type) (Y Z: Type) := + subst2 : X1 -> X2 -> Y -> Z. + +Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := + subst3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := + subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := + subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module SubstNotations. + Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. + + Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. +End SubstNotations. + +(** *** Type Class for Variables *) + +Class Var X Y := + ids : X -> Y. + +#[export] Instance idsRen : Var nat nat := id. + +(** ** Proofs for the substitution primitives. *) + +Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. + +Module CombineNotations. + Notation "f >> g" := (funcomp g f) (at level 50) : fscope. + + Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. + + #[ global ] + Open Scope fscope. + #[ global ] + Open Scope subst_scope. +End CombineNotations. + +Import CombineNotations. + + +(** A generic lifting of a renaming. *) +Definition up_ren (xi : nat -> nat) := + 0 .: (xi >> S). + +(** A generic proof that lifting of renamings composes. *) +Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) : + forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. +Proof. + intros [|x]. + - reflexivity. + - unfold up_ren. cbn. unfold funcomp. f_equal. apply E. +Qed. + +(** Eta laws. *) +Lemma scons_eta' {T} (f : nat -> T) : + pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_eta_id' : + pointwise_relation _ eq (var_zero .: shift) id. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) : + pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). +Proof. intros x. destruct x; reflexivity. Qed. + +(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) +#[export] Instance scons_morphism {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X). +Proof. + intros ? t -> sigma tau H. + intros [|x]. + cbn. reflexivity. + apply H. +Qed. + +#[export] Instance scons_morphism2 {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X). +Proof. + intros ? t -> sigma tau H ? x ->. + destruct x as [|x]. + cbn. reflexivity. + apply H. +Qed. + +(** ** Generic lifting of an allfv predicate *) +Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p. + +(** ** Notations for unscoped syntax *) +Module UnscopedNotations. + Include RenNotations. + Include SubstNotations. + Include CombineNotations. + + (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) + + Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. + + Notation "↑" := (shift) : subst_scope. + + #[global] + Open Scope fscope. + #[global] + Open Scope subst_scope. +End UnscopedNotations. + +(** ** Tactics for unscoped syntax *) + +(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *) +Tactic Notation "auto_case" tactic(t) := (match goal with + | [|- forall (i : nat), _] => intros []; t + end). + + +(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) +Ltac fsimpl := + repeat match goal with + | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) + | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) + | [|- context [id ?s]] => change (id s) with s + | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) + | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v + | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v + | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n) + | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) + | [|- context[var_zero]] => change var_zero with 0 + | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f) + | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta' + | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) + | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) + (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *) + | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce + | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce + end. \ No newline at end of file diff --git a/theories/common.v b/theories/common.v index 282038d..79b0b19 100644 --- a/theories/common.v +++ b/theories/common.v @@ -1,41 +1,52 @@ -Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect. +Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect. From Ltac2 Require Ltac2. Import Ltac2.Notations. Import Ltac2.Control. From Hammer Require Import Tactics. -Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) := - forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i). +Inductive lookup : nat -> list PTm -> PTm -> Prop := +| here A Γ : lookup 0 (cons A Γ) (ren_PTm shift A) +| there i Γ A B : + lookup i Γ A -> + lookup (S i) (cons B Γ) (ren_PTm shift A). -Lemma up_injective n m (ξ : fin n -> fin m) : - (forall i j, ξ i = ξ j -> i = j) -> - forall i j, (upRen_PTm_PTm ξ) i = (upRen_PTm_PTm ξ) j -> i = j. +Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) := + forall i A, lookup i Δ A -> lookup (ξ i) Γ (ren_PTm ξ A). + +Definition ren_inj (ξ : nat -> nat) := forall i j, ξ i = ξ j -> i = j. + +Lemma up_injective (ξ : nat -> nat) : + ren_inj ξ -> + ren_inj (upRen_PTm_PTm ξ). Proof. - sblast inv:option. + move => h i j. + case : i => //=; case : j => //=. + move => i j. rewrite /funcomp. hauto lq:on rew:off unfold:ren_inj. Qed. Local Ltac2 rec solve_anti_ren () := let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in intro $x; lazy_match! Constr.type (Control.hyp x) with - | fin _ -> _ _ => (ltac1:(case;hauto lq:on rew:off use:up_injective)) + | nat -> nat => (ltac1:(case => *//=; qauto l:on use:up_injective unfold:ren_inj)) | _ => solve_anti_ren () end. Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). -Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) : - (forall i j, ξ i = ξ j -> i = j) -> +Lemma ren_injective (a b : PTm) (ξ : nat -> nat) : + ren_inj ξ -> ren_PTm ξ a = ren_PTm ξ b -> a = b. Proof. - move : m ξ b. elim : n / a => //; try solve_anti_ren. + move : ξ b. elim : a => //; try solve_anti_ren. + move => p ihp ξ []//=. hauto lq:on inv:PTm, nat ctrs:- use:up_injective. Qed. Inductive HF : Set := | H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot. -Definition ishf {n} (a : PTm n) := +Definition ishf (a : PTm) := match a with | PPair _ _ => true | PAbs _ => true @@ -47,7 +58,7 @@ Definition ishf {n} (a : PTm n) := | _ => false end. -Definition toHF {n} (a : PTm n) := +Definition toHF (a : PTm) := match a with | PPair _ _ => H_Pair | PAbs _ => H_Abs @@ -59,54 +70,53 @@ Definition toHF {n} (a : PTm n) := | _ => H_Bot end. -Fixpoint ishne {n} (a : PTm n) := +Fixpoint ishne (a : PTm) := match a with | VarPTm _ => true | PApp a _ => ishne a | PProj _ a => ishne a - | PBot => true | PInd _ n _ _ => ishne n | _ => false end. -Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false. +Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false. -Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false. +Definition isuniv (a : PTm) := if a is PUniv _ then true else false. -Definition ispair {n} (a : PTm n) := +Definition ispair (a : PTm) := match a with | PPair _ _ => true | _ => false end. -Definition isnat {n} (a : PTm n) := if a is PNat then true else false. +Definition isnat (a : PTm) := if a is PNat then true else false. -Definition iszero {n} (a : PTm n) := if a is PZero then true else false. +Definition iszero (a : PTm) := if a is PZero then true else false. -Definition issuc {n} (a : PTm n) := if a is PSuc _ then true else false. +Definition issuc (a : PTm) := if a is PSuc _ then true else false. -Definition isabs {n} (a : PTm n) := +Definition isabs (a : PTm) := match a with | PAbs _ => true | _ => false end. -Definition ishf_ren n m (a : PTm n) (ξ : fin n -> fin m) : +Definition ishf_ren (a : PTm) (ξ : nat -> nat) : ishf (ren_PTm ξ a) = ishf a. Proof. case : a => //=. Qed. -Definition isabs_ren n m (a : PTm n) (ξ : fin n -> fin m) : +Definition isabs_ren (a : PTm) (ξ : nat -> nat) : isabs (ren_PTm ξ a) = isabs a. Proof. case : a => //=. Qed. -Definition ispair_ren n m (a : PTm n) (ξ : fin n -> fin m) : +Definition ispair_ren (a : PTm) (ξ : nat -> nat) : ispair (ren_PTm ξ a) = ispair a. Proof. case : a => //=. Qed. -Definition ishne_ren n m (a : PTm n) (ξ : fin n -> fin m) : +Definition ishne_ren (a : PTm) (ξ : nat -> nat) : ishne (ren_PTm ξ a) = ishne a. -Proof. move : m ξ. elim : n / a => //=. Qed. +Proof. move : ξ. elim : a => //=. Qed. -Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A : - renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift. -Proof. sfirstorder. Qed. +Lemma renaming_shift Γ (ρ : nat -> PTm) A : + renaming_ok (cons A Γ) Γ shift. +Proof. rewrite /renaming_ok. hauto lq:on ctrs:lookup. Qed.