Merge pull request #66 from ppedrot/move-logrel-intro

Move proofs of reducibility to theories/LogicalRelation/Introductions.

_CoqProject

@@ -37,16 +37,18 @@ theories/LogicalRelation/ShapeView.v
 theories/LogicalRelation/Reflexivity.v
 theories/LogicalRelation/Irrelevance.v
 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/LogicalRelation/SimpleArr.v
-theories/LogicalRelation/Id.v
+theories/LogicalRelation/Introductions/Universe.v
+theories/LogicalRelation/Introductions/Poly.v
+theories/LogicalRelation/Introductions/Pi.v
+theories/LogicalRelation/Introductions/Application.v
+theories/LogicalRelation/Introductions/SimpleArr.v
+theories/LogicalRelation/Introductions/Id.v
 
 theories/Validity/Validity.v
 theories/Validity/Irrelevance.v
@@ -85,4 +87,4 @@ theories/Decidability/UntypedSoundness.v
 theories/Decidability/UntypedCompleteness.v
 theories/Decidability.v
 
-theories/Decidability/Execution.v
+theories/Decidability/Execution.v

theories/LogicalRelation/InstKripke.v

@@ -1,7 +1,7 @@
 (** * LogRel.LogicalRelation.InstKripke: combinators to instantiate Kripke-style quantifications *)
 From Coq Require Import CRelationClasses.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction  Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight.
+From LogRel.LogicalRelation Require Import Induction  Escape Reflexivity Neutral Weakening Irrelevance Reduction Transitivity NormalRed EqRedRight.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.

theories/LogicalRelation/Introductions/Pi.v

