Compare commits
1 commit
Author | SHA1 | Date | |
---|---|---|---|
a27c41c5d1 |
12 changed files with 506 additions and 6873 deletions
42
README.org
42
README.org
|
@ -1,42 +0,0 @@
|
|||
* 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)
|
12
syntax.sig
12
syntax.sig
|
@ -1,19 +1,15 @@
|
|||
PTm(VarPTm) : Type
|
||||
PTag : Type
|
||||
BTag : Type
|
||||
Ty : Type
|
||||
|
||||
nat : Type
|
||||
Fun : Ty -> Ty -> Ty
|
||||
Prod : Ty -> Ty -> Ty
|
||||
Void : Ty
|
||||
|
||||
PL : PTag
|
||||
PR : PTag
|
||||
|
||||
PPi : BTag
|
||||
PSig : BTag
|
||||
|
||||
PAbs : (bind PTm in PTm) -> PTm
|
||||
PApp : PTm -> PTm -> PTm
|
||||
PPair : PTm -> PTm -> PTm
|
||||
PProj : PTag -> PTm -> PTm
|
||||
PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
|
||||
PUniv : nat -> PTm
|
||||
PBot : PTm
|
|
@ -5,20 +5,6 @@ Require Import Setoid Morphisms Relation_Definitions.
|
|||
|
||||
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 :=
|
||||
| PL : PTag
|
||||
| PR : PTag.
|
||||
|
@ -38,10 +24,7 @@ Inductive PTm (n_PTm : nat) : Type :=
|
|||
| 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.
|
||||
| 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.
|
||||
|
@ -73,28 +56,6 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0))
|
|||
(ap (fun x => PProj m_PTm t0 x) H1)).
|
||||
Qed.
|
||||
|
||||
Lemma congr_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) :
|
||||
fin (S m) -> fin (S n).
|
||||
Proof.
|
||||
|
@ -115,10 +76,6 @@ 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)
|
||||
| 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
|
||||
end.
|
||||
|
||||
Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
|
||||
|
@ -145,11 +102,6 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
|
|||
| 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
|
||||
end.
|
||||
|
||||
Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
|
||||
|
@ -188,11 +140,6 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
|
|||
(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 =>
|
||||
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.
|
||||
|
||||
Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
|
||||
|
@ -233,12 +180,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
|
|||
(extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
|
||||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
|
||||
| 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.
|
||||
|
||||
Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
|
||||
|
@ -280,12 +221,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
|
|||
(ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
|
||||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
|
||||
| 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.
|
||||
|
||||
Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
|
||||
|
@ -327,13 +262,6 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
|
|||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0)
|
||||
(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.
|
||||
|
||||
Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
|
||||
|
@ -384,13 +312,6 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
|
|||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0)
|
||||
(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.
|
||||
|
||||
Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
|
||||
|
@ -461,13 +382,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
|
|||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0)
|
||||
(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.
|
||||
|
||||
Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
|
||||
|
@ -540,13 +454,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
|
|||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0)
|
||||
(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.
|
||||
|
||||
Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
|
||||
|
@ -659,12 +566,6 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
|
|||
(rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
|
||||
| PProj _ s0 s1 =>
|
||||
congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
|
||||
| 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.
|
||||
|
||||
Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
|
||||
|
@ -736,6 +637,30 @@ 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.
|
||||
|
||||
|
@ -871,12 +796,6 @@ Core.
|
|||
|
||||
Arguments VarPTm {n_PTm}.
|
||||
|
||||
Arguments PBot {n_PTm}.
|
||||
|
||||
Arguments PUniv {n_PTm}.
|
||||
|
||||
Arguments PBind {n_PTm}.
|
||||
|
||||
Arguments PProj {n_PTm}.
|
||||
|
||||
Arguments PPair {n_PTm}.
|
||||
|
@ -885,9 +804,9 @@ Arguments PApp {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.
|
||||
|
||||
|
|
|
@ -1,69 +0,0 @@
|
|||
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 hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
|
||||
move /Wff_Cons_Inv : hΓ => [hΓ][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.
|
File diff suppressed because it is too large
Load diff
|
@ -1,97 +0,0 @@
|
|||
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ξ [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 hξ [?]. 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.
|
3023
theories/fp_red.v
3023
theories/fp_red.v
File diff suppressed because it is too large
Load diff
1335
theories/logrel.v
1335
theories/logrel.v
File diff suppressed because it is too large
Load diff
|
@ -1,179 +0,0 @@
|
|||
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.
|
|
@ -1,15 +0,0 @@
|
|||
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.
|
|
@ -1,676 +0,0 @@
|
|||
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 hΓ _ m Δ ξ hΔ hξ.
|
||||
rewrite hξ.
|
||||
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 Δ ξ hΔ hξ.
|
||||
apply : T_Abs; eauto.
|
||||
move : ihP(hΔ) (hξ); 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 Δ ξ hξ hΔ.
|
||||
eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
|
||||
- move => n Γ a A B ha iha m Δ ξ hΔ hξ. 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 Δ ξ hΔ hξ.
|
||||
move : ihPi (hΔ) (hξ). 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 Δ ξ hΔ hξ.
|
||||
apply : E_Pair; eauto.
|
||||
move : ihb hΔ hξ. 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 Δ ξ hΔ hξ.
|
||||
move : ihP (hξ) (hΔ). 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 Δ ξ hΔ hξ.
|
||||
move : {hP} ihP (hξ) (hΔ). 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 hξ hΔ. repeat move/[apply]. by asimpl.
|
||||
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ.
|
||||
apply : E_ProjPair2'; eauto. by asimpl.
|
||||
move : ihb hξ 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: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Ξ hξ 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Δ hρ.
|
||||
move : ihP (hΔ) (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ρ 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Δ hρ.
|
||||
move : ihPi (hΔ) (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Δ hρ.
|
||||
apply : E_Pair; eauto.
|
||||
move : ihb hΔ 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Δ hρ.
|
||||
move : ihP (hρ) (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Δ hρ.
|
||||
move : {hP} ihP (hρ) (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ρ hΔ. repeat move/[apply]. by asimpl.
|
||||
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ.
|
||||
apply : E_ProjPair2'; eauto. by asimpl.
|
||||
move : ihb hρ 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 Γ hΓ.
|
||||
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 [:hΓ]. apply : morphing_wt; eauto.
|
||||
abstract : hΓ. 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 hΓ 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 hΓ 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 hΓ 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 hΓ *. 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 hΓ 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 hΓ 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 hΓ 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.
|
|
@ -1,210 +0,0 @@
|
|||
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. ... *)
|
Loading…
Add table
Reference in a new issue