From 4fe006f2845d2af28a04c889f5530c31c78283c0 Mon Sep 17 00:00:00 2001 From: Martin Baillon Date: Tue, 21 Jan 2025 19:34:21 +0100 Subject: [PATCH] Add a Dtree for extensionality of codomain for Pis and Sigmas, and extensionality of functions. Through to SimpleArr.v --- theories/LogicalRelation.v | 73 ++- theories/LogicalRelation/Application.v | 28 +- theories/LogicalRelation/Irrelevance.v | 52 +- theories/LogicalRelation/Monotonicity.v | 148 +++++- theories/LogicalRelation/Neutral.v | 39 +- theories/LogicalRelation/NormalRed.v | 42 +- theories/LogicalRelation/Reduction.v | 14 +- theories/LogicalRelation/Reflexivity.v | 12 +- theories/LogicalRelation/SimpleArr.v | 647 ++++++++++++++++++------ theories/LogicalRelation/Transitivity.v | 18 +- theories/LogicalRelation/Weakening.v | 15 +- theories/Monad.v | 152 ++++++ 12 files changed, 998 insertions(+), 242 deletions(-) diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v index dbdd971a..7a817a3f 100644 --- a/theories/LogicalRelation.v +++ b/theories/LogicalRelation.v @@ -292,14 +292,24 @@ Module PolyRedPack. (ha : [ shpRed ρ f Hd | Δ ||- a : shp⟨ρ⟩]< k' >), forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)), LRPack@{i} k'' Δ (pos[a .: (ρ >> tRel)]) ; + posExtTree {Δ a b k'} (ρ : Δ ≤ Γ) : + forall (f : k' ≤ε k) + (Hd : [ |-[ ta ] Δ ]< k' >) + (ha : [ shpRed ρ f Hd | Δ ||- a : shp⟨ρ⟩]< k' >) + (hb : [ shpRed ρ f Hd | Δ ||- b : shp⟨ρ⟩]< k' >) + (heq : [ shpRed ρ f Hd | Δ ||- a ≅ b : shp⟨ρ⟩ ]< k' >), + DTree k' ; posExt {Δ a b k'} (ρ : Δ ≤ Γ) : forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >) (ha : [ shpRed ρ f Hd | Δ ||- a : shp⟨ρ⟩]< k' >) (hb : [ shpRed ρ f Hd | Δ ||- b : shp⟨ρ⟩]< k' >) (heq : [ shpRed ρ f Hd | Δ ||- a ≅ b : shp⟨ρ⟩ ]< k' >), - forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)), - [ (posRed ρ f Hd ha Ho) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ; + forall {k''} + (Hoa : over_tree k' k'' (posTree ρ f Hd ha)) + (Hob : over_tree k' k'' (posTree ρ f Hd hb)) + (Hoeq : over_tree k' k'' (posExtTree ρ f Hd ha hb heq)), + [ (posRed ρ f Hd ha Hoa) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ; }. Arguments PolyRedPack {_ _ _ _}. @@ -439,15 +449,15 @@ Inductive isLRFun `{ta : tag} `{WfContext ta} (funTree : forall {Δ k'} {a} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >) (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >), - DTree k'), - (forall {Δ k'} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >) - (domRed:= ΠA.(PolyRedPack.shpRed) ρ f h), - [domRed | Δ ||- (PiRedTy.dom ΠA)⟨ρ⟩ ≅ A'⟨ρ⟩]< k' >) -> - (forall {Δ k' a} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >) - (ha : [ ΠA.(PolyRedPack.shpRed) ρ f h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >), + DTree k') + (HeqA : forall {Δ k'} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >) + (domRed:= ΠA.(PolyRedPack.shpRed) ρ f h), + [domRed | Δ ||- (PiRedTy.dom ΠA)⟨ρ⟩ ≅ A'⟨ρ⟩]< k' >) + (Hred: forall {Δ k' a} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >) + (ha : [ ΠA.(PolyRedPack.shpRed) ρ f h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >), forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f h ha)) (Ho' : over_tree k' k'' (funTree ρ f h ha)), - [ΠA.(PolyRedPack.posRed) ρ f h ha Ho | Δ ||- t[a .: (ρ >> tRel)] : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' >) -> + [ΠA.(PolyRedPack.posRed) ρ f h ha Ho | Δ ||- t[a .: (ρ >> tRel)] : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' >), isLRFun ΠA (tLambda A' t) | NeLRFun : forall f : term, [Γ |- f ~ f : tProd (PiRedTy.dom ΠA) (PiRedTy.cod ΠA)]< k > -> isLRFun ΠA f. @@ -474,14 +484,23 @@ Module PiRedTm. forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha)) (Ho' : over_tree k' k'' (appTree ρ f Hd ha)), [ ΠA.(PolyRedPack.posRed) ρ f Hd ha Ho | Δ ||- tApp nf⟨ρ⟩ a : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' > ; + eqTree {Δ a b k'} (ρ : Δ ≤ Γ) : + forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >) + (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) + (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) + (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >), + DTree k' ; eq {Δ a b k'} (ρ : Δ ≤ Γ) : - forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >) - (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) - (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) - (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >), - forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha)) - (Ho' : over_tree k' k'' (appTree ρ f Hd ha)), - [ ΠA.(PolyRedPack.posRed) ρ f Hd ha Ho | Δ ||- tApp nf⟨ρ⟩ a ≅ tApp nf⟨ρ⟩ b : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)] ]< k'' > ; + forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >) + (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) + (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >) + (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >), + forall {k''} + (HoPi : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha)) + (Hoa : over_tree k' k'' (appTree ρ f Hd ha)) + (Hob : over_tree k' k'' (appTree ρ f Hd hb)) + (Hoeq : over_tree k' k'' (eqTree ρ f Hd ha hb eq)), + [ ΠA.(PolyRedPack.posRed) ρ f Hd ha HoPi | Δ ||- tApp nf⟨ρ⟩ a ≅ tApp nf⟨ρ⟩ b : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)] ]< k'' > ; }. Arguments PiRedTm {_ _ _ _ _ _ _ _ _}. @@ -1455,15 +1474,25 @@ Section PolyRed. (ha : [ shpRed ρ f Hd | Δ ||- a : shp⟨ρ⟩]< k' >), forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)), [ LogRel@{i j k l} l | Δ ||- pos[a .: (ρ >> tRel)]]< k'' > ; + posExtTree {Δ k' a b} + (ρ : Δ ≤ Γ) (f : k' ≤ε k) + (Hd : [ |- Δ ]< k' >) + (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >) + (hb : [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' >) + (hab : [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' >) : + DTree k' ; posExt {Δ k' a b} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (Hd : [ |- Δ ]< k' >) - (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >) : - [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' > -> - [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' > -> - forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)), - [ (posRed ρ f Hd ha Ho) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ; + (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >) + (hb : [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' >) + (hab : [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' >) : + forall {k''} + (Hoa : over_tree k' k'' (posTree ρ f Hd ha)) + (Hob : over_tree k' k'' (posTree ρ f Hd hb)) + (Hoeq : over_tree k' k'' (posExtTree ρ f Hd ha hb hab)), + [ (posRed ρ f Hd ha Hoa) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ; }. Definition from@{i j k l} {PA : PolyRedPack@{k} k Γ shp pos} @@ -1474,6 +1503,7 @@ Section PolyRed. - econstructor ; unshelve eapply PolyRedPack.shpAd. 4: eassumption. all: eauto. - eapply PolyRedPack.posTree ; eauto. - econstructor. unshelve eapply PolyRedPack.posAd. 8: exact Ho. tea. + - eapply (PolyRedPack.posExtTree PA (a := a) (b := b)) ; eassumption. - now eapply PolyRedPack.shpTy. - now eapply PolyRedPack.posTy. - now eapply PolyRedPack.posExt. @@ -1485,6 +1515,7 @@ Section PolyRed. - now eapply shpRed. - intros ; now eapply posTree. - intros; now eapply posRed. + - intros ; now eapply (posExtTree PA (a := a) (b := b)). - now eapply shpTy. - now eapply posTy. - intros; now eapply posExt. diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Application.v index 2a2c7ac4..15fbab09 100644 --- a/theories/LogicalRelation/Application.v +++ b/theories/LogicalRelation/Application.v @@ -158,7 +158,7 @@ Proof. set (h := invLRΠ _) in hΠ. epose proof (e := redtywf_whnf (PiRedTyPack.red h) whnf_tProd); symmetry in e; injection e; clear e; - destruct h as [?????? [?? domRed ? codRed codExt]] ; clear RΠ Rtt'; + destruct h as [?????? [?? domRed ? codRed codExtTree codExt]] ; clear RΠ Rtt'; intros; cbn in *; subst. assert (wfΓ : [|-Γ]< wl >) by gen_typing. assert [Γ ||- u' : F⟨@wk_id Γ⟩ | domRed _ _ (@wk_id Γ) (idε _) wfΓ]< wl > by irrelevance. @@ -175,18 +175,22 @@ Proof. 1:{ replace G[u..] with G[u .: @wk_id Γ >> tRel] by now bsimpl. unshelve eapply WLRTyEqIrrelevant'. - 5: exists (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X) ; intros wl' f Hover. - 5: irrelevance0 ; [ reflexivity | ]. - 5: unshelve eapply codExt. - 11: eapply LRTmEqSym; irrelevance. - 4-8: tea. + 5:{ unshelve eexists ; [eapply DTree_fusion ; [eapply DTree_fusion | ] | ]. + + exact (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X). + + exact (posTree _ _ u (@wk_id Γ) (idε _) wfΓ X0). + + eapply (codExtTree Γ wl u' u wk_id ((idε) wl) wfΓ) ; eauto. + now eapply LRTmEqSym; irrelevance. + + intros. + irrelevance0 ; [reflexivity | unshelve eapply codExt]. + 9: eapply over_tree_fusion_r, over_tree_fusion_l ; eassumption. + 2: do 2 (eapply over_tree_fusion_l) ; eassumption. + 1: now eapply LRTmEqSym; irrelevance. + eapply over_tree_fusion_r ; exact Hover'. + } 3: now bsimpl. 2: now replace G[u' .: @wk_id Γ >> tRel] with G[u'..] by now bsimpl. } - pose (fez:= (snd (appTerm0 hΠ Rt Ru RGu))). - pose (zef := (snd (appTerm0 hΠ Rt' Ru' RGu'))). unshelve epose proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _). 1: irrelevance. - cbn in *. eapply WtransEqTerm; eapply WtransEqTerm. - unshelve eapply (snd (appTerm0 hΠ Rt Ru RGu)). - unshelve epose proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _). 1: irrelevance. @@ -201,8 +205,10 @@ Proof. 5: unshelve eapply Hyp. 4: now bsimpl. 1,2,5: irrelevance. - 2: eapply over_tree_fusion_l ; exact Hover'. - eapply over_tree_fusion_r ; exact Hover'. + 2: do 2 (eapply over_tree_fusion_l) ; exact Hover'. + + eapply over_tree_fusion_r, over_tree_fusion_l ; exact Hover'. + + eapply over_tree_fusion_l, over_tree_fusion_r ; exact Hover'. + + do 2 (eapply over_tree_fusion_r) ; exact Hover'. - replace (_)⟨_⟩ with (PiRedTm.nf Rt') by now bsimpl. eapply WLRTmEqRedConv; tea. eapply WLRTmEqSym. diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v index a35938e0..243ff4d2 100644 --- a/theories/LogicalRelation/Irrelevance.v +++ b/theories/LogicalRelation/Irrelevance.v @@ -129,6 +129,9 @@ Proof. * eapply (PolyRed.posTree ΠA) ; now eapply eqv.(eqvShp). * eapply eqv.(eqvTree) ; eauto. now eapply eqv.(eqvShp). + eapply appTree ; now eapply eqv.(eqvShp). + - intros ; eapply DTree_fusion. + + eapply (PolyRed.posExtTree ΠA (a := a) (b := b)) ; now eapply eqv.(eqvShp). + + eapply (eqTree _ a b) ; now eapply eqv.(eqvShp). - now eapply redtmwf_conv. - eapply (convtm_conv refl). now apply eqPi. @@ -150,9 +153,9 @@ Proof. + eapply over_tree_fusion_r ; eassumption. - intros; unshelve eapply eqv.(eqvPos), eq. all: try now eapply eqv.(eqvShp). + 3-5: eapply over_tree_fusion_r ; eassumption. + do 2 (eapply over_tree_fusion_l) ; eassumption. + eapply over_tree_fusion_r, over_tree_fusion_l ; eassumption. - + eapply over_tree_fusion_r ; eassumption. Defined. Lemma ΠIrrelevanceTmEq t u : [Γ ||- t ≅ u : A | RA]< wl > -> [Γ ||- t ≅ u : A' | RA']< wl >. @@ -731,22 +734,31 @@ Proof. + intros Δ wl' a ρ f tΔ ra wl'' Hover ; cbn in *. eapply IHpos. eapply over_tree_fusion_l ; eassumption. + + intros. + eapply (PA.(PolyRed.posExtTree) (a := a) (b := b)). + all: pose (shpRed := PA.(PolyRed.shpRed) ρ f Hd). + all: destruct (LRIrrelevantPreds IH _ _ _ _ + (LRAd.adequate shpRed) + (LRAd.adequate (IHshp Δ _ ρ f Hd)) + (reflLRTyEq shpRed)) as [_ irrTmRed irrTmEq]. + * now eapply (snd (irrTmRed a)). + * now eapply (snd (irrTmRed b)). + * now eapply (snd (irrTmEq a b)). + now destruct PA. + now destruct PA. + cbn. intros Δ wl' a b ρ f tΔ ra rb rab wl''. set (p := LRIrrelevantPreds _ _ _ _ _ _ _ _). destruct p as [_ irrTmRed irrTmEq]. pose (ra' := snd (irrTmRed a) ra) ; cbn in *. - intros Hover. - pose (posRed := PA.(PolyRed.posRed) ρ f tΔ ra' (over_tree_fusion_r Hover)). + intros Hoa Hob Hoab. + pose (posRed := PA.(PolyRed.posRed) ρ f tΔ ra' (over_tree_fusion_r Hoa)). destruct (LRIrrelevantPreds IH _ _ _ _ (LRAd.adequate posRed) - (LRAd.adequate (IHpos Δ _ a ρ f tΔ ra' wl'' (over_tree_fusion_l Hover))) + (LRAd.adequate (IHpos Δ _ a ρ f tΔ ra' wl'' (over_tree_fusion_l Hoa))) (reflLRTyEq posRed)) as [irrTyEq _ _]. eapply (fst (irrTyEq (pos[b .: ρ >> tRel]))). - eapply PolyRed.posExt. - 1: exact (snd (irrTmRed b) rb). - exact (snd (irrTmEq a b) rab). + eapply PolyRed.posExt ; [ | eassumption]. + now eapply over_tree_fusion_r. Qed. @@ -1182,6 +1194,15 @@ Proof. intros ?? []; split; [eapply LRTmRedIrrelevant'| eapply LRTmEqIrrelevant']; tea. Qed. +Corollary WLRTmTmEqIrrelevant' lA lA' wl Γ A A' (e : A = A') + (lrA : W[Γ ||-< lA > A]< wl >) (lrA' : W[Γ ||-< lA'> A']< wl >) : + forall t u, + W[Γ ||- t : A | lrA]< wl > × W[Γ ||-< lA > t ≅ u : A | lrA]< wl > -> + W[Γ ||- t : A' | lrA']< wl > × W[Γ ||-< lA' > t ≅ u : A' | lrA']< wl >. +Proof. + intros ?? []; split; [eapply WLRTmRedIrrelevant'| eapply WLRTmEqIrrelevant']; tea. +Qed. + Set Printing Primitive Projection Parameters. Lemma NeNfEqSym {wl Γ k k' A} : [Γ ||-NeNf k ≅ k' : A]< wl > -> [Γ ||-NeNf k' ≅ k : A]< wl >. @@ -1225,15 +1246,22 @@ Proof. 1,2: tea. 2: now symmetry. + intros ; eapply DTree_fusion. - * now eapply eqTree. - * exact (PolyRed.posTree ΠA _ _ _ (SigRedTm.fstRed redL ρ f Hd)). + * eapply DTree_fusion. + -- now eapply eqTree. + -- exact (PolyRed.posTree ΠA _ _ _ (SigRedTm.fstRed redL ρ f Hd)). + * eapply (PolyRed.posExtTree ΠA ρ f Hd). + -- eapply (SigRedTm.fstRed redL ρ f Hd). + -- eapply (SigRedTm.fstRed redR ρ f Hd). + -- now eapply eqFst. + intros; now eapply ihshp. + intros; unshelve eapply ihpos. eapply LRTmEqRedConv. 2: unshelve eapply (eqSnd _ k') ; eauto ; cbn in *. - * now eapply PolyRed.posExt. - * now eapply over_tree_fusion_r. - * now eapply over_tree_fusion_l. + * eapply PolyRed.posExt. + -- eassumption. + -- now eapply over_tree_fusion_r. + * now eapply over_tree_fusion_r, over_tree_fusion_l. + * now do 2 (eapply over_tree_fusion_l). - intros ???? [] ???? [????? hprop]; unshelve econstructor; unfold_id_outTy; cbn in *. 3,4: tea. 1: now symmetry. diff --git a/theories/LogicalRelation/Monotonicity.v b/theories/LogicalRelation/Monotonicity.v index 71b26230..9c25ba27 100644 --- a/theories/LogicalRelation/Monotonicity.v +++ b/theories/LogicalRelation/Monotonicity.v @@ -92,13 +92,15 @@ Defined. + now eapply convty_Ltrans. + now eapply convty_Ltrans. + unshelve econstructor. - 4,5: destruct polyRed ; now eapply wft_Ltrans. + 5,6: destruct polyRed ; now eapply wft_Ltrans. * intros * f' Hd. eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto. * intros ???? f' Hd ha ; cbn in *. eapply (PolyRed.posTree polyRed) ; eauto. * intros ???? f' ??? Hover ; cbn in *. eapply (PolyRed.posRed polyRed) ; eassumption. + * intros ???? f' ????? ; cbn in *. + eapply (PolyRed.posExtTree polyRed (a := a) (b := b)) ; eassumption. * intros ???? f' ????? Hover Hover' ; cbn in *. eapply (PolyRed.posExt polyRed) ; eassumption. - intros ????? wl' f. @@ -120,13 +122,15 @@ Defined. + now eapply convty_Ltrans. + now eapply convty_Ltrans. + unshelve econstructor. - 4,5: destruct polyRed ; now eapply wft_Ltrans. + 5,6: destruct polyRed ; now eapply wft_Ltrans. * intros * f' Hd. - eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eauto. + eapply (PolyRed.shpRed polyRed) ; [eapply wfLCon_le_trans | ] ; eassumption. * intros ???? f' Hd ha ; cbn in *. - eapply (PolyRed.posTree polyRed) ; eauto. + eapply (PolyRed.posTree polyRed) ; eassumption. * intros ???? f' ??? Hover ; cbn in *. eapply (PolyRed.posRed polyRed) ; eassumption. + * intros ???? f' ????? ; cbn in *. + eapply (PolyRed.posExtTree polyRed (a := a)) ; eassumption. * intros ???? f' ????? Hover Hover' ; cbn in *. eapply (PolyRed.posExt polyRed) ; eassumption. - intros ????? ih1 ih2 wl' f. @@ -222,7 +226,15 @@ Proof. exact (IdRedTyEq.rhsRed X). Qed. - Lemma WEq_Ltrans@{h i j k l} {wl Γ wl' A B l} +Lemma Eq_Ltrans'@{h i j k l} {wl Γ wl' A B l} (f : wl' ≤ε wl) lrA lrA' : + [LogRel@{i j k l} l | Γ ||- A ≅ B | lrA]< wl > -> + [LogRel@{i j k l} l | Γ ||- A ≅ B | lrA']< wl' >. +Proof. + intros Heq ; irrelevance0 ; [reflexivity | ]. + now eapply (Eq_Ltrans f). +Qed. + +Lemma WEq_Ltrans@{h i j k l} {wl Γ wl' A B l} (f : wl' ≤ε wl) (lrA : W[Γ ||- A]< wl >) : WLogRelEq@{i j k l} l wl Γ A B lrA -> WLogRelEq@{i j k l} l wl' Γ A B (WLtrans@{h i j k l} f lrA). @@ -235,7 +247,15 @@ Qed. now eapply over_tree_Ltrans. Defined. - + +Lemma WEq_Ltrans'@{h i j k l} {wl Γ wl' A B l} + (f : wl' ≤ε wl) lrA lrA' : + WLogRelEq@{i j k l} l wl Γ A B lrA -> + WLogRelEq@{i j k l} l wl' Γ A B lrA'. +Proof. + intros Heq ; eapply WLRTyEqIrrelevant' ; [reflexivity | ]. + now eapply (WEq_Ltrans f). +Qed. Lemma isLRFun_Ltrans : forall wl wl' Γ t A l (f : wl' ≤ε wl) (ΠA : [Γ ||-Π< l > A]< wl >) (ΠA' : [Γ ||-Π< l > A]< wl' >), @@ -437,7 +457,7 @@ Lemma ΠTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ [Γ ||-Π t : A | ΠA ]< wl > -> [Γ ||-Π t : A | ΠA' ]< wl' >. Proof. intros t []. - unshelve econstructor ; [ | | eapply redtmwf_Ltrans ; eauto |..]. + unshelve econstructor ; [ | | | eapply redtmwf_Ltrans ; eauto |..]. 1: exact nf. 1:{ cbn in * ; intros. eapply DTree_fusion. @@ -454,10 +474,26 @@ Proof. unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ]. now inversion Heq. } - all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; [now econstructor | now econstructor | ]. + 1:{ cbn in * ; intros. + eapply DTree_fusion. + * unshelve eapply (eqTree _ a b). + 3: now eapply wfLCon_le_trans. + 2,3: eassumption. + all: irrelevance0 ; [ | eassumption ] ; f_equal. + all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; + [now econstructor | now econstructor | ]. + all: now inversion Heq. + * eapply (PolyRed.posExtTree ΠA (a:= a) (b := b) ρ (f0 •ε f) Hd). + all: irrelevance0 ; [ f_equal | eassumption]. + all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; + [now econstructor | now econstructor | ]. + all: now inversion Heq. + } + all: unshelve epose (Heq := redtywf_det _ _ (redtywf_Ltrans f ΠA.(ParamRedTyPack.red)) ΠA'.(ParamRedTyPack.red)) ; + [now econstructor | now econstructor | ]. all: inversion Heq. - 2: eapply convtm_Ltrans ; [eauto | now rewrite <- Heq]. - 2: eapply isLRFun_Ltrans ; eauto. + 2: eapply convtm_Ltrans ; [now eauto | now rewrite <- Heq]. + 2: eapply isLRFun_Ltrans ; now eauto. 1: now rewrite <- Heq. + cbn in * ; intros. irrelevance0 ; [ | unshelve eapply app]. @@ -466,10 +502,11 @@ Proof. * now eapply over_tree_fusion_l. + cbn in * ; intros. irrelevance0 ; [ | unshelve eapply eq]. - 9: now eapply over_tree_fusion_l. - 2: now eapply over_tree_fusion_r. - 1: now f_equal. - 1,2: irrelevance0 ; [ | eassumption] ; now f_equal. + 11: eapply over_tree_fusion_l ; exact Hoeq. + * now f_equal. + * now eapply over_tree_fusion_r. + * now eapply over_tree_fusion_l. + * eapply over_tree_fusion_l ; exact Hob. Defined. Lemma ΣTm_Ltrans (l : TypeLevel) (wl wl' : wfLCon) (Γ : context) (f : wl' ≤ε wl) (A : term) @@ -581,6 +618,14 @@ Proof. * eassumption. Qed. +Lemma Tm_Ltrans'@{h i j k l} {wl Γ wl' t A l} (f : wl' ≤ε wl) lrA lrA' : + [LogRel@{i j k l} l | Γ ||- t : A | lrA]< wl > -> + [LogRel@{i j k l} l | Γ ||- t : A | lrA']< wl' >. +Proof. + intros Hyp ; irrelevance0 ; [reflexivity | unshelve eapply Tm_Ltrans]. + 2-4: eassumption. +Qed. + Lemma WTm_Ltrans@{h i j k l} {wl Γ wl' A t l} (f : wl' ≤ε wl) (lrA : W[Γ ||- A]< wl >) : WLogRelTm@{i j k l} l wl Γ t A lrA -> @@ -592,7 +637,18 @@ Lemma WTm_Ltrans@{h i j k l} {wl Γ wl' A t l} - intros wl'' Hover Hover'. eapply (WRedTm _ Ht). now eapply over_tree_Ltrans. - Defined. + Defined. + + Lemma WTm_Ltrans'@{h i j k l} {wl Γ wl' A t l} + (f : wl' ≤ε wl) lrA lrA' : + WLogRelTm@{i j k l} l wl Γ t A lrA -> + WLogRelTm@{i j k l} l wl' Γ t A lrA'. + Proof. + intros Ht. + eapply WLRTmRedIrrelevant' ; [reflexivity | ]. + now eapply (WTm_Ltrans f). + Qed. + Lemma TmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l} (f : wl' ≤ε wl) (lrA : [Γ ||- A]< wl >) : [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA]< wl > -> @@ -726,6 +782,14 @@ Proof. Unshelve. all: assumption. Qed. +Lemma TmEq_Ltrans'@{h i j k l} {wl Γ wl' t u A l} (f : wl' ≤ε wl) lrA lrA': + [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA]< wl > -> + [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA']< wl' >. +Proof. + intros Ht ; irrelevance0 ; [reflexivity | ]. + now eapply (TmEq_Ltrans f). +Qed. + Lemma WTmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l} (f : wl' ≤ε wl) (lrA : W[Γ ||- A]< wl >) : WLogRelTmEq@{i j k l} l wl Γ t u A lrA -> @@ -737,6 +801,58 @@ Lemma WTmEq_Ltrans@{h i j k l} {wl Γ wl' t u A l} - intros wl'' Hover Hover'. eapply (WRedTmEq _ Htu). now eapply over_tree_Ltrans. - Defined. + Defined. + Lemma WTmEq_Ltrans'@{h i j k l} {wl Γ wl' t u A l} + (f : wl' ≤ε wl) lrA lrA' : + WLogRelTmEq@{i j k l} l wl Γ t u A lrA -> + WLogRelTmEq@{i j k l} l wl' Γ t u A lrA'. + Proof. + intros Ht. + eapply WLRTmEqIrrelevant' ; [reflexivity | ]. + now eapply (WTmEq_Ltrans f). + Qed. + End Red_Ltrans. + +Section Injection. + Context `{GenericTypingProperties}. + +Definition LogtoW@{h i j k l} {l : TypeLevel} {wl Γ A} + (RA : [ LogRel@{i j k l} l | Γ ||- A ]< wl >) : + WLogRel@{i j k l} l wl Γ A. +Proof. + exists (leaf wl). + intros wl' f ; exact (Ltrans@{h i j k l} f RA). +Defined. + +Definition TmLogtoW@{h i j k l} {l : TypeLevel} {wl Γ t A} + (RA : [ LogRel@{i j k l} l | Γ ||- A ]< wl >) + (Rt : [ LogRel@{i j k l} l | Γ ||- t : A | RA ]< wl >) : + WLogRelTm@{i j k l} l wl Γ t A (LogtoW@{h i j k l} RA). +Proof. + exists (leaf wl). + intros wl' f f' ; now eapply Tm_Ltrans. +Defined. + + +Definition EqLogtoW@{h i j k l} {l : TypeLevel} {wl Γ A B} + (RA : [ LogRel@{i j k l} l | Γ ||- A ]< wl >) + (Rt : [ LogRel@{i j k l} l | Γ ||- A ≅ B | RA ]< wl >) : + WLogRelEq@{i j k l} l wl Γ A B (LogtoW@{h i j k l} RA). +Proof. + exists (leaf wl). + intros wl' f f' ; now eapply Eq_Ltrans. +Defined. + + +Definition TmEqLogtoW@{h i j k l} {l : TypeLevel} {wl Γ t u A} + (RA : [ LogRel@{i j k l} l | Γ ||- A ]< wl >) + (Rt : [ LogRel@{i j k l} l | Γ ||- t ≅ u : A | RA ]< wl >) : + WLogRelTmEq@{i j k l} l wl Γ t u A (LogtoW@{h i j k l} RA). +Proof. + exists (leaf wl). + intros wl' f f' ; now eapply TmEq_Ltrans. +Defined. + +End Injection. diff --git a/theories/LogicalRelation/Neutral.v b/theories/LogicalRelation/Neutral.v index b052c2bb..92714960 100644 --- a/theories/LogicalRelation/Neutral.v +++ b/theories/LogicalRelation/Neutral.v @@ -234,7 +234,11 @@ intros l wl Γ A ΠA0 ihdom ihcod; split. [Γ |- n ~ n : A]< wl > -> [Γ ||-Π n : A | ΠA]< wl > := _ in _). { - intros. exists n (fun _ _ _ _ _ _ _ => leaf _) ; cbn. + intros. unshelve eexists n (fun _ _ _ _ _ _ _ => leaf _) _ ; cbn. + - intros * ha hb hab. + eapply DTree_fusion. + + exact (PolyRed.posTree polyRed ρ f Hd hb). + + exact (PolyRed.posExtTree polyRed ρ f Hd ha hb hab). - eapply redtmwf_refl. gen_typing. - eauto. @@ -280,7 +284,9 @@ intros l wl Γ A ΠA0 ihdom ihcod; split. 2: eapply Happ ; tea. 5:{ symmetry. unshelve eapply escapeEq, PolyRed.posExt. - 8: eassumption. all: eassumption. + 8: eassumption. all: try eassumption. + + now eapply over_tree_fusion_l. + + now eapply over_tree_fusion_r. } * now eapply wfLCon_le_trans. * now eapply wfc_Ltrans. @@ -415,10 +421,17 @@ Proof. 1: unshelve eapply convtm_over_tree. 2: intros ; eapply escapeEqTerm, (ihcod _ _ (tFst n) wk_id). Unshelve. - 1: unshelve eapply ((PolyRed.posTree polyRed wk_id (wfLCon_le_id _))). - 2: now gen_typing. - 11: exact H21. - 5: rewrite <- (wk_id_ren_on Γ n) ; now eapply hfst. + 1:{ eapply DTree_fusion ; [eapply DTree_fusion | ]. + 1,2: unshelve eapply ((PolyRed.posTree polyRed wk_id (wfLCon_le_id _))). + 2,4: now gen_typing. + 3: eapply (hfst n) ; eassumption. + 2: eapply (hfst n') ; eassumption. + eapply (PolyRed.posExtTree polyRed wk_id ((idε) wl) (wfc_wft H12)). + + eapply (hfst n) ; eassumption. + + eapply (hfst n') ; eassumption. + + now eapply hconv_fst. + } + 8: rewrite <- (wk_id_ren_on Γ n) ; now eapply hfst. 1,2,3: pose proof (Hyp := over_tree_le H21). + eapply typing_meta_conv. eapply ty_snd, ty_conv ; [now eapply ty_Ltrans | ]. @@ -436,13 +449,20 @@ Proof. now eapply wfLCon_le_id. now gen_typing. 2: now eapply hconv_fst. - revert H21 ; now destruct (wk_id_ren_on Γ n). + * do 2 (eapply over_tree_fusion_l) ; exact H21. + * eapply over_tree_fusion_r, over_tree_fusion_l ; exact H21. + * now eapply over_tree_fusion_r. + eapply convneu_Ltrans ; [eassumption | ]. eapply convne_meta_conv. 1:now eapply convneu_snd, convneu_conv. 1: now bsimpl. easy. + now bsimpl. + + now eapply wfLCon_le_id. + + now gen_typing. + + assert (Hyp := over_tree_fusion_l (over_tree_fusion_l H21)) ; clear H21 ; revert Hyp. + generalize (hfst n Γ wl wk_id ((idε) wl) (wfc_wft H12) H16 H18). + now destruct (wk_id_ren_on _ n). } split. unshelve refine ( let funred : forall n, @@ -492,12 +512,15 @@ Proof. [Δ |- cod[tFst n⟨ρ⟩ .: ρ >> tRel] ≅ cod[tFst n'⟨ρ⟩ .: ρ >> tRel]]< wl' >). { intros ; eapply convty_over_tree. intros wl'' Ho ; eapply escapeEq; unshelve eapply (PolyRed.posExt ΣA). - 2,3,5: eassumption. + 2,3: eassumption. + eapply Rn. + + do 2 (eapply over_tree_fusion_l) ; exact Ho. + eapply Rn'. + eapply hconv_fst. 1,2: now eapply ty_Ltrans. now eapply convneu_Ltrans. + + eapply over_tree_fusion_r, over_tree_fusion_l ; exact Ho. + + eapply over_tree_fusion_r ; exact Ho. } split; tea; unshelve eexists Rn Rn' _. + intros ; now eapply leaf. diff --git a/theories/LogicalRelation/NormalRed.v b/theories/LogicalRelation/NormalRed.v index 5ba66a07..267d9f17 100644 --- a/theories/LogicalRelation/NormalRed.v +++ b/theories/LogicalRelation/NormalRed.v @@ -52,10 +52,23 @@ Definition normRedΠ {wl Γ F G l} (h : [Γ ||- tProd F G]< wl >) : [Γ ||- tProd F G]< wl > := LRPi' (normRedΠ0 (invLRΠ h)). +Definition WnormRedΠ {wl Γ F G l} (h : W[Γ ||- tProd F G]< wl >) + : W[Γ ||- tProd F G]< wl >. +Proof. + exists (WT _ h). + intros wl' Hover ; now apply normRedΠ, (WRed _ h). +Defined. Definition normRedΣ {wl Γ F G l} (h : [Γ ||- tSig F G]< wl >) : [Γ ||- tSig F G]< wl > := LRSig' (normRedΣ0 (invLRΣ h)). +Definition WnormRedΣ {wl Γ F G l} (h : W[Γ ||- tSig F G]< wl >) + : W[Γ ||- tSig F G]< wl >. +Proof. + exists (WT _ h). + intros wl' Hover ; now apply normRedΣ, (WRed _ h). +Defined. + #[program] Definition normEqRedΣ {wl Γ F F' G G' l} (h : [Γ ||- tSig F G]< wl >) (heq : [Γ ||- _ ≅ tSig F' G' | h]< wl >) : [Γ ||- _ ≅ tSig F' G' | normRedΣ h]< wl > := @@ -69,13 +82,20 @@ Solve All Obligations with symmetry in e; injection e; clear e; destruct h ; intros; cbn in *; subst; eassumption. +Definition WnormEqRedΣ {wl Γ F F' G G' l} (h : W[Γ ||- tSig F G]< wl >) + (heq : W[Γ ||- _ ≅ tSig F' G' | h]< wl >) : W[Γ ||- _ ≅ tSig F' G' | WnormRedΣ h]< wl >. +Proof. + exists (WTEq _ heq). + intros wl' Hover Hover' ; now apply normEqRedΣ, (WRedEq _ heq). +Defined. + #[program] Definition normLambda {wl Γ F F' G t l RΠ} (Rlam : [Γ ||- tLambda F' t : tProd F G | normRedΠ RΠ ]< wl >) : [Γ ||- tLambda F' t : tProd F G | normRedΠ RΠ ]< wl > := {| PiRedTm.nf := tLambda F' t |}. Obligation 3. -eapply (PiRedTm.appTree Rlam ρ f Hd ha). +now eapply (PiRedTm.appTree Rlam ρ f Hd ha). Defined. Obligation 5. pose proof (e := redtmwf_whnf (PiRedTm.red Rlam) whnf_tLambda). @@ -84,12 +104,22 @@ eapply (f_equal (ren_term ρ)) in e ; cbn in *. rewrite e. now eapply app. Defined. +Obligation 6. +now eapply (PiRedTm.eqTree Rlam ρ f Hd ha hb eq). +Defined. Solve All Obligations with intros; pose proof (e := redtmwf_whnf (PiRedTm.red Rlam) whnf_tLambda); - destruct Rlam as [????? app eqq]; cbn in *; subst; + destruct Rlam as [?????? app eqq]; cbn in *; subst; first [eapply app | now eapply eqq| eassumption]. +Definition WnormLambda {wl Γ F F' G t l RΠ} + (Rlam : W[Γ ||- tLambda F' t : tProd F G | WnormRedΠ RΠ ]< wl >) : + W[Γ ||- tLambda F' t : tProd F G | WnormRedΠ RΠ ]< wl >. +Proof. + exists (WTTm _ Rlam). + intros wl' Hover Hover' ; now apply normLambda, (WRedTm _ Rlam). +Defined. #[program] Definition normPair {wl Γ F F' G G' f g l RΣ} @@ -130,6 +160,14 @@ Next Obligation. 4,5: eassumption. Defined. +Definition WnormPair {wl Γ F F' G G' f g l RΣ} + (Rp : W[Γ ||- tPair F' G' f g : tSig F G | WnormRedΣ RΣ ]< wl >) : + W[Γ ||- tPair F' G' f g : tSig F G | WnormRedΣ RΣ ]< wl >. +Proof. + exists (WTTm _ Rp). + intros wl' Hover Hover' ; now apply normPair, (WRedTm _ Rp). +Defined. + Definition invLRcan {wl Γ l A} (lr : [Γ ||- A]< wl >) (w : isType A) : [Γ ||- A]< wl > := match w as w in isType A return forall (lr : [Γ ||- A]< wl >), invLRTy lr (reflexivity A) w -> [Γ ||- A]< wl > with | UnivType => fun _ x => LRU_ x diff --git a/theories/LogicalRelation/Reduction.v b/theories/LogicalRelation/Reduction.v index 689213f2..f71bc6be 100644 --- a/theories/LogicalRelation/Reduction.v +++ b/theories/LogicalRelation/Reduction.v @@ -121,10 +121,16 @@ Proof. assert [Γ |-[ ta ] t ⤳* u : ΠA.(outTy)]< wl > by now eapply redtm_conv. assert [Γ |-[ ta ] t : ΠA.(outTy)]< wl > by (eapply ty_conv; gen_typing). unshelve refine (let rt : [LRPi' ΠA | Γ ||- t : A]< wl > := _ in _). - 1: exists f appTree ; tea ; constructor ; destruct red ; tea ; etransitivity ; tea. - split; tea; unshelve eexists ; tea. - intros; cbn. eapply eq; tea. - now apply reflLRTmEq. + 1: eexists f _ _ ; tea ; constructor ; destruct red ; tea ; etransitivity ; tea. + split; tea; unshelve eexists. + 1,2,4: tea. + 2:{ intros; cbn in *. eapply eq. + 1,2: eapply over_tree_fusion_l ; exact Ho'. + cbn in *. + eapply over_tree_fusion_r ; exact Ho'. + Unshelve. + now apply reflLRTmEq. + } - intros ? NA t ? Ru red; inversion Ru; subst. assert [Γ |- A ≅ tNat]< wl > by (destruct NA; gen_typing). assert [Γ |- t :⤳*: nf : tNat]< wl >. 1:{ diff --git a/theories/LogicalRelation/Reflexivity.v b/theories/LogicalRelation/Reflexivity.v index 763ee645..d1479efe 100644 --- a/theories/LogicalRelation/Reflexivity.v +++ b/theories/LogicalRelation/Reflexivity.v @@ -88,7 +88,6 @@ Section Reflexivities. pattern l, wl, Γ, A, lr; eapply LR_rect_TyUr; clear l wl Γ A lr; intros l wl Γ A. - intros h t [? ? ? ? Rt%RedTyRecFwd@{j k h i k}] ; cbn in *. (* Need an additional universe level h < i *) - Unset Printing Notations. pose proof (reflLRTyEq@{h i k j} Rt). unshelve econstructor. all : cbn. @@ -112,6 +111,17 @@ Section Reflexivities. all: cbn; now eauto. - intros; now eapply reflIdRedTmEq. Qed. + + Definition WreflLRTmEq@{h i j k l} {l wl Γ A} + (lr : WLogRel@{i j k l} l wl Γ A ) : + forall t, + W[ Γ ||- t : A | lr ]< wl > -> + W[ Γ ||- t ≅ t : A | lr ]< wl >. + Proof. + intros t [WTt WRedt] ; exists (WTt). + intros wl' Hover Hover' ; eapply reflLRTmEq@{h i j k l}. + now eapply WRedt. + Defined. (* Deprecated *) Corollary LRTmEqRefl@{h i j k l} {l wl Γ A eqTy redTm eqTm} (lr : LogRel@{i j k l} l wl Γ A eqTy redTm eqTm) : diff --git a/theories/LogicalRelation/SimpleArr.v b/theories/LogicalRelation/SimpleArr.v index 28d539b1..9966e4a8 100644 --- a/theories/LogicalRelation/SimpleArr.v +++ b/theories/LogicalRelation/SimpleArr.v @@ -1,6 +1,6 @@ From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Notations Utils BasicAst Context NormalForms Weakening GenericTyping LogicalRelation DeclarativeInstance. -From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Application. +From LogRel Require Import Notations Utils BasicAst LContexts Context NormalForms Weakening GenericTyping LogicalRelation Monad. +From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Monotonicity Transitivity Application. Set Universe Polymorphism. Set Printing Primitive Projection Parameters. @@ -8,88 +8,310 @@ Set Printing Primitive Projection Parameters. Section SimpleArrow. Context `{GenericTypingProperties}. - Lemma ArrRedTy0 {Γ l A B} : [Γ ||- A] -> [Γ ||- B] -> [Γ ||-Π arr A B]. + Lemma shiftPolyRed {wl Γ l A B} : + [Γ ||- A]< wl > -> + [Γ ||- B]< wl > -> + PolyRed wl Γ l A B⟨↑⟩. + Proof. + intros; escape; unshelve econstructor. + - intros; eapply wk ; eauto. + now eapply Ltrans. + - intros. + now econstructor. + - intros; bsimpl; rewrite <- rinstInst'_term; eapply wk. + + now eapply wfc_Ltrans. + + eapply Ltrans ; [ | eassumption]. + eapply wfLCon_le_trans ; eauto. + - intros ; now econstructor. + - now escape. + - renToWk; eapply wft_wk; gen_typing. + - intros; irrelevance0. + 2: replace (subst_term _ _) with B⟨ρ⟩. + 2: eapply wkEq, reflLRTyEq. + all: bsimpl; now rewrite rinstInst'_term. + Unshelve. 1: tea. + + now eapply wfc_Ltrans. + + eapply Ltrans ; [ | eassumption]. + eapply wfLCon_le_trans ; eauto. + Qed. + + + Lemma ArrRedTy0 {wl Γ l A B} : + [Γ ||- A]< wl > -> + [Γ ||- B]< wl > -> + [Γ ||-Π arr A B]< wl >. Proof. intros RA RB; escape. unshelve econstructor; [exact A| exact B⟨↑⟩|..]; tea. - - intros; now eapply wk. - - cbn; intros. - bsimpl; rewrite <- rinstInst'_term. - now eapply wk. - eapply redtywf_refl. now eapply wft_simple_arr. - - renToWk; eapply wft_wk; gen_typing. + - now unshelve eapply escapeEq, reflLRTyEq. - eapply convty_simple_arr; tea. - all: now unshelve eapply escapeEq, LRTyEqRefl_. - - intros; irrelevance0. - 2: replace (subst_term _ _) with B⟨ρ⟩. - 2: eapply wkEq, LRTyEqRefl_. - all: bsimpl; now rewrite rinstInst'_term. - Unshelve. all: tea. + all: now unshelve eapply escapeEq, reflLRTyEq. + - now eapply shiftPolyRed. Qed. - Lemma ArrRedTy {Γ l A B} : [Γ ||- A] -> [Γ ||- B] -> [Γ ||- arr A B]. + Lemma ArrRedTy {wl Γ l A B} : + [Γ ||- A]< wl > -> + [Γ ||- B]< wl > -> + [Γ ||- arr A B]< wl >. Proof. intros; eapply LRPi'; now eapply ArrRedTy0. Qed. - Lemma idred {Γ l A} (RA : [Γ ||- A]) : - [Γ ||- idterm A : arr A A | ArrRedTy RA RA]. + Lemma WArrRedTy {wl Γ l A B} : + W[Γ ||- A]< wl > -> + W[Γ ||- B]< wl > -> + W[Γ ||- arr A B]< wl >. + Proof. + intros [WTA WRedA] [WTB WRedB]. + exists (DTree_fusion _ WTA WTB). + intros ; eapply ArrRedTy. + - now eapply WRedA, over_tree_fusion_l. + - now eapply WRedB, over_tree_fusion_r. + Qed. + + Lemma shiftPolyRedEq {wl Γ l A A' B B'} + (RA : [Γ ||- A]< wl >) + (RB : [Γ ||- B]< wl >) + (PAB : PolyRed wl Γ l A B⟨↑⟩) : + [Γ ||- A ≅ A' | RA]< wl > -> + [Γ ||- B ≅ B' | RB]< wl > -> + PolyRedEq PAB A' B'⟨↑⟩. + Proof. + intros; escape; unshelve econstructor. + - intros ; now econstructor. + - intros; irrelevanceRefl; eapply wkEq. + unshelve eapply (Eq_Ltrans f) ; eassumption. + - intros; irrelevance0; rewrite shift_subst_scons; [reflexivity|]. + eapply wkEq, (Eq_Ltrans (wfLCon_le_trans _ f)) ; eassumption. + Unshelve. all: eauto. + now eapply wfc_Ltrans. + Qed. + + Lemma arrRedCong0 {wl Γ l A A' B B'} + (RA : [Γ ||- A]< wl >) + (RB : [Γ ||- B]< wl >) + (tyA' : [Γ |- A']< wl >) + (tyB' : [Γ |- B']< wl >) + (RAB : [Γ ||-Π arr A B]< wl >) : + [Γ ||- A ≅ A' | RA]< wl > -> + [Γ ||- B ≅ B' | RB]< wl > -> + [Γ ||-Π arr A B ≅ arr A' B' | normRedΠ0 RAB]< wl >. Proof. + intros RAA' RBB'; escape. + unshelve econstructor; cycle 2. + + eapply redtywf_refl; now eapply wft_simple_arr. + + now cbn. + + now eapply convty_simple_arr. + + now eapply shiftPolyRedEq. + Qed. + + Lemma arrRedCong {wl Γ l A A' B B'} + (RA : [Γ ||- A]< wl >) (RB : [Γ ||- B]< wl >) + (tyA' : [Γ |- A']< wl >) (tyB' : [Γ |- B']< wl >) : + [Γ ||- A ≅ A' | RA]< wl > -> + [Γ ||- B ≅ B' | RB]< wl > -> + [Γ ||- arr A B ≅ arr A' B' | normRedΠ (ArrRedTy RA RB)]< wl >. + Proof. + intros; now eapply arrRedCong0. + Qed. + + Lemma arrRedCong' {wl Γ l A A' B B'} + (RA : [Γ ||- A]< wl >) (RB : [Γ ||- B]< wl >) + (tyA' : [Γ |- A']< wl >) (tyB' : [Γ |- B']< wl >) + (RAB : [Γ ||- arr A B]< wl >) : + [Γ ||- A ≅ A' | RA]< wl > -> + [Γ ||- B ≅ B' | RB]< wl > -> + [Γ ||- arr A B ≅ arr A' B' | RAB]< wl >. + Proof. + intros; irrelevanceRefl; now eapply arrRedCong. + Qed. + + Lemma WarrRedCong' {wl Γ l A A' B B'} + (RA : W[Γ ||- A]< wl >) (RB : W[Γ ||- B]< wl >) + (tyA' : [Γ |- A']< wl >) (tyB' : [Γ |- B']< wl >) + (RAB : W[Γ ||- arr A B]< wl >) : + W[Γ ||- A ≅ A' | RA]< wl > -> + W[Γ ||- B ≅ B' | RB]< wl > -> + W[Γ ||- arr A B ≅ arr A' B' | RAB]< wl >. + Proof. + intros [WTAA WEqA] [WTBB WEqB]. + exists (DTree_fusion _ (DTree_fusion _ (WT _ RA) (WT _ RB)) + (DTree_fusion _ WTAA WTBB)). + intros wl' Hover hover'. + pose proof (f := over_tree_le Hover). + eapply arrRedCong'. + 1,2: now eapply wft_Ltrans. + - unshelve eapply WEqA. + + now do 2 (eapply over_tree_fusion_l). + + now eapply over_tree_fusion_l, over_tree_fusion_r. + - unshelve eapply WEqB. + + now eapply over_tree_fusion_r, over_tree_fusion_l. + + now do 2 (eapply over_tree_fusion_r). + Qed. + + Lemma polyRedArrExt {wl Γ l A B C} : + PolyRed wl Γ l A B -> PolyRed wl Γ l A C -> PolyRed wl Γ l A (arr B C). + Proof. + intros [tyA tyB RA RTree RB RBExtTree RBext] [_ tyC RA' RTree' RC RCExtTree RCext]. + unshelve econstructor. + 6: now eapply wft_simple_arr. + 1,5: eassumption. + + intros ; eapply DTree_fusion. + * unshelve eapply RTree. + 3-5: eassumption. + 2: irrelevance0 ; [ reflexivity | eassumption]. + * unshelve eapply RTree'. + 3-5: eassumption. + 2: irrelevance0 ; [ reflexivity | eassumption]. + + intros; rewrite subst_arr; refold. + apply ArrRedTy; [eapply RB| eapply RC]. + cbn in *. + * now eapply over_tree_fusion_l. + * now eapply over_tree_fusion_r. + + intros ; eapply DTree_fusion. + * unshelve eapply (RBExtTree _ _ a b). + 2-4: eassumption. + 1-3 : irrelevance0 ; [ reflexivity | eassumption]. + * unshelve eapply (RCExtTree _ _ a b). + 2-4: eassumption. + 1-3: irrelevance0 ; [reflexivity | eassumption]. + + intros. + irrelevance0; rewrite subst_arr; [refold; reflexivity|]; refold. + unshelve eapply arrRedCong. + 3,4: eapply escapeConv ; first [eapply RBext | eapply RCext] ; cycle 1. + 7,8: first [eapply RBext| eapply RCext]. + all: cbn in *. + Unshelve. + all: try (eapply over_tree_fusion_l ; eassumption). + all: try (eapply over_tree_fusion_r ; eassumption). + Qed. + + Lemma polyRedEqArrExt {wl Γ l A A' B B' C C'} + (PAB : PolyRed wl Γ l A B) (PAC : PolyRed wl Γ l A C) + (PAB' : PolyRed wl Γ l A' B') (PAC' : PolyRed wl Γ l A' C') + (PABC : PolyRed wl Γ l A (arr B C)) + (PABeq : PolyRedEq PAB A' B') + (PACeq : PolyRedEq PAC A' C') + : PolyRedEq PABC A' (arr B' C'). + Proof. + econstructor. + + intros; irrelevanceRefl; now unshelve eapply (PolyRedEq.shpRed PABeq). + + intros; irrelevance0; rewrite subst_arr; refold; [reflexivity|]. + pose proof (f' := over_tree_le Ho). + apply arrRedCong. + * eapply escapeConv. + unshelve eapply (PolyRedEq.posRed PABeq) ; cycle 1 ; try eassumption. + -- now irrelevance0. + -- do 3 (eapply over_tree_fusion_l) ; exact Ho' . + -- eapply over_tree_fusion_r ; do 2 (eapply over_tree_fusion_l) ; exact Ho'. + * eapply escape; unshelve eapply (PolyRed.posRed). + 5: exact f. + 4: eapply LRTmRedConv; tea. + 4: irrelevanceRefl; unshelve eapply (PolyRedEq.shpRed PABeq). + 1,2,3,4: eassumption. + eapply over_tree_fusion_r, over_tree_fusion_l ; exact Ho'. + * unshelve eapply (PolyRedEq.posRed PABeq). + 2,3: eassumption. + 1: now irrelevanceRefl. + all: cbn in *. + 1: now do 3 (eapply over_tree_fusion_l). + now eapply over_tree_fusion_r ; do 2 (eapply over_tree_fusion_l). + * unshelve eapply (PolyRedEq.posRed PACeq). + 2,3: eassumption. + 1: now irrelevanceRefl. + all: cbn in *. + eapply over_tree_fusion_l, over_tree_fusion_r ; exact Ho'. + do 2 (eapply over_tree_fusion_r) ; exact Ho'. + Qed. + + Lemma idred {wl Γ l A} (RA : [Γ ||- A]< wl >) : + [Γ ||- idterm A : arr A A | ArrRedTy RA RA]< wl >. + Proof. + eassert [_ | Γ,, A ||- tRel 0 : A⟨_⟩]< wl > as hrel. + { + eapply var0. + 1: reflexivity. + now escape. + } + Unshelve. + all: cycle -1. + { + erewrite <- wk1_ren_on. + eapply wk ; tea. + escape. + gen_typing. + } + eapply reflLRTmEq in hrel. normRedΠ ΠAA. - pose proof (LRTyEqRefl_ RA). + pose proof (reflLRTyEq RA). escape. - assert (h : forall Δ a (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) RA (ha : [Δ ||- a : A⟨ρ⟩ | RA]), - [Δ ||- tApp (idterm A)⟨ρ⟩ a : A⟨ρ⟩| RA] × - [Δ ||- tApp (idterm A)⟨ρ⟩ a ≅ a : A⟨ρ⟩| RA] + assert (h : forall Δ wl' a (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) + (wfΔ : [|- Δ]< wl' >) RA + (ha : [Δ ||- a : A⟨ρ⟩ | RA]< wl' >), + [Δ ||- tApp (idterm A)⟨ρ⟩ a : A⟨ρ⟩| RA]< wl' > × + [Δ ||- tApp (idterm A)⟨ρ⟩ a ≅ a : A⟨ρ⟩| RA]< wl' > ). 1:{ intros; cbn; escape. - assert [Δ |- A⟨ρ⟩] by now eapply wft_wk. - assert [Δ |- A⟨ρ⟩ ≅ A⟨ρ⟩] by now eapply convty_wk. + assert [Δ |- A⟨ρ⟩]< wl' > by (eapply wft_wk ; eauto ; now eapply wft_Ltrans). + assert [Δ |- A⟨ρ⟩ ≅ A⟨ρ⟩]< wl' > + by (eapply convty_wk ; eauto ; now eapply convty_Ltrans). eapply redSubstTerm; tea. now eapply redtm_id_beta. } - econstructor; cbn. - - eapply redtmwf_refl. - now eapply ty_id. - - constructor. - - apply tm_nf_lam. - + eapply reifyType, RA. - + apply tm_ne_nf, tm_ne_rel. - gen_typing. - - now eapply convtm_id. + unshelve econstructor; cbn. + 4: eapply redtmwf_refl; now eapply ty_id. + - intros ; now econstructor. + - intros ; now econstructor. + - eapply convtm_id; tea. + eapply wfc_wft; now escape. + - unshelve econstructor 1. + + intros ; now econstructor. + + intros; cbn; apply reflLRTyEq. + + intros; cbn. + irrelevance0; [|eapply (Tm_Ltrans Ho') ; exact ha]. + cbn; bsimpl; now rewrite rinstInst'_term. - intros; cbn; irrelevance0. - 2: now eapply h. - bsimpl; now rewrite rinstInst'_term. + 2: eapply h ; eauto. + 2: now eapply wfLCon_le_trans. + 2: now eapply wfc_Ltrans. + + bsimpl; now rewrite rinstInst'_term. + + now eapply (Tm_Ltrans Ho'). - intros ; cbn; irrelevance0; cycle 1. 1: eapply transEqTerm;[|eapply transEqTerm]. - + now eapply h. - + eassumption. - + eapply LRTmEqSym. now eapply h. + + eapply h. + * now eapply wfLCon_le_trans. + * now eapply wfc_Ltrans. + * now eapply (Tm_Ltrans Hoa). + + eapply (TmEq_Ltrans Hoa) ; eassumption. + + eapply (TmEq_Ltrans Hoa),LRTmEqSym ; now eapply h. + bsimpl; now rewrite rinstInst'_term. Qed. Section SimpleAppTerm. - Context {Γ t u F G l} - {RF : [Γ ||- F]} - (RG : [Γ ||- G]) - (hΠ := normRedΠ0 (ArrRedTy0 RF RG)) - (Rt : [Γ ||- t : arr F G | LRPi' hΠ]) - (Ru : [Γ ||- u : F | RF]). - - Lemma simple_app_id : [Γ ||- tApp (PiRedTm.nf Rt) u : G | RG ]. + Context {wl Γ t u F G l} + {RF : [Γ ||- F]< wl >} + (RG : [Γ ||- G]< wl >) + (hΠ := normRedΠ (ArrRedTy RF RG)) + (Rt : [Γ ||- t : arr F G | hΠ]< wl >) + (Ru : [Γ ||- u : F | RF]< wl >) + (WRG := Build_WLogRel l wl Γ G (leaf _) + (fun wl Hover => Ltrans (over_tree_le Hover) RG)). + + Lemma simple_app_id : W[Γ ||- tApp (PiRedTm.nf Rt) u : G | WRG ]< wl >. Proof. - irrelevance0. - 2: now eapply app_id. - now bsimpl. - Unshelve. 1: tea. - now bsimpl. + unshelve eapply WLRTmRedIrrelevant'. + 5: eapply app_id. + 1: tea. + 1,2: now bsimpl. + eassumption. Qed. Lemma simple_appTerm0 : - [Γ ||- tApp t u : G | RG] - × [Γ ||- tApp t u ≅ tApp (PiRedTm.nf Rt) u : G | RG]. + W[Γ ||- tApp t u : G | WRG]< wl > + × W[Γ ||- tApp t u ≅ tApp (PiRedTm.nf Rt) u : G | WRG]< wl >. Proof. - irrelevance0. + eapply WLRTmTmEqIrrelevant'. 2: now eapply appTerm0. now bsimpl. Unshelve. 1: tea. @@ -98,135 +320,252 @@ Section SimpleArrow. End SimpleAppTerm. - Lemma simple_appTerm {Γ t u F G l} - {RF : [Γ ||- F]} - (RG : [Γ ||- G]) - (RΠ : [Γ ||- arr F G]) - (Rt : [Γ ||- t : arr F G | RΠ]) - (Ru : [Γ ||- u : F | RF]) : - [Γ ||- tApp t u : G| RG]. - Proof. - unshelve eapply simple_appTerm0. - 3: irrelevance. - all: tea. - Qed. - - - Lemma simple_appcongTerm {Γ t t' u u' F G l} - {RF : [Γ ||- F]} - (RG : [Γ ||- G]) - (RΠ : [Γ ||- arr F G]) - (Rtt' : [Γ ||- t ≅ t' : _ | RΠ]) - (Ru : [Γ ||- u : F | RF]) - (Ru' : [Γ ||- u' : F | RF]) - (Ruu' : [Γ ||- u ≅ u' : F | RF ]) : - [Γ ||- tApp t u ≅ tApp t' u' : G | RG]. - Proof. - irrelevance0. - 2: eapply appcongTerm. - 2-5: tea. - now bsimpl. - Unshelve. tea. - now bsimpl. - Qed. - - Lemma arr_wk {Γ Δ A B} {ρ : Δ ≤ Γ} : arr A⟨ρ⟩ B⟨ρ⟩ = (arr A B)⟨ρ⟩. - Proof. cbn; now bsimpl. Qed. - - Lemma wkRedArr {Γ l A B f} - (RA : [Γ ||- A]) - (RB : [Γ ||- B]) - {Δ} (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) : - [Γ ||- f : arr A B | ArrRedTy RA RB] -> - [Δ ||- f⟨ρ⟩ : arr A⟨ρ⟩ B⟨ρ⟩ | ArrRedTy (wk ρ wfΔ RA) (wk ρ wfΔ RB)]. + Lemma simple_appTerm {wl Γ t u F G l} + {RF : [Γ ||- F]< wl >} + (RG : [Γ ||- G]< wl >) + (RΠ : [Γ ||- arr F G]< wl >) + (Rt : [Γ ||- t : arr F G | RΠ]< wl >) + (Ru : [Γ ||- u : F | RF]< wl >) : + W[Γ ||- tApp t u : G| (LogtoW RG)]< wl >. + Proof. + unshelve eapply WLRTmRedIrrelevant'. + 5: unshelve eapply appTerm. + 6-9: eauto. + 1: eapply LogtoW. + 1,2: now bsimpl. + Qed. + + + Lemma Wsimple_appTerm {wl Γ t u F G l} + {RF : W[Γ ||- F]< wl >} + (RG : W[Γ ||- G]< wl >) + (RΠ : W[Γ ||- arr F G]< wl >) + (Rt : W[Γ ||- t : arr F G | RΠ]< wl >) + (Ru : W[Γ ||- u : F | RF]< wl >) : + W[Γ ||- tApp t u : G| RG]< wl >. + Proof. + unshelve eapply WLRTmRedIrrelevant'. + 5: unshelve eapply WappTerm. + 6-9: eauto. + 1,2: now bsimpl. + Qed. + + + Lemma simple_appcongTerm {wl Γ t t' u u' F G l} + {RF : [Γ ||- F]< wl >} + (RG : [Γ ||- G]< wl >) + (RΠ : [Γ ||- arr F G]< wl >) + (Rtt' : [Γ ||- t ≅ t' : _ | RΠ]< wl >) + (Ru : [Γ ||- u : F | RF]< wl >) + (Ru' : [Γ ||- u' : F | RF]< wl >) + (Ruu' : [Γ ||- u ≅ u' : F | RF ]< wl >) : + W[Γ ||- tApp t u ≅ tApp t' u' : G | (LogtoW RG)]< wl >. + Proof. + unshelve eapply WLRTmEqIrrelevant'. + 5: unshelve eapply appcongTerm. + 7-12: tea. + 1: eapply LogtoW. + 1,2: now bsimpl. + Qed. + + + Lemma Wsimple_appcongTerm {wl Γ t t' u u' F G l} + {RF : W[Γ ||- F]< wl >} + (RG : W[Γ ||- G]< wl >) + (RΠ : W[Γ ||- arr F G]< wl >) + (Rtt' : W[Γ ||- t ≅ t' : _ | RΠ]< wl >) + (Ru : W[Γ ||- u : F | RF]< wl >) + (Ru' : W[Γ ||- u' : F | RF]< wl >) + (Ruu' : W[Γ ||- u ≅ u' : F | RF ]< wl >) : + W[Γ ||- tApp t u ≅ tApp t' u' : G | RG]< wl >. + Proof. + unshelve eapply WLRTmEqIrrelevant'. + 5: unshelve eapply WappcongTerm. + 7-12: tea. + 1,2: now bsimpl. + Qed. + + Lemma wkRedArr {wl Γ l A B f} + (RA : [Γ ||- A]< wl >) + (RB : [Γ ||- B]< wl >) + {Δ} (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]< wl >) : + [Γ ||- f : arr A B | ArrRedTy RA RB]< wl > -> + [Δ ||- f⟨ρ⟩ : arr A⟨ρ⟩ B⟨ρ⟩ | ArrRedTy (wk ρ wfΔ RA) (wk ρ wfΔ RB)]< wl >. Proof. intro; irrelevance0. 2: unshelve eapply wkTerm; cycle 3; tea. - symmetry; apply arr_wk. + symmetry; apply wk_arr. Qed. - Lemma compred {Γ l A B C f g} - (RA : [Γ ||- A]) - (RB : [Γ ||- B]) - (RC : [Γ ||- C]) : - [Γ ||- f : arr A B | ArrRedTy RA RB] -> - [Γ ||- g : arr B C | ArrRedTy RB RC] -> - [Γ ||- comp A g f : arr A C | ArrRedTy RA RC]. + Definition compred_appTree {wl Γ l A B C f g} + (RA : [Γ ||- A]< wl >) + (RB : [Γ ||- B]< wl >) + (RC : [Γ ||- C]< wl >) : + [LRPi' (normRedΠ0 (invLRΠ (ArrRedTy RA RB))) | Γ ||- f : arr A B ]< wl > -> + [LRPi' (normRedΠ0 (invLRΠ (ArrRedTy RB RC))) | Γ ||- g : arr B C ]< wl > -> + forall Δ wl' a (ρ : Δ ≤ Γ) (tau : wl' ≤ε wl) + (wfΔ : [|- Δ]< wl' >) + (ha : [PolyRedPack.shpRed (normRedΠ0 (invLRΠ (ArrRedTy RA RB))) ρ tau wfΔ | Δ ||- a + : (ParamRedTyPack.dom (normRedΠ0 (invLRΠ (ArrRedTy RA RB))))⟨ρ⟩ ]< wl' >), + DTree wl'. + Proof. + intros Rf Rg * ha. + unshelve eapply DTree_bind_over. + - eapply DTree_fusion. + + now unshelve eapply (PiRedTm.appTree (a := a) Rf). + + now unshelve eapply (PolyRedPack.posTree (normRedΠ0 (invLRΠ (ArrRedTy RA RB)))). + - intros wl'' Hover. + pose proof (f' := over_tree_le Hover). + unshelve eapply (PiRedTm.appTree Rg). + 3: eassumption. + 2: now eapply wfLCon_le_trans. + 2: now eapply wfc_Ltrans. + 2: irrelevance0 ; [ | eapply (PiRedTm.app Rf)] . + 2: eapply over_tree_fusion_l ; eassumption. + cbn. + bsimpl. + now rewrite rinstInst'_term. + Unshelve. + now eapply over_tree_fusion_r. + Defined. + + Lemma compred {wl Γ l A B C u v} + (RA : [Γ ||- A]< wl >) + (RB : [Γ ||- B]< wl >) + (RC : [Γ ||- C]< wl >) : + [Γ ||- u : arr A B | ArrRedTy RA RB]< wl > -> + [Γ ||- v : arr B C | ArrRedTy RB RC]< wl > -> + [Γ ||- comp A v u : arr A C | ArrRedTy RA RC]< wl >. Proof. - intros Rf Rg. - normRedΠin ΠAB Rf; normRedΠin ΠBC Rg; normRedΠ ΠAC. - assert (h : forall Δ a (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) RA (ha : [Δ ||- a : A⟨ρ⟩ | RA]), - [Δ ||- tApp g⟨ρ⟩ (tApp f⟨ρ⟩ a) : _ | wk ρ wfΔ RC]). + intros Ru Rv. + normRedΠin Ru; normRedΠin Rv; normRedΠ ΠAC. + pose (d := compred_appTree RA RB RC Ru Rv). + assert (h : forall Δ wl' a (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) + (wfΔ : [|- Δ]< wl' >) RA + (ha : [Δ ||- a : A⟨ρ⟩ | RA]< wl' >), + W[Δ ||- tApp v⟨ρ⟩ (tApp u⟨ρ⟩ a) : _ | Wwk ρ wfΔ (WLtrans f (LogtoW RC))]< wl' >). 1:{ - intros; eapply simple_appTerm; [|eapply simple_appTerm; tea]. - 1,2: eapply wkRedArr; irrelevance. - Unshelve. 1: eapply wk. all: tea. + intros. + eapply WLRTmRedIrrelevant' ; [reflexivity | ]. + unshelve eapply Wsimple_appTerm. + 5: eapply simple_appTerm. + 3: eapply TmLogtoW. + 2,3: eapply wkRedArr. + 1,2: irrelevance0 ; [reflexivity | ]. + 1,2: eapply (Tm_Ltrans f) ; eassumption. + eassumption. + Unshelve. + 3,6: eassumption. + 1: eapply LogtoW. + 1,2: eapply wk ; try eassumption. + all: now eapply (Ltrans f). } - assert (heq : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) RA - (ha : [Δ ||- a : A⟨ρ⟩ | RA]) (hb : [Δ ||- b : A⟨ρ⟩ | RA]) - (ha : [Δ ||- a ≅ b: A⟨ρ⟩ | RA]), - [Δ ||- tApp g⟨ρ⟩ (tApp f⟨ρ⟩ a) ≅ tApp g⟨ρ⟩ (tApp f⟨ρ⟩ b) : _ | wk ρ wfΔ RC]). + assert (heq : forall Δ wl' a b (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) + (wfΔ : [|- Δ]< wl' >) RA + (ha : [Δ ||- a : A⟨ρ⟩ | RA]< wl' >) + (hb : [Δ ||- b : A⟨ρ⟩ | RA]< wl' >) + (hab : [Δ ||- a ≅ b: A⟨ρ⟩ | RA]< wl' >), + W[Δ ||- tApp v⟨ρ⟩ (tApp u⟨ρ⟩ a) ≅ tApp v⟨ρ⟩ (tApp u⟨ρ⟩ b) : _ | + Wwk ρ wfΔ (WLtrans f (LogtoW RC))]< wl' >). 1:{ intros. - eapply simple_appcongTerm; [| | |eapply simple_appcongTerm; tea]. - 1,4: eapply LREqTermRefl_; eapply wkRedArr; irrelevance. - 1,2: eapply simple_appTerm; tea; eapply wkRedArr; irrelevance. - Unshelve. 1: eapply wk. all: tea. + eapply WLRTmEqIrrelevant' ; [reflexivity | ]. + eapply Wsimple_appcongTerm ; [| | | unshelve eapply simple_appcongTerm ]. + 1: eapply TmEqLogtoW. + 1,8: unshelve eapply reflLRTmEq, wkRedArr, (Tm_Ltrans' f). + 2,7,11,12,17-19: eassumption. + 1-4: now eapply (Ltrans f). + 1,2: unshelve eapply simple_appTerm. + 7,9: unshelve eapply wkRedArr, (Tm_Ltrans' f). + 13,14: irrelevance. + 6,10: now eapply ArrRedTy. + all: try eassumption. + 5: eapply wk ; eauto. + all: now eapply (Ltrans f). + Unshelve. + now eapply LogtoW, wk, (Ltrans f). } escape. - assert (beta : forall Δ a (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) RA (ha : [Δ ||- a : A⟨ρ⟩ | RA]), - [Δ ||- tApp (comp A g f)⟨ρ⟩ a : _ | wk ρ wfΔ RC] × - [Δ ||- tApp (comp A g f)⟨ρ⟩ a ≅ tApp g⟨ρ⟩ (tApp f⟨ρ⟩ a) : _ | wk ρ wfΔ RC]). + assert (beta : forall Δ wl' a (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) + (wfΔ : [|- Δ]< wl' >) RA + (ha : [Δ ||- a : A⟨ρ⟩ | RA]< wl' >), + W[Δ ||- tApp (comp A v u)⟨ρ⟩ a : _ | Wwk ρ wfΔ (WLtrans f (LogtoW RC))]< wl' > × + W[Δ ||- tApp (comp A v u)⟨ρ⟩ a ≅ tApp v⟨ρ⟩ (tApp u⟨ρ⟩ a) : _ | + Wwk ρ wfΔ (WLtrans f (LogtoW RC))]< wl' >). 1:{ intros; cbn. assert (eq : forall t : term, t⟨↑⟩⟨upRen_term_term ρ⟩ = t⟨ρ⟩⟨↑⟩) by (intros; now asimpl). do 2 rewrite eq. - eapply redSubstTerm. + eapply WredSubstTerm. + now eapply h. + eapply redtm_comp_beta. 6: cbn in *; now escape. - 5: erewrite arr_wk; eapply ty_wk; tea. + 5: now erewrite wk_arr; eapply ty_wk, ty_Ltrans; tea. 4: eapply typing_meta_conv. - 4: eapply ty_wk; tea. - 4: now rewrite <- arr_wk. - 1-3: now eapply wft_wk. + 4: now eapply ty_wk, ty_Ltrans; tea. + 4: exact (wk_arr (A := A) (B := B) ρ). + 1-3: now eapply wft_wk, wft_Ltrans. } econstructor. - eapply redtmwf_refl. - eapply ty_comp; cycle 2; tea. - - constructor. - - apply tm_nf_lam. - + now eapply reifyType. - + change (PiRedTy.dom (PiRedTyPack.toPiRedTy ΠAC)) with A. - change (PiRedTy.cod (PiRedTyPack.toPiRedTy ΠAC)) with C⟨↑⟩. - pose (ρ := @wk_step Γ Γ A wk_id). - assert (Hr : forall (t : term), t⟨↑⟩ = t⟨ρ⟩). - { unfold ρ; bsimpl; reflexivity. } - do 3 rewrite Hr. - eapply reifyTerm. - unshelve refine (h _ (tRel 0) ρ _ (wk _ _ RA) _). - 1,2: gen_typing. - apply var0; [|tea]; unfold ρ; bsimpl; reflexivity. - - cbn. eapply convtm_comp; cycle 3; tea. + eapply ty_comp ; cycle 2 ; now tea. + - cbn. eapply convtm_comp; cycle 6; tea. erewrite <- wk1_ren_on. - eapply escapeEqTerm. - eapply LREqTermRefl_. + eapply WescapeEqTerm. + eapply WreflLRTmEq. do 2 erewrite <- wk1_ren_on. eapply h. eapply var0; now bsimpl. - Unshelve. 1: gen_typing. - eapply wk; tea; gen_typing. - - intros; cbn. + { now eapply wfc_ty. } + unshelve eapply escapeEq, reflLRTyEq; tea. + unshelve eapply escapeEq, reflLRTyEq; tea. + Unshelve. 3: gen_typing. + 3: now eapply wfLCon_le_id. + 3: now eapply wk; tea; gen_typing. + 1:{ intros ; eapply DTree_fusion. + + now unshelve eapply (fst (beta _ _ _ _ _ Hd _ ha)). + + unshelve eapply (WTTmEq (Wwk ρ Hd (WLtrans f (LogtoW RC))) _). + 3: now unshelve eapply (snd (beta _ _ _ _ _ _ _ ha)). + } + intros ; eapply DTree_fusion. + + now unshelve eapply (WTTmEq _ (heq _ _ _ _ _ _ Hd _ ha hb eq)). + + exact (WT C⟨ρ⟩ (Wwk ρ Hd (WLtrans f (LogtoW RC)))). + - unshelve econstructor 1; intros; cbn. + + eapply h ; eassumption. + + 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. + 7: exact Ho'. + cbn ; now eapply over_tree_le. + - intros; cbn in *. irrelevance0. - 2: unshelve eapply beta; tea. - bsimpl; now rewrite rinstInst'_term. - - intros; irrelevance0; cycle 1. + 2: unshelve eapply (fst (beta _ _ _ _ _ _ _ _)) ; cbn. + 3,4,6: eassumption. + + bsimpl; now rewrite rinstInst'_term. + + now eapply over_tree_le. + + now eapply over_tree_fusion_l. + - intros * hb hab ** ; irrelevance0; cycle 1 ; cbn in *. 1: eapply transEqTerm;[|eapply transEqTerm]. - + unshelve eapply beta; tea. - + unshelve eapply heq; tea. - + eapply LRTmEqSym. - unshelve eapply beta; tea. - + cbn; bsimpl; now rewrite rinstInst'_term. - Qed. + 1:{ unshelve eapply (snd (beta _ _ _ _ _ _ _ _)) ; cbn in *. + 2,3,5: eassumption. + * now eapply over_tree_le. + * now eapply over_tree_fusion_r. + } + 2:{ eapply LRTmEqSym. + unshelve eapply (snd (beta _ _ _ _ _ _ _ _)). + 2: eassumption. + cbn in *. + eapply over_tree_fusion_r ; eassumption. + } + cbn in *. + irrelevance0 ; [ reflexivity | ]. + 2: cbn ; bsimpl ; now rewrite rinstInst'_term. + unshelve eapply heq. + 2,3,6-8: eassumption. + + now eapply over_tree_fusion_r. + + now eapply over_tree_fusion_l. + Qed. End SimpleArrow. diff --git a/theories/LogicalRelation/Transitivity.v b/theories/LogicalRelation/Transitivity.v index 4ac851e1..2495d252 100644 --- a/theories/LogicalRelation/Transitivity.v +++ b/theories/LogicalRelation/Transitivity.v @@ -110,24 +110,22 @@ Proof. unshelve epose proof (e := redtmwf_det _ _ (SigRedTm.red redR) (SigRedTm.red redL)); tea. 1,2: now eauto. unshelve eexists ; [exact tL | exact tR |..]. - - intros ; eapply DTree_fusion ; [eapply DTree_fusion | ]. + - intros ; do 2 (eapply DTree_fusion). + eapply eqtree ; eauto. + eapply eqtree' ; eauto. + eapply (PolyRed.posTree ΣA ρ f Hd (SigRedTm.fstRed redL ρ f Hd)). + + eapply (PolyRed.posExtTree ΣA ρ f Hd (SigRedTm.fstRed redL ρ f Hd) (SigRedTm.fstRed tL ρ f Hd)). + eapply LRTmEqSym ; rewrite <- e ; now eapply eqfst. - etransitivity; tea. now rewrite e. - intros; eapply ihdom ; [eapply eqfst| rewrite e; eapply eqfst']. - intros; eapply ihcod; [eapply eqsnd|] ; cbn in *. + now do 2 (eapply over_tree_fusion_l). + rewrite e. - eapply LRTmEqRedConv. - 2: eapply eqsnd'. - eapply PolyRed.posExt. - 1: eapply (SigRedTm.fstRed tL). - eapply LRTmEqSym. rewrite <- e. - eapply eqfst. - now eapply over_tree_fusion_r, over_tree_fusion_l. - Unshelve. - now eapply over_tree_fusion_r. + eapply LRTmEqRedConv ; [ unshelve eapply PolyRed.posExt | unshelve eapply eqsnd']. + 7: eassumption. + 3: now do 2 (eapply over_tree_fusion_r). + * now eapply over_tree_fusion_l, over_tree_fusion_r. + * now eapply over_tree_fusion_r, over_tree_fusion_l. Qed. diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v index d62043c5..a49659ef 100644 --- a/theories/LogicalRelation/Weakening.v +++ b/theories/LogicalRelation/Weakening.v @@ -27,11 +27,14 @@ Section Weakenings. irrelevance. cbn. assumption. + - intros ?? a b ρ' **. + unshelve eapply (posExtTree _ k' a b (ρ' ∘w ρ) f) ; eauto. + all: now irrelevance. - now eapply wft_wk. - eapply wft_wk; tea; eapply wfc_cons; tea; now eapply wft_wk. - intros ?? a b ρ' wfΔ' ** ; cbn in *. replace (_[b .: ρ' >> tRel]) with (pos[ b .: (ρ' ∘w ρ) >> tRel]) by (now bsimpl). - unshelve epose (posExt _ _ a b (ρ' ∘w ρ) wfΔ' Hd _ _ _ k'' Ho) ; irrelevance. + unshelve epose (posExt _ _ a b (ρ' ∘w ρ) wfΔ' Hd _ _ _ k'' Hoa Hob Hoeq) ; irrelevance. Qed. Lemma wkΠ {wl Γ Δ A l} @@ -262,6 +265,10 @@ Lemma wkEq@{i j k l} {wl Γ Δ A B l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lr eapply DTree_fusion ; [apply (appTree _ _ a (ρ' ∘w ρ) f Hd) | eapply (PolyRed.posTree ΠA (ρ' ∘w ρ) f Hd)]. all: irrelevance0 ; [ | eassumption] . all: subst ΠA'; bsimpl; try rewrite scons_comp'; reflexivity. + - intros ? a b ? ρ' f Hd ha hb hab. + eapply DTree_fusion ; [apply (eqTree _ a b _ (ρ' ∘w ρ) f Hd) | eapply (PolyRed.posExtTree ΠA (a:= a) (b:= b) (ρ' ∘w ρ) f Hd)]. + all: irrelevance0 ; [ | eassumption] . + all: subst ΠA'; bsimpl; try rewrite scons_comp'; reflexivity. - now eapply redtmwf_wk. - now apply convtm_wk. - now apply isLRFun_ren. @@ -272,13 +279,15 @@ Lemma wkEq@{i j k l} {wl Γ Δ A B l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lr + subst ΠA'; bsimpl; try rewrite scons_comp'; reflexivity. + now eapply over_tree_fusion_r. + now eapply over_tree_fusion_l. - - intros ??? wl' ρ' f ??????? ; cbn in *. + - intros ??? wl' ρ' f ????????? ; cbn in *. replace ((t ⟨ρ⟩)⟨ ρ' ⟩) with (t⟨ρ' ∘w ρ⟩) by now bsimpl. irrelevance0. - 2: unshelve apply eq; [| | eassumption|..] ; auto ; try (subst ΠA'; irrelevance). + 2: unshelve eapply (eq _ a b) ; [| | eassumption|..] ; auto ; try (subst ΠA'; irrelevance). + subst ΠA'; bsimpl; try rewrite scons_comp'; reflexivity. + now eapply over_tree_fusion_r. + now eapply over_tree_fusion_l. + + now eapply over_tree_fusion_l. + + now eapply over_tree_fusion_l. Defined. diff --git a/theories/Monad.v b/theories/Monad.v index 89165e25..9e94d893 100644 --- a/theories/Monad.v +++ b/theories/Monad.v @@ -131,6 +131,21 @@ Inductive DTree (k : wfLCon) : Type := DTree (k ,,l (ne, false)) -> DTree k. +Fixpoint DTree_bind (k : wfLCon) (F : forall k' (f : k' ≤ε k), DTree k') + (d : DTree k) : DTree k. +Proof. + refine (match d with + | leaf _ => F k (wfLCon_le_id _) + | @ϝnode _ n ne dt df => @ϝnode _ n ne _ _ + end). + + unshelve eapply DTree_bind ; [ | assumption]. + intros k' f ; eapply F, wfLCon_le_trans ; [eassumption | ]. + now eapply LCon_le_step, wfLCon_le_id. + + unshelve eapply DTree_bind ; [ | assumption]. + intros k' f ; eapply F, wfLCon_le_trans ; [eassumption | ]. + now eapply LCon_le_step, wfLCon_le_id. +Defined. + Fixpoint DTree_Ltrans (k k' : wfLCon) (f : k' ≤ε k) (d : DTree k) : DTree k'. Proof. refine (match d with @@ -285,6 +300,143 @@ Qed. Arguments over_tree_fusion_l [_ _ _ _] _. Arguments over_tree_fusion_r [_ _ _ _] _. +Fixpoint DTree_bind_over (k : wfLCon) (d : DTree k) : + (forall k' (H : over_tree k k' d), DTree k') -> DTree k. +Proof. + refine (match d with + | leaf _ => fun F => _ + | @ϝnode _ n ne dt df => fun F => _ + end). + - now eapply F, wfLCon_le_id. + - eapply (@ϝnode _ n ne). + + unshelve eapply DTree_bind_over ; [ assumption | ]. + intros k' f ; eapply F. cbn in *. + now rewrite (@decidInLCon_true k' n (over_tree_le f _ _ (in_here_l _))). + + unshelve eapply DTree_bind_over ; [ assumption | ]. + intros k' f ; eapply F. cbn in *. + now rewrite (@decidInLCon_false k' n (over_tree_le f _ _ (in_here_l _))). +Defined. + +Lemma DTree_bind_over_over k k' d P : + over_tree k k' (DTree_bind_over k d P) -> + over_tree k k' d. +Proof. + induction d ; cbn in * ; intros H. + - now eapply over_tree_le. + - destruct (decidInLCon k' n) ; cbn in *. + + eapply IHd1. + eassumption. + + eapply IHd2. + eassumption. + + assumption. +Qed. + +Fixpoint DTree_path (k k' : wfLCon) (d : DTree k) : + over_tree k k' d -> wfLCon. +Proof. + refine (match d with + | leaf _ => fun H => k + | @ϝnode _ n ne dt df => _ + end). + cbn in *. + refine (match decidInLCon k' n with + | or_inltrue _ => _ + | or_inlfalse _ => _ + | or_notinl _ => _ + end). + all: refine (fun H => _). + 1,2: exact (DTree_path _ _ _ H). + now inversion H. +Defined. + +Lemma DTree_path_le k k' d (Hover : over_tree k k' d) : + (DTree_path k k' d Hover) ≤ε k. +Proof. + induction d ; cbn. + - now eapply wfLCon_le_id. + - cbn in *. + revert Hover ; destruct (decidInLCon k' n) ; intros Hover. + + eapply wfLCon_le_trans ; [eapply IHd1 | ]. + now eapply LCon_le_step, wfLCon_le_id. + + eapply wfLCon_le_trans ; [eapply IHd2 | ]. + now eapply LCon_le_step, wfLCon_le_id. + + now destruct Hover. +Qed. + +Fixpoint DTree_path_over k k' d : + forall Hover : over_tree k k' d, + over_tree k (DTree_path k k' d Hover) d. +Proof. + refine (match d as d0 return + forall Hover, + over_tree k (DTree_path k k' d0 Hover) d0 + with + | leaf _ => fun Hover => _ + | @ϝnode _ n ne dt df => _ + end). + - now eapply wfLCon_le_id. + - cbn in *. + destruct (decidInLCon k' n) ; cbn in * ; intros Hover. + + rewrite (decidInLCon_true (DTree_path_le _ k' dt Hover _ _ (in_here_l _))). + now eapply DTree_path_over. + + rewrite (decidInLCon_false (DTree_path_le _ k' df Hover _ _ (in_here_l _))). + now eapply DTree_path_over. + + now destruct Hover. +Defined. + +Lemma DTree_path_inf k k' d Hover : + k' ≤ε (DTree_path k k' d Hover). +Proof. + induction d as [ | k n ne kt IHt kf IHf] ; cbn in * ; [assumption | ]. + destruct (decidInLCon k' n) ; cbn in *. + - now apply IHt. + - now apply IHf. + - now inversion Hover. +Qed. + + +Lemma DTree_bind_DTree_path (k k' : wfLCon) (d : DTree k) + (P : forall k' (H : over_tree k k' d), DTree k') + (Hover : over_tree k k' d) + (Hover' : over_tree k k' (DTree_bind_over k d P)) : + over_tree (DTree_path k k' d Hover) k' (P _ (DTree_path_over k k' d Hover)). +Proof. + revert P Hover Hover'. + induction d as [ | k n ne kt IHt kf IHf] ; cbn in * ; intros. + - assumption. + - destruct (decidInLCon k' n) ; cbn in *. + + set (P' := fun (k' : wfLCon) (f : over_tree (k,,l (ne, true)) k' kt) => + P k' + (@eq_sind_r (or_inLCon k' n) + (@or_inltrue k' n + (@over_tree_le (k,,l (ne, true)) k' kt f n true (@in_here_l k n true))) + (fun o : or_inLCon k' n => + match o with + | @or_inltrue _ _ _ => over_tree (k,,l (ne, true)) k' kt + | @or_inlfalse _ _ _ => over_tree (k,,l (ne, false)) k' kf + | @or_notinl _ _ _ => SFalse + end) f (decidInLCon k' n) + (@decidInLCon_true k' n + (@over_tree_le (k,,l (ne, true)) k' kt f n true (@in_here_l k n true))))). + now eapply (IHt P' Hover Hover'). + + set (P' := fun (k' : wfLCon) (f : over_tree (k,,l (ne, false)) k' kf) => + P k' + (@eq_sind_r (or_inLCon k' n) + (@or_inlfalse k' n + (@over_tree_le (k,,l (ne, _)) k' kf f n _ (@in_here_l k n _))) + (fun o : or_inLCon k' n => + match o with + | @or_inltrue _ _ _ => over_tree (k,,l (ne, true)) k' kt + | @or_inlfalse _ _ _ => over_tree (k,,l (ne, false)) k' kf + | @or_notinl _ _ _ => SFalse + end) f (decidInLCon k' n) + (@decidInLCon_false k' n + (@over_tree_le (k,,l (ne, false)) k' kf f n _ (@in_here_l k n _))))). + now eapply (IHf P' Hover Hover'). + + now destruct Hover. +Qed. + + Lemma split_to_over_tree (P : wfLCon -> Type) (Pe : forall wl n (ne : not_in_LCon (pi1 wl) n), P (wl ,,l (ne, true)) -> P (wl ,,l (ne, false)) -> P wl)