Compare commits

..

1 commit

Author SHA1 Message Date
a27c41c5d1 Add lemmas that bad forms are impossible 2025-01-29 12:19:45 -05:00
12 changed files with 506 additions and 6873 deletions

View file

@ -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)

View file

@ -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

View file

@ -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.

View file

@ -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 : 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.

File diff suppressed because it is too large Load diff

View file

@ -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].
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

File diff suppressed because it is too large Load diff

View file

@ -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.

View file

@ -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.

View file

@ -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 _ 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.

View file

@ -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. ... *)