Compare commits

..

121 commits

Author SHA1 Message Date
Yiyun Liu
d48d9db1b7 Finish the conversion proof completely 2025-02-17 23:31:12 -05:00
Yiyun Liu
9c5eb31edf Finish all cases of subtyping 2025-02-17 22:50:25 -05:00
Yiyun Liu
735c7f2046 Prove some simple soundness cases of subtyping 2025-02-17 21:43:21 -05:00
Yiyun Liu
067ae89b1d Finish soundness for subtyping 2025-02-17 18:34:48 -05:00
Yiyun Liu
ef3de3af3d Add the specification for algorithmic subtyping 2025-02-16 23:53:14 -05:00
Yiyun Liu
8daaae9831 Minor 2025-02-16 23:39:56 -05:00
Yiyun Liu
eaf59fc45e Finish all cases of algorithmic completeness 2025-02-16 23:25:32 -05:00
Yiyun Liu
21d9a2ce1b Add standardization_lo 2025-02-16 23:00:23 -05:00
Yiyun Liu
bdba6f50e5 Finish the soundness proof completely 2025-02-16 22:43:56 -05:00
Yiyun Liu
d24991e994 Finish most of the neu abs case 2025-02-16 20:43:04 -05:00
Yiyun Liu
49a254fbef Finish the pair pair case 2025-02-16 19:51:08 -05:00
Yiyun Liu
60a4eb886f Finish injectivity for pairs 2025-02-16 19:14:54 -05:00
Yiyun Liu
06d420aa7e Add stubs for lemmas needed for completeness 2025-02-16 01:22:15 -05:00
Yiyun Liu
0f48a485be Prove some impossible cases 2025-02-16 01:13:41 -05:00
Yiyun Liu
3fb6d411e7 Finish most of the pi pi case 2025-02-15 17:22:43 -05:00
Yiyun Liu
926c2284a5 Finish the pair pair case 2025-02-15 16:39:05 -05:00
Yiyun Liu
9d951a24c5 Add standardization theorem for djoin 2025-02-15 14:31:31 -05:00
Yiyun Liu
67f91970d6 Finish the admitted inversion lemmas that depend on SN 2025-02-15 14:04:04 -05:00
Yiyun Liu
9bd554b513 Add injectivity lemma for abs 2025-02-14 21:55:44 -05:00
Yiyun Liu
300530a93f Finish off some easy contradictory cases 2025-02-14 21:31:27 -05:00
Yiyun Liu
f0c18fd77e Finish the neutral app case 2025-02-14 21:11:27 -05:00
Yiyun Liu
8d765c495d Add some more injection lemmas for neutrals 2025-02-14 20:41:56 -05:00
186f2138e6 Finish the var base case 2025-02-14 19:08:41 -05:00
8fd6919538 Make progress on coqeq_complete 2025-02-14 16:57:53 -05:00
ea14ba9602 Prove most of cases of AbsAbs 2025-02-14 16:17:02 -05:00
5ed366f093 Prove some easy cases of completeness 2025-02-14 14:49:19 -05:00
093fc8f9cb Finish algo_metric_case 2025-02-14 13:29:44 -05:00
849169be7f Start coqeq_complete 2025-02-13 17:46:35 -05:00
0a70be3e57 Define the size metric for the completeness proof 2025-02-13 17:09:58 -05:00
Yiyun Liu
1f1b8a83db Pull out some inversion lemmas to prove later 2025-02-12 22:00:44 -05:00
Yiyun Liu
1d3920fce1 Prove the case for pair and neutral 2025-02-12 21:13:47 -05:00
Yiyun Liu
ba77752329 Add more cases to the soundness proof 2025-02-12 20:18:12 -05:00
Yiyun Liu
48adb34946 Add simplified projection lemma 2025-02-12 19:53:20 -05:00
Yiyun Liu
d053f93100 Finish the app neutral case 2025-02-12 19:27:42 -05:00
fa80294c5d Minor 2025-02-12 16:40:51 -05:00
761e96f414 Use the abstract tactic to finish off the symmetric casesa 2025-02-12 16:14:51 -05:00
5ac2bf1c40 Minor 2025-02-12 15:56:35 -05:00
823f61d89f Finish most cases of the soundness proof 2025-02-12 15:54:42 -05:00
15f8a9c687 Try a few cases of soundness 2025-02-11 19:15:06 -05:00
c1a8e9d2e1 Add the top-level subject reduction theorem 2025-02-10 21:51:27 -05:00
c5de86339f Finish subject reduction 2025-02-10 21:50:23 -05:00
bccf6eb860 Add Coquand's algorithm 2025-02-10 18:40:42 -05:00
8105b5c410 Add admissible simple rules 2025-02-10 17:01:40 -05:00
8f8f428562 Finish preservation 2025-02-10 14:16:43 -05:00
5918fdf47e Prove all but 5 cases of regularity 2025-02-10 13:51:35 -05:00
Yiyun Liu
26e3c1c42a Add some cases for regularity 2025-02-10 01:15:44 -05:00
Yiyun Liu
c8e84ef93c Finish morphing 2025-02-10 00:17:01 -05:00
Yiyun Liu
2c47d78ad6 Add stub for morphing 2025-02-09 23:32:07 -05:00
Yiyun Liu
ea1fba8ae9 Finish syntactic renaming 2025-02-09 20:41:27 -05:00
881b2e3825 Add missing premise 2025-02-09 17:05:43 -05:00
df5c6bf0b1 Minor 2025-02-09 17:05:36 -05:00
20bf38a3ca Fix the fundamental theorem yet again 2025-02-09 16:46:17 -05:00
5b925e3fa1 Add beta and eta rules to syntactic typing 2025-02-09 16:33:43 -05:00
133968dd23 Add semantic eta laws for pair 2025-02-09 16:25:34 -05:00
ab1bd8eef8 Add semantic rules for function beta and eta 2025-02-09 16:12:57 -05:00
Yiyun Liu
4396786701 Reformulate renaming 2025-02-08 22:56:45 -05:00
Yiyun Liu
932662d5d9 Finish soundness proof 2025-02-08 22:52:50 -05:00
Yiyun Liu
0c83044d72 Update the typing rules with projections 2025-02-08 22:45:07 -05:00
Yiyun Liu
5996c45526 Finish the semantic projection rules 2025-02-08 22:38:28 -05:00
Yiyun Liu
02e6c9e025 Add pi and sig subtyping semantic rules 2025-02-08 22:15:04 -05:00
Yiyun Liu
916e0bcd75 Change the conversion rules to use Sub instead of Eq 2025-02-08 21:06:51 -05:00
Yiyun Liu
f483d63f01 Fix the definition of semleq 2025-02-08 20:37:46 -05:00
0746e9a354 Finish subtyping semantics 2025-02-07 16:45:58 -05:00
4bc08e1897 Add one interpuniv sub case 2025-02-07 01:19:19 -05:00
707483d401 Add injectivity for subtyping 2025-02-07 00:43:12 -05:00
2f4ea2c78b Add more noconfusion lemmas for untyped subtyping 2025-02-07 00:39:34 -05:00
cf2726be8d Add subtyping 2025-02-06 23:41:38 -05:00
0e5b82b162 Move projection axioms to the subtyping relation 2025-02-06 21:40:26 -05:00
2e2e41cbe6 Add missing Univ rule 2025-02-06 18:15:25 -05:00
6daa275ac8 Prove the fundamental theorem 2025-02-06 18:09:19 -05:00
399c97fa82 Add the semantic well-typedness rules to the hint db 2025-02-06 17:58:38 -05:00
8d92f19d74 Add all(?) typing rules 2025-02-06 17:47:34 -05:00
10f339c5b6 Add some syntactic typing rules 2025-02-06 17:00:04 -05:00
82e21196c2 Minor 2025-02-06 16:31:50 -05:00
e7a26e6bd6 Finish all Bind proj lemmas 2025-02-06 16:20:56 -05:00
c25bac311c Add the first-component inversion lemma for pi and sigma 2025-02-06 16:02:03 -05:00
aca7ebaf1e Finish all the semantic theory for the system with type-directed eq 2025-02-06 15:42:35 -05:00
733e86c611 Finish SE_Pair 2025-02-06 15:20:40 -05:00
435c0e037e Finish (simplified) SE_Bind 2025-02-06 14:37:56 -05:00
1258ac263c Add structural rule for ctx equivalence 2025-02-06 14:37:25 -05:00
db911cff36 Finish the context equality lemma 2025-02-06 14:31:42 -05:00
286ceeed39 Need to extend the notion of semwt to cover arbitrarily scoped terms 2025-02-06 13:53:01 -05:00
fecac84977 Set up interpretation for typed equality 2025-02-06 13:21:30 -05:00
cd3b4981c7 Merge pull request 'logrelnew' () from logrelnew into master
Reviewed-on: 
2025-02-06 00:26:45 -05:00
c24cc7c9b0 Finish ST Conv 2025-02-06 00:08:02 -05:00
64bcf8e9c1 Finish Proj case 2025-02-05 23:56:47 -05:00
d6a96430f0 Add semantic typing 2025-02-05 21:44:35 -05:00
55ccc2bc1d Prove the enhanced interpuniv bind inversion principle 2025-02-05 21:28:39 -05:00
4134fbdada Finish InterpUniv_Join 2025-02-05 21:20:37 -05:00
76f8c32dad Finish the hard fun case for interpuniv_join 2025-02-05 21:14:31 -05:00
Yiyun Liu
1997e8bc12 Side step the need for join subst 2025-02-05 20:36:39 -05:00
Yiyun Liu
7cc6435ea3 Finish most of InterpUniv join 2025-02-05 20:06:03 -05:00
Yiyun Liu
af224831e4 Finish the injectivity of bind and noconfusion 2025-02-05 18:56:47 -05:00
e444c8408f Show that sne and bind are not joinable 2025-02-05 16:52:25 -05:00
0e254c5ac3 Start the proof that joinability preserves meaning 2025-02-05 15:47:51 -05:00
7f29fe0347 Add induction principle for InterpUniv 2025-02-05 14:44:26 -05:00
2393cc5103 Finish adequacy ext 2025-02-05 14:04:44 -05:00
f83af1241b Merge remote-tracking branch 'origin/logrel' into logrelnew 2025-02-05 13:46:08 -05:00
38a0416b2c Add a constant to avoid kripke LR 2025-02-04 22:14:27 -05:00
ee24f8093e Add logical relation for SN 2025-02-04 16:05:02 -05:00
e923194e3d Finish adding pi and sigma types 2025-02-04 15:29:47 -05:00
d9b5ef1267 Refactor the impossible case proof 2025-02-04 15:06:17 -05:00
Yiyun Liu
bd7af7b297 Add README file 2025-02-03 22:47:49 -05:00
84cd0715c7 Prove structural properties of DJoin 2025-02-03 14:55:31 -05:00
3d42581bbe Finish the confluence proof 2025-02-03 14:23:12 -05:00
f3f3991b02 Finish rred standardization 2025-02-03 12:16:56 -05:00
a0c20851fe Prove confluence of beta 2025-02-02 21:57:41 -05:00
cf31e6d285 Finish the confluence proof of ered 2025-02-02 20:48:39 -05:00
Yiyun Liu
376fce619c Save progress 2025-02-02 20:21:06 -05:00
Yiyun Liu
5624415bc9 Finish antirenaming for injective rens 2025-02-02 20:08:37 -05:00
6cc3a65163 Discharge one case of antirenaming using injective renaming 2025-02-02 19:42:42 -05:00
Yiyun Liu
ecb50f1ab7 Add comment about the antirenaming proof 2025-01-31 21:56:58 -05:00
Yiyun Liu
d2cd3105c7 stuck on antirenaming because of scoped syntax 2025-01-31 21:45:55 -05:00
Yiyun Liu
580e3a8251 Prove that ered is strongly normalizing 2025-01-31 20:54:33 -05:00
Yiyun Liu
f57e10be93 Finish extracting leftmost-outermost red from sn 2025-01-31 20:10:56 -05:00
Yiyun Liu
571779a4dd Fix name change errors for EPar 2025-01-31 17:32:35 -05:00
Yiyun Liu
5dd3428e2b Merge remote-tracking branch 'forgejo/nonessential' 2025-01-31 17:31:21 -05:00
Yiyun Liu
5a7f46a8a1 Finish the enhanced eta postponement 2025-01-30 23:29:25 -05:00
Yiyun Liu
51ac5ffbd6 Finish eta postponement 2025-01-30 23:10:11 -05:00
9134cfec8a Finish a few cases of eta postponement 2025-01-30 22:18:58 -05:00
d925a8bcaa Minor cleanup 2025-01-30 20:23:57 -05:00
12 changed files with 6294 additions and 257 deletions

