Replace term reducibility in the logical relation by the diagonal of reducible term conversion

_CoqProject

@@ -31,6 +31,8 @@ theories/LogicalRelation/Weakening.v
 theories/LogicalRelation/Universe.v
 theories/LogicalRelation/Neutral.v
 theories/LogicalRelation/Transitivity.v
+theories/LogicalRelation/InstKripke.v
+theories/LogicalRelation/EqRedRight.v
 theories/LogicalRelation/Reduction.v
 theories/LogicalRelation/NormalRed.v
 theories/LogicalRelation/Application.v

theories/Consequences.v

@@ -56,20 +56,20 @@ Section NatCanonicityInduction.
   Qed.
 
   Lemma nat_red_empty_ind :
-    (forall t, [ε ||-Nat t : tNat | red_nat_empty] ->
+    (forall t u, [ε ||-Nat t ≅ u : tNat | red_nat_empty] ->
     ∑ n : nat, [ε |- t ≅ n : tNat]) ×
-    (forall t, NatProp red_nat_empty t -> ∑ n : nat, [ε |- t ≅ n : tNat]).
+    (forall t u, NatPropEq red_nat_empty t u -> ∑ n : nat, [ε |- t ≅ n : tNat]).
   Proof.
-    apply NatRedInduction.
-    - intros * [? []] ? _ [n] ; refold.
+    apply NatRedEqInduction.
+    - intros * [? []] ? ? _ [n] ; refold.
       exists n.
       now etransitivity.
     - exists 0 ; cbn.
       now repeat constructor.
-    - intros ? _ [n].
+    - intros ? ? _ [n].
       exists (S n) ; simpl.
       now econstructor.
-    - intros ? [? [? _ _]].
+    - intros ? ? [? ? []].
       exfalso.
       now eapply no_neutral_empty_ctx.
   Qed.
@@ -80,7 +80,7 @@ Section NatCanonicityInduction.
     intros Ht.
     assert [LRNat_ one red_nat_empty | ε ||- t : tNat] as ?%nat_red_empty_ind.
     {
-      apply Fundamental in Ht as [?? Vt%reducibleTm].
+      apply Fundamental in Ht as [?? Vt%reducibleTmEq].
       irrelevance.
     }
     now assumption.

theories/DeclarativeSubst.v

@@ -7,7 +7,7 @@ From LogRel Require Import LogicalRelation Validity Fundamental.
 From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Transitivity.
 From LogRel.Substitution Require Import Properties Irrelevance.
 
-(** Currently, this is obtained as a consequence of the fundamental lemma. 
+(** Currently, this is obtained as a consequence of the fundamental lemma.
 However, it could be alternatively proven much earlier, by a direct induction. *)
 
 Set Printing Primitive Projection Parameters.
@@ -44,20 +44,14 @@ Proof.
     unshelve eapply transEq.
     4: now apply Vconv.
     2-3: unshelve eapply VB ; tea.
-    all: irrValid.
+    eapply urefl; now eapply irrelevanceSubstEq.
   - intros * Ht * HΔ Hσ.
     unshelve eapply Fundamental_subst_conv in Hσ as [].
     1,3: boundary.
-    apply Fundamental in Ht as [VΓ VA Vt Vu Vtu] ; cbn in *.
+    apply Fundamental in Ht as [VΓ VA Vtu] ; cbn in *.
     unshelve eapply escapeEqTerm.
     2: now unshelve eapply VA ; tea ; irrValid.
-    cbn.
-    eapply transEqTerm.
-    + cbn.
-      unshelve eapply Vtu.
-    + cbn.
-      eapply Vu.
-      all: irrValid.
+    cbn. unshelve eapply Vtu.
 Qed.
 
 
@@ -149,16 +143,16 @@ Section MoreSubst.
 
   Theorem typing_substmap1 Γ T :
   (forall (t : term), [Γ ,, T |- t : T⟨↑⟩] ->
-    forall (A : term), [Γ,, T |- A] -> 
+    forall (A : term), [Γ,, T |- A] ->
       [Γ,, T |- A[t]⇑]) ×
   (forall (t : term), [Γ ,, T |- t : T⟨↑⟩] ->
-    forall (A u : term), [Γ,, T |- u : A] -> 
+    forall (A u : term), [Γ,, T |- u : A] ->
       [Γ,, T |- u[t]⇑ : A[t]⇑]) ×
   (forall (t t' : term), [Γ ,, T |- t ≅ t' : T⟨↑⟩] ->
     forall (A B : term), [Γ,, T |- A ≅ B] ->
       [Γ,, T |- A[t]⇑ ≅ B[t']⇑]) ×
   (forall (t t' : term), [Γ ,, T |- t ≅ t' : T⟨↑⟩] ->
-    forall (A u v : term), [Γ,, T |- u ≅ v : A] -> 
+    forall (A u v : term), [Γ,, T |- u ≅ v : A] ->
       [Γ,, T |- u[t]⇑ ≅ v[t']⇑ : A[t]⇑]).
   Proof.
     repeat match goal with |- _ × _ => split end.