Add semantic rules for function beta and eta

theories/logrel.v

@@ -755,6 +755,13 @@ Proof.
   asimpl. hauto lq:on.
 Qed.
 
+Lemma ST_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 ST_App. Qed.
+
 Lemma ST_Pair n Γ (a b : PTm n) A B i :
   Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊨ a ∈ A ->
@@ -1010,6 +1017,48 @@ Proof.
   apply SemWt_SemEq; eauto using DJoin.AbsCong, ST_Abs.
 Qed.
 
+Lemma SBind_inv1 n Γ i p (A : PTm n) B :
+  Γ ⊨ PBind p A B ∈ PUniv i ->
+  Γ ⊨ A ∈ PUniv i.
+  move /SemWt_Univ => h. apply SemWt_Univ.
+  hauto lq:on rew:off  use:InterpUniv_Bind_inv.
+Qed.
+
+Lemma SE_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)) ∈ PBind PPi A B.
+Proof.
+  move => hΓ h0 h1. apply : ST_Abs; eauto.
+  have hA : Γ ⊨ A ∈ PUniv i by eauto using SBind_inv1.
+  eapply ST_App' with (A := ren_PTm shift A)(B:= ren_PTm (upRen_PTm_PTm shift) B). by asimpl.
+  2 : {
+    apply ST_Var.
+    eauto using SemWff_cons.
+  }
+  change (PBind PPi (ren_PTm shift A) (ren_PTm (upRen_PTm_PTm shift) B)) with
+    (ren_PTm shift (PBind PPi A B)).
+  apply : weakening_Sem; eauto.
+Qed.
+
+Lemma SE_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.
+Proof.
+  move => h h0 h1. apply SemWt_SemEq; eauto using ST_App, ST_Abs.
+  move => ρ hρ.
+  have {}/h0 := hρ.
+  move => [k][PA][hPA]hb.
+  move : ρ_ok_cons hPA hb (hρ); repeat move/[apply].
+  move => {}/h1.
+  by asimpl.
+  apply DJoin.FromRRed0.
+  apply RRed.AppAbs.
+Qed.
+
 Lemma SE_Conv' n Γ (a b : PTm n) A B i :
   Γ ⊨ a ≡ b ∈ A ->
   Γ ⊨ B ∈ PUniv i ->
@@ -1094,13 +1143,6 @@ Proof.
   apply : ST_Conv_E; eauto using ST_App, DJoin.cong, DJoin.symmetric, SBind_inst.
 Qed.
 
-Lemma SBind_inv1 n Γ i p (A : PTm n) B :
-  Γ ⊨ PBind p A B ∈ PUniv i ->
-  Γ ⊨ A ∈ PUniv i.
-  move /SemWt_Univ => h. apply SemWt_Univ.
-  hauto lq:on rew:off  use:InterpUniv_Bind_inv.
-Qed.
-
 Lemma SSu_Eq n Γ (A B : PTm n) i :
   Γ ⊨ A ≡ B ∈ PUniv i ->
   Γ ⊨ A ≲ B.

theories/structural.v

@@ -24,6 +24,71 @@ Proof.
   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 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 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 /\ Γ ⊢ A ∈ PUniv i). *)
+(* Proof. *)
+(*   apply wt_mutual => //=. *)
+(*   - admit. *)
+(*   - admit. *)
+
+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_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. hauto lq:on use:E_Bind, wff_mutual. 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 Δ Γ ξ ->
@@ -40,6 +105,14 @@ Proof.
   - 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.
-    apply iha; last by apply renaming_up.
-    econstructor; eauto.
-    by apply renaming_up.
+    move : ihP(hΔ) (hξ); repeat move/[apply]. move/Pi_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.
+  - move => n Γ i p A0 A1 B0 B1 hΓ _ hA ihA hB ihB m Δ ξ hΔ hξ.
+    apply E_Bind'; eauto.
+    apply ihB; last by hauto l:on use:renaming_up.

theories/typing.v

@@ -9,10 +9,10 @@ Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
   ⊢ Γ ->
   Γ ⊢ VarPTm i ∈ Γ i
 
-| T_Bind n Γ i j p (A : PTm n) (B : PTm (S n)) :
+| T_Bind n Γ i 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)
+  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) ->
@@ -61,11 +61,12 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
   Γ ⊢ b ≡ c ∈ A ->
   Γ ⊢ a ≡ c ∈ A
 
-| E_Bind n Γ i j p (A0 A1 : PTm n) B0 B1 :
+| 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 j ->
-  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv (max i j)
+  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) ->