yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: yiyunliu:fc666956e220a851d339be29319b8187daa91f5f
Branches Tags
yiyunliu:master
yiyunliu:ext-rep
yiyunliu:cleanup
yiyunliu:unscoped
yiyunliu:bove-capretta
yiyunliu:nat
yiyunliu:subtyping
yiyunliu:logrelnew
yiyunliu:logrel
yiyunliu:antirenaming
yiyunliu:nonessential
yiyunliu:tstar
..
compare: yiyunliu:11d23afa45c544bed48aa848b2b58d8af7ca8ca2
Branches Tags
yiyunliu:ext-rep
yiyunliu:master
yiyunliu:cleanup
yiyunliu:unscoped
yiyunliu:bove-capretta
yiyunliu:nat
yiyunliu:subtyping
yiyunliu:logrelnew
yiyunliu:logrel
yiyunliu:antirenaming
yiyunliu:nonessential
yiyunliu:tstar

No commits in common. "fc666956e220a851d339be29319b8187daa91f5f" and "11d23afa45c544bed48aa848b2b58d8af7ca8ca2" have entirely different histories.
fc666956e2 ... 11d23afa45

3 changed files with 88 additions and 941 deletions
Download patch file Download diff file Expand all files Collapse all files

2
syntax.sig
View file

@ -9,7 +9,7 @@ Void : Ty
PL : PTag
PR : PTag
PAbs : (bind PTm in PTm) -> PTm
PAbs : Ty -> (bind PTm in PTm) -> PTm
PApp : PTm -> PTm -> PTm
PPair : PTm -> PTm -> PTm
PProj : PTag -> PTm -> PTm

110
theories/Autosubst2/syntax.v
View file

@ -19,17 +19,43 @@ Proof.
exact (eq_refl).
Qed.
Inductive Ty : Type :=
| Fun : Ty -> Ty -> Ty
| Prod : Ty -> Ty -> Ty
| Void : Ty.
Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
(ap (fun x => Fun t0 x) H1)).
Qed.
Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
(ap (fun x => Prod t0 x) H1)).
Qed.
Lemma congr_Void : Void = Void.
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
| PAbs : Ty -> 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.
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 {m_PTm : nat} {s0 : Ty} {s1 : PTm (S m_PTm)} {t0 : Ty}
{t1 : PTm (S m_PTm)} (H0 : s0 = t0) (H1 : s1 = t1) :
PAbs m_PTm s0 s1 = PAbs m_PTm t0 t1.
Proof.
exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)).
exact (eq_trans (eq_trans eq_refl (ap (fun x => PAbs m_PTm x s1) H0))
(ap (fun x => PAbs m_PTm t0 x) H1)).
Qed.
Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm}
@ -72,7 +98,7 @@ 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)
| PAbs _ s0 s1 => PAbs n_PTm s0 (ren_PTm (upRen_PTm_PTm xi_PTm) s1)
| 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)
@ -96,7 +122,7 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
:=
match s with
| VarPTm _ s0 => sigma_PTm s0
| PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0)
| PAbs _ s0 s1 => PAbs n_PTm s0 (subst_PTm (up_PTm_PTm sigma_PTm) s1)
| PApp _ s0 s1 =>
PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
| PPair _ s0 s1 =>
@ -129,9 +155,9 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
: 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)
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s1)
| PApp _ s0 s1 =>
congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0)
(idSubst_PTm sigma_PTm Eq_PTm s1)
@ -168,10 +194,10 @@ Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat}
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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upExtRen_PTm_PTm _ _ Eq_PTm) s0)
(upExtRen_PTm_PTm _ _ Eq_PTm) s1)
| PApp _ s0 s1 =>
congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
(extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
@ -209,10 +235,10 @@ Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat}
subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 =>
congr_PAbs
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
(upExt_PTm_PTm _ _ Eq_PTm) s0)
(upExt_PTm_PTm _ _ Eq_PTm) s1)
| PApp _ s0 s1 =>
congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
(ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
@ -249,10 +275,10 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
{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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
(upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) 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)
@ -299,10 +325,10 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
{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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(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)
(up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) 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)
@ -369,10 +395,10 @@ Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(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)
(up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) 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)
@ -441,10 +467,10 @@ Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(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)
(up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) 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)
@ -554,10 +580,10 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
(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
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
(rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
(rinstInst_up_PTm_PTm _ _ Eq_PTm) 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)
@ -637,30 +663,6 @@ Proof.
exact (fun x => eq_refl).
Qed.
Inductive Ty : Type :=
| Fun : Ty -> Ty -> Ty
| Prod : Ty -> Ty -> Ty
| Void : Ty.
Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
(ap (fun x => Fun t0 x) H1)).
Qed.
Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
(ap (fun x => Prod t0 x) H1)).
Qed.
Lemma congr_Void : Void = Void.
Proof.
exact (eq_refl).
Qed.
Class Up_PTm X Y :=
up_PTm : X -> Y.

917
theories/fp_red.v
View file

File diff suppressed because it is too large Load diff