42
README.org Normal file
View file

@ -0,0 +1,42 @@
* Church Rosser, surjective pairing, and strong normalization
This repository contains a mechanized proof that the lambda calculus
with beta and eta rules for functions and pairs is in fact confluent
for the subset of terms that are "strongly $\beta$-normalizing".
Our notion of $\beta$-strong normalization, based on Abel's POPLMark
Reloaded survey, is inductively defined
and captures a strict subset of the usual notion of strong
normalization in the sense that ill-formed terms such as $\pi_1
\lambda x . x$ are rejected.
* Joinability: A transitive equational relation
The joinability relation $a \Leftrightarrow b$, which is true exactly
when $\exists c, a \leadsto_{\beta\eta} c \wedge b
\leadsto_{\beta\eta} c$, is transitive on the set of strongly
normalizing terms thanks to the Church-Rosser theorem proven in this
repository.
** Joinability and logical predicates
When building a logical predicate where adequacy ensures beta strong
normalization, we can then show that two types $A \Leftrightarrow B$
share the same meaning if both are semantically well-formed. The
strong normalization constraint can be extracted from adequacy so we
have transitivity of $A \Leftrightarrow B$ available in the proof that
the logical predicate is functional over joinable terms.
** Joinability and typed equality
For systems with a type-directed equality, the same joinability
relation can be used to model the equality. The fundamental theorem
for the judgmental equality would take the following form: $\vdash a
\equiv b \in A$ implies $\vDash a, b \in A$ and $a \Leftrightarrow b$.
Note that such a result does not immediately give us the decidability
of type conversion because the algorithm of beta-eta normalization
may identify more terms when eta is not type-preserving. However, I
believe Coquand's algorithm can be proven correct using the method
described in [[https://www.researchgate.net/publication/226663076_Justifying_Algorithms_for_be-Conversion][Goguen 2005]]. We have all the ingredients needed:
- Strong normalization of beta (needed for the termination metric)
- Church-Rosser for $\beta$-SN terms (the disciplined expansion of
Coquand's algorithm preserves both SN and typing)

View file

@ -1,15 +1,19 @@
PTm(VarPTm) : Type PTm(VarPTm) : Type
PTag : Type PTag : Type
Ty : Type BTag : Type
Fun : Ty -> Ty -> Ty nat : Type
Prod : Ty -> Ty -> Ty
Void : Ty
PL : PTag PL : PTag
PR : PTag PR : PTag
PPi : BTag
PSig : BTag
PAbs : (bind PTm in PTm) -> PTm PAbs : (bind PTm in PTm) -> PTm
PApp : PTm -> PTm -> PTm PApp : PTm -> PTm -> PTm
PPair : PTm -> PTm -> PTm PPair : PTm -> PTm -> PTm
PProj : PTag -> PTm -> PTm PProj : PTag -> PTm -> PTm
PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
PUniv : nat -> PTm
PBot : PTm

View file

@ -5,6 +5,20 @@ Require Import Setoid Morphisms Relation_Definitions.
Module Core. Module Core.
Inductive BTag : Type :=
| PPi : BTag
| PSig : BTag.
Lemma congr_PPi : PPi = PPi.
Proof.
exact (eq_refl).
Qed.
Lemma congr_PSig : PSig = PSig.
Proof.
exact (eq_refl).
Qed.
Inductive PTag : Type := Inductive PTag : Type :=
| PL : PTag | PL : PTag
| PR : PTag. | PR : PTag.
@ -24,7 +38,10 @@ Inductive PTm (n_PTm : nat) : Type :=
| PAbs : PTm (S n_PTm) -> PTm n_PTm | PAbs : PTm (S n_PTm) -> PTm n_PTm
| PApp : PTm n_PTm -> PTm 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 | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
| PProj : PTag -> 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.
Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_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. (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
@ -56,6 +73,28 @@ 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)). (ap (fun x => PProj m_PTm t0 x) H1)).
Qed. 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.
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)).
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) : Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
fin (S m) -> fin (S n). fin (S m) -> fin (S n).
Proof. Proof.
@ -76,6 +115,10 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
| PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_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) | 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) | 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
end. end.
Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
@ -102,6 +145,11 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
| PPair _ s0 s1 => | PPair _ s0 s1 =>
PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm 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) | 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
end. end.
Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm) Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
@ -140,6 +188,11 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
(idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s1)
| PProj _ s0 s1 => | PProj _ s0 s1 =>
congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm 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
end. end.
Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
@ -180,6 +233,12 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
(extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) (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) congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
| 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
end. end.
Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
@ -221,6 +280,12 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
(ext_PTm sigma_PTm tau_PTm Eq_PTm s1) (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) congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
| 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
end. end.
Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@ -262,6 +327,13 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
| PProj _ s0 s1 => | PProj _ s0 s1 =>
congr_PProj (eq_refl s0) congr_PProj (eq_refl s0)
(compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
| 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
end. end.
Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat} Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
@ -312,6 +384,13 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
| PProj _ s0 s1 => | PProj _ s0 s1 =>
congr_PProj (eq_refl s0) congr_PProj (eq_refl s0)
(compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
| 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
end. end.
Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@ -382,6 +461,13 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
| PProj _ s0 s1 => | PProj _ s0 s1 =>
congr_PProj (eq_refl s0) congr_PProj (eq_refl s0)
(compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
| 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
end. end.
Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@ -454,6 +540,13 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
| PProj _ s0 s1 => | PProj _ s0 s1 =>
congr_PProj (eq_refl s0) congr_PProj (eq_refl s0)
(compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
| 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
end. end.
Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
@ -566,6 +659,12 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
(rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) (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) congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
| 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
end. end.
Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat} Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
@ -637,30 +736,6 @@ Proof.
exact (fun x => eq_refl). exact (fun x => eq_refl).
Qed. 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 := Class Up_PTm X Y :=
up_PTm : X -> Y. up_PTm : X -> Y.
@ -796,6 +871,12 @@ Core.
Arguments VarPTm {n_PTm}. Arguments VarPTm {n_PTm}.
Arguments PBot {n_PTm}.
Arguments PUniv {n_PTm}.
Arguments PBind {n_PTm}.
Arguments PProj {n_PTm}. Arguments PProj {n_PTm}.
Arguments PPair {n_PTm}. Arguments PPair {n_PTm}.
@ -804,9 +885,9 @@ Arguments PApp {n_PTm}.
Arguments PAbs {n_PTm}. Arguments PAbs {n_PTm}.
#[global]Hint Opaque subst_PTm: rewrite. #[global] Hint Opaque subst_PTm: rewrite.
#[global]Hint Opaque ren_PTm: rewrite. #[global] Hint Opaque ren_PTm: rewrite.
End Extra. End Extra.

69
theories/admissible.v Normal file
View file

@ -0,0 +1,69 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
From Hammer Require Import Tactics.
Require Import ssreflect.
Require Import Psatz.
Require Import Coq.Logic.FunctionalExtensionality.
Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), Γ) Sort Prop.
Lemma Wff_Cons_Inv n Γ (A : PTm n) :
funcomp (ren_PTm shift) (scons A Γ) ->
Γ /\ exists i, Γ A PUniv i.
Proof.
elim /wff_inv => //= _.
move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
Equality.simplify_dep_elim.
have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
move /(_ var_zero) : (h).
rewrite /funcomp. asimpl.
move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
move => ?. subst.
have : Γ0 = Γ. extensionality i.
move /(_ (Some i)) : h.
rewrite /funcomp. asimpl.
move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
done.
move => ?. subst. sfirstorder.
Qed.
Lemma T_Abs n Γ (a : PTm (S n)) A B :
funcomp (ren_PTm shift) (scons A Γ) a B ->
Γ PAbs a PBind PPi A B.
Proof.
move => ha.
have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) B PUniv i by sfirstorder use:regularity.
have : funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
move /Wff_Cons_Inv : => [][j]hA.
hauto lq:on rew:off use:T_Bind', typing.T_Abs.
Qed.
Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
Γ A0 A1 PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) B0 B1 PUniv i ->
Γ PBind p A0 B0 PBind p A1 B1 PUniv i.
Proof.
move => h0 h1.
have : Γ A0 PUniv i by hauto l:on use:regularity.
have : Γ by sfirstorder use:wff_mutual.
move : E_Bind h0 h1; repeat move/[apply].
firstorder.
Qed.
Lemma E_App n Γ (b0 b1 a0 a1 : PTm n) A B :
Γ b0 b1 PBind PPi A B ->
Γ a0 a1 A ->
Γ PApp b0 a0 PApp b1 a1 subst_PTm (scons a0 VarPTm) B.
Proof.
move => h.
have [i] : exists i, Γ PBind PPi A B PUniv i by hauto l:on use:regularity.
move : E_App h. by repeat move/[apply].
Qed.
Lemma E_Proj2 n Γ (a b : PTm n) A B :
Γ a b PBind PSig A B ->
Γ PProj PR a PProj PR b subst_PTm (scons (PProj PL a) VarPTm) B.
Proof.
move => h.
have [i] : exists i, Γ PBind PSig A B PUniv i by hauto l:on use:regularity.
move : E_Proj2 h; by repeat move/[apply].
Qed.

