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

Compare commits

base: yiyunliu:main
Branches Tags
yiyunliu:main
yiyunliu:cred
yiyunliu:commute-rules
yiyunliu:boolean-nojunk
yiyunliu:boolean
yiyunliu:norm
yiyunliu:norm-take3
yiyunliu:erase
yiyunliu:normalization-2
yiyunliu:norm-take2
yiyunliu:normalization
yiyunliu:sigma-type
yiyunliu:master
..
compare: yiyunliu:master
Branches Tags
yiyunliu:cred
yiyunliu:commute-rules
yiyunliu:boolean-nojunk
yiyunliu:boolean
yiyunliu:main
yiyunliu:norm
yiyunliu:norm-take3
yiyunliu:erase
yiyunliu:normalization-2
yiyunliu:norm-take2
yiyunliu:normalization
yiyunliu:sigma-type
yiyunliu:master

1 commit
main ... master

Author SHA1 Message Date
Yiyun Liu
a9de3013c9 Revise the par reduction relation 2024-12-20 16:26:32 -05:00
6 changed files with 235 additions and 3596 deletions
Show stats Expand all files Collapse all files

1
README.md
View file

@ -1 +0,0 @@
This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.

14
syntax.sig
View file

@ -1,16 +1,8 @@
nat : Type
Tm(VarTm) : Type
PTag : Type
TTag : Type
-- nat : Type
TPi : TTag
TSig : TTag
PL : PTag
PR : PTag
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
Bot : Tm
Univ : nat -> Tm
Proj1 : Tm -> Tm
Proj2 : Tm -> Tm

174
theories/Autosubst2/syntax.v
View file