@@ -0,0 +1,47 @@
+From Coq Require Import ssrbool.
+From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
+From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
+
+Set Universe Polymorphism.
+
+Section PolyRedPi.
+  Context `{GenericTypingProperties}.
+
+  Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π<l> tProd A B].
+  Proof.
+    econstructor; tea; pose proof (polyRedId PAB) as []; escape.
+    + eapply redtywf_refl; gen_typing.
+    + unshelve eapply escapeEq; tea; eapply reflLRTyEq.
+    + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq.
+  Defined.
+
+  Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-<l> tProd A B] := LRPi' (LRPiPoly0 PAB).
+
+  Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB].
+  Proof.
+    econstructor; cbn; tea.
+    + eapply redtywf_refl; gen_typing.
+    + pose proof (polyRedEqId PAB Peq) as []; now escape.
+    + pose proof (polyRedEqId PAB Peq) as []; escape.
+      eapply convty_prod; tea.
+      eapply escape; now apply (polyRedId PAB).
+  Qed.
+
+  Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-<l> tProd A B ≅ tProd A' B' | LRPiPoly PAB].
+  Proof.
+    now eapply LRPiPolyEq0.
+  Qed.
+
+  Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||-<l> tProd A B]):
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-<l> tProd A B ≅ tProd A' B' | RAB].
+  Proof.
+    intros; irrelevanceRefl; now eapply LRPiPolyEq.
+  Qed.
+
+End PolyRedPi.

theories/LogicalRelation/Introductions/Poly.v

@@ -0,0 +1,134 @@
+From Coq Require Import ssrbool.
+From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
+From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Transitivity EqRedRight InstKripke.
+
+Set Universe Polymorphism.
+
+Lemma subst_wk_id_tail Γ P t : P[t .: @wk_id Γ >> tRel] = P[t..].
+Proof. setoid_rewrite id_ren; now bsimpl. Qed.
+
+Set Printing Primitive Projection Parameters.
+
+Section PolyValidity.
+
+  Context `{GenericTypingProperties}.
+
+  Lemma mkPolyRed {Γ l A B} (wfΓ : [|-Γ])
+    (RA : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> A⟨ρ⟩])
+    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ] -> [Δ ||-<l> B[a .: ρ >> tRel]])
+    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ]),
+      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
+    PolyRed Γ l A B.
+  Proof.
+    assert [Γ |- A] by (eapply escape; now eapply instKripke).
+    unshelve econstructor; tea.
+    unshelve epose proof (h := RB _ (tRel 0) (tRel 0) (@wk1 Γ A) _ _).
+    + gen_typing.
+    + eapply var0; tea; now rewrite wk1_ren_on.
+    + escape. now rewrite <- eq_id_subst_scons in Esch.
+  Qed.
+
+  Lemma mkPolyRed' {Γ l A B} (RA : [Γ ||-<l> A])
+    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA] -> [Δ ||-<l> B[a .: ρ >> tRel]])
+    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA]),
+      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
+    PolyRed Γ l A B.
+  Proof.
+    unshelve eapply mkPolyRed; tea.
+    escape; gen_typing.
+  Qed.
+
+
+  Lemma polyCodSubstRed {Γ l F G} (RF : [Γ ||-<l> F]) :
+    PolyRed Γ l F G -> forall t u, [Γ ||-<l> t ≅ u : _ | RF] -> [Γ ||-<l> G[t..]].
+  Proof.
+    intros PFG ???.
+    assert (wfΓ : [|- Γ]) by (escape ; gen_typing).
+    erewrite <- subst_wk_id_tail.
+    eapply (PolyRed.posRed PFG wk_id wfΓ ).
+    irrelevance.
+  Qed.
+
+  Lemma polyCodSubstExtRed {Γ l F G} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
+    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
+    [Γ ||-<l> G[t..] ≅ G[u..]| RG t u Rt].
+  Proof.
+    intros. assert (wfΓ : [|- Γ]) by (escape; gen_typing).
+    irrelevance0; erewrite <- subst_wk_id_tail; [reflexivity|].
+    unshelve eapply (PolyRed.posExt PFG wk_id wfΓ); irrelevance.
+  Qed.
+
+  Lemma polyRedId {Γ l F G} : PolyRed Γ l F G -> [Γ ||-<l> F] × [Γ ,, F ||-<l> G].
+  Proof.
+    intros PFG; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    split; [exact (instKripke wfΓ (PolyRed.shpRed PFG))| exact (instKripkeSubst wfΓ (PolyRed.posRed PFG))].
+  Qed.
+
+  Lemma polyRedEqId {Γ l F F' G G'} (PFG : PolyRed Γ l F G) (RFG := polyRedId PFG) :
+    PolyRedEq PFG F' G' -> [Γ ||-<l> F ≅ F' | fst RFG] × [Γ ,, F ||-<l> G ≅ G' | snd RFG].
+  Proof.
+    intros PFGeq; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    split.
+    - pose (instKripkeEq wfΓ (PolyRedEq.shpRed PFGeq)); irrelevance.
+    - unshelve epose proof (instKripkeSubstEq wfΓ  _).
+      7: intros; eapply LRTransEq; [|unshelve eapply (PolyRedEq.posRed PFGeq _ _ (urefl hab))];
+        try (unshelve eapply (PolyRed.posExt PFG); tea).
+      irrelevance.
+  Qed.
+
+  Lemma polyRedEqCodSubstExt {Γ l F F' G G'} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
+    PolyRedEq PFG F' G' ->
+    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
+    [Γ ||-<l> G[t..] ≅ G'[u..]| RG t u Rt].
+  Proof.
+    intros Peq *; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    unshelve epose proof (h := posRedExt Peq wk_id wfΓ _).
+    3: irrelevance.
+    rewrite subst_wk_id_tail in h; irrelevance.
+  Qed.
+
+  Lemma polyRedSubst {Γ l A B t} (PAB : PolyRed Γ l A B)
+    (Rt : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    (Rtext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] ≅ t[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    : PolyRed Γ l A B[t]⇑.
+  Proof.
+    destruct PAB; opector; tea.
+    + intros; rewrite liftSubst_scons_eq.
+      unshelve eapply posRed; [..| eapply Rt]; tea ; now irrelevanceRefl.
+    + unshelve epose proof (posRed _ t t (@wk1 Γ A) _ _).
+      - escape; gen_typing.
+      - replace t with t[tRel 0 .: @wk1 Γ A >> tRel].
+        2:{ bsimpl; rewrite scons_eta'; now asimpl. }
+        eapply Rt.
+        eapply var0; tea; now rewrite wk1_ren_on.
+      - escape.
+        replace (B[_]) with B[t .: @wk1 Γ A >> tRel]; tea.
+        now setoid_rewrite wk1_ren.
+    + intros; irrelevance0; rewrite liftSubst_scons_eq;[reflexivity|].
+      unshelve eapply posExt; tea; eapply Rt + eapply Rtext; cbn; irrelevanceRefl.
+      1: now eapply lrefl.
+      1: now eapply urefl.
+      eassumption.
+  Qed.
+
+  Lemma polyRedEqSubst {Γ l A B t u} (PAB : PolyRed Γ l A B)
+    (Rtu : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] ≅ u[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    (PABt : PolyRed Γ l A B[t]⇑)
+    : PolyRedEq PABt A B[u]⇑.
+  Proof.
+    constructor.
+    - intros; eapply reflLRTyEq.
+    - intros; irrelevance0; rewrite liftSubst_scons_eq; [reflexivity|].
+      unshelve eapply PolyRed.posExt; cycle 1; tea.
+      eapply Rtu; irrelevanceRefl; now eapply lrefl.
+  Qed.
+
+End PolyValidity.

theories/LogicalRelation/SimpleArr.v → theories/LogicalRelation/Introductions/SimpleArr.v

@@ -1,5 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Application.
+From LogRel.LogicalRelation.Introductions Require Import Poly Pi.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.
@@ -24,14 +25,8 @@ Section SimpleArrow.
 
   Lemma ArrRedTy0 {Γ l A B} : [Γ ||-<l> A] -> [Γ ||-<l> B] -> [Γ ||-Π<l> arr A B].
   Proof.
-    intros RA RB; escape.
-    unshelve econstructor; [exact A| exact B⟨↑⟩|..]; tea.
-    - eapply redtywf_refl.
-      now eapply wft_simple_arr.
-    - now unshelve eapply escapeEq, reflLRTyEq.
-    - eapply convty_simple_arr; tea.
-      all: now unshelve eapply escapeEq, reflLRTyEq.
-    - now eapply shiftPolyRed.
+    intros RA RB.
+    now apply LRPiPoly0, shiftPolyRed.
   Qed.
 
   Lemma ArrRedTy {Γ l A B} : [Γ ||-<l> A] -> [Γ ||-<l> B] -> [Γ ||-<l> arr A B].

theories/TypingProperties/LogRelConsequences.v

@@ -4,6 +4,7 @@ From LogRel.TypingProperties Require Import PropertiesDefinition DeclarativeProp
 
 From LogRel Require Import LogicalRelation Fundamental.
 From LogRel.LogicalRelation Require Import Escape Irrelevance Transitivity Neutral Induction NormalRed.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
 From LogRel.Validity Require Import Validity Escape Poly Irrelevance.
 
 (** ** Stability of typing under substitution *)

theories/Validity/Introductions/Pi.v

@@ -1,53 +1,11 @@
 From Coq Require Import ssrbool.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Poly Pi.
 From LogRel.Validity Require Import Validity Irrelevance Properties SingleSubst Reflexivity Universe Poly.
 
 Set Universe Polymorphism.
 
-
-Section PolyRedPi.
-  Context `{GenericTypingProperties}.
-
-  Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π<l> tProd A B].
-  Proof.
-    econstructor; tea; pose proof (polyRedId PAB) as []; escape.
-    + eapply redtywf_refl; gen_typing.
-    + unshelve eapply escapeEq; tea; eapply reflLRTyEq.
-    + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq.
-  Defined.
-
-  Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-<l> tProd A B] := LRPi' (LRPiPoly0 PAB).
-
-  Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB].
-  Proof.
-    econstructor; cbn; tea.
-    + eapply redtywf_refl; gen_typing.
-    + pose proof (polyRedEqId PAB Peq) as []; now escape.
-    + pose proof (polyRedEqId PAB Peq) as []; escape.
-      eapply convty_prod; tea.
-      eapply escape; now apply (polyRedId PAB).
-  Qed.
-
-  Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-<l> tProd A B ≅ tProd A' B' | LRPiPoly PAB].
-  Proof.
-    now eapply LRPiPolyEq0.
-  Qed.
-
-  Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||-<l> tProd A B]):
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-<l> tProd A B ≅ tProd A' B' | RAB].
-  Proof.
-    intros; irrelevanceRefl; now eapply LRPiPolyEq.
-  Qed.
-
-End PolyRedPi.
-
-
 Section PiTyValidity.
 
   Context `{GenericTypingProperties}.