1648
theories/algorithmic.v Normal file

File diff suppressed because it is too large Load diff

97
theories/common.v Normal file
View file

@ -0,0 +1,97 @@
Require Import Autosubst2.fintype Autosubst2.syntax 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).
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 q:on depth:2))
| _ => solve_anti_ren ()
end.
Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
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.
Proof.
sblast inv:option.
Qed.
Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
(forall i j, ξ i = ξ j -> i = j) ->
ren_PTm ξ a = ren_PTm ξ b ->
a = b.
Proof.
move : m ξ b.
elim : n / a => //; try solve_anti_ren.
move => n a iha m ξ []//=.
move => u [h].
apply iha in h. by subst.
destruct i, j=>//=.
hauto l:on.
move => n p A ihA B ihB m ξ []//=.
move => b A0 B0 [?]. subst.
move => ?. have ? : A0 = A by firstorder. subst.
move => ?. have : B = B0. apply : ihB; eauto.
sauto.
congruence.
Qed.
Definition ishf {n} (a : PTm n) :=
match a with
| PPair _ _ => true
| PAbs _ => true
| PUniv _ => true
| PBind _ _ _ => true
| _ => false
end.
Fixpoint ishne {n} (a : PTm n) :=
match a with
| VarPTm _ => true
| PApp a _ => ishne a
| PProj _ a => ishne a
| PBot => true
| _ => false
end.
Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
Definition ispair {n} (a : PTm n) :=
match a with
| PPair _ _ => true
| _ => false
end.
Definition isabs {n} (a : PTm n) :=
match a with
| PAbs _ => true
| _ => false
end.
Definition ishf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
ishf (ren_PTm ξ a) = ishf a.
Proof. case : a => //=. Qed.
Definition isabs_ren n m (a : PTm n) (ξ : fin n -> fin m) :
isabs (ren_PTm ξ a) = isabs a.
Proof. case : a => //=. Qed.
Definition ispair_ren n m (a : PTm n) (ξ : fin n -> fin m) :
ispair (ren_PTm ξ a) = ispair a.
Proof. case : a => //=. Qed.
Definition ishne_ren n m (a : PTm n) (ξ : fin n -> fin m) :
ishne (ren_PTm ξ a) = ishne a.
Proof. move : m ξ. elim : n / a => //=. Qed.

File diff suppressed because it is too large Load diff

1335
theories/logrel.v Normal file

File diff suppressed because it is too large Load diff

179
theories/preservation.v Normal file
View file