@ -5,43 +5,13 @@ Require Import Setoid Morphisms Relation_Definitions.
Module Core.
Inductive PTag : Type :=
| PL : PTag
| PR : PTag.
Lemma congr_PL : PL = PL.
Proof.
exact (eq_refl).
Qed.
Lemma congr_PR : PR = PR.
Proof.
exact (eq_refl).
Qed.
Inductive TTag : Type :=
| TPi : TTag
| TSig : TTag.
Lemma congr_TPi : TPi = TPi.
Proof.
exact (eq_refl).
Qed.
Lemma congr_TSig : TSig = TSig.
Proof.
exact (eq_refl).
Qed.
Inductive Tm (n_Tm : nat) : Type :=
| VarTm : fin n_Tm -> Tm n_Tm
| Abs : Tm (S n_Tm) -> Tm n_Tm
| App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
| 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
| Bot : Tm n_Tm
| Univ : nat -> Tm n_Tm.
| Proj1 : Tm n_Tm -> Tm n_Tm
| Proj2 : Tm n_Tm -> Tm n_Tm.
Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
(H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0.
@ -65,33 +35,16 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair m_Tm x s1) H0))
(ap (fun x => Pair m_Tm t0 x) H1)).
Qed.
Lemma congr_Proj {m_Tm : nat} {s0 : PTag} {s1 : Tm m_Tm} {t0 : PTag}
{t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) :
Proj m_Tm s0 s1 = Proj m_Tm t0 t1.
Lemma congr_Proj1 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
Proj1 m_Tm s0 = Proj1 m_Tm t0.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj m_Tm x s1) H0))
(ap (fun x => Proj m_Tm t0 x) H1)).
exact (eq_trans eq_refl (ap (fun x => Proj1 m_Tm x) H0)).
Qed.
Lemma congr_TBind {m_Tm : nat} {s0 : TTag} {s1 : Tm m_Tm} {s2 : Tm (S m_Tm)}
{t0 : TTag} {t1 : Tm m_Tm} {t2 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1)
(H2 : s2 = t2) : TBind m_Tm s0 s1 s2 = TBind m_Tm t0 t1 t2.
Lemma congr_Proj2 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
Proj2 m_Tm s0 = Proj2 m_Tm t0.
Proof.
exact (eq_trans
(eq_trans (eq_trans eq_refl (ap (fun x => TBind m_Tm x s1 s2) H0))
(ap (fun x => TBind m_Tm t0 x s2) H1))
(ap (fun x => TBind m_Tm t0 t1 x) H2)).
Qed.
Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm.
Proof.
exact (eq_refl).
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)).
exact (eq_trans eq_refl (ap (fun x => Proj2 m_Tm x) H0)).
Qed.
Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
@ -113,11 +66,8 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
| Abs _ s0 => Abs n_Tm (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
| App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
| Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
| 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)
| Bot _ => Bot n_Tm
| Univ _ s0 => Univ n_Tm s0
| Proj1 _ s0 => Proj1 n_Tm (ren_Tm xi_Tm s0)
| Proj2 _ s0 => Proj2 n_Tm (ren_Tm xi_Tm s0)
end.
Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@ -140,11 +90,8 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
| Abs _ s0 => Abs n_Tm (subst_Tm (up_Tm_Tm sigma_Tm) s0)
| App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
| Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
| 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)
| Bot _ => Bot n_Tm
| Univ _ s0 => Univ n_Tm s0
| Proj1 _ s0 => Proj1 n_Tm (subst_Tm sigma_Tm s0)
| Proj2 _ s0 => Proj2 n_Tm (subst_Tm sigma_Tm s0)
end.
Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@ -179,12 +126,8 @@ subst_Tm sigma_Tm s = s :=
| Pair _ s0 s1 =>
congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
(idSubst_Tm sigma_Tm Eq_Tm s1)
| Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
| 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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 => congr_Proj1 (idSubst_Tm sigma_Tm Eq_Tm s0)
| Proj2 _ s0 => congr_Proj2 (idSubst_Tm sigma_Tm Eq_Tm s0)
end.
Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@ -221,14 +164,8 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
| Pair _ s0 s1 =>
congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
(extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 => congr_Proj1 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
| Proj2 _ s0 => congr_Proj2 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
end.
Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@ -267,13 +204,8 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
| Pair _ s0 s1 =>
congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
(ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
| Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 => congr_Proj1 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
| Proj2 _ s0 => congr_Proj2 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
end.
Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@ -311,14 +243,8 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
| Pair _ s0 s1 =>
congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
(compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 => congr_Proj1 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
| Proj2 _ s0 => congr_Proj2 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
end.
Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@ -365,16 +291,10 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
| Pair _ s0 s1 =>
congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
(compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0)
(compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
congr_TBind (eq_refl s0)
(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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 =>
congr_Proj1 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
| Proj2 _ s0 =>
congr_Proj2 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
end.
Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@ -442,16 +362,10 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
| Pair _ s0 s1 =>
congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
(compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0)
(compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
congr_TBind (eq_refl s0)
(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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 =>
congr_Proj1 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
| Proj2 _ s0 =>
congr_Proj2 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
end.
Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@ -520,16 +434,10 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
| Pair _ s0 s1 =>
congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
(compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0)
(compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
congr_TBind (eq_refl s0)
(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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 =>
congr_Proj1 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
| Proj2 _ s0 =>
congr_Proj2 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
end.
Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@ -638,14 +546,8 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
| Pair _ s0 s1 =>
congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
(rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
| Proj _ s0 s1 =>
congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
| TBind _ s0 s1 s2 =>
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)
| Bot _ => congr_Bot
| Univ _ s0 => congr_Univ (eq_refl s0)
| Proj1 _ s0 => congr_Proj1 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
| Proj2 _ s0 => congr_Proj2 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
end.
Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@ -844,13 +746,9 @@ Core.
Arguments VarTm {n_Tm}.
Arguments Univ {n_Tm}.
Arguments Proj2 {n_Tm}.
Arguments Bot {n_Tm}.
Arguments TBind {n_Tm}.
Arguments Proj {n_Tm}.
Arguments Proj1 {n_Tm}.
Arguments Pair {n_Tm}.

20
theories/diagram.txt
View file

@ -1,20 +0,0 @@
a0 --> a3
| |
| |
v v
a1 --> a4
(Abs a3) >>* a2
Abs a0 ----> (Abs a3) >>* a2
| |
| |
Abs a1 ----> (Abs a4) >>*
a0 >> a1
| |
| |
v v
b0 >> b1

2573
theories/fp_red.v
View file

File diff suppressed because it is too large Load diff

1003
theories/logrel.v
View file

File diff suppressed because it is too large Load diff