Prove PairEta

theories/admissible.v

@@ -16,6 +16,70 @@ Proof.
   hauto lq:on rew:off inv:Wff use:T_Bind', typing.T_Abs.
 Qed.
 
+
+Lemma App_Inv Γ (b a : PTm) 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 : Γ u U / hu => //=.
+  - 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 Γ (a : PTm) U :
+  Γ ⊢ PAbs a ∈ U ->
+  exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
+Proof.
+  move E : (PAbs a) => u hu.
+  move : a E. elim : Γ u U / hu => //=.
+  - 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 E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
+  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+Proof.
+  move => 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 T_Eta Γ A a B :
+  A :: Γ ⊢ a ∈ B ->
+  A :: Γ ⊢ PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a)) (VarPTm var_zero) ∈ B.
+Proof.
+  move => ha.
+  have hΓ' : ⊢ A :: Γ by sfirstorder use:wff_mutual.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto lq:on inv:Wff.
+  have hΓ : ⊢ Γ by hauto lq:on inv:Wff.
+  eapply T_App' with (B  := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  apply T_Abs. eapply renaming; eauto; cycle 1. apply renaming_up. apply renaming_shift.
+  econstructor; eauto. sauto l:on use:renaming.
+  apply T_Var => //.
+  by constructor.
+Qed.
+
 Lemma E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
   (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
@@ -46,3 +110,155 @@ Proof.
   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.
+
+Lemma E_FunExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PPi A B ->
+  Γ ⊢ b ∈ PBind PPi A B ->
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B.
+Proof.
+  hauto l:on use:regularity, E_FunExt.
+Qed.
+
+Lemma E_PairExt Γ (a b : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B. hauto l:on use:regularity, E_PairExt. Qed.
+
+Lemma renaming_comp Γ Δ Ξ ξ0 ξ1 :
+  renaming_ok Γ Δ ξ0 -> renaming_ok Δ Ξ ξ1 ->
+  renaming_ok Γ Ξ (funcomp ξ0 ξ1).
+  rewrite /renaming_ok => h0 h1 i A.
+  move => {}/h1 {}/h0.
+  by asimpl.
+Qed.
+
+Lemma E_AppEta Γ (b : PTm) A B :
+  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
+Proof.
+  move => h.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
+  have [j [hA hB]] : exists i, Γ ⊢ A ∈ PUniv i /\ A :: Γ ⊢ B ∈ PUniv i by hauto lq:on use:Bind_Inv.
+  have {i} {}hPi : Γ ⊢ PBind PPi A B ∈ PUniv j by sfirstorder use:T_Bind, wff_mutual.
+  have hΓ : ⊢ A :: Γ by hauto lq:on use:Bind_Inv, Wff_Cons'.
+  have hΓ' :  ⊢ ren_PTm shift A :: A :: Γ by sauto lq:on use:renaming, renaming_shift inv:Wff.
+  apply E_FunExt; eauto.
+  apply T_Abs.
+  eapply T_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  change (PBind _ _ _) with (ren_PTm shift (PBind PPi A B)).
+
+  eapply renaming; eauto.
+  apply renaming_shift.
+  constructor => //.
+  by constructor.
+
+  apply : E_Transitive. simpl.
+  apply E_AppAbs' with (i := j)(A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B); eauto.
+  by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  constructor => //.
+  by constructor.
+  asimpl.
+  eapply T_App' with (A := ren_PTm shift (ren_PTm shift A)) (B := ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B)); cycle 2.
+  constructor. econstructor; eauto. sauto lq:on use:renaming, renaming_shift.
+  by constructor. asimpl. substify. by asimpl.
+  have -> : PBind PPi (ren_PTm shift (ren_PTm shift A)) (ren_PTm (upRen_PTm_PTm shift) (ren_PTm (upRen_PTm_PTm shift) B))=  (ren_PTm (funcomp shift shift) (PBind PPi A B)) by asimpl.
+  eapply renaming; eauto. by eauto using renaming_shift, renaming_comp.
+  asimpl. renamify.
+  eapply E_App' with (A := ren_PTm shift A) (B := ren_PTm (upRen_PTm_PTm shift) B). by asimpl; rewrite subst_scons_id.
+  hauto q:on use:renaming, renaming_shift.
+  sauto lq:on use:renaming, renaming_shift, E_Refl.
+  constructor. constructor=>//. constructor.
+Qed.
+
+Lemma Proj1_Inv Γ (a : PTm ) 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 : Γ u U / hu => //=.
+  - 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 Γ (a : PTm) 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 : Γ u U / hu => //=.
+  - 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 Γ (a b : PTm ) 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 : Γ u U / hu => //=.
+  - 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_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => 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 E_ProjPair2 : forall (a b : PTm) Γ (A : PTm),
+    Γ ⊢ PProj PR (PPair a b) ∈ A -> Γ ⊢ PProj PR (PPair a b) ≡ b ∈ A.
+Proof.
+  move => a b Γ A. move /Proj2_Inv.
+  move => [A0][B0][ha]h.
+  have hr := ha.
+  move /Pair_Inv : ha => [A1][B1][ha][hb]hU.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity.
+  have /E_Symmetric : Γ ⊢ (PProj PL (PPair a b)) ≡ a ∈ A1 by eauto using  E_ProjPair1 with wt.
+  move /Su_Sig_Proj2 : hU. repeat move/[apply]. move => hB.
+  apply : E_Conv; eauto.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair2; eauto.
+Qed.
+
+
+Lemma E_PairEta Γ a A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PPair (PProj PL a) (PProj PR a) ≡ a ∈ PBind PSig A B.
+Proof.
+  move => h.
+  have [i hSig] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto use:regularity.
+  apply E_PairExt => //.
+  eapply T_Pair; eauto with wt.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto with wt.
+  apply E_ProjPair2.
+  apply : T_Proj2; eauto with wt.
+Qed.

theories/algorithmic.v

@@ -586,7 +586,8 @@ Proof.
     have [h2 h3] : Γ ⊢ A2 ≲ A0 /\ Γ ⊢ A2 ≲ A1 by hauto l:on use:Su_Pi_Proj1.
     apply E_Conv with (A := PBind PPi A2 B2); cycle 1.
     eauto using E_Symmetric, Su_Eq.
-    apply : E_Abs; eauto. hauto l:on use:regularity.
+    apply : E_Abs; eauto.
+
     apply iha.
     move /Su_Pi_Proj2_Var in hp0.
     apply : T_Conv; eauto.
@@ -607,13 +608,12 @@ Proof.
     have /regularity_sub0 [i' hPi0] := hPi.
     have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi A2 B2.
     apply : E_AppEta; eauto.
-    hauto l:on use:regularity.
     apply T_Conv with (A := A);eauto.
     eauto using Su_Eq.
     move => ?.
     suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi A2 B2
       by eauto using E_Transitive.
-    apply : E_Abs; eauto. hauto l:on use:regularity.
+    apply : E_Abs; eauto.
     apply iha.
     move /Su_Pi_Proj2_Var in hPi'.
     apply : T_Conv; eauto.
@@ -665,7 +665,7 @@ Proof.
     have hA02 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Sig_Proj1.
     have hu'  : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
     move => [:ih0'].
-    apply : E_Transitive; last (apply E_Symmetric; apply : E_PairEta).
+    apply : E_Transitive; last (apply : E_PairEta).
     apply : E_Pair; eauto. hauto l:on use:regularity.
     abstract : ih0'.
     apply ih0. apply : T_Conv; eauto.
@@ -678,7 +678,6 @@ Proof.
     move /E_Symmetric in ih0'.
     move /regularity_sub0 in hA'.
     hauto l:on use:bind_inst.
-    hauto l:on use:regularity.
     eassumption.
   (* Same as before *)
   - move {hAppL}.

theories/logrel.v

@@ -619,10 +619,6 @@ Proof.
   split; apply : InterpUniv_cumulative; eauto.
 Qed.
 
-(* Semantic context wellformedness *)
-Definition SemWff Γ := forall (i : nat) A, lookup i Γ A -> exists j, Γ ⊨ A ∈ PUniv j.
-Notation "⊨ Γ" := (SemWff Γ) (at level 70).
-
 Lemma ρ_ok_id Γ :
   ρ_ok Γ VarPTm.
 Proof.
@@ -763,6 +759,34 @@ Proof.
   move : weakening_Sem h0 h1; repeat move/[apply]. done.
 Qed.
 
+Reserved Notation "⊨ Γ"  (at level 70).
+
+Inductive SemWff : list PTm -> Prop :=
+| SemWff_nil :
+  ⊨ nil
+| SemWff_cons Γ A i :
+  ⊨ Γ ->
+  Γ ⊨ A ∈ PUniv i ->
+  (* -------------- *)
+  ⊨ (cons A Γ)
+where "⊨ Γ" := (SemWff Γ).
+
+(* Semantic context wellformedness *)
+Lemma SemWff_lookup Γ :
+  ⊨ Γ ->
+  forall (i : nat) A, lookup i Γ A -> exists j, Γ ⊨ A ∈ PUniv j.
+Proof.
+  move => h. elim : Γ / h.
+  - by inversion 1.
+  - move => Γ A i hΓ ihΓ hA  j B.
+    elim /lookup_inv => //=_.
+    + move => ? ? ? [*]. subst.
+      eauto using weakening_Sem_Univ.
+    + move => i0 Γ0 A0 B0 hl ? [*]. subst.
+      move : ihΓ hl => /[apply]. move => [j hA0].
+      eauto using weakening_Sem_Univ.
+Qed.
+
 Lemma SemWt_SN Γ (a : PTm) A :
   Γ ⊨ a ∈ A ->
   SN a /\ SN A.
@@ -784,25 +808,6 @@ Lemma SemLEq_SN_Sub Γ (a b : PTm) :
   SN a /\ SN b /\ Sub.R a b.
 Proof. hauto l:on use:SemLEq_SemWt, SemWt_SN. Qed.
 
-(* Structural laws for Semantic context wellformedness *)
-Lemma SemWff_nil : SemWff nil.
-Proof. hfcrush inv:lookup. Qed.
-
-Lemma SemWff_cons Γ (A : PTm) i :
-    ⊨ Γ ->
-    Γ ⊨ A ∈ PUniv i ->
-    (* -------------- *)
-    ⊨ (cons A Γ).
-Proof.
-  move => h h0.
-  move => j A0.  elim/lookup_inv => //=_.
-  - hauto q:on use:weakening_Sem.
-  - move => i0 Γ0 A1 B + ? [*]. subst.
-    move : h => /[apply]. move => [k hk].
-    exists k. change (PUniv k) with (ren_PTm shift (PUniv k)).
-    eauto using weakening_Sem.
-Qed.
-
 (* Semantic typing rules *)
 Lemma ST_Var' Γ (i : nat) A j :
   lookup i Γ A ->
@@ -819,7 +824,7 @@ Lemma ST_Var Γ (i : nat) A :
   ⊨ Γ ->
   lookup i Γ A ->
   Γ ⊨ VarPTm i ∈ A.
-Proof. hauto l:on use:ST_Var' unfold:SemWff. Qed.
+Proof. hauto l:on use:ST_Var', SemWff_lookup. Qed.
 
 Lemma InterpUniv_Bind_nopf p i (A : PTm) B PA :
   ⟦ A ⟧ i ↘ PA ->
@@ -1516,6 +1521,36 @@ Proof.
   rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
 Qed.
 
+Lemma SE_PairExt Γ (a b : PTm) A B i :
+  Γ ⊨ PBind PSig A B ∈ PUniv i ->
+  Γ ⊨ a ∈ PBind PSig A B ->
+  Γ ⊨ b ∈ PBind PSig A B ->
+  Γ ⊨ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊨ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊨ a ≡ b ∈ PBind PSig A B.
+Proof.
+  move => h0 ha hb h1 h2.
+  suff h : Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B /\
+           Γ ⊨ PPair (PProj PL b) (PProj PR b) ≡ b ∈ PBind PSig A B /\
+           Γ ⊨ PPair (PProj PL a) (PProj PR a) ≡ PPair (PProj PL b) (PProj PR b) ∈ PBind PSig A B
+    by decompose [and] h; eauto using SE_Transitive, SE_Symmetric.
+  eauto 20 using SE_PairEta, SE_Symmetric, SE_Pair.
+Qed.
+
+Lemma SE_FunExt Γ (a b : PTm) A B i :
+  Γ ⊨ PBind PPi A B ∈ PUniv i ->
+  Γ ⊨ a ∈ PBind PPi A B ->
+  Γ ⊨ b ∈ PBind PPi A B ->
+  A :: Γ ⊨ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊨ a ≡ b ∈ PBind PPi A B.
+Proof.
+  move => hpi ha hb he.
+  move : SE_Abs (hpi) he. repeat move/[apply]. move => he.
+  have /SE_Symmetric : Γ ⊨ PAbs (PApp (ren_PTm shift a) (VarPTm var_zero)) ≡ a ∈ PBind PPi A B by eauto using SE_AppEta.
+  have : Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B by eauto using SE_AppEta.
+  eauto using SE_Transitive.
+Qed.
+
 Lemma SE_Nat Γ (a b : PTm) :
   Γ ⊨ a ≡ b ∈ PNat ->
   Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
@@ -1666,4 +1701,4 @@ Qed.
 
 #[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv
   SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2
-  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem.
+  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong SE_PairExt SE_FunExt : sem.

theories/preservation.v

@@ -1,80 +1,9 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing structural fp_red admissible.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 Require Import Coq.Logic.FunctionalExtensionality.
 
-Lemma App_Inv Γ (b a : PTm) 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 : Γ u U / hu => //=.
-  - 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 Γ (a : PTm) U :
-  Γ ⊢ PAbs a ∈ U ->
-  exists A B, (cons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
-Proof.
-  move E : (PAbs a) => u hu.
-  move : a E. elim : Γ u U / hu => //=.
-  - 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 Γ (a : PTm ) 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 : Γ u U / hu => //=.
-  - 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 Γ (a : PTm) 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 : Γ u U / hu => //=.
-  - 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 Γ (a b : PTm ) 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 : Γ u U / hu => //=.
-  - 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 Ind_Inv Γ P (a : PTm) b c U :
   Γ ⊢ PInd P a b c ∈ U ->
@@ -93,36 +22,58 @@ Proof.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-Lemma E_AppAbs : forall (a : PTm) (b : PTm) Γ (A : PTm),
+Lemma E_Abs Γ a b A B :
-  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+  A :: Γ ⊢ a ≡ b ∈ B ->
+  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B.
 Proof.
-  move => 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.
+  have [i hA] : exists i, Γ ⊢ A ∈ PUniv i by hauto l:on use:wff_mutual inv:Wff.
-  apply : E_AppAbs; eauto.
+  have [j hB] : exists j, A :: Γ ⊢ B ∈ PUniv j by hauto l:on use:regularity.
-  eauto using T_Conv.
+  have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
+  have hΓ' : ⊢ A::Γ by eauto with wt.
+  set k := max i j.
+  have [? ?] : i <= k /\ j <= k by lia.
+  have {}hA : Γ ⊢ A ∈ PUniv k by hauto l:on use:T_Conv, Su_Univ.
+  have {}hB : A :: Γ ⊢ B ∈ PUniv k by hauto lq:on use:T_Conv, Su_Univ.
+  have hPi : Γ ⊢ PBind PPi A B ∈ PUniv k by eauto with wt.
+  apply : E_FunExt; eauto with wt.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  hauto lq:on rew:off use:regularity, T_Abs.
+  apply : E_Transitive => /=. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  apply /E_Symmetric /E_Transitive. apply E_AppAbs.
+  hauto lq:on use:T_Eta, regularity.
+  asimpl. rewrite !subst_scons_id. by apply E_Symmetric.
 Qed.
 
-Lemma E_ProjPair1 : forall (a b : PTm) Γ (A : PTm),
+Lemma E_Pair Γ a0 b0 a1 b1 A B i :
-    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+  Γ ⊢ 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.
 Proof.
-  move => a b Γ A.
+  move => hSig ha hb.
-  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  have [ha0 ha1] : Γ ⊢ a0 ∈ A /\ Γ ⊢ a1 ∈ A by hauto l:on use:regularity.
-  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [hb0 hb1] : Γ ⊢ b0 ∈ subst_PTm (scons a0 VarPTm) B /\
-  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+                     Γ ⊢ b1 ∈ subst_PTm (scons a0 VarPTm) B by hauto l:on use:regularity.
-  move /Su_Sig_Proj1 in hS.
+  have hp : Γ ⊢ PPair a0 b0 ∈ PBind PSig A B by eauto with wt.
-  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  have hp' : Γ ⊢ PPair a1 b1 ∈ PBind PSig A B. econstructor; eauto with wt; [idtac].
-  apply : E_Conv; eauto.
+  apply : T_Conv; eauto. apply : Su_Sig_Proj2; by eauto using Su_Eq, E_Refl.
-  apply : E_ProjPair1; eauto.
+  have ea : Γ ⊢ PProj PL (PPair a0 b0) ≡ a0 ∈ A by eauto with wt.
+  have : Γ ⊢ PProj PR (PPair a0 b0) ≡ b0 ∈ subst_PTm (scons a0 VarPTm) B by eauto with wt.
+  have : Γ ⊢ PProj PL (PPair a1 b1) ≡ a1 ∈ A by eauto using E_ProjPair1 with wt.
+  have : Γ ⊢ PProj PR (PPair a1 b1) ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B.
+  apply : E_Conv; eauto using E_ProjPair2 with wt.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. apply E_ProjPair1. by eauto with wt.
+  by eauto using E_Symmetric.
+  move => *.
+  apply : E_PairExt; eauto using E_Symmetric, E_Transitive.
+  apply : E_Conv. by eauto using E_Symmetric, E_Transitive.
+  apply : Su_Sig_Proj2. apply /Su_Eq /E_Refl. eassumption.
+  apply : E_Transitive. by eauto. apply /E_Symmetric /E_Transitive.
+  by eauto using E_ProjPair1.
+  eauto.
 Qed.
 
 Lemma Suc_Inv Γ (a : PTm) A :
@@ -159,7 +110,7 @@ Proof.
         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.
+      move => ?. apply : E_Conv; eauto. apply : typing.E_ProjPair2; eauto.
   - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
   - move => P a b c Γ A.
     move /Ind_Inv.

theories/soundness.v

@@ -7,7 +7,7 @@ Theorem fundamental_theorem :
   (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
   (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
   (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
-  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
+  apply wt_mutual; eauto with sem.
   Unshelve. all : exact 0.
 Qed.
 

theories/structural.v

@@ -137,12 +137,12 @@ Lemma E_ProjPair2' Γ (a b : PTm) A B i U :
   Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U.
 Proof. move => ->. apply E_ProjPair2. Qed.
 
-Lemma E_AppEta' Γ (b : PTm ) A B i u :
+(* Lemma E_AppEta' Γ (b : PTm ) A B i u : *)
-  u = (PApp (ren_PTm shift b) (VarPTm var_zero)) ->
+(*   u = (PApp (ren_PTm shift b) (VarPTm var_zero)) -> *)
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+(*   Γ ⊢ PBind PPi A B ∈ (PUniv i) -> *)
-  Γ ⊢ b ∈ PBind PPi A B ->
+(*   Γ ⊢ b ∈ PBind PPi A B -> *)
-  Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B.
+(*   Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B. *)
-Proof. qauto l:on use:wff_mutual, E_AppEta. Qed.
+(* Proof. qauto l:on use:wff_mutual, E_AppEta. Qed. *)
 
 Lemma Su_Pi_Proj2' Γ (a0 a1 A0 A1 : PTm ) B0 B1 U T :
   U = subst_PTm (scons a0 VarPTm) B0 ->
@@ -222,17 +222,7 @@ Proof.
   - hauto lq:on ctrs:Wt,LEq.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
-  - move => Γ a b A B i hPi ihPi ha iha Δ ξ 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 => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ξ hΔ hξ.
-    apply : E_Pair; eauto.
-    move : ihb hΔ hξ. repeat move/[apply].
-    by asimpl.
   - move => *. apply : E_Proj2'; eauto. by asimpl.
   - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
     move => Δ ξ hΔ hξ [:hP' hren].
@@ -302,9 +292,12 @@ Proof.
     move /(_ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
     move /(_ ltac:(by eauto using renaming_up)).
     by asimpl.
-  - move => *.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ.
-    apply : E_AppEta'; eauto. by asimpl.
+    apply : E_FunExt; eauto. move : ihe1. asimpl. apply.
-  - qauto l:on use:E_PairEta.
+    hfcrush use:Bind_Inv.
+    by apply renaming_up.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ.
+    apply : E_PairExt; eauto. move : ihR. asimpl. by apply.
   - hauto lq:on ctrs:LEq.
   - qauto l:on ctrs:LEq.
   - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
@@ -447,17 +440,7 @@ Proof.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on ctrs:Eq.
   - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
-  - move => Γ a b A B i hPi ihPi ha iha Δ ρ 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 => Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb Δ ρ 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.
   - move => Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
@@ -524,9 +507,14 @@ Proof.
     move /(_ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
     move /(_ ltac:(sauto l:on use:morphing_up)).
     asimpl. substify. by asimpl.
-  - move => *.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb he0 ihe1 Δ ξ hΔ hξ.
-    apply : E_AppEta'; eauto. by asimpl.
+    move  : ihPi (hΔ) (hξ); repeat move/[apply]. move /[dup] /Bind_Inv => ihPi ?.
-  - qauto l:on use:E_PairEta.
+    decompose [and ex] ihPi.
+    apply : E_FunExt; eauto. move : ihe1. asimpl. apply.
+    by eauto with wt.
+    by eauto using morphing_up with wt.
+  - move => Γ a b A B i hPi ihPi ha iha hb ihb hL ihL hR ihR Δ ξ hΔ hξ.
+    apply : E_PairExt; eauto. move : ihR. asimpl. by apply.
   - hauto lq:on ctrs:LEq.
   - qauto l:on ctrs:LEq.
   - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
@@ -667,7 +655,6 @@ Proof.
     sfirstorder.
     apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
     hauto lq:on.
-  - 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.
@@ -677,7 +664,6 @@ Proof.
     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 => Γ i a b A B hS _ hab [iha][ihb][j]ihs.
     repeat split => //=; eauto with wt.
@@ -726,15 +712,6 @@ Proof.
     subst Ξ.
     move : morphing_wt hc; repeat move/[apply]. asimpl. by apply.
     sauto lq:on use:substing_wt.
-  - move => Γ b A B i hP _ hb [i0 ihb].
-    repeat split => //=; eauto with wt.
-    have {}hb : (cons 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. asimpl. by rewrite subst_scons_id.
-    apply T_Var. sfirstorder use:wff_mutual.
-    apply here.
-  - hauto lq:on ctrs:Wt.
   - move => Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
     have ? : ⊢ Γ by sfirstorder use:wff_mutual.
     exists (max i j).

theories/typing.v

@@ -89,23 +89,12 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
   (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
 
-| E_Abs Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  (cons A Γ) ⊢ a ≡ b ∈ B ->
-  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
-
 | E_App Γ i (b0 b1 a0 a1 : PTm) 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 Γ (a0 a1 b0 b1 : PTm) 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 Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
@@ -164,16 +153,20 @@ with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
   (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
   Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
 
-(* Eta *)
+| E_FunExt Γ (a b : PTm) A B i :
-| E_AppEta Γ (b : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  Γ ⊢ a ∈ PBind PPi A B ->
   Γ ⊢ b ∈ PBind PPi A B ->
-  Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
+  A :: Γ ⊢ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B ->
+  Γ ⊢ a ≡ b ∈ PBind PPi A B
 
-| E_PairEta Γ (a : PTm ) A B i :
+| E_PairExt Γ (a b : PTm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ PBind PSig A B ∈ PUniv i ->
   Γ ⊢ a ∈ PBind PSig A B ->
-  Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
+  Γ ⊢ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B
 
 with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
@@ -242,10 +235,3 @@ Scheme wf_ind := Induction for Wff 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. ... *)