Merge pull request #56 from CoqHott/strenghten-negative-inversion-con…

…version Saturate negative conversion rules with inversions
CoqHott · Sep 27, 2023 · e6330aa · e6330aa
2 parents 3aa8b6a + 1740d3d
commit e6330aa
Show file tree

Hide file tree

Showing 9 changed files with 312 additions and 51 deletions.
diff --git a/theories/GenericTyping.v b/theories/GenericTyping.v
@@ -125,11 +125,24 @@ Section RedDefinitions.
   }.
 
   Inductive isWfFun (Γ : context) (A B : term) : term -> Set :=
-    LamWfFun : forall A' t : term, [Γ |- A ≅ A'] -> isWfFun Γ A B (tLambda A' t)
+    LamWfFun : forall A' t : term,
+      [Γ |- A'] -> [Γ |- A ≅ A'] -> [Γ,, A |- t : B] -> [Γ,, A' |- t : B] -> isWfFun Γ A B (tLambda A' t)
   | NeWfFun : forall f : term, [Γ |- f ~ f : tProd A B] -> isWfFun Γ A B f.
 
   Inductive isWfPair (Γ : context) (A B : term) : term -> Set :=
-    PairWfPair : forall A' B' a b : term, [Γ |- A ≅ A'] -> isWfPair Γ A B (tPair A' B' a b)
+    PairWfPair : forall A' B' a b : term,
+      [Γ |- A'] -> [Γ |- A ≅ A'] ->
+      [Γ,, A' |- B] ->
+      [Γ,, A' |- B'] ->
+      [Γ,, A |- B'] ->
+      [Γ,, A |- B ≅ B'] ->
+      [Γ,, A' |- B ≅ B'] ->
+      [Γ |- a : A] ->
+      [Γ |- B[a..]] ->
+      [Γ |- B'[a..]] ->
+      [Γ |- B[a..] ≅ B'[a..]] ->
+      [Γ |- b : B[a..]] ->
+      isWfPair Γ A B (tPair A' B' a b)
   | NeWfPair : forall n : term, [Γ |- n ~ n : tSig A B] -> isWfPair Γ A B n.
 
 End RedDefinitions.
@@ -963,7 +976,11 @@ Section GenericConsequences.
     2: eapply convty_simple_arr; cycle 1; tea.
     eapply convtm_eta; tea.
     { renToWk; apply wft_wk; [apply wfc_cons|]; tea. }
-    2,4: constructor; first [now apply lrefl|tea].
+    2:{ constructor; first [now eapply lrefl|now apply ty_var0|tea]. }
+    3:{ constructor; first [now eapply lrefl|now apply ty_var0|tea].
+        eapply ty_conv; [now apply ty_var0|].
+        do 2 rewrite <- (@wk1_ren_on Γ A'); apply convty_wk; [|now symmetry].
+        now apply wfc_cons. }
     1,2: eapply ty_id; tea; now symmetry.
     assert [|- Γ,, A] by gen_typing.
     assert [Γ,, A |-[ ta ] A⟨@wk1 Γ A⟩] by now eapply wft_wk. 
@@ -1101,9 +1118,22 @@ Section GenericConsequences.
     [Γ |- comp A g f ≅ comp A g' f' : arr A C].
   Proof.
     intros.
+    assert (Hup : forall X Y h, [Γ |- h : arr X Y] -> [Γ,, A |- h⟨↑⟩ : arr X⟨↑⟩ Y⟨↑⟩]).
+    { intros; rewrite <- arr_ren1, <- !(wk1_ren_on Γ A).
+      apply (ty_wk (@wk1 Γ A)); [|now rewrite wk1_ren_on].
+      now apply wfc_cons. }
     eapply convtm_eta; tea.
     { renToWk; apply wft_wk; [apply wfc_cons|]; tea. }
-    2,4: now constructor.
+    2:{ assert [Γ,, A |-[ ta ] tApp g⟨↑⟩ (tApp f⟨↑⟩ (tRel 0)) : C⟨↑⟩].
+        { eapply (ty_simple_app (A := B⟨↑⟩)); first [now apply wft_wk1|now apply Hup|idtac].
+          eapply (ty_simple_app (A := A⟨↑⟩)); first [now apply wft_wk1|now apply Hup|idtac].
+          now apply ty_var0. }
+        constructor; tea. }
+    3:{ assert [Γ,, A |-[ ta ] tApp g'⟨↑⟩ (tApp f'⟨↑⟩ (tRel 0)) : C⟨↑⟩].
+        { eapply (ty_simple_app (A := B⟨↑⟩)); first [now apply wft_wk1|now apply Hup|idtac].
+          eapply (ty_simple_app (A := A⟨↑⟩)); first [now apply wft_wk1|now apply Hup|idtac].
+          now apply ty_var0. }
+        constructor; tea. }
     1,2: eapply ty_comp.
     4,5,9,10: tea.
     all: tea.
@@ -1134,19 +1164,21 @@ Section GenericConsequences.
     [Γ,, A' |- t' : B'] ->
     [Γ |- A ≅ A'] ->
     [Γ,, A |- B ≅ B'] ->
+    [Γ,, A' |- B ≅ B'] ->
     [Γ,, A |- t ≅ t' : B] ->
     [Γ |- tLambda A t ≅ tLambda A' t' : tProd A B].
   Proof.
     intros.
     assert [|- Γ,, A] by gen_typing.
     apply convtm_eta ; tea.
     - gen_typing.
-    - constructor; now eapply lrefl.
+    - constructor; first[now eapply lrefl|tea].
     - eapply ty_conv.
       1: eapply ty_lam ; tea.
       symmetry.
       now eapply convty_prod.
-    - now constructor.
+    - constructor; tea.
+      now eapply ty_conv.
     - eapply @convtm_exp with (t' := t) (u' := t'); tea.
       3: now eapply lrefl.
       2: eapply redtm_conv ; cbn ; [eapply redtm_meta_conv |..] ; [eapply redtm_beta |..].

diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v
@@ -400,6 +400,18 @@ Definition PiRedTyEq `{ta : tag}
 Module PiRedTyEq := ParamRedTyEq.
 Notation "[ Γ ||-Π A ≅ B | ΠA ]" := (PiRedTyEq (Γ:=Γ) (A:=A) ΠA B).
 
+Inductive isLRFun `{ta : tag} `{WfContext ta}
+  `{WfType ta} `{ConvType ta} `{RedType ta} `{Typing ta} `{ConvTerm ta} `{ConvNeuConv ta}
+  {Γ : context} {A : term} (ΠA : PiRedTy Γ A) : term -> Type :=
+| LamLRFun : forall A' t : term,
+  (forall {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]) (domRed:= ΠA.(PolyRedPack.shpRed) ρ h),
+      [domRed | Δ ||- (PiRedTy.dom ΠA)⟨ρ⟩ ≅ A'⟨ρ⟩]) ->
+  (forall {Δ a} (ρ : Δ ≤ Γ) (h : [ |- Δ ])
+    (ha : [ ΠA.(PolyRedPack.shpRed) ρ h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ]),
+      [ΠA.(PolyRedPack.posRed) ρ h ha | Δ ||- t[a .: (ρ >> tRel)] : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]) ->
+  isLRFun ΠA (tLambda A' t)
+| NeLRFun : forall f : term, [Γ |- f ~ f : tProd (PiRedTy.dom ΠA) (PiRedTy.cod ΠA)] -> isLRFun ΠA f.
+
 Module PiRedTm.
 
   Record PiRedTm `{ta : tag} `{WfContext ta}
@@ -409,7 +421,7 @@ Module PiRedTm.
   : Type := {
     nf : term;
     red : [ Γ |- t :⤳*: nf : tProd ΠA.(PiRedTy.dom) ΠA.(PiRedTy.cod) ];
-    isfun : isWfFun Γ ΠA.(PiRedTy.dom) ΠA.(PiRedTy.cod) nf;
+    isfun : isLRFun ΠA nf;
     refl : [ Γ |- nf ≅ nf : tProd ΠA.(PiRedTy.dom) ΠA.(PiRedTy.cod) ];
     app {Δ a} (ρ : Δ ≤ Γ) (h : [ |- Δ ])
       (ha : [ ΠA.(PolyRedPack.shpRed) ρ h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ])
@@ -466,6 +478,26 @@ Definition SigRedTyEq `{ta : tag}
   {Γ : context} {A : term} (ΠA : SigRedTy Γ A) (B : term) :=
   ParamRedTyEq (T:=tSig) Γ A B ΠA.
 
+Module SigRedTy := ParamRedTyPack.
+
+Inductive isLRPair `{ta : tag} `{WfContext ta}
+  `{WfType ta} `{ConvType ta} `{RedType ta} `{Typing ta} `{ConvTerm ta} `{ConvNeuConv ta}
+  {Γ : context} {A : term} (ΣA : SigRedTy Γ A) : term -> Type :=
+| PairLRpair : forall (A' B' a b : term)
+  (rdom : forall {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]),
+      [ΣA.(PolyRedPack.shpRed) ρ h | Δ ||- (SigRedTy.dom ΣA)⟨ρ⟩ ≅ A'⟨ρ⟩])
+  (rcod : forall {Δ a} (ρ : Δ ≤ Γ) (h : [ |- Δ ])
+    (ha : [ ΣA.(PolyRedPack.shpRed) ρ h | Δ ||- a : ΣA.(PiRedTy.dom)⟨ρ⟩ ]),
+      [ΣA.(PolyRedPack.posRed) ρ h ha | Δ ||- (SigRedTy.cod ΣA)[a .: (ρ >> tRel)] ≅ B'[a .: (ρ >> tRel)]])
+  (rfst : forall {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]),
+      [ΣA.(PolyRedPack.shpRed) ρ h | Δ ||- a⟨ρ⟩ : (SigRedTy.dom ΣA)⟨ρ⟩])
+  (rsnd : forall {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]),
+      [ΣA.(PolyRedPack.posRed) ρ h (rfst ρ h) | Δ ||- b⟨ρ⟩ : (SigRedTy.cod ΣA)[a⟨ρ⟩ .: (ρ >> tRel)] ]),
+
+  isLRPair ΣA (tPair A' B' a b)
+
+| NeLRPair : forall p : term, [Γ |- p ~ p : tSig (SigRedTy.dom ΣA) (SigRedTy.cod ΣA)] -> isLRPair ΣA p.
+
 Module SigRedTm.
 
   Record SigRedTm `{ta : tag} `{WfContext ta}
@@ -475,7 +507,7 @@ Module SigRedTm.
   : Type := {
     nf : term;
     red : [ Γ |- t :⤳*: nf : ΣA.(outTy) ];
-    isfun : isWfPair Γ ΣA.(PiRedTy.dom) ΣA.(PiRedTy.cod) nf;
+    ispair : isLRPair ΣA nf;
     refl : [ Γ |- nf ≅ nf : ΣA.(outTy) ];
     fstRed {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]) :
       [ΣA.(PolyRedPack.shpRed) ρ h | Δ ||- tFst nf⟨ρ⟩ : ΣA.(ParamRedTyPack.dom)⟨ρ⟩] ;

diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v
@@ -73,7 +73,6 @@ Proof.
   - eapply symLRPack; eapply eqv.(eqvPos).
 Qed.
 
-
 (** *** Lemmas for product types *)
 
 (** A difficulty is that we need to show the equivalence right away, rather than only an implication,
@@ -108,7 +107,10 @@ Proof.
   intros []; cbn in *; econstructor; tea.
   - now eapply redtmwf_conv.
   - destruct isfun as [A₀ t₀|n Hn].
-    + constructor; transitivity (PiRedTy.dom ΠA); [now symmetry|tea].
+    + constructor.
+      * intros; now eapply eqv.(eqvShp).
+      * intros; unshelve eapply eqv.(eqvPos); [|eauto].
+        now apply eqv.(eqvShp).
     + constructor; now eapply convneu_conv.
   - eapply (convtm_conv refl).
     apply eqPi.
@@ -180,8 +182,13 @@ Proof.
   intros []; cbn in *; unshelve econstructor; tea.
   - intros; unshelve eapply eqv.(eqvShp); now auto.
   - now eapply redtmwf_conv.
-  - destruct isfun as [A₀ t₀|n Hn].
-    + constructor; transitivity (PiRedTy.dom ΣA); [now symmetry|tea].
+  - destruct ispair as [A₀ B₀ a b|n Hn].
+    + unshelve econstructor.
+      * intros; now unshelve eapply eqv.(eqvShp).
+      * intros; now eapply eqv.(eqvShp).
+      * intros; unshelve eapply eqv.(eqvPos); [|now eauto].
+        now unshelve eapply eqv.(eqvShp).
+      * intros; now eapply eqv.(eqvPos).
     + constructor; now eapply convneu_conv.
   - now eapply convtm_conv.
   - intros; unshelve eapply eqv.(eqvPos); now auto.

diff --git a/theories/LogicalRelation/Reduction.v b/theories/LogicalRelation/Reduction.v
@@ -238,7 +238,7 @@ Proof.
     eapply redtmwf_refl; gen_typing.
   - intros ???????? [? red] red' ?.
     unshelve erewrite (redtmwf_det _ _ red' red); tea.
-    1: now eapply isFun_whnf, isWfFun_isFun.
+    1: eapply isFun_whnf; destruct isfun; constructor; tea; now eapply convneu_whne.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ?????? Rt red' ?; inversion Rt; subst.
@@ -254,7 +254,7 @@ Proof.
     Unshelve. 2: tea.
   - intros ???????? [? red] red' ?.
     unshelve erewrite (redtmwf_det _ _ red' red); tea.
-    1: now eapply isPair_whnf, isWfPair_isPair.
+    1: eapply isPair_whnf; destruct ispair; constructor; tea; now eapply convneu_whne.
     econstructor; tea.
     eapply redtmwf_refl; gen_typing.
   - intros ???????? [? red] red' ?.

diff --git a/theories/LogicalRelation/SimpleArr.v b/theories/LogicalRelation/SimpleArr.v
@@ -140,7 +140,11 @@ Section SimpleArrow.
     econstructor; cbn.
     - eapply redtmwf_refl.
       now eapply ty_id.
-    - now constructor.
+    - constructor.
+      + intros; cbn; apply reflLRTyEq.
+      + intros; cbn.
+        irrelevance0; [|apply ha].
+        cbn; bsimpl; now rewrite rinstInst'_term.
     - eapply convtm_id; tea.
       eapply wfc_wft; now escape.
     - intros; cbn; irrelevance0.
@@ -277,8 +281,12 @@ Section SimpleArrow.
     econstructor.
     - eapply redtmwf_refl.
       eapply ty_comp; cycle 2; tea.
-    - constructor; cbn.
-      unshelve eapply escapeEq, reflLRTyEq; [|tea].
+    - constructor; intros; cbn.
+      + apply reflLRTyEq.
+      + assert (Hrw : forall t, t⟨↑⟩[a .: ρ >> tRel] = t⟨ρ⟩).
+        { intros; bsimpl; symmetry; now apply rinstInst'_term. }
+        do 2 rewrite Hrw; irrelevance0; [symmetry; apply Hrw|].
+        unshelve eapply h; tea.
     - cbn. eapply convtm_comp; cycle 6; tea.
       erewrite <- wk1_ren_on.
       eapply escapeEqTerm.
@@ -302,6 +310,6 @@ Section SimpleArrow.
       + eapply LRTmEqSym.
         unshelve eapply beta; tea.
       + cbn; bsimpl; now rewrite rinstInst'_term.
-  Qed. 
+  Qed.
 
 End SimpleArrow.
diff --git a/theories/LogicalRelation/Transitivity.v b/theories/LogicalRelation/Transitivity.v
@@ -59,9 +59,12 @@ Lemma transEqTermΠ {Γ lA A t u v} {ΠA : [Γ ||-Π<lA> A]}
   [Γ ||-Π u ≅ v : A | ΠA ] ->
   [Γ ||-Π t ≅ v : A | ΠA ].
 Proof.
-  intros [tL] [? tR];
+  intros [tL] [? tR].
+  assert (forall t (red : [Γ ||-Π t : _ | ΠA]), whnf (PiRedTm.nf red)).
+  { intros ? [? ? isfun]; simpl; destruct isfun; constructor; tea.
+    now eapply convneu_whne. }
   unshelve epose proof (e := redtmwf_det _ _ (PiRedTm.red redR) (PiRedTm.red redL)); tea.
-  1,2: apply isFun_whnf; eapply isWfFun_isFun, PiRedTm.isfun.
+  1,2: now eauto.
   exists tL tR.
   + etransitivity; tea. now rewrite e.
   + intros. eapply ihcod.
@@ -83,9 +86,12 @@ Lemma transEqTermΣ {Γ lA A t u v} {ΣA : [Γ ||-Σ<lA> A]}
   [Γ ||-Σ u ≅ v : A | ΣA ] ->
   [Γ ||-Σ t ≅ v : A | ΣA ].
 Proof.
-  intros [tL ?? eqfst eqsnd] [? tR ? eqfst' eqsnd'];
+  intros [tL ?? eqfst eqsnd] [? tR ? eqfst' eqsnd'].
+  assert (forall t (red : [Γ ||-Σ t : _ | ΣA]), whnf (SigRedTm.nf red)).
+  { intros ? [? ? ispair]; simpl; destruct ispair; constructor; tea.
+    now eapply convneu_whne. }
   unshelve epose proof (e := redtmwf_det _ _ (SigRedTm.red redR) (SigRedTm.red redL)); tea.
-  1,2: eapply isPair_whnf, isWfPair_isPair; apply SigRedTm.isfun.
+  1,2: now eauto.
   exists tL tR.
   + etransitivity; tea. now rewrite e.
   + intros; eapply ihdom ; [eapply eqfst| rewrite e; eapply eqfst'].

diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v
@@ -174,13 +174,23 @@ Section Weakenings.
       Unshelve. all: tea.
   Qed.
 
-  Lemma isWfFun_ren : forall Γ Δ A B t (ρ : Δ ≤ Γ),
-    [|- Δ] ->
-    isWfFun Γ A B t -> isWfFun Δ A⟨ρ⟩ B⟨upRen_term_term ρ⟩ t⟨ρ⟩.
+  Lemma isLRFun_ren : forall Γ Δ t A l (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (ΠA : [Γ ||-Π< l > A]),
+    isLRFun ΠA t -> isLRFun (wkΠ ρ wfΔ ΠA) t⟨ρ⟩.
   Proof.
-  intros * ? []; constructor; tea.
-  + now apply convty_wk.
-  + change [Δ |- f⟨ρ⟩ ~ f⟨ρ⟩ : (tProd A B)⟨ρ⟩].
+  intros * [A' t' Hdom Ht|]; constructor; tea.
+  + intros Ξ ρ' *; cbn.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    irrelevance0; [apply eq|].
+    rewrite <- eq.
+    now unshelve apply Hdom.
+  + intros Ξ a ρ' wfΞ *; cbn.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    unshelve eassert (Ht0 := Ht Ξ a (ρ' ∘w ρ) wfΞ _).
+    { cbn in ha; irrelevance0; [symmetry; apply eq|tea]. }
+    replace (t'⟨upRen_term_term ρ⟩[a .: ρ' >> tRel]) with (t'[a .: (ρ' ∘w ρ) >> tRel]) by now bsimpl.
+    irrelevance0; [|apply Ht0].
+    now bsimpl.
+  + change [Δ |- f⟨ρ⟩ ~ f⟨ρ⟩ : (tProd (PiRedTy.dom ΠA) (PiRedTy.cod ΠA))⟨ρ⟩].
     now eapply convneu_wk.
   Qed.
 
@@ -193,7 +203,7 @@ Section Weakenings.
     intros [t].
     exists (t⟨ρ⟩); try change (tProd _ _) with (ΠA.(outTy)⟨ρ⟩).
     + now eapply redtmwf_wk.
-    + now apply isWfFun_ren.
+    + now apply isLRFun_ren.
     + now apply convtm_wk.
     + intros ? a ρ' ??.
       replace ((t ⟨ρ⟩)⟨ ρ' ⟩) with (t⟨ρ' ∘w ρ⟩) by now bsimpl.
@@ -213,13 +223,32 @@ Section Weakenings.
     intros []; constructor. all: gen_typing.
   Qed.  
 
-  Lemma isWfPair_ren : forall Γ Δ A B t (ρ : Δ ≤ Γ),
-    [|- Δ] ->
-    isWfPair Γ A B t -> isWfPair Δ A⟨ρ⟩ B⟨upRen_term_term ρ⟩ t⟨ρ⟩.
+  Lemma isLRPair_ren : forall Γ Δ t A l (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (ΣA : [Γ ||-Σ< l > A]),
+    isLRPair ΣA t -> isLRPair (wkΣ ρ wfΔ ΣA) t⟨ρ⟩.
   Proof.
-  intros * ? []; constructor; tea.
-  + now apply convty_wk.
-  + change [Δ |- n⟨ρ⟩ ~ n⟨ρ⟩ : (tSig A B)⟨ρ⟩].
+  intros * [A' B' a b Hdom Hcod Hfst Hsnd|]; unshelve econstructor; tea.
+  + refold; intros Ξ ρ' wfΞ.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    rewrite <- eq; irrelevance0; [|now unshelve apply Hfst].
+    now bsimpl.
+  + intros Ξ ρ' *; cbn.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    irrelevance0; [apply eq|].
+    rewrite <- eq.
+    now unshelve apply Hdom.
+  + intros Ξ a' ρ' wfΞ ha'; cbn.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    unshelve eassert (Hcod0 := Hcod Ξ a' (ρ' ∘w ρ) wfΞ _).
+    { cbn in ha'; irrelevance0; [symmetry; apply eq|tea]. }
+    replace (B'⟨upRen_term_term ρ⟩[a' .: ρ' >> tRel]) with B'[a' .: (ρ' ∘w ρ) >> tRel] by now bsimpl.
+    irrelevance0; [|apply Hcod0].
+    now bsimpl.
+  + refold; intros Ξ ρ' wfΞ.
+    assert (eq : forall t, t⟨ρ' ∘w ρ⟩ = t⟨ρ⟩⟨ρ'⟩) by now bsimpl.
+    rewrite <- eq.
+    irrelevance0; [|now unshelve apply Hsnd].
+    now bsimpl.
+  + change [Δ |- p⟨ρ⟩ ~ p⟨ρ⟩ : (tSig (SigRedTy.dom ΣA) (SigRedTy.cod ΣA))⟨ρ⟩].
     now eapply convneu_wk.
   Qed.
 
@@ -234,7 +263,7 @@ Section Weakenings.
       2: now unshelve eapply fstRed.
       cbn; symmetry; apply wk_comp_ren_on.
     + now eapply redtmwf_wk.
-    + apply isWfPair_ren; assumption.
+    + apply isLRPair_ren; assumption.
     + eapply convtm_wk; eassumption.
     + intros ? ρ' ?;  irrelevance0.
       2: rewrite wk_comp_ren_on; now unshelve eapply sndRed.