@ -0,0 +1,179 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red.
From Hammer Require Import Tactics.
Require Import ssreflect.
Require Import Psatz.
Require Import Coq.Logic.FunctionalExtensionality.
Lemma App_Inv n Γ (b a : PTm n) U :
Γ PApp b a U ->
exists A B, Γ b PBind PPi A B /\ Γ a A /\ Γ subst_PTm (scons a VarPTm) B U.
Proof.
move E : (PApp b a) => u hu.
move : b a E. elim : n Γ u U / hu => n //=.
- move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
exists A,B.
repeat split => //=.
have [i] : exists i, Γ PBind PPi A B PUniv i by sfirstorder use:regularity.
hauto lq:on use:bind_inst, E_Refl.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Abs_Inv n Γ (a : PTm (S n)) U :
Γ PAbs a U ->
exists A B, funcomp (ren_PTm shift) (scons A Γ) a B /\ Γ PBind PPi A B U.
Proof.
move E : (PAbs a) => u hu.
move : a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B i hP _ ha _ a0 [*]. subst.
exists A, B. repeat split => //=.
hauto lq:on use:E_Refl, Su_Eq.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Proj1_Inv n Γ (a : PTm n) U :
Γ PProj PL a U ->
exists A B, Γ a PBind PSig A B /\ Γ A U.
Proof.
move E : (PProj PL a) => u hu.
move :a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B ha _ a0 [*]. subst.
exists A, B. split => //=.
eapply regularity in ha.
move : ha => [i].
move /Bind_Inv => [j][h _].
by move /E_Refl /Su_Eq in h.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Proj2_Inv n Γ (a : PTm n) U :
Γ PProj PR a U ->
exists A B, Γ a PBind PSig A B /\ Γ subst_PTm (scons (PProj PL a) VarPTm) B U.
Proof.
move E : (PProj PR a) => u hu.
move :a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B ha _ a0 [*]. subst.
exists A, B. split => //=.
have ha' := ha.
eapply regularity in ha.
move : ha => [i ha].
move /T_Proj1 in ha'.
apply : bind_inst; eauto.
apply : E_Refl ha'.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Pair_Inv n Γ (a b : PTm n) U :
Γ PPair a b U ->
exists A B, Γ a A /\
Γ b subst_PTm (scons a VarPTm) B /\
Γ PBind PSig A B U.
Proof.
move E : (PPair a b) => u hu.
move : a b E. elim : n Γ u U / hu => n //=.
- move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
exists A,B. repeat split => //=.
move /E_Refl /Su_Eq : hS. apply.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
Γ PApp (PAbs a) b A -> Γ PApp (PAbs a) b subst_PTm (scons b VarPTm) a A.
Proof.
move => n a b Γ A ha.
move /App_Inv : ha.
move => [A0][B0][ha][hb]hS.
move /Abs_Inv : ha => [A1][B1][ha]hS0.
have hb' := hb.
move /E_Refl in hb.
have hS1 : Γ A0 A1 by sfirstorder use:Su_Pi_Proj1.
have [i hPi] : exists i, Γ PBind PPi A1 B1 PUniv i by sfirstorder use:regularity_sub0.
move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
move => h.
apply : E_Conv; eauto.
apply : E_AppAbs; eauto.
eauto using T_Conv.
Qed.
Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
Γ PProj PL (PPair a b) A -> Γ PProj PL (PPair a b) a A.
Proof.
move => n a b Γ A.
move /Proj1_Inv. move => [A0][B0][hab]hA0.
move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
have [i ?] : exists i, Γ PBind PSig A1 B1 PUniv i by sfirstorder use:regularity_sub0.
move /Su_Sig_Proj1 in hS.
have {hA0} {}hS : Γ A1 A by eauto using Su_Transitive.
apply : E_Conv; eauto.
apply : E_ProjPair1; eauto.
Qed.
Lemma RRed_Eq n Γ (a b : PTm n) A :
Γ a A ->
RRed.R a b ->
Γ a b A.
Proof.
move => + h. move : Γ A. elim : n a b /h => n.
- apply E_AppAbs.
- move => p a b Γ A.
case : p => //=.
+ apply E_ProjPair1.
+ move /Proj2_Inv. move => [A0][B0][hab]hA0.
move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
have [i ?] : exists i, Γ PBind PSig A1 B1 PUniv i by sfirstorder use:regularity_sub0.
have : Γ PPair a b PBind PSig A1 B1 by hauto lq:on ctrs:Wt.
move /T_Proj1.
move /E_ProjPair1 /E_Symmetric => h.
have /Su_Sig_Proj1 hSA := hS.
have : Γ subst_PTm (scons a VarPTm) B1 subst_PTm (scons (PProj PL (PPair a b)) VarPTm) B0 by
apply : Su_Sig_Proj2; eauto.
move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
move {hS}.
move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
- qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
- move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
have {}/iha iha := ih0.
have [i hP] : exists i, Γ PBind PPi A0 B0 PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_App; eauto using E_Refl.
- move => a0 b0 b1 ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
have {}/iha iha := ih1.
have [i hP] : exists i, Γ PBind PPi A0 B0 PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_App; eauto.
sfirstorder use:E_Refl.
- move => a0 a1 b ha iha Γ A /Pair_Inv.
move => [A0][B0][h0][h1]hU.
have [i hP] : exists i, Γ PBind PSig A0 B0 PUniv i by eauto using regularity_sub0.
have {}/iha iha := h0.
apply : E_Conv; eauto.
apply : E_Pair; eauto using E_Refl.
- move => a b0 b1 ha iha Γ A /Pair_Inv.
move => [A0][B0][h0][h1]hU.
have [i hP] : exists i, Γ PBind PSig A0 B0 PUniv i by eauto using regularity_sub0.
have {}/iha iha := h1.
apply : E_Conv; eauto.
apply : E_Pair; eauto using E_Refl.
- case.
+ move => a0 a1 ha iha Γ A /Proj1_Inv [A0][B0][h0]hU.
apply : E_Conv; eauto.
qauto l:on ctrs:Eq,Wt.
+ move => a0 a1 ha iha Γ A /Proj2_Inv [A0][B0][h0]hU.
have [i hP] : exists i, Γ PBind PSig A0 B0 PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_Proj2; eauto.
- move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
have {}/ihA ihA := h0.
apply : E_Conv; eauto.
apply E_Bind'; eauto using E_Refl.
- move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
have {}/ihA ihA := h1.
apply : E_Conv; eauto.
apply E_Bind'; eauto using E_Refl.
Qed.
Theorem subject_reduction n Γ (a b A : PTm n) :
Γ a A ->
RRed.R a b ->
Γ b A.
Proof. hauto lq:on use:RRed_Eq, regularity. Qed.

15
theories/soundness.v Normal file
View file

@ -0,0 +1,15 @@
Require Import Autosubst2.fintype Autosubst2.syntax.
Require Import fp_red logrel typing.
From Hammer Require Import Tactics.
Theorem fundamental_theorem :
(forall n (Γ : fin n -> PTm n), Γ -> Γ) /\
(forall n Γ (a A : PTm n), Γ a A -> Γ a A) /\
(forall n Γ (a b A : PTm n), Γ a b A -> Γ a b A) /\
(forall n Γ (a b : PTm n), Γ a b -> Γ a b).
apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
Unshelve. all : exact 0.
Qed.
Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ a b -> SN a /\ SN b /\ Sub.R a b.
Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.

676
theories/structural.v Normal file
View file

