From 98969e42e72520530d6d1d42ed0ff1bbc62afcb1 Mon Sep 17 00:00:00 2001 From: Martin Baillon Date: Mon, 29 Jan 2024 16:15:34 +0100 Subject: [PATCH] New notations + Monad definition --- theories/LContexts.v | 12 ++- theories/LogicalRelation.v | 31 +++++- theories/LogicalRelation/Application.v | 6 +- theories/LogicalRelation/Monad.v | 49 ---------- theories/LogicalRelation/Weakening.v | 13 ++- theories/LogicalRelation2.v | 11 ++- theories/Monad.v | 125 +++++++++++++++++++++++++ theories/Monad2.v | 21 +---- 8 files changed, 183 insertions(+), 85 deletions(-) delete mode 100644 theories/LogicalRelation/Monad.v create mode 100644 theories/Monad.v diff --git a/theories/LContexts.v b/theories/LContexts.v index 92817489..bdf03632 100644 --- a/theories/LContexts.v +++ b/theories/LContexts.v @@ -170,9 +170,13 @@ Notation " l ≤ε l' " := (wfLCon_le l l') (at level 40). Definition wfLCon_le_id l : l ≤ε l := fun n b ne => ne. +Notation " 'idε' " := (wfLCon_le_id) (at level 40). + Definition wfLCon_le_trans {l l' l''} : l ≤ε l' -> l' ≤ε l'' -> l ≤ε l'' := fun f f' n b ne => f n b (f' n b ne). +Notation " a •ε b " := (wfLCon_le_trans a b) (at level 40). + Lemma LCon_le_in_LCon {l l' n b} {ne : not_in_LCon (pi1 l') n} : l ≤ε l' -> in_LCon l n b -> l ≤ε (l' ,,l (ne , b)). Proof. @@ -527,7 +531,7 @@ Proof. | cons a q => _ end) ; intros. - refine (P wl _ _). - now eapply wfLCon_le_id. + now eapply (idε). eapply Lack_nil_AllInLCon. now symmetry. - refine (max _ _). @@ -542,9 +546,9 @@ Proof. now eapply Lack_n_add. * intros * τ allinl. refine (P wl' _ allinl). - eapply wfLCon_le_trans ; try eassumption. - eapply LCon_le_step. - now eapply wfLCon_le_id. + unshelve eapply (_ •ε _). + 3: eapply LCon_le_step ; now eapply wfLCon_le_id. + eassumption. + unshelve refine (Max_Bar_aux _ n q _ _). * unshelve eapply wfLCons ; [exact wl | exact a | | exact false]. eapply Lack_n_notinLCon. diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v index 7ec57b47..84d2281d 100644 --- a/theories/LogicalRelation.v +++ b/theories/LogicalRelation.v @@ -1,6 +1,6 @@ (** * LogRel.LogicalRelation: Definition of the logical relation *) From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping. +From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping Monad. Set Primitive Projections. Set Universe Polymorphism. @@ -272,7 +272,29 @@ Notation "[ R | Γ ||-U t ≅ u : A | l ]< wl >" := (URedTmEq R wl Γ t u A l) ( (** ** Reducibility of product types *) Module PiRedTy. - + Lemma ez `{ta : tag} + `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} + {l : wfLCon} {Γ : context} {A : term} : True. + Proof. + assert (dom : term) by admit. + assert (cod : term) by admit. + assert (domRed : forall Δ (ρ : Δ ≤ Γ), + Weak l (fun l' alpha => [ |- Δ ]< l' > -> LRPack l' Δ dom⟨ρ⟩)) by admit. + assert (Δ : context) by admit. + assert (ρ : Δ ≤ Γ) by admit. + + + pose (zfe := fun Q => BType l _ Q (domRed _ ρ) ) ; cbn in zfe. + assert ( forall wl' : wfLCon, + ([ |-[ ta ] Δ ]< wl' > -> LRPack wl' Δ dom⟨ρ⟩) -> Type). + intros wl' Dom. + refine (forall (Hd : [ |-[ ta ] Δ ]< wl' >), _). + refine (forall a : term, _). + refine (forall ha : [ Dom Hd | Δ ||- a : dom⟨ρ⟩]< wl' >, _). + refine (Dial wl' _). + intros wl''. + eapply LRPack. + exact wl''. Record PiRedTy@{i} `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} {l : wfLCon} {Γ : context} {A : term} @@ -283,9 +305,8 @@ Module PiRedTy. domTy : [Γ |- dom]< l >; codTy : [Γ ,, dom |- cod]< l > ; eq : [Γ |- tProd dom cod ≅ tProd dom cod]< l > ; - domN : nat ; - domRed {Δ l'} (ρ : Δ ≤ Γ) (τ : l' ≤ε l) (Ninfl : AllInLCon domN l') : - [ |- Δ ]< l' > -> LRPack@{i} l' Δ dom⟨ρ⟩ ; + dom {Δ} (ρ : Δ ≤ Γ) : Weak l (fun l' τ => [ |- Δ ]< l' > -> LRPack@{i} l' Δ dom⟨ρ⟩) ; + }. codomN {Δ a l'} (ρ : Δ ≤ Γ) (τ : l' ≤ε l) (Ninfl : AllInLCon domN l') (h : [ |- Δ ]< l' >) (ha : [ (domRed ρ τ Ninfl h) | Δ ||- a : dom⟨ρ⟩]< l' >) : diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Application.v index 8a8007e9..1f3fa200 100644 --- a/theories/LogicalRelation/Application.v +++ b/theories/LogicalRelation/Application.v @@ -123,6 +123,7 @@ Section AppTerm. refine (max (max (max RFN RuN) (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))) _). unshelve refine (Max_Bar _ _ _). + About Max_Bar_Bar_lub. + assumption. + exact (max (max RFN RuN) (max (PiRedTyPack.domN hΠ) (PiRedTm.redN Rt))). @@ -194,11 +195,6 @@ About AppTyN_subproof. now eapply Nat.le_max_l). + now eapply Bar_lub_ub. + now eapply Bar_lub_AllInLCon. - + clear Ninfl τ wl'. - (intros ; - rewrite (AllInLCon_Irrel _ _ ne0 ne') ; - rewrite (wfLCon_le_Irrel _ _ τ τ'); - reflexivity). } reflexivity. Defined. diff --git a/theories/LogicalRelation/Monad.v b/theories/LogicalRelation/Monad.v deleted file mode 100644 index 56a89b4c..00000000 --- a/theories/LogicalRelation/Monad.v +++ /dev/null @@ -1,49 +0,0 @@ -From LogRel.AutoSubst Require Import core unscoped Ast Extra. -Require Import PeanoNat. -From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping. - -Record Weak (wl : wfLCon) (P : wfLCon -> Type) : Type := - { PN : nat ; - WP : forall wl' : wfLCon, wl' ≤ε wl -> AllInLCon PN wl' -> P wl' ; - }. - -Definition Wret (wl : wfLCon) (P : wfLCon -> Type) - (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'') - (p : P wl) : Weak wl P. -Proof. - unshelve econstructor. - - exact 0. - - intros ; now eapply Pe. -Defined. - -Definition Wbind (wl : wfLCon) (P Q : wfLCon -> Type) - (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'') - (Qe : forall wl' wl'', wl'' ≤ε wl' -> Q wl' -> Q wl'') - (f : forall wl', wl' ≤ε wl -> P wl' -> Weak wl' Q) - (p : Weak wl P) : Weak wl Q. -Proof. - unshelve econstructor. - - unshelve refine (max (PN wl P p) (Max_Bar _ _ _)). - + exact wl. - + exact (PN _ _ p). - + intros wl' tau Ninfl. - eapply PN. - eapply f. - * eassumption. - * eapply WP ; try eassumption. - - intros wl' tau Ninfl. - unshelve eapply WP. - 4:{ eapply AllInLCon_le ; try eassumption. - etransitivity. - eapply (Max_Bar_Bar_lub _ _ - (fun wl'0 tau0 Ninfl0 => PN wl'0 Q (f wl'0 tau0 (WP wl P p wl'0 tau0 Ninfl0)))). - eapply Nat.le_max_r. - } - eapply Bar_lub_smaller. - Unshelve. - + eassumption. - + eapply AllInLCon_le ; try eassumption. - now eapply Nat.le_max_l. - + now eapply Bar_lub_ub. - + now eapply Bar_lub_AllInLCon. -Defined. diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v index 19df1cc3..fd19a02a 100644 --- a/theories/LogicalRelation/Weakening.v +++ b/theories/LogicalRelation/Weakening.v @@ -17,12 +17,14 @@ Section Weakenings. [Δ ||-Π< l > A⟨ρ⟩]< wl >. Proof. destruct ΠA as[dom cod]; cbn in *. - assert (domRed' : forall Δ' wl' (ρ' : Δ' ≤ Δ) (τ : wl' ≤ε wl) + unshelve refine (let domRed' : forall Δ' wl' (ρ' : Δ' ≤ Δ) (τ : wl' ≤ε wl) (Ninfl : AllInLCon domN wl'), - [|- Δ']< wl' > -> [Δ' ||-< l > dom⟨ρ⟩⟨ρ'⟩ ]< wl' >). + [|- Δ']< wl' > -> [Δ' ||-< l > dom⟨ρ⟩⟨ρ'⟩ ]< wl' > := _ in _). { - intros ? ? ρ' ??; replace (_⟨_⟩) with (dom⟨ρ' ∘w ρ⟩) by now bsimpl. - econstructor ; now unshelve eapply domRed. + intros ? ? ρ' ??. + replace (_⟨_⟩) with (dom⟨ρ' ∘w ρ⟩) by now bsimpl. + econstructor. + now unshelve eapply domRed. } set (cod' := cod⟨wk_up dom ρ⟩). unshelve refine @@ -144,7 +146,8 @@ Section Weakenings. + exact (dom⟨ρ⟩). + exact (cod⟨wk_up dom ρ⟩). + exact domN. - + unfold wkΠ'. intros ; unshelve eapply (codomN Δ0 a l' (ρ0 ∘w ρ) τ Ninfl Ninfl' h). + + unfold wkΠ'. + intros ; unshelve eapply (codomN Δ0 a l' (ρ0 ∘w ρ) τ Ninfl Ninfl' h). subst X. irrelevance. + change (tProd _ _) with ((tProd dom cod)⟨ρ⟩); gen_typing. diff --git a/theories/LogicalRelation2.v b/theories/LogicalRelation2.v index 3584ddbd..0c3e6e54 100644 --- a/theories/LogicalRelation2.v +++ b/theories/LogicalRelation2.v @@ -269,10 +269,10 @@ Export URedTm(URedTm,Build_URedTm,URedTmEq,Build_URedTmEq). Notation "[ R | Γ ||-U t : A | l ]< wl >" := (URedTm R wl Γ t A l) (at level 0, R, Γ, t, A, wl, l at level 50). Notation "[ R | Γ ||-U t ≅ u : A | l ]< wl >" := (URedTmEq R wl Γ t u A l) (at level 0, R, Γ, t, u, A, wl, l at level 50). + (** ** Reducibility of product types *) Module PiRedTy. - Print BType. Lemma ez `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} @@ -297,6 +297,15 @@ Module PiRedTy. exact wl''. exact Δ. exact (cod[a .: (ρ >> tRel)]). + + pose (Y := BType l _ (fun (wl' : wfLCon) (Dom : [ |-[ ta ] Δ ]< wl' > -> LRPack wl' Δ dom⟨ρ⟩) => + forall (Hd : [ |-[ ta ] Δ ]< wl' >) (a : term) + (ha : [ Dom Hd | Δ ||- a : dom⟨ρ⟩]< wl' >), + Dial wl' (fun wl'' => (LRPack wl'' Δ (cod[a .: (ρ >> tRel)])))) + (domRed _ ρ)). + cbn in Y. + pose (tzfd := zfe X). + apply zfe in X. pose (test:= fun R => BType_dep l _ (fun wl' Dom => forall (a : term) (Hd : [ |-[ ta ] Δ ]< wl' >) diff --git a/theories/Monad.v b/theories/Monad.v new file mode 100644 index 00000000..99001821 --- /dev/null +++ b/theories/Monad.v @@ -0,0 +1,125 @@ +From LogRel.AutoSubst Require Import core unscoped Ast Extra. +Require Import PeanoNat. +From LogRel Require Import Utils BasicAst Notations Context LContexts NormalForms Weakening GenericTyping. + +Record Psh (wl : wfLCon) := + { typ : forall wl', wl' ≤ε wl -> Type ; + mon : forall wl' wl'' (alpha : wl' ≤ε wl) (beta : wl'' ≤ε wl') + (delta : wl'' ≤ε wl), + typ wl' alpha -> typ wl'' delta + }. + +Arguments typ [_] _. +Arguments mon [_ _ _] _. + +Record Weak (wl : wfLCon) (P : forall wl', wl' ≤ε wl -> Type) : Type := + { PN : nat ; + WP : forall (wl' : wfLCon) (alpha : wl' ≤ε wl), + AllInLCon PN wl' -> P wl' alpha ; + }. + + +Lemma monot (wl wl' wl'' : wfLCon) + (P : forall wl', wl' ≤ε wl -> Type) + (alpha : wl' ≤ε wl) + (beta : wl'' ≤ε wl') : + Weak wl' (fun wl'' dzeta => P wl'' (dzeta •ε alpha)) -> + Weak wl'' (fun wl''' dzeta => P wl''' ((dzeta •ε beta) •ε alpha)). +Proof. + intros [N WN]. + exists N. + intros wl''' dzeta allinl. + exact (WN wl''' (dzeta •ε beta) allinl). +Qed. + + +Definition Wbind (wl : wfLCon) (P Q : forall wl', wl' ≤ε wl -> Type) + (Pe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl), + wl'' ≤ε wl' -> P wl' alpha -> P wl'' beta) + (Qe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl), + wl'' ≤ε wl' -> Q wl' alpha -> Q wl'' beta) + (f : forall wl' (alpha : wl' ≤ε wl), + P wl' alpha -> Weak wl' (fun wl'' beta => Q wl'' (beta •ε alpha))) : + forall wl' (alpha : wl' ≤ε wl), + Weak wl' (fun wl'' beta => P wl'' (beta •ε alpha)) -> + Weak wl' (fun wl'' beta => Q wl'' (beta •ε alpha)). +Proof. + intros * [N W]. + unshelve econstructor. + { unshelve eapply (max N _). + unshelve eapply Max_Bar. + - exact wl'. + - exact N. + - intros wl'' beta allinl. + unshelve eapply (f wl'' (beta •ε alpha)). + now eapply W. + } + intros wl'' beta allinl. + unshelve eapply Qe. + 4: unshelve eapply f. + { unshelve eapply (Bar_lub (Bar_lub wl' wl'' N beta _) wl''). + 3: now eapply Bar_lub_smaller. + 3: eassumption. + eapply AllInLCon_le. + eapply Nat.le_max_l. + eassumption. + } + + unshelve eapply Bar_lub_smaller. + + eapply (Bar_lub wl' wl'' N beta _). + + now eapply Bar_lub_ub. + + unshelve eapply (_ •ε alpha). + now eapply Bar_lub_ub. + + eapply W. + now eapply Bar_lub_AllInLCon. + + eapply AllInLCon_le ; [ | now eapply Bar_lub_AllInLCon]. + etransitivity ; [ |now eapply Nat.le_max_r]. + etransitivity ; [ | now eapply Max_Bar_Bar_lub]. + cbn. + reflexivity. +Qed. + + +Definition Wret (wl : wfLCon) (P : forall wl', wl' ≤ε wl -> Type) + (Pe : forall wl' (alpha : wl' ≤ε wl) wl'' (beta : wl'' ≤ε wl), + wl'' ≤ε wl' -> P wl' alpha -> P wl'' beta) + (p : P wl (idε wl)) : Weak wl P. +Proof. + unshelve econstructor. + - exact 0. + - intros ; now eapply Pe. +Defined. + + +(* +Definition Wbind (wl : wfLCon) (P Q : wfLCon -> Type) + (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'') + (Qe : forall wl' wl'', wl'' ≤ε wl' -> Q wl' -> Q wl'') + (f : forall wl', wl' ≤ε wl -> P wl' -> Weak wl' Q) + (p : Weak wl P) : Weak wl Q. +Proof. + unshelve econstructor. + - unshelve refine (max (PN wl P p) (Max_Bar _ _ _)). + + exact wl. + + exact (PN _ _ p). + + intros wl' tau Ninfl. + eapply PN. + eapply f. + * eassumption. + * eapply WP ; try eassumption. + - intros wl' tau Ninfl. + unshelve eapply WP. + 4:{ eapply AllInLCon_le ; try eassumption. + etransitivity. + eapply (Max_Bar_Bar_lub _ _ + (fun wl'0 tau0 Ninfl0 => PN wl'0 Q (f wl'0 tau0 (WP wl P p wl'0 tau0 Ninfl0)))). + eapply Nat.le_max_r. + } + eapply Bar_lub_smaller. + Unshelve. + + eassumption. + + eapply AllInLCon_le ; try eassumption. + now eapply Nat.le_max_l. + + now eapply Bar_lub_ub. + + now eapply Bar_lub_AllInLCon. +Defined. +*) diff --git a/theories/Monad2.v b/theories/Monad2.v index 203a5097..9852306c 100644 --- a/theories/Monad2.v +++ b/theories/Monad2.v @@ -32,30 +32,19 @@ Proof. now eapply wfLCon_le_id. Qed. -(*Fixpoint BType (wl : wfLCon) (P : wfLCon -> Type) - (Pe : forall wl' wl'', wl'' ≤ε wl' -> P wl' -> P wl'') +Fixpoint BType (wl : wfLCon) (P : wfLCon -> Type) (Q : forall wl', P wl' -> Type) - (Qe : forall wl' wl'' (f : wl'' ≤ε wl') (p : P wl') (p' : P wl''), - Q wl' p -> Q wl'' p') - (p : Dial wl P) : Type. -Proof. - refine ( match p with - | eta _ _ x => _ - | ϝdig _ _ pt pf => _ - end). - - clear p. - - := + (p : Dial wl P) : Type := match p with | eta _ _ x => Q wl x - | ϝdig _ _ pt pf => prod (BType _ P Q pt) (BType _ P Q pf) + | ϝdig _ _ pt pf => prod (@BType _ P Q pt) (BType _ P Q pf) end. -Fixpoint BType_dep (wl : wfLCon) (P : wfLCon -> Type) +(*Fixpoint BType_dep (wl : wfLCon) (P : wfLCon -> Type) (Q : forall wl', P wl' -> Type) (R : forall wl' p, Q wl' p -> Type) (p : Dial wl P) : - BType wl P Q p -> Type := + BType wl P Pe Q Qe p -> Type := match p with | eta _ _ x => fun H => R wl x H | ϝdig _ _ pt pf => fun H => prod (BType_dep _ P Q R pt (fst H))