@ -0,0 +1,676 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing.
From Hammer Require Import Tactics.
Require Import ssreflect.
Require Import Psatz.
Lemma wff_mutual :
(forall n (Γ : fin n -> PTm n), Γ -> True) /\
(forall n Γ (a A : PTm n), Γ a A -> Γ) /\
(forall n Γ (a b A : PTm n), Γ a b A -> Γ) /\
(forall n Γ (A B : PTm n), Γ A B -> Γ).
Proof. apply wt_mutual; eauto. Qed.
#[export]Hint Constructors Wt Wff Eq : wt.
Lemma renaming_up n m (ξ : fin n -> fin m) Δ Γ A :
renaming_ok Δ Γ ξ ->
renaming_ok (funcomp (ren_PTm shift) (scons (ren_PTm ξ A) Δ)) (funcomp (ren_PTm shift) (scons A Γ)) (upRen_PTm_PTm ξ) .
Proof.
move => h i.
destruct i as [i|].
asimpl. rewrite /renaming_ok in h.
rewrite /funcomp. rewrite -h.
by asimpl.
by asimpl.
Qed.
Lemma Su_Wt n Γ a i :
Γ a @PUniv n i ->
Γ a a.
Proof. hauto lq:on ctrs:LEq, Eq. Qed.
Lemma Wt_Univ n Γ a A i
(h : Γ a A) :
Γ @PUniv n i PUniv (S i).
Proof.
hauto lq:on ctrs:Wt use:wff_mutual.
Qed.
Lemma Bind_Inv n Γ p (A : PTm n) B U :
Γ PBind p A B U ->
exists i, Γ A PUniv i /\
funcomp (ren_PTm shift) (scons A Γ) B PUniv i /\
Γ PUniv i U.
Proof.
move E :(PBind p A B) => T h.
move : p A B E.
elim : n Γ T U / h => //=.
- hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
- hauto lq:on rew:off ctrs:LEq.
Qed.
(* Lemma Pi_Inv n Γ (A : PTm n) B U : *)
(* Γ ⊢ PBind PPi A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PPi A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
(* Lemma Bind_Inv n Γ (A : PTm n) B U : *)
(* Γ ⊢ PBind PSig A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PSig A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
Lemma T_App' n Γ (b a : PTm n) A B U :
U = subst_PTm (scons a VarPTm) B ->
Γ b PBind PPi A B ->
Γ a A ->
Γ PApp b a U.
Proof. move => ->. apply T_App. Qed.
Lemma T_Pair' n Γ (a b : PTm n) A B i U :
U = subst_PTm (scons a VarPTm) B ->
Γ a A ->
Γ b U ->
Γ PBind PSig A B (PUniv i) ->
Γ PPair a b PBind PSig A B.
Proof.
move => ->. eauto using T_Pair.
Qed.
Lemma T_Proj2' n Γ (a : PTm n) A B U :
U = subst_PTm (scons (PProj PL a) VarPTm) B ->
Γ a PBind PSig A B ->
Γ PProj PR a U.
Proof. move => ->. apply T_Proj2. Qed.
Lemma E_Proj2' n Γ i (a b : PTm n) A B U :
U = subst_PTm (scons (PProj PL a) VarPTm) B ->
Γ PBind PSig A B (PUniv i) ->
Γ a b PBind PSig A B ->
Γ PProj PR a PProj PR b U.
Proof.
move => ->. apply E_Proj2.
Qed.
Lemma E_Bind' n Γ i p (A0 A1 : PTm n) B0 B1 :
Γ A0 PUniv i ->
Γ A0 A1 PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) B0 B1 PUniv i ->
Γ PBind p A0 B0 PBind p A1 B1 PUniv i.
Proof. hauto lq:on use:E_Bind, wff_mutual. Qed.
Lemma E_App' n Γ i (b0 b1 a0 a1 : PTm n) A B U :
U = subst_PTm (scons a0 VarPTm) B ->
Γ PBind PPi A B (PUniv i) ->
Γ b0 b1 PBind PPi A B ->
Γ a0 a1 A ->
Γ PApp b0 a0 PApp b1 a1 U.
Proof. move => ->. apply E_App. Qed.
Lemma E_AppAbs' n Γ (a : PTm (S n)) b A B i u U :
u = subst_PTm (scons b VarPTm) a ->
U = subst_PTm (scons b VarPTm ) B ->
Γ PBind PPi A B PUniv i ->
Γ b A ->
funcomp (ren_PTm shift) (scons A Γ) a B ->
Γ PApp (PAbs a) b u U.
move => -> ->. apply E_AppAbs. Qed.
Lemma E_ProjPair2' n Γ (a b : PTm n) A B i U :
U = subst_PTm (scons a VarPTm) B ->
Γ PBind PSig A B (PUniv i) ->
Γ a A ->
Γ b subst_PTm (scons a VarPTm) B ->
Γ PProj PR (PPair a b) b U.
Proof. move => ->. apply E_ProjPair2. Qed.
Lemma E_AppEta' n Γ (b : PTm n) A B i u :
u = (PApp (ren_PTm shift b) (VarPTm var_zero)) ->
Γ PBind PPi A B (PUniv i) ->
Γ b PBind PPi A B ->
Γ PAbs u b PBind PPi A B.
Proof. qauto l:on use:wff_mutual, E_AppEta. Qed.
Lemma Su_Pi_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
U = subst_PTm (scons a0 VarPTm) B0 ->
T = subst_PTm (scons a1 VarPTm) B1 ->
Γ PBind PPi A0 B0 PBind PPi A1 B1 ->
Γ a0 a1 A1 ->
Γ U T.
Proof. move => -> ->. apply Su_Pi_Proj2. Qed.
Lemma Su_Sig_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
U = subst_PTm (scons a0 VarPTm) B0 ->
T = subst_PTm (scons a1 VarPTm) B1 ->
Γ PBind PSig A0 B0 PBind PSig A1 B1 ->
Γ a0 a1 A0 ->
Γ U T.
Proof. move => -> ->. apply Su_Sig_Proj2. Qed.
Lemma renaming :
(forall n (Γ : fin n -> PTm n), Γ -> True) /\
(forall n Γ (a A : PTm n), Γ a A -> forall m Δ (ξ : fin n -> fin m), Δ -> renaming_ok Δ Γ ξ ->
Δ ren_PTm ξ a ren_PTm ξ A) /\
(forall n Γ (a b A : PTm n), Γ a b A -> forall m Δ (ξ : fin n -> fin m), Δ -> renaming_ok Δ Γ ξ ->
Δ ren_PTm ξ a ren_PTm ξ b ren_PTm ξ A) /\
(forall n Γ (A B : PTm n), Γ A B -> forall m Δ (ξ : fin n -> fin m), Δ -> renaming_ok Δ Γ ξ ->
Δ ren_PTm ξ A ren_PTm ξ B).
Proof.
apply wt_mutual => //=; eauto 3 with wt.
- move => n Γ i _ m Δ ξ .
rewrite .
by apply T_Var.
- hauto lq:on rew:off ctrs:Wt, Wff use:renaming_up.
- move => n Γ a A B i hP ihP ha iha m Δ ξ .
apply : T_Abs; eauto.
move : ihP() (); repeat move/[apply]. move/Bind_Inv.
hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up.
- move => *. apply : T_App'; eauto. by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ξ .
eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
- move => n Γ a A B ha iha m Δ ξ . apply : T_Proj2'; eauto. by asimpl.
- hauto lq:on ctrs:Wt,LEq.
- hauto lq:on ctrs:Eq.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ξ .
move : ihPi () (). repeat move/[apply].
move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) PUniv j by qauto l:on ctrs:Wt.
move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up.
- move => *. apply : E_App'; eauto. by asimpl.
- move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ξ .
apply : E_Pair; eauto.
move : ihb . repeat move/[apply].
by asimpl.
- move => *. apply : E_Proj2'; eauto. by asimpl.
- qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ξ .
move : ihP () (). repeat move/[apply].
move /Bind_Inv.
move => [j][h0][h1]h2.
have ? : Δ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:renaming_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ .
move : {hP} ihP () (). repeat move/[apply].
move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto.
move : ihb . repeat move/[apply]. by asimpl.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ .
apply : E_ProjPair2'; eauto. by asimpl.
move : ihb ; repeat move/[apply]. by asimpl.
- move => *.
apply : E_AppEta'; eauto. by asimpl.
- qauto l:on use:E_PairEta.
- hauto lq:on ctrs:LEq.
- qauto l:on ctrs:LEq.
- hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
- hauto lq:on ctrs:Wff use:Su_Sig, renaming_up.
- hauto q:on ctrs:LEq.
- hauto lq:on ctrs:LEq.
- qauto l:on ctrs:LEq.
- move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
- move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
Qed.
Definition morphing_ok {n m} Δ Γ (ρ : fin n -> PTm m) :=
forall i, Δ ρ i subst_PTm ρ (Γ i).
Lemma morphing_ren n m p Ξ Δ Γ
(ρ : fin n -> PTm m) (ξ : fin m -> fin p) :
Ξ ->
renaming_ok Ξ Δ ξ -> morphing_ok Δ Γ ρ ->
morphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
Proof.
move => hρ.
move => i.
rewrite {1}/funcomp.
have -> :
subst_PTm (funcomp (ren_PTm ξ) ρ) (Γ i) =
ren_PTm ξ (subst_PTm ρ (Γ i)) by asimpl.
eapply renaming; eauto.
Qed.
Lemma morphing_ext n m Δ Γ (ρ : fin n -> PTm m) (a : PTm m) (A : PTm n) :
morphing_ok Δ Γ ρ ->
Δ a subst_PTm ρ A ->
morphing_ok
Δ (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ).
Proof.
move => h ha i. destruct i as [i|]; by asimpl.
Qed.
Lemma T_Var' n Γ (i : fin n) U :
U = Γ i ->
Γ ->
Γ VarPTm i U.
Proof. move => ->. apply T_Var. Qed.
Lemma renaming_wt : forall n Γ (a A : PTm n), Γ a A -> forall m Δ (ξ : fin n -> fin m), Δ -> renaming_ok Δ Γ ξ -> Δ ren_PTm ξ a ren_PTm ξ A.
Proof. sfirstorder use:renaming. Qed.
Lemma renaming_wt' : forall n m Δ Γ a A (ξ : fin n -> fin m) u U,
u = ren_PTm ξ a -> U = ren_PTm ξ A ->
Γ a A -> Δ ->
renaming_ok Δ Γ ξ -> Δ u U.
Proof. hauto use:renaming_wt. 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 morphing_up n m Γ Δ (ρ : fin n -> PTm m) (A : PTm n) k :
morphing_ok Γ Δ ρ ->
Γ subst_PTm ρ A PUniv k ->
morphing_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) (funcomp (ren_PTm shift) (scons A Δ)) (up_PTm_PTm ρ).
Proof.
move => h h1 [:hp]. apply morphing_ext.
rewrite /morphing_ok.
move => i.
rewrite {2}/funcomp.
apply : renaming_wt'; eauto. by asimpl.
abstract : hp. qauto l:on ctrs:Wff use:wff_mutual.
eauto using renaming_shift.
apply : T_Var';eauto. rewrite /funcomp. by asimpl.
Qed.
Lemma Wff_Cons' n Γ (A : PTm n) i :
Γ A PUniv i ->
(* -------------------------------- *)
funcomp (ren_PTm shift) (scons A Γ).
Proof. hauto lq:on rew:off use:Wff_Cons, wff_mutual. Qed.
Lemma weakening_wt : forall n Γ (a A B : PTm n) i,
Γ B PUniv i ->
Γ a A ->
funcomp (ren_PTm shift) (scons B Γ) ren_PTm shift a ren_PTm shift A.
Proof.
move => n Γ a A B i hB ha.
apply : renaming_wt'; eauto.
apply : Wff_Cons'; eauto.
apply : renaming_shift; eauto.
Qed.
Lemma weakening_wt' : forall n Γ (a A B : PTm n) i U u,
u = ren_PTm shift a ->
U = ren_PTm shift A ->
Γ B PUniv i ->
Γ a A ->
funcomp (ren_PTm shift) (scons B Γ) u U.
Proof. move => > -> ->. apply weakening_wt. Qed.
Lemma morphing :
(forall n (Γ : fin n -> PTm n), Γ -> True) /\
(forall n Γ (a A : PTm n), Γ a A -> forall m Δ (ρ : fin n -> PTm m), Δ -> morphing_ok Δ Γ ρ ->
Δ subst_PTm ρ a subst_PTm ρ A) /\
(forall n Γ (a b A : PTm n), Γ a b A -> forall m Δ (ρ : fin n -> PTm m), Δ -> morphing_ok Δ Γ ρ ->
Δ subst_PTm ρ a subst_PTm ρ b subst_PTm ρ A) /\
(forall n Γ (A B : PTm n), Γ A B -> forall m Δ (ρ : fin n -> PTm m), Δ -> morphing_ok Δ Γ ρ ->
Δ subst_PTm ρ A subst_PTm ρ B).
Proof.
apply wt_mutual => //=.
- hauto lq:on use:morphing_up, Wff_Cons', T_Bind.
- move => n Γ a A B i hP ihP ha iha m Δ ρ hρ.
move : ihP () (hρ); repeat move/[apply].
move /Bind_Inv => [j][h0][h1]h2. move {hP}.
have ? : Δ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) PUniv i by hauto lq:on ctrs:Wt.
apply : T_Abs; eauto.
apply : iha.
hauto lq:on use:Wff_Cons', Bind_Inv.
apply : morphing_up; eauto.
- move => *; apply : T_App'; eauto; by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ρ hρ .
eapply T_Pair' with (U := subst_PTm ρ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
- hauto lq:on use:T_Proj1.
- move => *. apply : T_Proj2'; eauto. by asimpl.
- hauto lq:on ctrs:Wt,LEq.
- qauto l:on ctrs:Wt.
- hauto lq:on ctrs:Eq.
- hauto lq:on ctrs:Eq.
- hauto lq:on ctrs:Eq.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ρ hρ.
move : ihPi () (hρ). repeat move/[apply].
move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) PUniv j by qauto l:on ctrs:Wt.
move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up.
- move => *. apply : E_App'; eauto. by asimpl.
- move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ρ hρ.
apply : E_Pair; eauto.
move : ihb hρ. repeat move/[apply].
by asimpl.
- hauto q:on ctrs:Eq.
- move => *. apply : E_Proj2'; eauto. by asimpl.
- qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ρ hρ.
move : ihP (hρ) (). repeat move/[apply].
move /Bind_Inv.
move => [j][h0][h1]h2.
have ? : Δ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:morphing_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hρ.
move : {hP} ihP (hρ) (). repeat move/[apply].
move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto.
move : ihb hρ . repeat move/[apply]. by asimpl.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hρ.
apply : E_ProjPair2'; eauto. by asimpl.
move : ihb hρ ; repeat move/[apply]. by asimpl.
- move => *.
apply : E_AppEta'; eauto. by asimpl.
- qauto l:on use:E_PairEta.
- hauto lq:on ctrs:LEq.
- qauto l:on ctrs:LEq.
- hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
- hauto lq:on ctrs:Wff use:Su_Sig, morphing_up.
- hauto q:on ctrs:LEq.
- hauto lq:on ctrs:LEq.
- qauto l:on ctrs:LEq.
- move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
- move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
Qed.
Lemma morphing_wt : forall n Γ (a A : PTm n), Γ a A -> forall m Δ (ρ : fin n -> PTm m), Δ -> morphing_ok Δ Γ ρ -> Δ subst_PTm ρ a subst_PTm ρ A.
Proof. sfirstorder use:morphing. Qed.
Lemma morphing_wt' : forall n m Δ Γ a A (ρ : fin n -> PTm m) u U,
u = subst_PTm ρ a -> U = subst_PTm ρ A ->
Γ a A -> Δ ->
morphing_ok Δ Γ ρ -> Δ u U.
Proof. hauto use:morphing_wt. Qed.
Lemma morphing_id : forall n (Γ : fin n -> PTm n), Γ -> morphing_ok Γ Γ VarPTm.
Proof.
move => n Γ .
rewrite /morphing_ok.
move => i. asimpl. by apply T_Var.
Qed.
Lemma substing_wt : forall n Γ (a : PTm (S n)) (b A : PTm n) B,
funcomp (ren_PTm shift) (scons A Γ) a B ->
Γ b A ->
Γ subst_PTm (scons b VarPTm) a subst_PTm (scons b VarPTm) B.
Proof.
move => n Γ a b A B ha hb [:]. apply : morphing_wt; eauto.
abstract : . sfirstorder use:wff_mutual.
apply morphing_ext; last by asimpl.
by apply morphing_id.
Qed.
(* Could generalize to all equal contexts *)
Lemma ctx_eq_subst_one n (A0 A1 : PTm n) i j Γ a A :
funcomp (ren_PTm shift) (scons A0 Γ) a A ->
Γ A0 PUniv i ->
Γ A1 PUniv j ->
Γ A1 A0 ->
funcomp (ren_PTm shift) (scons A1 Γ) a A.
Proof.
move => h0 h1 h2 h3.
replace a with (subst_PTm VarPTm a); last by asimpl.
replace A with (subst_PTm VarPTm A); last by asimpl.
have ? : Γ by sfirstorder use:wff_mutual.
apply : morphing_wt; eauto.
apply : Wff_Cons'; eauto.
move => k. destruct k as [k|].
- asimpl.
eapply weakening_wt' with (a := VarPTm k);eauto using T_Var.
by substify.
- move => [:hΓ'].
apply : T_Conv.
apply T_Var.
abstract : hΓ'.
eauto using Wff_Cons'.
rewrite /funcomp. asimpl. substify. asimpl.
renamify.
eapply renaming; eauto.
apply : renaming_shift; eauto.
Qed.
Lemma bind_inst n Γ p (A : PTm n) B i a0 a1 :
Γ PBind p A B PUniv i ->
Γ a0 a1 A ->
Γ subst_PTm (scons a0 VarPTm) B subst_PTm (scons a1 VarPTm) B.
Proof.
move => h h0.
have {}h : Γ PBind p A B PBind p A B by eauto using E_Refl, Su_Eq.
case : p h => //=; hauto l:on use:Su_Pi_Proj2, Su_Sig_Proj2.
Qed.
Lemma Cumulativity n Γ (a : PTm n) i j :
i <= j ->
Γ a PUniv i ->
Γ a PUniv j.
Proof.
move => h0 h1. apply : T_Conv; eauto.
apply Su_Univ => //=.
sfirstorder use:wff_mutual.
Qed.
Lemma T_Bind' n Γ i j p (A : PTm n) (B : PTm (S n)) :
Γ A PUniv i ->
funcomp (ren_PTm shift) (scons A Γ) B PUniv j ->
Γ PBind p A B PUniv (max i j).
Proof.
move => h0 h1.
have [*] : i <= max i j /\ j <= max i j by lia.
qauto l:on ctrs:Wt use:Cumulativity.
Qed.
Hint Resolve T_Bind' : wt.
Lemma regularity :
(forall n (Γ : fin n -> PTm n), Γ -> forall i, exists j, Γ Γ i PUniv j) /\
(forall n Γ (a A : PTm n), Γ a A -> exists i, Γ A PUniv i) /\
(forall n Γ (a b A : PTm n), Γ a b A -> Γ a A /\ Γ b A /\ exists i, Γ A PUniv i) /\
(forall n Γ (A B : PTm n), Γ A B -> exists i, Γ A PUniv i /\ Γ B PUniv i).
Proof.
apply wt_mutual => //=; eauto with wt.
- move => n Γ A i ihΓ hA _ j.
destruct j as [j|].
have := ihΓ j.
move => [j0 hj].
exists j0. apply : renaming_wt' => //=; eauto using renaming_shift.
reflexivity. econstructor; eauto.
exists i. rewrite {2}/funcomp. simpl.
apply : renaming_wt'; eauto. reflexivity.
econstructor; eauto.
apply : renaming_shift; eauto.
- move => n Γ b a A B hb [i ihb] ha [j iha].
move /Bind_Inv : ihb => [k][h0][h1]h2.
move : substing_wt ha h1; repeat move/[apply].
move => h. exists k.
move : h. by asimpl.
- hauto lq:on use:Bind_Inv.
- move => n Γ a A B ha [i /Bind_Inv[j][h0][h1]h2].
exists j. have : Γ PProj PL a A by qauto use:T_Proj1.
move : substing_wt h1; repeat move/[apply].
by asimpl.
- sfirstorder.
- sfirstorder.
- sfirstorder.
- move => n Γ i p A0 A1 B0 B1 ihΓ hA0
[i0 ihA0] hA [ihA [ihA' [i1 ihA'']]].
move => hB [ihB0 [ihB1 [i2 ihB2]]].
repeat split => //=.
qauto use:T_Bind.
apply T_Bind; eauto.
apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
eauto using T_Univ.
- hauto lq:on ctrs:Wt,Eq.
- move => n Γ i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]]
ha [iha0 [iha1 [i1 iha2]]].
repeat split.
qauto use:T_App.
apply : T_Conv; eauto.
qauto use:T_App.
move /E_Symmetric in ha.
by eauto using bind_inst.
hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt.
- hauto lq:on use:bind_inst db:wt.
- hauto lq:on use:Bind_Inv db:wt.
- move => n Γ i a b A B hS _ hab [iha][ihb][j]ihs.
repeat split => //=; eauto with wt.
apply : T_Conv; eauto with wt.
move /E_Symmetric /E_Proj1 in hab.
eauto using bind_inst.
move /T_Proj1 in iha.
hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
- hauto lq:on ctrs:Wt.
- hauto q:on use:substing_wt db:wt.
- hauto l:on use:bind_inst db:wt.
- move => n Γ b A B i ihΓ hP _ hb [i0 ihb].
repeat split => //=; eauto with wt.
have {}hb : funcomp (ren_PTm shift) (scons A Γ) ren_PTm shift b ren_PTm shift (PBind PPi A B)
by hauto lq:on use:weakening_wt, Bind_Inv.
apply : T_Abs; eauto.
apply : T_App'; eauto; rewrite-/ren_PTm.
by asimpl.
apply T_Var. sfirstorder use:wff_mutual.
- hauto lq:on ctrs:Wt.
- move => n Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
have ? : Γ by sfirstorder use:wff_mutual.
exists (max i j).
have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia.
qauto l:on use:T_Conv, Su_Univ.
- move => n Γ i j *. exists (S (max i j)).
have [? ?] : S i <= S (Nat.max i j) /\ S j <= S (Nat.max i j) by lia.
hauto lq:on ctrs:Wt,LEq.
- move => n Γ A0 A1 B0 B1 i ihΓ hA0 _ hA1 [i0][ih0]ih1 hB[j0][ihB0]ihB1.
exists (max i0 j0).
split; eauto with wt.
apply T_Bind'; eauto.
sfirstorder use:ctx_eq_subst_one.
- move => n Γ A0 A1 B0 B1 i ihΓ hA1 _ hA0 [i0][ihA0]ihA1 hB[i1][ihB0]ihB1.
exists (max i0 i1). repeat split; eauto with wt.
apply T_Bind'; eauto.
sfirstorder use:ctx_eq_subst_one.
- sfirstorder.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1.
move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1.
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
exists (max i0 i1).
split.
+ apply Cumulativity with (i := i0); eauto.
have : Γ a0 A0 by eauto using T_Conv.
move : substing_wt ih0';repeat move/[apply]. by asimpl.
+ apply Cumulativity with (i := i1); eauto.
move : substing_wt ih1' iha1;repeat move/[apply]. by asimpl.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1.
move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1.
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
exists (max i0 i1).
split.
+ apply Cumulativity with (i := i0); eauto.
move : substing_wt iha0 ih0';repeat move/[apply]. by asimpl.
+ apply Cumulativity with (i := i1); eauto.
have : Γ a1 A1 by eauto using T_Conv.
move : substing_wt ih1';repeat move/[apply]. by asimpl.
Qed.
Lemma Var_Inv n Γ (i : fin n) A :
Γ VarPTm i A ->
Γ /\ Γ Γ i A.
Proof.
move E : (VarPTm i) => u hu.
move : i E.
elim : n Γ u A / hu=>//=.
- move => n Γ i i0 [?]. subst.
repeat split => //=.
have h : Γ VarPTm i Γ i by eauto using T_Var.
eapply regularity in h.
move : h => [i0]?.
apply : Su_Eq. apply E_Refl; eassumption.
- sfirstorder use:Su_Transitive.
Qed.
Lemma renaming_su' : forall n m Δ Γ (ξ : fin n -> fin m) (A B : PTm n) u U ,
u = ren_PTm ξ A ->
U = ren_PTm ξ B ->
Γ A B ->
Δ -> renaming_ok Δ Γ ξ ->
Δ u U.
Proof. move => > -> ->. hauto l:on use:renaming. Qed.
Lemma weakening_su : forall n Γ (A0 A1 B : PTm n) i,
Γ B PUniv i ->
Γ A0 A1 ->
funcomp (ren_PTm shift) (scons B Γ) ren_PTm shift A0 ren_PTm shift A1.
Proof.
move => n Γ A0 A1 B i hB hlt.
apply : renaming_su'; eauto.
apply : Wff_Cons'; eauto.
apply : renaming_shift; eauto.
Qed.
Lemma regularity_sub0 : forall n Γ (A B : PTm n), Γ A B -> exists i, Γ A PUniv i.
Proof. hauto lq:on use:regularity. Qed.
Lemma Su_Pi_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 :
Γ PBind PPi A0 B0 PBind PPi A1 B1 ->
funcomp (ren_PTm shift) (scons A1 Γ) B0 B1.
Proof.
move => h.
have /Su_Pi_Proj1 h1 := h.
have /regularity_sub0 [i h2] := h1.
move /weakening_su : (h) h2. move => /[apply].
move => h2.
apply : Su_Pi_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
apply E_Refl. apply T_Var' with (i := var_zero); eauto.
sfirstorder use:wff_mutual.
by asimpl.
by asimpl.
Qed.
Lemma Su_Sig_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 :
Γ PBind PSig A0 B0 PBind PSig A1 B1 ->
funcomp (ren_PTm shift) (scons A0 Γ) B0 B1.
Proof.
move => h.
have /Su_Sig_Proj1 h1 := h.
have /regularity_sub0 [i h2] := h1.
move /weakening_su : (h) h2. move => /[apply].
move => h2.
apply : Su_Sig_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
apply E_Refl. apply T_Var' with (i := var_zero); eauto.
sfirstorder use:wff_mutual.
by asimpl.
by asimpl.
Qed.

210
theories/typing.v Normal file
View file

@ -0,0 +1,210 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
Reserved Notation "⊢ Γ" (at level 70).
Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
| T_Var n Γ (i : fin n) :
Γ ->
Γ VarPTm i Γ i
| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
Γ A PUniv i ->
funcomp (ren_PTm shift) (scons A Γ) B PUniv i ->
Γ PBind p A B PUniv i
| T_Abs n Γ (a : PTm (S n)) A B i :
Γ PBind PPi A B (PUniv i) ->
funcomp (ren_PTm shift) (scons A Γ) a B ->
Γ PAbs a PBind PPi A B
| T_App n Γ (b a : PTm n) A B :
Γ b PBind PPi A B ->
Γ a A ->
Γ PApp b a subst_PTm (scons a VarPTm) B
| T_Pair n Γ (a b : PTm n) A B i :
Γ PBind PSig A B (PUniv i) ->
Γ a A ->
Γ b subst_PTm (scons a VarPTm) B ->
Γ PPair a b PBind PSig A B
| T_Proj1 n Γ (a : PTm n) A B :
Γ a PBind PSig A B ->
Γ PProj PL a A
| T_Proj2 n Γ (a : PTm n) A B :
Γ a PBind PSig A B ->
Γ PProj PR a subst_PTm (scons (PProj PL a) VarPTm) B
| T_Univ n Γ i :
Γ ->
Γ PUniv i : PTm n PUniv (S i)
| T_Conv n Γ (a : PTm n) A B :
Γ a A ->
Γ A B ->
Γ a B
with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
(* Structural *)
| E_Refl n Γ (a : PTm n) A :
Γ a A ->
Γ a a A
| E_Symmetric n Γ (a b : PTm n) A :
Γ a b A ->
Γ b a A
| E_Transitive n Γ (a b c : PTm n) A :
Γ a b A ->
Γ b c A ->
Γ a c A
(* Congruence *)
| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
Γ ->
Γ A0 PUniv i ->
Γ A0 A1 PUniv i ->
funcomp (ren_PTm shift) (scons A0 Γ) B0 B1 PUniv i ->
Γ PBind p A0 B0 PBind p A1 B1 PUniv i
| E_Abs n Γ (a b : PTm (S n)) A B i :
Γ PBind PPi A B (PUniv i) ->
funcomp (ren_PTm shift) (scons A Γ) a b B ->
Γ PAbs a PAbs b PBind PPi A B
| E_App n Γ i (b0 b1 a0 a1 : PTm n) A B :
Γ PBind PPi A B (PUniv i) ->
Γ b0 b1 PBind PPi A B ->
Γ a0 a1 A ->
Γ PApp b0 a0 PApp b1 a1 subst_PTm (scons a0 VarPTm) B
| E_Pair n Γ (a0 a1 b0 b1 : PTm n) A B i :
Γ PBind PSig A B (PUniv i) ->
Γ a0 a1 A ->
Γ b0 b1 subst_PTm (scons a0 VarPTm) B ->
Γ PPair a0 b0 PPair a1 b1 PBind PSig A B
| E_Proj1 n Γ (a b : PTm n) A B :
Γ a b PBind PSig A B ->
Γ PProj PL a PProj PL b A
| E_Proj2 n Γ i (a b : PTm n) A B :
Γ PBind PSig A B (PUniv i) ->
Γ a b PBind PSig A B ->
Γ PProj PR a PProj PR b subst_PTm (scons (PProj PL a) VarPTm) B
| E_Conv n Γ (a b : PTm n) A B :
Γ a b A ->
Γ A B ->
Γ a b B
(* Beta *)
| E_AppAbs n Γ (a : PTm (S n)) b A B i:
Γ PBind PPi A B PUniv i ->
Γ b A ->
funcomp (ren_PTm shift) (scons A Γ) a B ->
Γ PApp (PAbs a) b subst_PTm (scons b VarPTm) a subst_PTm (scons b VarPTm ) B
| E_ProjPair1 n Γ (a b : PTm n) A B i :
Γ PBind PSig A B (PUniv i) ->
Γ a A ->
Γ b subst_PTm (scons a VarPTm) B ->
Γ PProj PL (PPair a b) a A
| E_ProjPair2 n Γ (a b : PTm n) A B i :
Γ PBind PSig A B (PUniv i) ->
Γ a A ->
Γ b subst_PTm (scons a VarPTm) B ->
Γ PProj PR (PPair a b) b subst_PTm (scons a VarPTm) B
(* Eta *)
| E_AppEta n Γ (b : PTm n) A B i :
Γ ->
Γ PBind PPi A B (PUniv i) ->
Γ b PBind PPi A B ->
Γ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) b PBind PPi A B
| E_PairEta n Γ (a : PTm n) A B i :
Γ PBind PSig A B (PUniv i) ->
Γ a PBind PSig A B ->
Γ a PPair (PProj PL a) (PProj PR a) PBind PSig A B
with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
(* Structural *)
| Su_Transitive n Γ (A B C : PTm n) :
Γ A B ->
Γ B C ->
Γ A C
(* Congruence *)
| Su_Univ n Γ i j :
Γ ->
i <= j ->
Γ PUniv i : PTm n PUniv j
| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i :
Γ ->
Γ A0 PUniv i ->
Γ A1 A0 ->
funcomp (ren_PTm shift) (scons A0 Γ) B0 B1 ->
Γ PBind PPi A0 B0 PBind PPi A1 B1
| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i :
Γ ->
Γ A1 PUniv i ->
Γ A0 A1 ->
funcomp (ren_PTm shift) (scons A1 Γ) B0 B1 ->
Γ PBind PSig A0 B0 PBind PSig A1 B1
(* Injecting from equalities *)
| Su_Eq n Γ (A : PTm n) B i :
Γ A B PUniv i ->
Γ A B
(* Projection axioms *)
| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
Γ PBind PPi A0 B0 PBind PPi A1 B1 ->
Γ A1 A0
| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
Γ PBind PSig A0 B0 PBind PSig A1 B1 ->
Γ A0 A1
| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
Γ PBind PPi A0 B0 PBind PPi A1 B1 ->
Γ a0 a1 A1 ->
Γ subst_PTm (scons a0 VarPTm) B0 subst_PTm (scons a1 VarPTm) B1
| Su_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
Γ PBind PSig A0 B0 PBind PSig A1 B1 ->
Γ a0 a1 A0 ->
Γ subst_PTm (scons a0 VarPTm) B0 subst_PTm (scons a1 VarPTm) B1
with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
| Wff_Nil :
null
| Wff_Cons n Γ (A : PTm n) i :
Γ ->
Γ A PUniv i ->
(* -------------------------------- *)
funcomp (ren_PTm shift) (scons A Γ)
where
"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
Scheme wf_ind := Induction for Wff Sort Prop
with wt_ind := Induction for Wt Sort Prop
with eq_ind := Induction for Eq Sort Prop
with le_ind := Induction for LEq Sort Prop.
Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.
(* Lemma lem : *)
(* (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
(* (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...) /\ *)
(* (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *)
(* (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *)
(* Proof. apply wt_mutual. ... *)