From c672358cfa131f39c2edee0c83d76a8069cc9838 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sun, 16 Jul 2023 17:14:01 +0200 Subject: [PATCH] factor out the representation of bunches better - make sure that we reuse the syntax of bunches in the s4 formalization --- _CoqProject | 12 +- theories/analytic_completion.v | 2 +- theories/bunch_decomp.v | 2 +- theories/bunches.v | 266 ++++ theories/cutelim.v | 20 +- theories/formula.v | 50 + theories/interp.v | 112 +- theories/{cutelim_s4.v => s4/cutelim.v} | 59 +- theories/s4/formula.v | 52 + theories/{interp_s4.v => s4/interp.v} | 129 +- theories/s4/seqcalc.v | 152 ++ theories/s4/seqcalc_height.v | 1037 +++++++++++++ theories/seqcalc.v | 8 +- theories/seqcalc_height.v | 2 +- theories/seqcalc_height_s4.v | 1785 ----------------------- theories/seqcalc_s4.v | 453 ------ theories/syntax.v | 153 -- theories/terms.v | 10 +- 18 files changed, 1647 insertions(+), 2657 deletions(-) create mode 100644 theories/bunches.v create mode 100644 theories/formula.v rename theories/{cutelim_s4.v => s4/cutelim.v} (95%) create mode 100644 theories/s4/formula.v rename theories/{interp_s4.v => s4/interp.v} (62%) create mode 100644 theories/s4/seqcalc.v create mode 100644 theories/s4/seqcalc_height.v delete mode 100644 theories/seqcalc_height_s4.v delete mode 100644 theories/seqcalc_s4.v delete mode 100644 theories/syntax.v diff --git a/_CoqProject b/_CoqProject index 95737ed..d086cea 100644 --- a/_CoqProject +++ b/_CoqProject @@ -10,7 +10,8 @@ theories/algebra/derived_laws.v theories/algebra/bi.v theories/algebra/from_monoid.v theories/algebra/from_closure.v -theories/syntax.v +theories/bunches.v +theories/formula.v theories/terms.v theories/analytic_completion.v theories/bunch_decomp.v @@ -19,8 +20,9 @@ theories/interp.v theories/seqcalc_height.v theories/cutelim.v -theories/seqcalc_s4.v -theories/interp_s4.v -theories/seqcalc_height_s4.v -theories/cutelim_s4.v +theories/s4/formula.v +theories/s4/seqcalc.v +theories/s4/interp.v +theories/s4/seqcalc_height.v +theories/s4/cutelim.v diff --git a/theories/analytic_completion.v b/theories/analytic_completion.v index 124f57e..633ca8d 100644 --- a/theories/analytic_completion.v +++ b/theories/analytic_completion.v @@ -1,7 +1,7 @@ (** Analytic completion of a structural rule *) From Coq Require Import ssreflect. From bunched.algebra Require Import bi. -From bunched Require Import syntax interp terms prelude.sets. +From bunched Require Import bunches terms prelude.sets. From stdpp Require Import prelude base gmap fin_sets. Section analytic_completion. diff --git a/theories/bunch_decomp.v b/theories/bunch_decomp.v index b4e9999..713563e 100644 --- a/theories/bunch_decomp.v +++ b/theories/bunch_decomp.v @@ -1,7 +1,7 @@ (** Inductive representation for decomposition of bunches, and associated properties *) From Coq Require Import ssreflect. From stdpp Require Import prelude gmap functions. -From bunched Require Export syntax terms. +From bunched Require Export bunches terms. (** * Alternative representation of decomposition of bunches *) (** We have an inductive type that characterizes when a bunch can be diff --git a/theories/bunches.v b/theories/bunches.v new file mode 100644 index 0000000..f91795c --- /dev/null +++ b/theories/bunches.v @@ -0,0 +1,266 @@ +(* Bunches *) +From Coq Require Import ssreflect. +From stdpp Require Import prelude gmap fin_sets. +From bunched.algebra Require Import bi. + +Declare Scope bunch_scope. +Delimit Scope bunch_scope with B. + +(** * Generic syntax for bunches *) +Inductive sep := Comma | SemiC. + +Inductive bunch {formula : Type} : Type := +| frml (ϕ : formula) +| bnul (s : sep) +| bbin (s : sep) (Δ Γ : bunch) +. + +(* Definition semic {frml} (Δ Γ : @bunch frml) := bbin SemiC Δ Γ. *) +(* Definition comma {frml} (Δ Γ : @bunch frml) := bbin Comma Δ Γ. *) +(* Definition top {frml} : @bunch frml := bnul SemiC. *) +(* Definition empty {frml} : @bunch frml := bnul Comma. *) + +Notation "∅ₐ" := (bnul SemiC) : bunch_scope. +Notation "∅ₘ" := (bnul Comma) : bunch_scope. +Notation "Δ ';,' Γ" := (bbin SemiC Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. +Notation "Δ ',,' Γ" := (bbin Comma Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. + +(** ** Bunched contexts with a hole *) +Inductive bunch_ctx_item {frml : Type} : Type := +| CtxL (s : sep) (Δ2 : @bunch frml) +| CtxR (s : sep) (Δ1 : @bunch frml) +. + +Definition CtxCommaL {frml} (Δ2 : bunch) : @bunch_ctx_item frml + := CtxL Comma Δ2. +Definition CtxSemicL {frml} (Δ2 : bunch) : @bunch_ctx_item frml + := CtxL SemiC Δ2. +Definition CtxCommaR {frml} (Δ1 : bunch) : @bunch_ctx_item frml + := CtxR Comma Δ1. +Definition CtxSemicR {frml} (Δ1 : bunch) : @bunch_ctx_item frml + := CtxR SemiC Δ1. + +Definition bunch_ctx {frml} := list (@bunch_ctx_item frml). + +Definition fill_item {frml} (F : @bunch_ctx_item frml) (Δ : bunch) : bunch := + match F with + | CtxL s Δ2 => bbin s Δ Δ2 + | CtxR s Δ1 => bbin s Δ1 Δ + end. + +Definition fill {frml} (Π : @bunch_ctx frml) (Δ : bunch) : bunch := + foldl (flip fill_item) Δ Π. + +#[global] Instance bunch_fmap : FMap (@bunch) := + fix go A B f Δ {struct Δ} := let _ : FMap (@bunch) := @go in + match Δ with + | bnul s => bnul s + | bbin s Δ Δ' => bbin s (fmap f Δ) (fmap f Δ') + | frml ϕ => frml (f ϕ) + end%B. + +Definition bunch_ctx_item_map {A B} (f : A → B) (F : @bunch_ctx_item A) := + match F with + | CtxL s Δ => CtxL s (f <$> Δ) + | CtxR s Δ => CtxR s (f <$> Δ) + end. + +Definition bunch_ctx_map {A B} (f : A → B) (Π : @bunch_ctx A) := map (bunch_ctx_item_map f) Π. + + +(** ** Bunch equivalence *) +(** Equivalence on bunches is defined to be the least congruence + that satisfies the monoidal laws for (empty and comma) and (top + and semicolon). *) +Inductive bunch_equiv {frml} : @bunch frml → @bunch frml → Prop := +| BE_refl Δ : Δ =? Δ +| BE_sym Δ1 Δ2 : Δ1 =? Δ2 → Δ2 =? Δ1 +| BE_trans Δ1 Δ2 Δ3 : Δ1 =? Δ2 → Δ2 =? Δ3 → Δ1 =? Δ3 +| BE_cong C Δ1 Δ2 : Δ1 =? Δ2 → fill C Δ1 =? fill C Δ2 +| BE_unit_l s Δ : bbin s (bnul s) Δ =? Δ +| BE_comm s Δ1 Δ2 : bbin s Δ1 Δ2 =? bbin s Δ2 Δ1 +| BE_assoc s Δ1 Δ2 Δ3 : bbin s Δ1 (bbin s Δ2 Δ3) =? bbin s (bbin s Δ1 Δ2) Δ3 +where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B). + +(** Register [bunch_equiv] as [(≡)] *) +#[export] Instance equiv_bunch_equiv frml : Equiv (@bunch frml) := bunch_equiv. + +(** * Properties *) + +#[export] Instance equivalence_bunch_equiv frml : Equivalence ((≡@{@bunch frml})). +Proof. + repeat split. + - intro x. econstructor. + - intros x y Hxy. by econstructor. + - intros x y z Hxy Hyz. by econstructor. +Qed. + +#[export] Instance bbin_comm frml s : Comm (≡@{@bunch frml}) (bbin s). +Proof. intros X Y. apply BE_comm. Qed. +#[export] Instance bbin_assoc frml s : Assoc (≡@{@bunch frml}) (bbin s). +Proof. intros X Y Z. apply BE_assoc. Qed. +#[export] Instance bbin_leftid frml s : LeftId (≡@{@bunch frml}) (bnul s) (bbin s). +Proof. intros X. apply BE_unit_l. Qed. +#[export] Instance bbin_rightid frml s : RightId (≡@{@bunch frml}) (bnul s) (bbin s). +Proof. intros X. rewrite comm. apply BE_unit_l. Qed. + +#[export] Instance fill_proper frml Π : Proper ((≡) ==> (≡@{@bunch frml})) (fill Π). +Proof. intros X Y. apply BE_cong. Qed. + +#[export] Instance bbin_proper frml s : Proper ((≡) ==> (≡) ==> (≡@{@bunch frml})) (bbin s). +Proof. + intros Δ1 Δ2 H Δ1' Δ2' H'. + change ((fill [CtxL s Δ1'] Δ1) ≡ (fill [CtxL s Δ2'] Δ2)). + etrans. + { eapply BE_cong; eauto. } + simpl. + change ((fill [CtxR s Δ2] Δ1') ≡ (fill [CtxR s Δ2] Δ2')). + eapply BE_cong; eauto. +Qed. + +Lemma fill_app {frml} (Π Π' : @bunch_ctx frml) (Δ : bunch) : + fill (Π ++ Π') Δ = fill Π' (fill Π Δ). +Proof. by rewrite /fill foldl_app. Qed. + +Lemma bunch_map_fill {A B} (f : A → B) Π Δ : + f <$> (fill Π Δ) = fill (bunch_ctx_map f Π) (f <$> Δ). +Proof. + revert Δ. induction Π as [|F Π IH] =>Δ/=//. + rewrite IH. f_equiv. by destruct F; simpl. +Qed. + +Global Instance bunch_map_proper {A B} (f : A → B) : Proper ((≡) ==> (≡@{bunch})) (fmap f). +Proof. + intros Δ1 Δ2 HD. induction HD; simpl; eauto. + - etrans; eauto. + - rewrite !bunch_map_fill. by f_equiv. + - by rewrite left_id. + - by rewrite comm. + - by rewrite assoc. +Qed. + +Section interp. + Variable (PROP : bi). + Context {formula : Type}. + Notation bunch := (@bunch formula). + Notation bunch_ctx := (@bunch_ctx formula). + + Implicit Types (A B C : PROP). + Implicit Type Δ : bunch. + Implicit Type Π : bunch_ctx. + + Variable (i : formula → PROP). + + Definition sep_interp (sp : sep) : PROP → PROP → PROP := + match sp with + | Comma => (∗) + | SemiC => (∧) + end%I. + #[export] Instance sep_interp_proper sp : Proper ((≡) ==> (≡) ==> (≡)) (sep_interp sp). + Proof. destruct sp; apply _. Qed. + #[export] Instance sep_interp_mono sp : Proper ((⊢) ==> (⊢) ==> (⊢)) (sep_interp sp). + Proof. destruct sp; apply _. Qed. + + Fixpoint bunch_interp (Δ : bunch) : PROP := + match Δ with + | frml ϕ => i ϕ + | ∅ₐ => True + | ∅ₘ => emp + | bbin sp Δ Δ' => sep_interp sp (bunch_interp Δ) (bunch_interp Δ') + end%B%I. + + Definition bunch_ctx_item_interp (F : bunch_ctx_item) : PROP → PROP := + λ P, match F with + | CtxL sp Δ => sep_interp sp P (bunch_interp Δ) + | CtxR sp Δ => sep_interp sp (bunch_interp Δ) P + end%I. + + Definition bunch_ctx_interp Π : PROP → PROP := + λ P, foldl (flip bunch_ctx_item_interp) P Π. + + Lemma bunch_ctx_interp_cons F Π A : + bunch_ctx_interp (F::Π) A = bunch_ctx_interp Π (bunch_ctx_item_interp F A). + Proof. reflexivity. Qed. + + Global Instance bunch_ctx_interp_proper Π : Proper ((≡) ==> (≡)) (bunch_ctx_interp Π). + Proof. + induction Π as [|F Π]=>X Y HXY. + - simpl; auto. + - simpl. + eapply IHΠ. + destruct F; solve_proper. + Qed. + + Lemma bunch_ctx_interp_decomp Π Δ : + bunch_interp (fill Π Δ) ≡ bunch_ctx_interp Π (bunch_interp Δ). + Proof. + revert Δ. induction Π as [|C Π IH]=>Δ; first by reflexivity. + apply bi.equiv_entails_2. + - destruct C; simpl; by rewrite IH. + - destruct C; simpl; by rewrite IH. + Qed. + + Lemma bunch_interp_fill_item_mono (C : bunch_ctx_item) Δ Δ' : + (bunch_interp Δ ⊢ bunch_interp Δ') → + bunch_interp (fill_item C Δ) ⊢ bunch_interp (fill_item C Δ'). + Proof. + intros H1. + induction C as [ sp ? | sp ? ]; simpl; by rewrite H1. + Qed. + + Lemma bunch_interp_fill_mono Π Δ Δ' : + (bunch_interp Δ ⊢ bunch_interp Δ') → + bunch_interp (fill Π Δ) ⊢ bunch_interp (fill Π Δ'). + Proof. + revert Δ Δ'. + induction Π as [|C Π IH]=> Δ Δ' H1; eauto. + simpl. apply IH. + by apply bunch_interp_fill_item_mono. + Qed. + + Lemma bunch_ctx_interp_exist Π {I} (P : I → PROP) : + bunch_ctx_interp Π (∃ (i : I), P i : PROP)%I ≡ + (∃ i, bunch_ctx_interp Π (P i))%I. + Proof. + revert P. induction Π as [|F Π]=>P. + { simpl. reflexivity. } + rewrite bunch_ctx_interp_cons. + Opaque bunch_ctx_interp. + destruct F as [sp ?|sp ?]; destruct sp; simpl. + + rewrite bi.sep_exist_r. + apply (IHΠ (λ i, P i ∗ bunch_interp Δ2)%I). + + rewrite bi.and_exist_r. + apply (IHΠ (λ i, P i ∧ bunch_interp Δ2)%I). + + rewrite bi.sep_exist_l. + apply (IHΠ (λ i, bunch_interp Δ1 ∗ P i)%I). + + rewrite bi.and_exist_l. + apply (IHΠ (λ i, bunch_interp Δ1 ∧ P i)%I). + Qed. + + Global Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp. + Proof. + intros Δ1 Δ2. induction 1; eauto. + - etrans; eassumption. + - apply bi.equiv_entails_2. + + apply bunch_interp_fill_mono; eauto. + by apply bi.equiv_entails_1_1. + + apply bunch_interp_fill_mono; eauto. + by apply bi.equiv_entails_1_2. + - simpl. destruct s; by rewrite left_id. + - simpl. destruct s; by rewrite comm. + - simpl. destruct s; by rewrite assoc. + Qed. + + Global Instance bunch_ctx_interp_mono Π : Proper ((⊢) ==> (⊢)) (bunch_ctx_interp Π). + Proof. + induction Π as [|F Π]=>P1 P2 HP; first by simpl; auto. + rewrite !bunch_ctx_interp_cons. + apply IHΠ. + destruct F as [[|] ? | [|] ?]; simpl; f_equiv; eauto. + Qed. + +End interp. + +Arguments sep_interp {_} _ _ _. +Arguments bunch_interp {_ _} _ _. + diff --git a/theories/cutelim.v b/theories/cutelim.v index 2719da0..4bdc373 100644 --- a/theories/cutelim.v +++ b/theories/cutelim.v @@ -2,7 +2,7 @@ From Coq Require Import ssreflect. From stdpp Require Import prelude gmap. From bunched.algebra Require Import bi from_monoid from_closure. -From bunched Require Import seqcalc seqcalc_height interp terms syntax. +From bunched Require Import seqcalc seqcalc_height. (** * Parameters to the proof: a list of simple structural extensions *) Parameter rules : list structural_rule. @@ -85,7 +85,7 @@ Lemma C_collapse (X : C) Γ Δ : Proof. intros HX. apply C_intro=>ϕ Hϕ. - apply collapse_l. by apply (Hϕ _). + apply BI_Collapse_L. by apply (Hϕ _). Qed. Lemma C_collapse_inv (X : C) Γ Δ : @@ -93,7 +93,7 @@ Lemma C_collapse_inv (X : C) Γ Δ : Proof. intros HX. apply C_intro=>ϕ Hϕ. - apply collapse_l_inv. by apply (Hϕ _). + apply BI_Collapse_L_inv. by apply (Hϕ _). Qed. (** Some calculations in the model. *) @@ -414,19 +414,19 @@ Proof. { intros Δ [H1 H2] ϕ Hϕ. eapply (BI_Contr []) ; simpl. simpl in *. - apply (collapse_l_inv ([CtxSemicR Δ])). + apply (BI_Collapse_L_inv ([CtxSemicR Δ])). simpl. apply impl_r_inv. eapply H1. intros Δ1 HΔ1. simpl. apply BI_Impl_R. rewrite comm. - apply (collapse_l [CtxSemicL Δ1]). simpl. - apply (collapse_l_inv ([CtxSemicR Δ])). simpl. + apply (BI_Collapse_L [CtxSemicL Δ1]). simpl. + apply (BI_Collapse_L_inv ([CtxSemicR Δ])). simpl. apply impl_r_inv. eapply H2. intros Δ2 HΔ2. simpl. apply BI_Impl_R. rewrite comm. - apply (collapse_l [CtxSemicL Δ2]). simpl. + apply (BI_Collapse_L [CtxSemicL Δ2]). simpl. eapply (Hϕ _). destruct HΔ1 as (Δs1 & HΔs1 & HDs1eq). destruct HΔ2 as (Δs2 & HΔs2 & HDs2eq). @@ -511,9 +511,9 @@ Proof. { apply C_extensions. } intros H2%(seq_interp_sound (PROP:=C_alg) C_atom); last first. { apply C_extensions. } - change (seq_interp C_atom Δ ψ) with (bunch_interp C_atom Δ ⊢@{C_alg} formula_interp C_atom ψ) in H1. + change (seq_interp C_atom Δ ψ) with (bunch_interp (formula_interp C_atom) Δ ⊢@{C_alg} formula_interp C_atom ψ) in H1. change (seq_interp C_atom (fill Γ (frml ψ)) ϕ) with - (bunch_interp C_atom (fill Γ (frml ψ)) ⊢@{C_alg} formula_interp C_atom ϕ) in H2. + (bunch_interp (formula_interp C_atom) (fill Γ (frml ψ)) ⊢@{C_alg} formula_interp C_atom ϕ) in H2. apply C_interp_cf. unfold seq_interp. etrans; last apply H2. @@ -522,4 +522,4 @@ Proof. Qed. (* Print Assumptions cut. *) -(* ==> Depends only on rules and rules_good *) +(* ==> Depends only on `rules` and `rules_good` *) diff --git a/theories/formula.v b/theories/formula.v new file mode 100644 index 0000000..3bcaa9b --- /dev/null +++ b/theories/formula.v @@ -0,0 +1,50 @@ +From Coq Require Import ssreflect. +From stdpp Require Import prelude gmap fin_sets. +From bunched.algebra Require Import bi. +From bunched Require Import bunches. + +(** * Formulas *) +Definition atom := nat. + +Inductive formula : Type := +| TOP +| EMP +| BOT +| ATOM (A : atom) +| CONJ (ϕ ψ : formula) +| DISJ (ϕ ψ : formula) +| SEP (ϕ ψ : formula) +| IMPL (ϕ ψ : formula) +| WAND (ϕ ψ : formula) +. + +(** "Collapse" internalizes the bunch as a formula. *) +Fixpoint collapse (Δ : @bunch formula) : formula := + match Δ with + | frml ϕ => ϕ + | ∅ₐ => TOP + | ∅ₘ => EMP + | Δ ,, Δ' => SEP (collapse Δ) (collapse Δ') + | Δ ;, Δ' => CONJ (collapse Δ) (collapse Δ') + end%B. + +Inductive collapse_gr : @bunch formula → formula → Prop := +| collapse_frml ϕ : collapse_gr (frml ϕ) ϕ +| collapse_top : collapse_gr ∅ₐ%B TOP +| collapse_emp : collapse_gr ∅ₘ%B EMP +| collapse_sep Δ1 Δ2 ϕ1 ϕ2 : + collapse_gr Δ1 ϕ1 → + collapse_gr Δ2 ϕ2 → + collapse_gr (Δ1 ,, Δ2)%B (SEP ϕ1 ϕ2) +| collapse_conj Δ1 Δ2 ϕ1 ϕ2 : + collapse_gr Δ1 ϕ1 → + collapse_gr Δ2 ϕ2 → + collapse_gr (Δ1 ;, Δ2)%B (CONJ ϕ1 ϕ2) +. + +Lemma collapse_gr_sound Δ : collapse_gr Δ (collapse Δ). +Proof. induction Δ; simpl; try destruct s; try by econstructor. Qed. + +Lemma collapse_gr_complete Δ ϕ : collapse_gr Δ ϕ → collapse Δ = ϕ. +Proof. induction 1; simpl; subst; eauto. Qed. + diff --git a/theories/interp.v b/theories/interp.v index c213649..63bd0d4 100644 --- a/theories/interp.v +++ b/theories/interp.v @@ -1,7 +1,7 @@ From Coq Require Import ssreflect. From bunched.algebra Require Import bi. From stdpp Require Import prelude. -From bunched Require Import syntax. +From bunched Require Import bunches formula. (** * Interpretation of BI intro the associated algebras *) @@ -31,23 +31,7 @@ Section interp. | WAND ϕ ψ => formula_interp ϕ -∗ formula_interp ψ end%I. - Definition sep_interp (sp : sep) : PROP → PROP → PROP := - match sp with - | Comma => (∗) - | SemiC => (∧) - end%I. - #[export] Instance sep_interp_proper sp : Proper ((≡) ==> (≡) ==> (≡)) (sep_interp sp). - Proof. destruct sp; apply _. Qed. - #[export] Instance sep_interp_mono sp : Proper ((⊢) ==> (⊢) ==> (⊢)) (sep_interp sp). - Proof. destruct sp; apply _. Qed. - - Fixpoint bunch_interp (Δ : bunch) : PROP := - match Δ with - | frml ϕ => formula_interp ϕ - | ∅ₐ => True - | ∅ₘ => emp - | bbin sp Δ Δ' => sep_interp sp (bunch_interp Δ) (bunch_interp Δ') - end%B%I. + Notation bunch_interp := (bunch_interp formula_interp). Lemma bunch_interp_collapse Δ : bunch_interp Δ = formula_interp (collapse Δ). @@ -60,96 +44,6 @@ Section interp. Definition seq_interp Δ ϕ : Prop := (bunch_interp Δ ⊢ formula_interp ϕ). - Definition bunch_ctx_item_interp (F : bunch_ctx_item) : PROP → PROP := - λ P, match F with - | CtxL sp Δ => sep_interp sp P (bunch_interp Δ) - | CtxR sp Δ => sep_interp sp (bunch_interp Δ) P - end%I. - - Definition bunch_ctx_interp Π : PROP → PROP := - λ P, foldl (flip bunch_ctx_item_interp) P Π. - - Lemma bunch_ctx_interp_cons F Π A : - bunch_ctx_interp (F::Π) A = bunch_ctx_interp Π (bunch_ctx_item_interp F A). - Proof. reflexivity. Qed. - - Global Instance bunch_ctx_interp_proper Π : Proper ((≡) ==> (≡)) (bunch_ctx_interp Π). - Proof. - induction Π as [|F Π]=>X Y HXY. - - simpl; auto. - - simpl. - eapply IHΠ. - destruct F; solve_proper. - Qed. - - Lemma bunch_ctx_interp_decomp Π Δ : - bunch_interp (fill Π Δ) ≡ bunch_ctx_interp Π (bunch_interp Δ). - Proof. - revert Δ. induction Π as [|C Π IH]=>Δ; first by reflexivity. - apply bi.equiv_entails_2. - - destruct C; simpl; by rewrite IH. - - destruct C; simpl; by rewrite IH. - Qed. - - Lemma bunch_interp_fill_item_mono (C : bunch_ctx_item) Δ Δ' : - (bunch_interp Δ ⊢ bunch_interp Δ') → - bunch_interp (fill_item C Δ) ⊢ bunch_interp (fill_item C Δ'). - Proof. - intros H1. - induction C as [ sp ? | sp ? ]; simpl; by rewrite H1. - Qed. - - Lemma bunch_interp_fill_mono Π Δ Δ' : - (bunch_interp Δ ⊢ bunch_interp Δ') → - bunch_interp (fill Π Δ) ⊢ bunch_interp (fill Π Δ'). - Proof. - revert Δ Δ'. - induction Π as [|C Π IH]=> Δ Δ' H1; eauto. - simpl. apply IH. - by apply bunch_interp_fill_item_mono. - Qed. - - Lemma bunch_ctx_interp_exist Π {I} (P : I → PROP) : - bunch_ctx_interp Π (∃ (i : I), P i : PROP)%I ≡ - (∃ i, bunch_ctx_interp Π (P i))%I. - Proof. - revert P. induction Π as [|F Π]=>P. - { simpl. reflexivity. } - rewrite bunch_ctx_interp_cons. - Opaque bunch_ctx_interp. - destruct F as [sp ?|sp ?]; destruct sp; simpl. - + rewrite bi.sep_exist_r. - apply (IHΠ (λ i, P i ∗ bunch_interp Δ2)%I). - + rewrite bi.and_exist_r. - apply (IHΠ (λ i, P i ∧ bunch_interp Δ2)%I). - + rewrite bi.sep_exist_l. - apply (IHΠ (λ i, bunch_interp Δ1 ∗ P i)%I). - + rewrite bi.and_exist_l. - apply (IHΠ (λ i, bunch_interp Δ1 ∧ P i)%I). - Qed. - - Global Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp. - Proof. - intros Δ1 Δ2. induction 1; eauto. - - etrans; eassumption. - - apply bi.equiv_entails_2. - + apply bunch_interp_fill_mono; eauto. - by apply bi.equiv_entails_1_1. - + apply bunch_interp_fill_mono; eauto. - by apply bi.equiv_entails_1_2. - - simpl. destruct s0; by rewrite left_id. - - simpl. destruct s0; by rewrite comm. - - simpl. destruct s0; by rewrite assoc. - Qed. - - Global Instance bunch_ctx_interp_mono Π : Proper ((⊢) ==> (⊢)) (bunch_ctx_interp Π). - Proof. - induction Π as [|F Π]=>P1 P2 HP; first by simpl; auto. - rewrite !bunch_ctx_interp_cons. - apply IHΠ. - destruct F as [[|] ? | [|] ?]; simpl; f_equiv; eauto. - Qed. - Global Instance seq_interp_proper : Proper ((≡) ==> (=) ==> (≡)) seq_interp. Proof. intros Δ1 Δ2 HΔ ϕ ? <-. rewrite /seq_interp /=. @@ -159,6 +53,4 @@ Section interp. End interp. Arguments formula_interp {_} _ _. -Arguments bunch_interp {_} _ _. Arguments seq_interp {_} _ _ _. -Arguments sep_interp {_} _ _ _. diff --git a/theories/cutelim_s4.v b/theories/s4/cutelim.v similarity index 95% rename from theories/cutelim_s4.v rename to theories/s4/cutelim.v index d4bd655..9904f9a 100644 --- a/theories/cutelim_s4.v +++ b/theories/s4/cutelim.v @@ -2,7 +2,10 @@ From Coq Require Import ssreflect. From stdpp Require Import prelude. From bunched.algebra Require Import bi. -From bunched Require Import seqcalc_height_s4 seqcalc_s4 interp_s4. +From bunched.s4 Require Import formula seqcalc_height seqcalc interp. +From bunched Require Import bunches. +Notation bunch := (@bunch formula). + (** The first algebra that we consider is a purely "combinatorial" one: predicates [(bunch/≡) → Prop] *) @@ -38,7 +41,7 @@ Module PB. Qed. Program Definition PB_emp : PB := - {| PBPred := (λ Δ, Δ ≡ empty) |}. + {| PBPred := (λ Δ, Δ ≡ ∅ₘ)%B |}. Next Obligation. solve_proper. Qed. Program Definition PB_sep (X Y : PB) : PB := @@ -85,7 +88,7 @@ Module PB. Lemma emp_sep_1 P : P ⊢ emp ∗ P. Proof. intros Δ HP. compute. - eexists empty%B,_. repeat split. + eexists ∅ₘ%B,_. repeat split. - done. - eapply HP. - by rewrite left_id. @@ -271,7 +274,7 @@ Module Cl. Qed. Lemma C_necessitate (X : C) Δ : - X Δ → X (bunch_map BOX Δ). + X Δ → X (fmap BOX Δ). Proof. destruct X as [X Xcl]. simpl. intros HX. rewrite Xcl. @@ -280,7 +283,7 @@ Module Cl. Qed. Lemma C_bunch_box_idemp (X : C) Δ : - X (bunch_map BOX (bunch_map BOX Δ)) → X (bunch_map BOX Δ). + X (fmap BOX (fmap BOX Δ)) → X (fmap BOX Δ). Proof. destruct X as [X Xcl]. simpl. intros HX. rewrite Xcl. @@ -314,19 +317,17 @@ Module Cl. destruct X as [X Xcl]. simpl. revert Γ. induction Δ=>Γ; simpl; eauto. - intros HX. rewrite Xcl=>ϕ Hϕ. - by apply BI_True_L, Hϕ. - - intros HX. rewrite Xcl=>ϕ Hϕ. - by apply BI_Emp_L, Hϕ. - - intros HX. rewrite Xcl=>ϕ Hϕ. - apply BI_Sep_L, Hϕ. - apply (IHΔ1 (CtxCommaL _::Γ)); simpl. - apply (IHΔ2 (CtxCommaR _::Γ)); simpl. - apply HX. + destruct s; by econstructor; apply Hϕ. - intros HX. rewrite Xcl=>ϕ Hϕ. - apply BI_Conj_L, Hϕ. - apply (IHΔ1 (CtxSemicL _::Γ)); simpl. - apply (IHΔ2 (CtxSemicR _::Γ)); simpl. - apply HX. + destruct s. + + apply BI_Sep_L, Hϕ. + apply (IHΔ1 (CtxCommaL _::Γ)); simpl. + apply (IHΔ2 (CtxCommaR _::Γ)); simpl. + apply HX. + + apply BI_Conj_L, Hϕ. + apply (IHΔ1 (CtxSemicL _::Γ)); simpl. + apply (IHΔ2 (CtxSemicR _::Γ)); simpl. + apply HX. Qed. Lemma C_collapse_inv (X : C) Γ Δ : @@ -334,7 +335,7 @@ Module Cl. Proof. destruct X as [X Xcl]. simpl. rewrite !Xcl. intros HX ϕ Hϕ. - simpl in HX. apply collapse_l_inv. + simpl in HX. apply BI_Collapse_L_inv. by apply HX. Qed. @@ -417,7 +418,7 @@ Module Cl. rewrite Yc. intros ψ Hψ. specialize (H ((Δ' ↾ HX), (ψ ↾ Hψ))). simpl in *. apply impl_r_inv in H. - by apply (collapse_l_inv [CtxSemicR Δ]). + by apply (BI_Collapse_L_inv [CtxSemicR Δ]). Qed. Definition C_emp : C := cl' PB_emp. @@ -448,11 +449,11 @@ Module Cl. rewrite Yc. intros ψ Hψ. specialize (H ((Δ' ↾ HX), (ψ ↾ Hψ))). simpl in *. apply wand_r_inv in H. - by apply (collapse_l_inv [CtxCommaR Δ]). + by apply (BI_Collapse_L_inv [CtxCommaR Δ]). Qed. Program Definition PB_box (X: PB) : PB := - {| PBPred := λ Δ, ∃ Δ', Δ ≡ bunch_map BOX Δ' ∧ X Δ' |}. + {| PBPred := λ Δ, ∃ Δ', Δ ≡ fmap BOX Δ' ∧ X Δ' |}. Next Obligation. solve_proper. Qed. Definition C_box (X : C) : C := cl' (PB_box X). @@ -531,7 +532,7 @@ Module Cl. Lemma emp_sep_1 P : P ⊢ emp ∗ P. Proof. intros Δ HP. eapply cl_unit. - exists empty, Δ. rewrite left_id. + exists ∅ₘ%B, Δ. rewrite left_id. repeat split; eauto. intros ϕ Hϕ. eapply Hϕ. simpl. reflexivity. Qed. @@ -560,7 +561,7 @@ Module Cl. Definition C_pure (ϕ : Prop) : C := cl' (PB_pure ϕ). Program Definition PB_top : PB := - {| PBPred := (λ Δ, Δ ≡ top) |}. + {| PBPred := (λ Δ, Δ ≡ ∅ₐ)%B |}. Next Obligation. solve_proper. Qed. @@ -570,7 +571,7 @@ Module Cl. Proof. apply cl_adj. intros Δ _. - rewrite -(BE_semic_unit_l Δ). + rewrite -(BE_unit_l _ Δ). apply C_weaken. apply cl_unit. simpl. reflexivity. Qed. @@ -605,7 +606,7 @@ Module Cl. intros Δ. destruct 1 as (Δ' & HD & HX). simpl. intros D1 H1 f Hf. rewrite HD. - rewrite comm. apply (collapse_l_inv [CtxSemicR D1]). simpl. + rewrite comm. apply (BI_Collapse_L_inv [CtxSemicR D1]). simpl. apply impl_r_inv. apply H1. intros D2. destruct 1 as (D2' & HD2 & HY). simpl. apply BI_Impl_R. @@ -637,16 +638,16 @@ Module Cl. Lemma box_true : C_pure True ⊢ C_box (C_pure True). Proof. apply cl_adj. intros Δ _. - rewrite -(BE_semic_unit_l Δ). + rewrite -(BE_unit_l _ Δ). apply C_weaken. apply cl_unit. - simpl. exists top. simpl. split; auto. + simpl. exists ∅ₐ%B. simpl. split; auto. apply cl_unit. done. Qed. Lemma box_emp : emp ⊢ C_box emp. Proof. apply cl_mono. intros Δ HD; simpl. - exists empty. split; eauto. apply cl_unit. + exists ∅ₘ%B. split; eauto. apply cl_unit. simpl. reflexivity. Qed. @@ -882,7 +883,7 @@ Proof. apply Hϕ2. unfold inner_interp. apply H3. apply (C_collapse_inv _ [] (fill Γ Δ)). simpl. cut (formula_interp C_alg C_box C_atom (collapse (fill Γ Δ)) (frml (collapse (fill Γ Δ)))). - { apply (bunch_interp_collapse C_alg C_box C_atom). } + { by rewrite bunch_interp_collapse. } apply okada_property. } simpl. rewrite -H2. apply bunch_interp_fill_mono, H1. diff --git a/theories/s4/formula.v b/theories/s4/formula.v new file mode 100644 index 0000000..d5189a2 --- /dev/null +++ b/theories/s4/formula.v @@ -0,0 +1,52 @@ +From Coq Require Import ssreflect. +From stdpp Require Import prelude gmap fin_sets. +From bunched.algebra Require Import bi. +From bunched Require Import bunches. + +(** * Formulas *) +Definition atom := nat. + +(** ** Formulas and bunches *) +Inductive formula : Type := +| TOP +| EMP +| BOT +| ATOM (A : atom) +| CONJ (ϕ ψ : formula) +| DISJ (ϕ ψ : formula) +| SEP (ϕ ψ : formula) +| IMPL (ϕ ψ : formula) +| WAND (ϕ ψ : formula) +| BOX (ϕ : formula) +. + +(** "Collapse" internalizes the bunch as a formula. *) +Fixpoint collapse (Δ : @bunch formula) : formula := + match Δ with + | frml ϕ => ϕ + | ∅ₐ => TOP + | ∅ₘ => EMP + | Δ ,, Δ' => SEP (collapse Δ) (collapse Δ') + | Δ ;, Δ' => CONJ (collapse Δ) (collapse Δ') + end%B. + +Inductive collapse_gr : @bunch formula → formula → Prop := +| collapse_frml ϕ : collapse_gr (frml ϕ) ϕ +| collapse_top : collapse_gr ∅ₐ%B TOP +| collapse_emp : collapse_gr ∅ₘ%B EMP +| collapse_sep Δ1 Δ2 ϕ1 ϕ2 : + collapse_gr Δ1 ϕ1 → + collapse_gr Δ2 ϕ2 → + collapse_gr (Δ1 ,, Δ2)%B (SEP ϕ1 ϕ2) +| collapse_conj Δ1 Δ2 ϕ1 ϕ2 : + collapse_gr Δ1 ϕ1 → + collapse_gr Δ2 ϕ2 → + collapse_gr (Δ1 ;, Δ2)%B (CONJ ϕ1 ϕ2) +. + +Lemma collapse_gr_sound Δ : collapse_gr Δ (collapse Δ). +Proof. induction Δ; simpl; try destruct s; try by econstructor. Qed. + +Lemma collapse_gr_complete Δ ϕ : collapse_gr Δ ϕ → collapse Δ = ϕ. +Proof. induction 1; simpl; subst; eauto. Qed. + diff --git a/theories/interp_s4.v b/theories/s4/interp.v similarity index 62% rename from theories/interp_s4.v rename to theories/s4/interp.v index a9b5749..9b78ad7 100644 --- a/theories/interp_s4.v +++ b/theories/s4/interp.v @@ -1,7 +1,8 @@ From Coq Require Import ssreflect. From stdpp Require Import prelude. From bunched.algebra Require Import bi. -From bunched Require Import seqcalc_s4. +From bunched Require Import bunches. +From bunched.s4 Require Import formula seqcalc. (** * Interpretation of the sequent calculus in an arbitrary BI. *) @@ -19,6 +20,8 @@ Section interp. Variable (PROP : bi). Variable (box : PROP → PROP). Context `{!BiBox PROP box}. + Notation bunch := (@bunch formula). + Notation bunch_ctx := (@bunch_ctx formula). Notation "□ A" := (box A) : bi_scope. @@ -44,111 +47,37 @@ Section interp. | BOX ϕ => □ (formula_interp ϕ) end%I. - Fixpoint bunch_interp (Δ : bunch) : PROP := - match Δ with - | frml ϕ => formula_interp ϕ - | top => True - | empty => emp - | (Δ ,, Δ')%B => bunch_interp Δ ∗ bunch_interp Δ' - | (Δ ;, Δ')%B => bunch_interp Δ ∧ bunch_interp Δ' - end%I. + Notation bunch_interp := (bunch_interp formula_interp). Lemma bunch_interp_collapse Δ : - bunch_interp Δ ≡ formula_interp (collapse Δ). - Proof. - induction Δ; simpl; eauto. - - by rewrite IHΔ1 IHΔ2. - - by rewrite IHΔ1 IHΔ2. - Qed. - - Definition seq_interp Δ ϕ : Prop := - (bunch_interp Δ ⊢ formula_interp ϕ). - - Definition bunch_ctx_item_interp (C : bunch_ctx_item) : PROP → PROP := - λ P, match C with - | CtxCommaL Δ => P ∗ bunch_interp Δ - | CtxCommaR Δ => bunch_interp Δ ∗ P - | CtxSemicL Δ => P ∧ bunch_interp Δ - | CtxSemicR Δ => bunch_interp Δ ∧ P - end%I. - - Definition bunch_ctx_interp Π : PROP → PROP := - λ P, foldl (flip bunch_ctx_item_interp) P Π. - - Lemma bunch_ctx_interp_cons F Π A : - bunch_ctx_interp (F::Π) A = bunch_ctx_interp Π (bunch_ctx_item_interp F A). - Proof. reflexivity. Qed. - - Global Instance bunch_ctx_interp_proper Π : Proper ((≡) ==> (≡)) (bunch_ctx_interp Π). - Proof. - induction Π as [|F Π]=>X Y HXY. - - simpl; auto. - - simpl. - eapply IHΠ. - destruct F; solve_proper. - Qed. - - Lemma bunch_ctx_interp_decomp Π Δ : - bunch_interp (fill Π Δ) ≡ bunch_ctx_interp Π (bunch_interp Δ). - Proof. - revert Δ. induction Π as [|C Π IH]=>Δ; first by reflexivity. - apply bi.equiv_entails_2. - - destruct C; simpl; by rewrite IH. - - destruct C; simpl; by rewrite IH. - Qed. - - Lemma bunch_interp_fill_item_mono (C : bunch_ctx_item) Δ Δ' : - (bunch_interp Δ ⊢ bunch_interp Δ') → - bunch_interp (fill_item C Δ) ⊢ bunch_interp (fill_item C Δ'). - Proof. - intros H1. - induction C as [ ? | ? | ? | ? ]; simpl; by rewrite H1. - Qed. - - Lemma bunch_interp_fill_mono Π Δ Δ' : - (bunch_interp Δ ⊢ bunch_interp Δ') → - bunch_interp (fill Π Δ) ⊢ bunch_interp (fill Π Δ'). + bunch_interp Δ = formula_interp (collapse Δ). Proof. - revert Δ Δ'. - induction Π as [|C Π IH]=> Δ Δ' H1; eauto. - simpl. apply IH. - by apply bunch_interp_fill_item_mono. + induction Δ as [ϕ|sp|sp Δ1 IH1 Δ2 IH2]; try destruct sp; simpl; eauto. + - by rewrite IH1 IH2. + - by rewrite IH1 IH2. Qed. Lemma bunch_interp_box Δ : - bunch_interp (bunch_map BOX Δ) ⊢ box (bunch_interp Δ). + bunch_interp (BOX <$> Δ) ⊢ □ (bunch_interp Δ). Proof. - induction Δ; simpl; eauto. - - apply bi_box_true. + induction Δ as [ϕ|sp|sp Δ1 IH1 Δ2 IH2]; try destruct sp; simpl; eauto. - apply bi_box_emp. - - rewrite IHΔ1 IHΔ2. apply bi_box_sep. - - rewrite IHΔ1 IHΔ2. apply bi_box_conj. + - apply bi_box_true. + - rewrite IH1 IH2. apply bi_box_sep. + - rewrite IH1 IH2. apply bi_box_conj. Qed. - Lemma bunch_interp_box_idem Δ : - bunch_interp (bunch_map BOX Δ) ⊢ bunch_interp (bunch_map BOX (bunch_map BOX Δ)). + + Lemma bunch_interp_box_idem (Δ : bunch) : + bunch_interp (BOX <$> Δ) ⊢ bunch_interp (BOX <$> (BOX <$> Δ)). Proof. - induction Δ; simpl; eauto. + induction Δ as [ϕ|sp|sp Δ1 IH1 Δ2 IH2]; try destruct sp; simpl; eauto. - apply bi_box_idem. - - by rewrite IHΔ1 IHΔ2. - - by rewrite IHΔ1 IHΔ2. + - by rewrite IH1 IH2. + - by rewrite IH1 IH2. Qed. - Global Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp. - Proof. - intros Δ1 Δ2. induction 1; eauto. - - etrans; eassumption. - - apply bi.equiv_entails_2. - + apply bunch_interp_fill_mono; eauto. - by apply bi.equiv_entails_1_1. - + apply bunch_interp_fill_mono; eauto. - by apply bi.equiv_entails_1_2. - - simpl. by rewrite left_id. - - simpl. by rewrite comm. - - simpl. by rewrite assoc. - - simpl. by rewrite left_id. - - simpl. by rewrite comm. - - simpl. by rewrite assoc. - Qed. + Definition seq_interp Δ ϕ : Prop := + (bunch_interp Δ ⊢ formula_interp ϕ). Global Instance seq_interp_proper : Proper ((≡) ==> (=) ==> (≡)) seq_interp. Proof. @@ -177,7 +106,7 @@ Section interp. - induction C as [|C Π IH]; simpl. { apply bi.False_elim. } rewrite -IH. - destruct C; simpl; apply bunch_interp_fill_mono; simpl. + destruct C as [[] ?| [] ?]; simpl; apply bunch_interp_fill_mono; simpl. all: by rewrite ?left_absorb ?right_absorb. - apply bi.True_intro. - by rewrite IHproves1 IHproves2. @@ -187,9 +116,9 @@ Section interp. revert ϕ ψ. induction Π as [|F Π] => /= ϕ ψ IH1 IH2. { apply bi.or_elim; eauto. } - destruct F; simpl; simpl in IH1, IH2; + destruct F as [[] ? IH1|[] ? IH2]; simpl; simpl in IH1, IH2; rewrite bunch_ctx_interp_decomp; - cbn[bunch_interp formula_interp]. + cbn[sep_interp bunch_interp formula_interp]. + rewrite bi.sep_or_r. unfold seq_interp in *. etrans. @@ -203,10 +132,10 @@ Section interp. rewrite bunch_ctx_interp_decomp. cbn[bunch_interp formula_interp]. by rewrite bunch_interp_collapse. - + rewrite bi.sep_or_l. + + rewrite bi.and_or_r. unfold seq_interp in *. etrans. - 2:{ eapply (IHΠ (SEP (collapse Δ1) ϕ) (SEP (collapse Δ1) ψ)). + 2:{ eapply (IHΠ (CONJ ϕ (collapse Δ2)) (CONJ ψ (collapse Δ2))). - rewrite -IH1. apply bunch_interp_fill_mono; simpl. by rewrite bunch_interp_collapse. @@ -216,10 +145,10 @@ Section interp. rewrite bunch_ctx_interp_decomp. cbn[bunch_interp formula_interp]. by rewrite bunch_interp_collapse. - + rewrite bi.and_or_r. + + rewrite bi.sep_or_l. unfold seq_interp in *. etrans. - 2:{ eapply (IHΠ (CONJ ϕ (collapse Δ2)) (CONJ ψ (collapse Δ2))). + 2:{ eapply (IHΠ (SEP (collapse Δ1) ϕ) (SEP (collapse Δ1) ψ)). - rewrite -IH1. apply bunch_interp_fill_mono; simpl. by rewrite bunch_interp_collapse. diff --git a/theories/s4/seqcalc.v b/theories/s4/seqcalc.v new file mode 100644 index 0000000..212aab1 --- /dev/null +++ b/theories/s4/seqcalc.v @@ -0,0 +1,152 @@ +(** BI + □ *) +From Coq Require Import ssreflect. +From stdpp Require Import prelude. +From bunched.algebra Require Import bi. +From bunched Require Export bunches bunch_decomp. +From bunched.s4 Require Import formula. + +Declare Scope bunch_scope. +Delimit Scope bunch_scope with B. + +(** ** Sequent calculus itself *) +Reserved Notation "P ⊢ᴮ Q" (at level 99, Q at level 200, right associativity). +Inductive proves : bunch → formula → Prop := +(* structural *) +| BI_Axiom (a : atom) : frml (ATOM a) ⊢ᴮ ATOM a +| BI_Equiv Δ Δ' ϕ : + (Δ ≡ Δ') → (Δ ⊢ᴮ ϕ) → + Δ' ⊢ᴮ ϕ +| BI_Weaken C Δ Δ' ϕ : (fill C Δ ⊢ᴮ ϕ) → + fill C (Δ ;, Δ') ⊢ᴮ ϕ +| BI_Contr C Δ ϕ : (fill C (Δ ;, Δ) ⊢ᴮ ϕ) → + fill C Δ ⊢ᴮ ϕ +(* modalities *) +| BI_Box_L Π ϕ ψ : + (fill Π (frml ϕ) ⊢ᴮ ψ) → + fill Π (frml (BOX ϕ)) ⊢ᴮ ψ +| BI_Box_R Δ ϕ : + (BOX <$> Δ ⊢ᴮ ϕ) → + BOX <$> Δ ⊢ᴮ BOX ϕ +(* multiplicatives *) +| BI_Emp_R : + ∅ₘ ⊢ᴮ EMP +| BI_Emp_L C ϕ : + (fill C ∅ₘ ⊢ᴮ ϕ) → + fill C (frml EMP) ⊢ᴮ ϕ +| BI_Sep_R Δ Δ' ϕ ψ : + (Δ ⊢ᴮ ϕ) → + (Δ' ⊢ᴮ ψ) → + Δ ,, Δ' ⊢ᴮ SEP ϕ ψ +| BI_Sep_L C ϕ ψ χ : + (fill C (frml ϕ ,, frml ψ) ⊢ᴮ χ) → + fill C (frml (SEP ϕ ψ)) ⊢ᴮ χ +| BI_Wand_R Δ ϕ ψ : + (Δ ,, frml ϕ ⊢ᴮ ψ) → + Δ ⊢ᴮ WAND ϕ ψ +| BI_Wand_L C Δ ϕ ψ χ : + (Δ ⊢ᴮ ϕ) → + (fill C (frml ψ) ⊢ᴮ χ) → + fill C (Δ ,, frml (WAND ϕ ψ)) ⊢ᴮ χ +(* additives *) +| BI_False_L C ϕ : + fill C (frml BOT) ⊢ᴮ ϕ +| BI_True_R Δ : + Δ ⊢ᴮ TOP +| BI_True_L C ϕ : + (fill C ∅ₐ ⊢ᴮ ϕ) → + fill C (frml TOP) ⊢ᴮ ϕ +| BI_Conj_R Δ Δ' ϕ ψ : + (Δ ⊢ᴮ ϕ) → + (Δ' ⊢ᴮ ψ) → + Δ ;, Δ' ⊢ᴮ CONJ ϕ ψ +| BI_Conj_L C ϕ ψ χ : + (fill C (frml ϕ ;, frml ψ) ⊢ᴮ χ) → + fill C (frml (CONJ ϕ ψ)) ⊢ᴮ χ +| BI_Disj_R1 Δ ϕ ψ : + (Δ ⊢ᴮ ϕ) → + Δ ⊢ᴮ DISJ ϕ ψ +| BI_Disj_R2 Δ ϕ ψ : + (Δ ⊢ᴮ ψ) → + Δ ⊢ᴮ DISJ ϕ ψ +| BI_Disj_L Π ϕ ψ χ : + (fill Π (frml ϕ) ⊢ᴮ χ) → + (fill Π (frml ψ) ⊢ᴮ χ) → + fill Π (frml (DISJ ϕ ψ)) ⊢ᴮ χ +| BI_Impl_R Δ ϕ ψ : + (Δ ;, frml ϕ ⊢ᴮ ψ) → + Δ ⊢ᴮ IMPL ϕ ψ +| BI_Impl_L C Δ ϕ ψ χ : + (Δ ⊢ᴮ ϕ) → + (fill C (frml ψ) ⊢ᴮ χ) → + fill C (Δ ;, frml (IMPL ϕ ψ)) ⊢ᴮ χ +where "Δ ⊢ᴮ ϕ" := (proves Δ%B ϕ%B). + + +Global Instance proves_proper : Proper ((≡) ==> (=) ==> (≡)) proves. +Proof. + intros D1 D2 HD ϕ ? <-. + split; intros H. + - eapply BI_Equiv; eauto. + - eapply BI_Equiv; [ symmetry | ]; eauto. +Qed. + +(** Additional lemmas for bunch_decompose and box *) +Lemma bunch_decomp_box_frml Π ϕ Δ : + bunch_decomp (BOX <$> Δ) Π (frml ϕ) → ∃ ψ, ϕ = BOX ψ. +Proof. + revert Π. induction Δ=>/= Π H1; try by inversion H1. + - inversion H1; simplify_eq/=. naive_solver. + - inversion H1 as [Δ|sp Δ1' Δ2' Π' Δ H1' |sp Δ1' Δ2' Π' Δ H1']; simplify_eq/=. + + eapply IHΔ1; eauto. + + eapply IHΔ2; eauto. +Qed. + +Lemma bunch_decomp_box Δ Π ϕ : + bunch_decomp (BOX <$> Δ) Π (frml (BOX ϕ)) → + ∃ Π', Π = bunch_ctx_map BOX Π' ∧ bunch_decomp Δ Π' (frml ϕ). +Proof. + revert Π. induction Δ=>/= Π H1; try by inversion H1. + - inversion H1. simplify_eq/=. exists []. split; eauto. + econstructor. + - inversion H1 as [Δ|sp Δ1' Δ2' Π' Δ H1' |sp Δ1' Δ2' Π' Δ H1']; simplify_eq/=. + + destruct (IHΔ1 _ H1') as (Π'1 & -> & Hdec). + exists (Π'1 ++ [CtxL s Δ2]). + rewrite /bunch_ctx_map map_app /=. split; auto. + by econstructor. + + destruct (IHΔ2 _ H1') as (Π'1 & -> & Hdec). + exists (Π'1 ++ [CtxR s Δ1]). + rewrite /bunch_ctx_map map_app /=. split; auto. + by econstructor. +Qed. + +(** Some convenient derived rules *) +Lemma BI_Boxes_L Π Δ ϕ : + (fill Π Δ ⊢ᴮ ϕ) → + (fill Π (BOX <$> Δ) ⊢ᴮ ϕ). +Proof. + revert Π. induction Δ=> Π IH /=; eauto. + - by apply BI_Box_L. + - apply (IHΔ1 ((CtxL s (fmap BOX Δ2))::Π)). simpl. + apply (IHΔ2 ((CtxR s Δ1)::Π)). done. +Qed. + +Lemma BI_Collapse_L Π Δ ϕ : + (fill Π Δ ⊢ᴮ ϕ) → + (fill Π (frml (collapse Δ)) ⊢ᴮ ϕ). +Proof. + revert Π. induction Δ=>Π; simpl; eauto. + - intros HX. + destruct s. + + by apply BI_Emp_L, HX. + + by apply BI_True_L, HX. + - intros HX. + destruct s. + + apply BI_Sep_L. + apply (IHΔ1 (CtxCommaL _::Π)); simpl. + apply (IHΔ2 (CtxCommaR _::Π)); simpl. + apply HX. + + apply BI_Conj_L. + apply (IHΔ1 (CtxSemicL _::Π)); simpl. + apply (IHΔ2 (CtxSemicR _::Π)); simpl. + apply HX. +Qed. diff --git a/theories/s4/seqcalc_height.v b/theories/s4/seqcalc_height.v new file mode 100644 index 0000000..fb5ed80 --- /dev/null +++ b/theories/s4/seqcalc_height.v @@ -0,0 +1,1037 @@ +(* Sequent calculus with upper bounds on proof size. + Useful for doing induction on. + + The main purpose this file is to provide the inversion lemmas (at the very bottom of the file). + *) +From Coq Require Import ssreflect. +From stdpp Require Import prelude. +From bunched.algebra Require Import bi. +From bunched.s4 Require Import formula seqcalc. + +Reserved Notation "P ⊢ᴮ{ n } Q" (at level 99, n, Q at level 200, right associativity). +Reserved Notation "Δ =?{ n } Δ'" (at level 99, n at level 200). + +Section SeqcalcHeight. + Notation bunch := (@bunch formula). + Implicit Type Δ : bunch. + Implicit Type ψ ϕ : formula. + + (** ** Alternative formulation of bunch equivalences *) + Inductive bunch_equiv : bunch → bunch → Prop := + | BE_cong Π Δ1 Δ2 : + Δ1 =? Δ2 → + fill Π Δ1 =? fill Π Δ2 + | BE_comma_unit_l Δ : + (∅ₘ ,, Δ)%B =? Δ + | BE_comma_comm Δ1 Δ2 : + (Δ1 ,, Δ2)%B =? (Δ2 ,, Δ1)%B + | BE_comma_assoc Δ1 Δ2 Δ3 : (Δ1 ,, (Δ2 ,, Δ3))%B =? ((Δ1 ,, Δ2) ,, Δ3)%B + | BE_semic_unit_l Δ : (∅ₐ ;, Δ)%B =? Δ + | BE_semic_comm Δ1 Δ2 : (Δ1 ;, Δ2)%B =? (Δ2 ;, Δ1)%B + | BE_semic_assoc Δ1 Δ2 Δ3 : (Δ1 ;, (Δ2 ;, Δ3))%B =? ((Δ1 ;, Δ2) ;, Δ3)%B + where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B). + + Definition bunch_equiv_h := rtsc (bunch_equiv). + + Lemma bunch_equiv_1 Δ Δ' : + (Δ =? Δ') → (Δ ≡ Δ'). + Proof. induction 1; by econstructor; eauto. Qed. + + Lemma bunch_equiv_2 Δ Δ' : + (Δ ≡ Δ') → (bunch_equiv_h Δ Δ'). + Proof. + induction 1. + all: try by (eapply rtsc_lr; destruct s; econstructor). + - unfold bunch_equiv_h. reflexivity. + - by symmetry. + - etrans; eauto. + - eapply rtc_congruence; eauto. + intros X Y. apply sc_congruence. clear X Y. + intros X Y ?. by econstructor. + Qed. + + Local Lemma bunch_equiv_fill_1 Δ Π ϕ : + fill Π (frml ϕ) =? Δ → + ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). + Proof. + intros Heq. + remember (fill Π (frml ϕ)) as Y. + revert Π HeqY. + induction Heq=>C' heqY; symmetry in heqY. + + apply bunch_decomp_complete in heqY. + apply bunch_decomp_ctx in heqY. + destruct heqY as [H1 | H2]. + * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]]. + destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]]. + simplify_eq/=. + exists (C2 ++ Π). rewrite fill_app. split; first done. + intros Δ. rewrite !fill_app HC2 //. + * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0). + specialize (Hdec0 Δ2). apply bunch_decomp_correct in Hdec0. + exists (C1 Δ2). split ; eauto. + intros Δ. rewrite HC1. + assert (Δ1 ≡ Δ2) as <-. + { by apply bunch_equiv_1. } + by rewrite HC2. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + { inversion H4. } + apply bunch_decomp_correct in H4. + exists Π. split; eauto. + intros X. rewrite fill_app /= left_id //. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxCommaR Δ2]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + * exists (Π ++ [CtxCommaL Δ1]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxCommaL Δ2;CtxCommaL Δ3])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + * inversion H4; simplify_eq/=. + ** exists (Π0 ++ [CtxCommaR Δ1;CtxCommaL Δ3])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + ** exists (Π0 ++ [CtxCommaR (Δ1,,Δ2)])%B. split. + { simpl. rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + { inversion H4. } + apply bunch_decomp_correct in H4. + exists Π. split; eauto. + intros X. rewrite fill_app /= left_id //. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxSemicR Δ2]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + * exists (Π ++ [CtxSemicL Δ1]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxSemicL Δ2;CtxSemicL Δ3])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + * inversion H4; simplify_eq/=. + ** exists (Π0 ++ [CtxSemicR Δ1;CtxSemicL Δ3])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + ** exists (Π0 ++ [CtxSemicR (Δ1;,Δ2)])%B. split. + { simpl. rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + Qed. + + Local Lemma bunch_equiv_fill_2 Δ Π ϕ : + Δ =? fill Π (frml ϕ) → + ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). + Proof. + intros Heq. + remember (fill Π (frml ϕ)) as Y. + revert Π HeqY. + induction Heq=>C' heqY; symmetry in heqY. + + apply bunch_decomp_complete in heqY. + apply bunch_decomp_ctx in heqY. + destruct heqY as [H1 | H2]. + * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]]. + destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]]. + simplify_eq/=. + exists (C2 ++ Π). rewrite fill_app. split; first done. + intros Δ. rewrite !fill_app HC2 //. + * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0). + specialize (Hdec0 Δ1). apply bunch_decomp_correct in Hdec0. + exists (C1 Δ1). split ; eauto. + intros Δ. rewrite HC1. + assert (Δ1 ≡ Δ2) as ->. + { by apply bunch_equiv_1. } + by rewrite HC2. + + exists (C' ++ [CtxCommaR ∅ₘ]%B). simpl; split. + { rewrite fill_app /=. by rewrite heqY. } + intros X; rewrite fill_app/=. + by rewrite left_id. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxCommaR Δ1]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + * exists (Π ++ [CtxCommaL Δ2]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * inversion H4; simplify_eq/=. + ** exists (Π0 ++ [CtxCommaL (Δ2 ,, Δ3)])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + ** exists (Π0 ++ [CtxCommaL Δ3;CtxCommaR Δ1])%B. split. + { simpl. rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + * exists (Π ++ [CtxCommaR Δ2;CtxCommaR Δ1])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + + exists (C' ++ [ CtxSemicR ∅ₐ]%B). simpl; split. + { rewrite fill_app /=. by rewrite heqY. } + intros X; rewrite fill_app/=. + by rewrite left_id. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * exists (Π ++ [CtxSemicR Δ1]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + * exists (Π ++ [CtxSemicL Δ2]). split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite comm. + + apply bunch_decomp_complete in heqY. + inversion heqY; simplify_eq/=. + * inversion H4; simplify_eq/=. + ** exists (Π0 ++ [CtxSemicL (Δ2 ;, Δ3)])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + ** exists (Π0 ++ [CtxSemicL Δ3;CtxSemicR Δ1])%B. split. + { simpl. rewrite fill_app/=. + apply bunch_decomp_correct in H5. + by rewrite H5. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + * exists (Π ++ [CtxSemicR Δ2;CtxSemicR Δ1])%B. split. + { rewrite fill_app/=. + apply bunch_decomp_correct in H4. + by rewrite H4. } + intros Δ. rewrite !fill_app/=. + by rewrite assoc. + Qed. + + Lemma bunch_equiv_fill Δ Π ϕ : + Δ ≡ (fill Π (frml ϕ)) → + ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). + Proof. + intros H%bunch_equiv_2. + revert Δ H. eapply rtc_ind_l. + { exists Π. eauto. } + intros X Y HXY HY. clear HY. + intros (C0 & -> & HC0). + destruct HXY as [HXY|HXY]. + - apply bunch_equiv_fill_2 in HXY. + destruct HXY as (C' & -> & HC'). + eexists; split; eauto. + intros ?. by rewrite HC' HC0. + - apply bunch_equiv_fill_1 in HXY. + destruct HXY as (C' & -> & HC'). + eexists; split; eauto. + intros ?. by rewrite HC' HC0. + Qed. + + (** * SEQUENT CALCULUS *) + Polymorphic Inductive proves : bunch → formula → nat → Prop := + (* structural *) + | BI_Higher Δ ϕ n : (Δ ⊢ᴮ{n} ϕ) → (Δ ⊢ᴮ{S n} ϕ) + | BI_Axiom (a : atom) : frml (ATOM a) ⊢ᴮ{0} ATOM a + | BI_Equiv Δ Δ' ϕ n : + (Δ ≡ Δ') → (Δ ⊢ᴮ{n} ϕ) → + Δ' ⊢ᴮ{S n} ϕ + | BI_Weaken Π Δ Δ' ϕ n : (fill Π Δ ⊢ᴮ{n} ϕ) → + fill Π (Δ ;, Δ') ⊢ᴮ{S n} ϕ + | BI_Contr Π Δ ϕ n : (fill Π (Δ ;, Δ) ⊢ᴮ{n} ϕ) → + fill Π Δ ⊢ᴮ{S n} ϕ + (* | BI_Cut Π Δ ϕ ψ : (Δ ⊢ᴮ ψ) → *) + (* (fill Π (frml ψ) ⊢ᴮ ϕ) → *) + (* fill Π Δ ⊢ᴮ ϕ *) + (* modal *) + | BI_Box_L Π ϕ ψ n : + (fill Π (frml ϕ) ⊢ᴮ{n} ψ) → + fill Π (frml (BOX ϕ)) ⊢ᴮ{S n} ψ + | BI_Box_R Δ ϕ n : + (BOX <$> Δ ⊢ᴮ{n} ϕ) → + BOX <$> Δ ⊢ᴮ{S n} BOX ϕ + (* multiplicatives *) + | BI_Emp_R : + ∅ₘ ⊢ᴮ{0} EMP + | BI_Emp_L Π ϕ n : + (fill Π ∅ₘ ⊢ᴮ{n} ϕ) → + fill Π (frml EMP) ⊢ᴮ{S n} ϕ + | BI_Sep_R Δ Δ' ϕ ψ n m : + (Δ ⊢ᴮ{n} ϕ) → + (Δ' ⊢ᴮ{m} ψ) → + Δ ,, Δ' ⊢ᴮ{S (n `max` m)} SEP ϕ ψ + | BI_Sep_L Π ϕ ψ χ n : + (fill Π (frml ϕ ,, frml ψ) ⊢ᴮ{n} χ) → + fill Π (frml (SEP ϕ ψ)) ⊢ᴮ{S n} χ + | BI_Wand_R Δ ϕ ψ n : + (Δ ,, frml ϕ ⊢ᴮ{n} ψ) → + Δ ⊢ᴮ{S n} WAND ϕ ψ + | BI_Wand_L Π Δ ϕ ψ χ n m : + (Δ ⊢ᴮ{n} ϕ) → + (fill Π (frml ψ) ⊢ᴮ{m} χ) → + fill Π (Δ ,, frml (WAND ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ + (* additives *) + | BI_False_L Π ϕ : + fill Π (frml BOT) ⊢ᴮ{0} ϕ + | BI_True_R Δ : + Δ ⊢ᴮ{0} TOP + | BI_True_L Π ϕ n : + (fill Π ∅ₐ ⊢ᴮ{n} ϕ) → + fill Π (frml TOP) ⊢ᴮ{S n} ϕ + | BI_Conj_R Δ Δ' ϕ ψ n m : + (Δ ⊢ᴮ{n} ϕ) → + (Δ' ⊢ᴮ{m} ψ) → + Δ ;, Δ' ⊢ᴮ{S (n `max` m)} CONJ ϕ ψ + | BI_Conj_L Π ϕ ψ χ n : + (fill Π (frml ϕ ;, frml ψ) ⊢ᴮ{n} χ) → + fill Π (frml (CONJ ϕ ψ)) ⊢ᴮ{S n} χ + | BI_Disj_R1 Δ ϕ ψ n : + (Δ ⊢ᴮ{n} ϕ) → + Δ ⊢ᴮ{S n} DISJ ϕ ψ + | BI_Disj_R2 Δ ϕ ψ n : + (Δ ⊢ᴮ{n} ψ) → + Δ ⊢ᴮ{S n} DISJ ϕ ψ + | BI_Disj_L Π ϕ ψ χ n m : + (fill Π (frml ϕ) ⊢ᴮ{n} χ) → + (fill Π (frml ψ) ⊢ᴮ{m} χ) → + fill Π (frml (DISJ ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ + | BI_Impl_R Δ ϕ ψ n : + (Δ ;, frml ϕ ⊢ᴮ{n} ψ) → + Δ ⊢ᴮ{S n} IMPL ϕ ψ + | BI_Impl_L Π Δ ϕ ψ χ n m: + (Δ ⊢ᴮ{n} ϕ) → + (fill Π (frml ψ) ⊢ᴮ{m} χ) → + fill Π (Δ ;, frml (IMPL ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ + where "Δ ⊢ᴮ{ n } ϕ" := (proves Δ%B ϕ%B n). + + Lemma provesN_proves n Δ ϕ : + (Δ ⊢ᴮ{ n } ϕ) → Δ ⊢ᴮ ϕ. + Proof. + induction 1; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + by econstructor; eauto. + Qed. + + Lemma proves_provesN Δ ϕ : + (Δ ⊢ᴮ ϕ) → ∃ n, Δ ⊢ᴮ{n} ϕ. + Proof. + induction 1. + all: try destruct IHproves as [n IH]. + all: try (destruct IHproves1 as [n1 IH1]; + destruct IHproves2 as [n2 IH2]). + all: try by eexists; econstructor; eauto. + Qed. + + (** * Inversion lemmas *) + Local Ltac bind_ctx := + match goal with + | [ |- fill ?Π ?Δ,, ?Δ' ⊢ᴮ{_} _ ] => + replace (fill Π Δ,, Δ')%B + with (fill (Π ++ [CtxCommaL Δ']) Δ)%B + by rewrite fill_app// + | [ |- fill ?Π ?Δ;, ?Δ' ⊢ᴮ{_} _ ] => + replace (fill Π Δ;, Δ')%B + with (fill (Π ++ [CtxSemicL Δ']) Δ)%B + by rewrite fill_app// + end. + + Local Ltac commute_left_rule IH := + intros ->; bind_ctx; + econstructor; eauto; rewrite fill_app; by eapply IH. + + Lemma wand_r_inv' Δ ϕ ψ n : + (Δ ⊢ᴮ{n} WAND ϕ ψ) → + (Δ ,, frml ϕ ⊢ᴮ{n} ψ)%B. + Proof. + remember (WAND ϕ ψ) as A. + intros H. revert ϕ ψ HeqA. + induction H; intros A B; try by inversion 1. + all: try by (commute_left_rule IHproves). + - intros ->. by constructor; apply IHproves. + - intros ->. eapply BI_Equiv. + { rewrite -H. reflexivity. } + by apply IHproves. + - intros ?; simplify_eq/=. by apply BI_Higher. + - commute_left_rule IHproves2. + - intros ?; simplify_eq/=. + bind_ctx. eapply BI_Disj_L. + + rewrite fill_app/=. by eapply IHproves1. + + rewrite fill_app/=. by eapply IHproves2. + - commute_left_rule IHproves2. + Qed. + + Lemma impl_r_inv' Δ ϕ ψ n : + (Δ ⊢ᴮ{n} IMPL ϕ ψ) → + (Δ ;, frml ϕ ⊢ᴮ{n} ψ)%B. + Proof. + remember (IMPL ϕ ψ) as A. + intros H. revert ϕ ψ HeqA. + induction H; intros A B; try by inversion 1. + all: try by (commute_left_rule IHproves). + - intros ->. by constructor; apply IHproves. + - intros ->. eapply BI_Equiv. + { rewrite -H. reflexivity. } + by apply IHproves. + - commute_left_rule IHproves2. + - intros ?; simplify_eq/=. + bind_ctx. eapply BI_Disj_L. + + rewrite fill_app/=. by eapply IHproves1. + + rewrite fill_app/=. by eapply IHproves2. + - intros ?; simplify_eq/=. by apply BI_Higher. + - commute_left_rule IHproves2. + Qed. + + Lemma box_l_inv' Δ Π ϕ χ n : + (Δ ⊢ᴮ{n} χ) → + Δ = fill Π (frml (BOX (BOX ϕ))) → + (fill Π (frml (BOX ϕ)) ⊢ᴮ{n} χ). + Proof. + revert Π Δ χ. + induction n using lt_wf_ind. rename H into IHproves. + intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. + inversion PROOF; simplify_eq/= => Heq. + - (* raising the pf height *) + apply BI_Higher. + eapply IHproves; eauto. + - (* axiom *) + apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. + - (* equivalence of bunches *) + simplify_eq/=. + destruct (bunch_equiv_fill _ _ _ H) as [Π2 [-> HΠ2]]. + eapply BI_Equiv. + { apply HΠ2. } + eapply IHproves; eauto. + - (* weakening *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [Π1 [HΠ0 HΠ]]. + inversion HΠ0; simplify_eq/=. + * rewrite !fill_app/=. + apply BI_Weaken. + rewrite -fill_app. + eapply IHproves; eauto. + by apply bunch_decomp_correct, bunch_decomp_app. + * rewrite !fill_app/=. + by apply BI_Weaken. + + rename Π into Π'. + rename Π0 into Π0'. + destruct H2 as (Π0 & Π1 & HΠ0 & HΠ1 & Hdec0). + rewrite -HΠ1. + apply BI_Weaken. + rewrite -HΠ0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* contraction *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]; last first. + + rename Π0 into Π0'. + destruct H2 as (Π0 & Π1 & HΠ0 & HΠ1 & Hdec0). + rewrite -HΠ1. + apply BI_Contr. + rewrite -HΠ0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + + destruct H1 as [C0 [HC0 ->]]. + apply bunch_decomp_correct in HC0. + simplify_eq/=. + rename Π0 into Π. + assert (fill Π (fill C0 (frml (BOX ϕ));, fill C0 (frml (BOX (BOX ϕ)))) ⊢ᴮ{ n0} χ) as IH1. + { specialize (IHproves n0 (lt_n_Sn _)). + set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml (BOX (BOX ϕ))))] ++ Π)%B). + specialize (IHproves C2 _ _ H). + revert IHproves. rewrite /C2 !fill_app /=. + eauto. } + rewrite fill_app. + apply BI_Contr. + set (C2 := (C0 ++ [CtxSemicR (fill C0 (frml (BOX ϕ)))] ++ Π)%B). + replace (fill Π (fill C0 (frml (BOX ϕ));, fill C0 (frml (BOX ϕ))))%B + with (fill C2 (frml (BOX ϕ)))%B by rewrite fill_app//. + eapply IHproves; eauto. + rewrite /C2 fill_app/=//. + - (* box L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + by apply BI_Higher. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Box_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* box R *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_box in Heq. + destruct Heq as (Π' & -> & ->%bunch_decomp_correct). + change (frml (BOX ϕ)) with (BOX <$> (frml ϕ)). + rewrite -(bunch_map_fill BOX). apply BI_Box_R. + rewrite bunch_map_fill /=. eapply IHproves; eauto. + rewrite bunch_map_fill //. + - (* emp R *) + exfalso. + apply bunch_decomp_complete in Heq. + inversion Heq. + - (* emp L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Emp_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* sep R *) + apply bunch_decomp_complete in Heq. + inversion Heq; simplify_eq/=. + + rewrite fill_app /=. + eapply BI_Sep_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + + rewrite fill_app /=. + eapply BI_Sep_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + - (* sep L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Sep_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* wand R *) + apply BI_Wand_R. + assert ((fill Π (frml (BOX ϕ)),, frml ϕ0) = + fill (Π ++ [CtxCommaL (frml ϕ0)]) (frml (BOX ϕ)))%B as ->. + { rewrite fill_app//. } + eapply IHproves; eauto. rewrite -Heq fill_app /= //. + - (* wand L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + * rewrite !fill_app/=. + eapply BI_Wand_L; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + * exfalso. inversion H6. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Wand_L; eauto. + rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + - (* bot L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_False_L. + - (* top R *) apply BI_True_R. + - (* top L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_True_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* conjR *) + apply bunch_decomp_complete in Heq. + inversion Heq; simplify_eq/=. + + rewrite fill_app /=. + eapply BI_Conj_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + + rewrite fill_app /=. + eapply BI_Conj_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + - (* conjL *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Conj_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* disj R 1 *) + eapply BI_Disj_R1. + eapply IHproves; eauto. + - (* disj R 2 *) + eapply BI_Disj_R2. + eapply IHproves; eauto. + - (* disj L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Disj_L. + * rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + * rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + - (* impl R *) + apply BI_Impl_R. + assert ((fill Π (frml (BOX ϕ));, frml ϕ0) = + fill (Π ++ [CtxSemicL (frml ϕ0)]) (frml (BOX ϕ)))%B as ->. + { rewrite fill_app//. } + eapply IHproves; eauto. rewrite -Heq fill_app /= //. + - (* impl L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + * rewrite !fill_app/=. + eapply BI_Impl_L; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + * exfalso. inversion H6. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Impl_L; eauto. + rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + Qed. + + Lemma collapse_l_inv' Δ Π Δ' ϕ χ n : + collapse_gr Δ' ϕ → + (Δ ⊢ᴮ{n} χ) → + Δ = fill Π (frml ϕ) → + (fill Π Δ' ⊢ᴮ{n} χ). + Proof. + revert Π Δ Δ' ϕ χ. + induction n as [n IHproves] using lt_wf_ind. + intros Π Δ Δ' ϕ χ Hcoll PROOF Heq. symmetry in Heq. revert Heq. + inversion PROOF; simplify_eq/= => Heq. + (* induction H => C' Heq; symmetry in Heq. *) + - (* raising the pf height *) + apply BI_Higher. + eapply IHproves; eauto. + - (* axiom *) + apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. + inversion Hcoll. by econstructor. + - (* equivalence of bunches *) + simplify_eq/=. + destruct (bunch_equiv_fill _ _ _ H) as [C2 [-> HC2]]. + eapply BI_Equiv. + { apply HC2. } + eapply IHproves; eauto. + - (* weakening *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + * rewrite !fill_app/=. + apply BI_Weaken. + rewrite -fill_app. + eapply IHproves; eauto. + by apply bunch_decomp_correct, bunch_decomp_app. + * rewrite !fill_app/=. + by apply BI_Weaken. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Weaken. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* contraction *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]; last first. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Contr. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + + destruct H1 as [C0 [HC0 ->]]. + apply bunch_decomp_correct in HC0. + simplify_eq/=. + assert (fill Π0 (fill C0 Δ';, fill C0 (frml ϕ)) ⊢ᴮ{ n0} χ) as IH1. + { specialize (IHproves n0 (lt_n_Sn _)). + set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml ϕ))] ++ Π0)%B). + specialize (IHproves C2 _ _ _ _ Hcoll H). + revert IHproves. rewrite /C2 !fill_app /=. + eauto. } + rewrite fill_app. + apply BI_Contr. + set (C2 := (C0 ++ [CtxSemicR (fill C0 Δ')] ++ Π0)%B). + replace (fill Π0 (fill C0 Δ';, fill C0 Δ'))%B + with (fill C2 Δ')%B by rewrite fill_app//. + eapply IHproves; eauto. + rewrite /C2 fill_app//. + - (* box L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; simplify_eq/=. + apply BI_Box_L; done. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Box_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* box R *) + assert (∃ ψ, ϕ = BOX ψ) as [ψ Hψ]. + { eapply bunch_decomp_box_frml. + by apply bunch_decomp_complete. } + subst. inversion Hcoll; simplify_eq/=. + rewrite Heq. by apply BI_Box_R. + - (* emp R *) + exfalso. + apply bunch_decomp_complete in Heq. + inversion Heq. + - (* emp L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; simplify_eq/=. + * by apply BI_Emp_L. + * by apply BI_Higher. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Emp_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* sep R *) + apply bunch_decomp_complete in Heq. + inversion Heq; simplify_eq/=. + + rewrite fill_app /=. + eapply BI_Sep_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + + rewrite fill_app /=. + eapply BI_Sep_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + - (* sep L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; simplify_eq/=; eauto. + assert (fill Π0 (Δ1,, frml ψ) ⊢ᴮ{ n0} χ) as H1. + { replace (fill Π0 (Δ1,, frml ψ))%B + with (fill ([CtxCommaL (frml ψ)]++Π0) Δ1) + by rewrite fill_app//. + eapply IHproves; eauto. } + replace (fill Π0 (Δ1,, Δ2))%B + with (fill ([CtxCommaR Δ1]++Π0) Δ2) + by rewrite fill_app//. + apply BI_Higher. + eapply IHproves; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Sep_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* wand R *) + apply BI_Wand_R. + replace (fill Π Δ',, frml ϕ0)%B + with (fill (Π ++ [CtxCommaL (frml ϕ0)]) Δ')%B + by rewrite fill_app//. + eapply IHproves; eauto. rewrite -Heq fill_app /= //. + - (* wand L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + * rewrite !fill_app/=. + eapply BI_Wand_L; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + * inversion H6; subst. + inversion Hcoll; subst. + simpl. + eapply BI_Wand_L; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Wand_L; eauto. + rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + - (* bot L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_False_L. + - (* top R *) apply BI_True_R. + - (* top L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; subst; eauto. + by apply BI_Higher. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_True_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* conjR *) + apply bunch_decomp_complete in Heq. + inversion Heq; simplify_eq/=. + + rewrite fill_app /=. + eapply BI_Conj_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + + rewrite fill_app /=. + eapply BI_Conj_R; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + - (* conjL *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; simplify_eq/=; eauto. + assert (fill Π0 (Δ1;, frml ψ) ⊢ᴮ{ n0} χ) as H1. + { replace (fill Π0 (Δ1;, frml ψ))%B + with (fill ([CtxSemicL (frml ψ)]++Π0) Δ1) + by rewrite fill_app//. + eapply IHproves; eauto. } + replace (fill Π0 (Δ1;, Δ2))%B + with (fill ([CtxSemicR Δ1]++Π0) Δ2) + by rewrite fill_app//. + apply BI_Higher. + eapply IHproves; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Conj_L. + rewrite -HC0. + eapply IHproves; eauto. + apply bunch_decomp_correct. apply Hdec0. + - (* disj R 1 *) + eapply BI_Disj_R1. + eapply IHproves; eauto. + - (* disj R 2 *) + eapply BI_Disj_R2. + eapply IHproves; eauto. + - (* disj L *) + apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + inversion Hcoll; simplify_eq/=; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Disj_L. + * rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + * rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + - (* impl R *) + apply BI_Impl_R. + replace (fill Π Δ';, frml ϕ0)%B + with (fill (Π ++ [CtxSemicL (frml ϕ0)]) Δ')%B + by rewrite fill_app//. + eapply IHproves; eauto. rewrite -Heq fill_app /= //. + - apply bunch_decomp_complete in Heq. + apply bunch_decomp_ctx in Heq. + destruct Heq as [H1 | H2]. + + destruct H1 as [C1 [HC0 HC]]. + inversion HC0; simplify_eq/=. + * rewrite !fill_app/=. + eapply BI_Impl_L; eauto. + eapply IHproves; eauto; first lia. + by apply bunch_decomp_correct. + * inversion H6; subst. + inversion Hcoll; simplify_eq/=; eauto. + + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). + rewrite -HC1. + apply BI_Impl_L; eauto. + rewrite -HC0. + eapply IHproves; eauto; first lia. + apply bunch_decomp_correct. apply Hdec0. + Qed. + + +(** Derivable rules / inversion lemmas *) + +Lemma impl_r_inv Δ ϕ ψ : + (Δ ⊢ᴮ IMPL ϕ ψ) → + (Δ ;, frml ϕ ⊢ᴮ ψ)%B. +Proof. + intros [n H]%proves_provesN. + eapply provesN_proves. + by apply impl_r_inv'. +Qed. +Lemma wand_r_inv Δ ϕ ψ : + (Δ ⊢ᴮ WAND ϕ ψ) → + (Δ ,, frml ϕ ⊢ᴮ ψ)%B. +Proof. + intros [n H]%proves_provesN. + eapply provesN_proves. + by apply wand_r_inv'. +Qed. +Lemma sep_l_inv Π ϕ ψ χ : + (fill Π (frml (SEP ϕ ψ)) ⊢ᴮ χ) → + (fill Π (frml ϕ,, frml ψ) ⊢ᴮ χ). +Proof. + intros [n H]%proves_provesN. + eapply provesN_proves. + eapply collapse_l_inv'; eauto. + by repeat constructor. +Qed. +Lemma conj_l_inv Π ϕ ψ χ : + (fill Π (frml (CONJ ϕ ψ)) ⊢ᴮ χ) → + (fill Π (frml ϕ;, frml ψ) ⊢ᴮ χ). +Proof. + intros [n H]%proves_provesN. + eapply provesN_proves. + eapply collapse_l_inv'; eauto. + by repeat constructor. +Qed. + +Lemma box_l_inv Π Δ ϕ : + (fill Π (BOX <$> (BOX <$> Δ)) ⊢ᴮ ϕ) → + (fill Π (BOX <$> Δ) ⊢ᴮ ϕ). +Proof. + revert Π. induction Δ; simpl; eauto. + - intros Π [n H]%proves_provesN. + eapply provesN_proves. + eapply box_l_inv'; eauto. + - intros Π H1. + change (fill Π (bbin s (BOX <$> Δ1) (BOX <$> Δ2)))%B + with (fill (CtxR s (BOX <$> Δ1)::Π) (BOX <$> Δ2)). + apply IHΔ2. simpl. + change (fill Π (bbin s (BOX <$> Δ1) (BOX <$> (BOX <$> Δ2))))%B + with (fill (CtxL s (BOX <$> (BOX <$> Δ2))::Π) (BOX <$> Δ1)). + apply IHΔ1. simpl. done. +Qed. + +Lemma BI_Collapse_L_inv Π Δ ϕ : + (fill Π (frml (collapse Δ)) ⊢ᴮ ϕ) → + (fill Π Δ ⊢ᴮ ϕ). +Proof. + intros [n H]%proves_provesN. + eapply provesN_proves. + eapply collapse_l_inv'; eauto. + apply collapse_gr_sound. +Qed. + +End SeqcalcHeight. diff --git a/theories/seqcalc.v b/theories/seqcalc.v index 6cdff72..3291993 100644 --- a/theories/seqcalc.v +++ b/theories/seqcalc.v @@ -2,7 +2,7 @@ From Coq Require Import ssreflect. From stdpp Require Import prelude gmap fin_sets. From bunched.algebra Require Import bi. -From bunched Require Export syntax interp terms. +From bunched Require Export bunches formula terms interp. Module Type ANALYTIC_STRUCT_EXT. (** An _analytic structural rule_ is a rule of the form @@ -138,7 +138,7 @@ Proof. Qed. (** "Collapsing" a bunch as a derived left rule *) -Lemma collapse_l (Π : bunch_ctx) (Δ : bunch) (ϕ : formula) : +Lemma BI_Collapse_L (Π : bunch_ctx) (Δ : bunch) (ϕ : formula) : (fill Π Δ ⊢ᴮ ϕ) → fill Π (frml (collapse Δ)) ⊢ᴮ ϕ. Proof. revert Π. induction Δ=>Π; simpl; eauto. @@ -182,7 +182,7 @@ Proof. apply bi.and_intro; eauto. - assert (rule_valid PROP Ts T) as HH. { eapply Hrules; auto. } - specialize (HH (bunch_interp s ∘ Δs)). + specialize (HH (bunch_interp (formula_interp s) ∘ Δs)). rewrite bunch_ctx_interp_decomp. rewrite bterm_ctx_alg_act. rewrite HH. @@ -207,7 +207,7 @@ Proof. - by apply bi.or_intro_l. - by apply bi.or_intro_r. - rewrite bunch_ctx_interp_decomp. simpl. - trans (bunch_ctx_interp PROP s Π (∃ (x : bool), if x then bunch_interp s (frml ϕ) else bunch_interp s (frml ψ))). + trans (bunch_ctx_interp PROP (formula_interp s) Π (∃ (x : bool), if x then bunch_interp (formula_interp s) (frml ϕ) else bunch_interp (formula_interp s) (frml ψ))). { apply bunch_ctx_interp_mono. apply bi.or_elim. - by eapply (bi.exist_intro' _ _ true). diff --git a/theories/seqcalc_height.v b/theories/seqcalc_height.v index 2dd1f06..3e89e37 100644 --- a/theories/seqcalc_height.v +++ b/theories/seqcalc_height.v @@ -806,7 +806,7 @@ Module SeqcalcHeight(R : ANALYTIC_STRUCT_EXT). eapply collapse_l_inv'; eauto. by repeat constructor. Qed. - Lemma collapse_l_inv C Δ ϕ : + Lemma BI_Collapse_L_inv C Δ ϕ : (fill C (frml (collapse Δ)) ⊢ᴮ ϕ) → (fill C Δ ⊢ᴮ ϕ). Proof. diff --git a/theories/seqcalc_height_s4.v b/theories/seqcalc_height_s4.v deleted file mode 100644 index 9a63ac5..0000000 --- a/theories/seqcalc_height_s4.v +++ /dev/null @@ -1,1785 +0,0 @@ -(* Sequent calculus with upper bounds on proof size. - Useful for doing induction on. - - The main purpose this file is to provide the inversion lemmas (at the very bottom of the file). - *) -From Coq Require Import ssreflect. -From stdpp Require Import prelude. -From bunched.algebra Require Import bi. -From bunched Require Import seqcalc_s4. - -Reserved Notation "P ⊢ᴮ{ n } Q" (at level 99, n, Q at level 200, right associativity). -Reserved Notation "Δ =?{ n } Δ'" (at level 99, n at level 200). - -Section SeqcalcHeight. - - Implicit Type Δ : bunch. - Implicit Type ψ ϕ : formula. - - (** ** Alternative formulation of bunch equivalences *) - Inductive bunch_equiv : bunch → bunch → Prop := - | BE_cong Π Δ1 Δ2 : - Δ1 =? Δ2 → - fill Π Δ1 =? fill Π Δ2 - | BE_comma_unit_l Δ : - (empty ,, Δ)%B =? Δ - | BE_comma_comm Δ1 Δ2 : - (Δ1 ,, Δ2)%B =? (Δ2 ,, Δ1)%B - | BE_comma_assoc Δ1 Δ2 Δ3 : (Δ1 ,, (Δ2 ,, Δ3))%B =? ((Δ1 ,, Δ2) ,, Δ3)%B - | BE_semic_unit_l Δ : (top ;, Δ)%B =? Δ - | BE_semic_comm Δ1 Δ2 : (Δ1 ;, Δ2)%B =? (Δ2 ;, Δ1)%B - | BE_semic_assoc Δ1 Δ2 Δ3 : (Δ1 ;, (Δ2 ;, Δ3))%B =? ((Δ1 ;, Δ2) ;, Δ3)%B - where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B). - - Definition bunch_equiv_h := rtsc (bunch_equiv). - - Lemma bunch_equiv_1 Δ Δ' : - (Δ =? Δ') → (Δ ≡ Δ'). - Proof. induction 1; by econstructor; eauto. Qed. - - Lemma bunch_equiv_2 Δ Δ' : - (Δ ≡ Δ') → (bunch_equiv_h Δ Δ'). - Proof. - induction 1. - all: try by (eapply rtsc_lr; econstructor). - - unfold bunch_equiv_h. reflexivity. - - by symmetry. - - etrans; eauto. - - eapply rtc_congruence; eauto. - intros X Y. apply sc_congruence. clear X Y. - intros X Y ?. by econstructor. - Qed. - - Local Lemma bunch_equiv_fill_1 Δ Π ϕ : - fill Π (frml ϕ) =? Δ → - ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). - Proof. - intros Heq. - remember (fill Π (frml ϕ)) as Y. - revert Π HeqY. - induction Heq=>C' heqY; symmetry in heqY. - + apply bunch_decomp_complete in heqY. - apply bunch_decomp_ctx in heqY. - destruct heqY as [H1 | H2]. - * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]]. - destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]]. - simplify_eq/=. - exists (C2 ++ Π). rewrite fill_app. split; first done. - intros Δ. rewrite !fill_app HC2 //. - * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0). - specialize (Hdec0 Δ2). apply bunch_decomp_correct in Hdec0. - exists (C1 Δ2). split ; eauto. - intros Δ. rewrite HC1. - assert (Δ1 ≡ Δ2) as <-. - { by apply bunch_equiv_1. } - by rewrite HC2. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - { inversion H3. } - apply bunch_decomp_correct in H3. - exists Π. split; eauto. - intros X. rewrite fill_app /= left_id //. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxCommaR Δ2]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - * exists (Π ++ [CtxCommaL Δ1]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxCommaL Δ2;CtxCommaL Δ3])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - * inversion H3; simplify_eq/=. - ** exists (Π0 ++ [CtxCommaR Δ1;CtxCommaL Δ3])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - ** exists (Π0 ++ [CtxCommaR (Δ1,,Δ2)])%B. split. - { simpl. rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - { inversion H3. } - apply bunch_decomp_correct in H3. - exists Π. split; eauto. - intros X. rewrite fill_app /= left_id //. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxSemicR Δ2]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - * exists (Π ++ [CtxSemicL Δ1]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxSemicL Δ2;CtxSemicL Δ3])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - * inversion H3; simplify_eq/=. - ** exists (Π0 ++ [CtxSemicR Δ1;CtxSemicL Δ3])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - ** exists (Π0 ++ [CtxSemicR (Δ1;,Δ2)])%B. split. - { simpl. rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - Qed. - - Local Lemma bunch_equiv_fill_2 Δ Π ϕ : - Δ =? fill Π (frml ϕ) → - ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). - Proof. - intros Heq. - remember (fill Π (frml ϕ)) as Y. - revert Π HeqY. - induction Heq=>C' heqY; symmetry in heqY. - + apply bunch_decomp_complete in heqY. - apply bunch_decomp_ctx in heqY. - destruct heqY as [H1 | H2]. - * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]]. - destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]]. - simplify_eq/=. - exists (C2 ++ Π). rewrite fill_app. split; first done. - intros Δ. rewrite !fill_app HC2 //. - * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0). - specialize (Hdec0 Δ1). apply bunch_decomp_correct in Hdec0. - exists (C1 Δ1). split ; eauto. - intros Δ. rewrite HC1. - assert (Δ1 ≡ Δ2) as ->. - { by apply bunch_equiv_1. } - by rewrite HC2. - + exists (C' ++ [CtxCommaR empty]). simpl; split. - { rewrite fill_app /=. by rewrite heqY. } - intros X; rewrite fill_app/=. - by rewrite left_id. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxCommaR Δ1]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - * exists (Π ++ [CtxCommaL Δ2]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * inversion H3; simplify_eq/=. - ** exists (Π0 ++ [CtxCommaL (Δ2 ,, Δ3)])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - ** exists (Π0 ++ [CtxCommaL Δ3;CtxCommaR Δ1])%B. split. - { simpl. rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - * exists (Π ++ [CtxCommaR Δ2;CtxCommaR Δ1])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - + exists (C' ++ [CtxSemicR top]). simpl; split. - { rewrite fill_app /=. by rewrite heqY. } - intros X; rewrite fill_app/=. - by rewrite left_id. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * exists (Π ++ [CtxSemicR Δ1]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - * exists (Π ++ [CtxSemicL Δ2]). split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite comm. - + apply bunch_decomp_complete in heqY. - inversion heqY; simplify_eq/=. - * inversion H3; simplify_eq/=. - ** exists (Π0 ++ [CtxSemicL (Δ2 ;, Δ3)])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - ** exists (Π0 ++ [CtxSemicL Δ3;CtxSemicR Δ1])%B. split. - { simpl. rewrite fill_app/=. - apply bunch_decomp_correct in H4. - by rewrite H4. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - * exists (Π ++ [CtxSemicR Δ2;CtxSemicR Δ1])%B. split. - { rewrite fill_app/=. - apply bunch_decomp_correct in H3. - by rewrite H3. } - intros Δ. rewrite !fill_app/=. - by rewrite assoc. - Qed. - - Lemma bunch_equiv_fill Δ Π ϕ : - Δ ≡ (fill Π (frml ϕ)) → - ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ). - Proof. - intros H%bunch_equiv_2. - revert Δ H. eapply rtc_ind_l. - { exists Π. eauto. } - intros X Y HXY HY. clear HY. - intros (C0 & -> & HC0). - destruct HXY as [HXY|HXY]. - - apply bunch_equiv_fill_2 in HXY. - destruct HXY as (C' & -> & HC'). - eexists; split; eauto. - intros ?. by rewrite HC' HC0. - - apply bunch_equiv_fill_1 in HXY. - destruct HXY as (C' & -> & HC'). - eexists; split; eauto. - intros ?. by rewrite HC' HC0. - Qed. - - (** * SEQUENT CALCULUS *) - Polymorphic Inductive proves : bunch → formula → nat → Prop := - (* structural *) - | BI_Higher Δ ϕ n : (Δ ⊢ᴮ{n} ϕ) → (Δ ⊢ᴮ{S n} ϕ) - | BI_Axiom (a : atom) : frml (ATOM a) ⊢ᴮ{0} ATOM a - | BI_Equiv Δ Δ' ϕ n : - (Δ ≡ Δ') → (Δ ⊢ᴮ{n} ϕ) → - Δ' ⊢ᴮ{S n} ϕ - | BI_Weaken Π Δ Δ' ϕ n : (fill Π Δ ⊢ᴮ{n} ϕ) → - fill Π (Δ ;, Δ') ⊢ᴮ{S n} ϕ - | BI_Contr Π Δ ϕ n : (fill Π (Δ ;, Δ) ⊢ᴮ{n} ϕ) → - fill Π Δ ⊢ᴮ{S n} ϕ - (* | BI_Cut Π Δ ϕ ψ : (Δ ⊢ᴮ ψ) → *) - (* (fill Π (frml ψ) ⊢ᴮ ϕ) → *) - (* fill Π Δ ⊢ᴮ ϕ *) - (* modal *) - | BI_Box_L Π ϕ ψ n : - (fill Π (frml ϕ) ⊢ᴮ{n} ψ) → - fill Π (frml (BOX ϕ)) ⊢ᴮ{S n} ψ - | BI_Box_R Δ ϕ n : - (BOX <·> Δ ⊢ᴮ{n} ϕ) → - BOX <·> Δ ⊢ᴮ{S n} BOX ϕ - (* multiplicatives *) - | BI_Emp_R : - empty ⊢ᴮ{0} EMP - | BI_Emp_L Π ϕ n : - (fill Π empty ⊢ᴮ{n} ϕ) → - fill Π (frml EMP) ⊢ᴮ{S n} ϕ - | BI_Sep_R Δ Δ' ϕ ψ n m : - (Δ ⊢ᴮ{n} ϕ) → - (Δ' ⊢ᴮ{m} ψ) → - Δ ,, Δ' ⊢ᴮ{S (n `max` m)} SEP ϕ ψ - | BI_Sep_L Π ϕ ψ χ n : - (fill Π (frml ϕ ,, frml ψ) ⊢ᴮ{n} χ) → - fill Π (frml (SEP ϕ ψ)) ⊢ᴮ{S n} χ - | BI_Wand_R Δ ϕ ψ n : - (Δ ,, frml ϕ ⊢ᴮ{n} ψ) → - Δ ⊢ᴮ{S n} WAND ϕ ψ - | BI_Wand_L Π Δ ϕ ψ χ n m : - (Δ ⊢ᴮ{n} ϕ) → - (fill Π (frml ψ) ⊢ᴮ{m} χ) → - fill Π (Δ ,, frml (WAND ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ - (* additives *) - | BI_False_L Π ϕ : - fill Π (frml BOT) ⊢ᴮ{0} ϕ - | BI_True_R Δ : - Δ ⊢ᴮ{0} TOP - | BI_True_L Π ϕ n : - (fill Π top ⊢ᴮ{n} ϕ) → - fill Π (frml TOP) ⊢ᴮ{S n} ϕ - | BI_Conj_R Δ Δ' ϕ ψ n m : - (Δ ⊢ᴮ{n} ϕ) → - (Δ' ⊢ᴮ{m} ψ) → - Δ ;, Δ' ⊢ᴮ{S (n `max` m)} CONJ ϕ ψ - | BI_Conj_L Π ϕ ψ χ n : - (fill Π (frml ϕ ;, frml ψ) ⊢ᴮ{n} χ) → - fill Π (frml (CONJ ϕ ψ)) ⊢ᴮ{S n} χ - | BI_Disj_R1 Δ ϕ ψ n : - (Δ ⊢ᴮ{n} ϕ) → - Δ ⊢ᴮ{S n} DISJ ϕ ψ - | BI_Disj_R2 Δ ϕ ψ n : - (Δ ⊢ᴮ{n} ψ) → - Δ ⊢ᴮ{S n} DISJ ϕ ψ - | BI_Disj_L Π ϕ ψ χ n m : - (fill Π (frml ϕ) ⊢ᴮ{n} χ) → - (fill Π (frml ψ) ⊢ᴮ{m} χ) → - fill Π (frml (DISJ ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ - | BI_Impl_R Δ ϕ ψ n : - (Δ ;, frml ϕ ⊢ᴮ{n} ψ) → - Δ ⊢ᴮ{S n} IMPL ϕ ψ - | BI_Impl_L Π Δ ϕ ψ χ n m: - (Δ ⊢ᴮ{n} ϕ) → - (fill Π (frml ψ) ⊢ᴮ{m} χ) → - fill Π (Δ ;, frml (IMPL ϕ ψ)) ⊢ᴮ{S (n `max` m)} χ - where "Δ ⊢ᴮ{ n } ϕ" := (proves Δ%B ϕ%B n). - - Lemma provesN_proves n Δ ϕ : - (Δ ⊢ᴮ{ n } ϕ) → Δ ⊢ᴮ ϕ. - Proof. - induction 1; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - by econstructor; eauto. - Qed. - - Lemma proves_provesN Δ ϕ : - (Δ ⊢ᴮ ϕ) → ∃ n, Δ ⊢ᴮ{n} ϕ. - Proof. - induction 1. - all: try destruct IHproves as [n IH]. - all: try (destruct IHproves1 as [n1 IH1]; - destruct IHproves2 as [n2 IH2]). - all: try by eexists; econstructor; eauto. - Qed. - - (** * Inversion lemmas *) - Local Ltac bind_ctx := - match goal with - | [ |- fill ?Π ?Δ,, ?Δ' ⊢ᴮ{_} _ ] => - replace (fill Π Δ,, Δ')%B - with (fill (Π ++ [CtxCommaL Δ']) Δ)%B - by rewrite fill_app// - | [ |- fill ?Π ?Δ;, ?Δ' ⊢ᴮ{_} _ ] => - replace (fill Π Δ;, Δ')%B - with (fill (Π ++ [CtxSemicL Δ']) Δ)%B - by rewrite fill_app// - end. - - Local Ltac commute_left_rule IH := - intros ->; bind_ctx; - econstructor; eauto; rewrite fill_app; by eapply IH. - - Lemma wand_r_inv' Δ ϕ ψ n : - (Δ ⊢ᴮ{n} WAND ϕ ψ) → - (Δ ,, frml ϕ ⊢ᴮ{n} ψ)%B. - Proof. - remember (WAND ϕ ψ) as A. - intros H. revert ϕ ψ HeqA. - induction H; intros A B; try by inversion 1. - all: try by (commute_left_rule IHproves). - - intros ->. by constructor; apply IHproves. - - intros ->. eapply BI_Equiv. - { rewrite -H. reflexivity. } - by apply IHproves. - - intros ?; simplify_eq/=. by apply BI_Higher. - - commute_left_rule IHproves2. - - intros ?; simplify_eq/=. - bind_ctx. eapply BI_Disj_L. - + rewrite fill_app/=. by eapply IHproves1. - + rewrite fill_app/=. by eapply IHproves2. - - commute_left_rule IHproves2. - Qed. - - Lemma impl_r_inv' Δ ϕ ψ n : - (Δ ⊢ᴮ{n} IMPL ϕ ψ) → - (Δ ;, frml ϕ ⊢ᴮ{n} ψ)%B. - Proof. - remember (IMPL ϕ ψ) as A. - intros H. revert ϕ ψ HeqA. - induction H; intros A B; try by inversion 1. - all: try by (commute_left_rule IHproves). - - intros ->. by constructor; apply IHproves. - - intros ->. eapply BI_Equiv. - { rewrite -H. reflexivity. } - by apply IHproves. - - commute_left_rule IHproves2. - - intros ?; simplify_eq/=. - bind_ctx. eapply BI_Disj_L. - + rewrite fill_app/=. by eapply IHproves1. - + rewrite fill_app/=. by eapply IHproves2. - - intros ?; simplify_eq/=. by apply BI_Higher. - - commute_left_rule IHproves2. - Qed. - - Lemma box_l_inv' Δ Π ϕ χ n : - (Δ ⊢ᴮ{n} χ) → - Δ = fill Π (frml (BOX (BOX ϕ))) → - (fill Π (frml (BOX ϕ)) ⊢ᴮ{n} χ). - Proof. - revert Π Δ χ. - induction n using lt_wf_ind. rename H into IHproves. - intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. - inversion PROOF; simplify_eq/= => Heq. - - (* raising the pf height *) - apply BI_Higher. - eapply IHproves; eauto. - - (* axiom *) - apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. - - (* equivalence of bunches *) - simplify_eq/=. - destruct (bunch_equiv_fill _ _ _ H) as [Π2 [-> HΠ2]]. - eapply BI_Equiv. - { apply HΠ2. } - eapply IHproves; eauto. - - (* weakening *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [Π1 [HΠ0 HΠ]]. - inversion HΠ0; simplify_eq/=. - * rewrite !fill_app/=. - apply BI_Weaken. - rewrite -fill_app. - eapply IHproves; eauto. - by apply bunch_decomp_correct, bunch_decomp_app. - * rewrite !fill_app/=. - by apply BI_Weaken. - + rename Π into Π'. - rename Π0 into Π0'. - destruct H2 as (Π0 & Π1 & HΠ0 & HΠ1 & Hdec0). - rewrite -HΠ1. - apply BI_Weaken. - rewrite -HΠ0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* contraction *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]; last first. - + rename Π0 into Π0'. - destruct H2 as (Π0 & Π1 & HΠ0 & HΠ1 & Hdec0). - rewrite -HΠ1. - apply BI_Contr. - rewrite -HΠ0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - + destruct H1 as [C0 [HC0 ->]]. - apply bunch_decomp_correct in HC0. - simplify_eq/=. - rename Π0 into Π. - assert (fill Π (fill C0 (frml (BOX ϕ));, fill C0 (frml (BOX (BOX ϕ)))) ⊢ᴮ{ n0} χ) as IH1. - { specialize (IHproves n0 (lt_n_Sn _)). - set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml (BOX (BOX ϕ))))] ++ Π)%B). - specialize (IHproves C2 _ _ H). - revert IHproves. rewrite /C2 !fill_app /=. - eauto. } - rewrite fill_app. - apply BI_Contr. - set (C2 := (C0 ++ [CtxSemicR (fill C0 (frml (BOX ϕ)))] ++ Π)%B). - replace (fill Π (fill C0 (frml (BOX ϕ));, fill C0 (frml (BOX ϕ))))%B - with (fill C2 (frml (BOX ϕ)))%B by rewrite fill_app//. - eapply IHproves; eauto. - rewrite /C2 fill_app/=//. - - (* box L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - by apply BI_Higher. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Box_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* box R *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_box in Heq. - destruct Heq as (Π' & -> & ->%bunch_decomp_correct). - change (frml (BOX ϕ)) with (BOX <·> (frml ϕ)). - rewrite -(bunch_map_fill BOX). apply BI_Box_R. - rewrite bunch_map_fill /=. eapply IHproves; eauto. - rewrite bunch_map_fill //. - - (* emp R *) - exfalso. - apply bunch_decomp_complete in Heq. - inversion Heq. - - (* emp L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Emp_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* sep R *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* sep L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Sep_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* wand R *) - apply BI_Wand_R. - assert ((fill Π (frml (BOX ϕ)),, frml ϕ0) = - fill (Π ++ [CtxCommaL (frml ϕ0)]) (frml (BOX ϕ)))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* wand L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Wand_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Wand_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* bot L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_False_L. - - (* top R *) apply BI_True_R. - - (* top L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_True_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* conjR *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* conjL *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Conj_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* disj R 1 *) - eapply BI_Disj_R1. - eapply IHproves; eauto. - - (* disj R 2 *) - eapply BI_Disj_R2. - eapply IHproves; eauto. - - (* disj L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Disj_L. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* impl R *) - apply BI_Impl_R. - assert ((fill Π (frml (BOX ϕ));, frml ϕ0) = - fill (Π ++ [CtxSemicL (frml ϕ0)]) (frml (BOX ϕ)))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* impl L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Impl_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Impl_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - Qed. - - Lemma sep_l_inv' Δ Π ϕ ψ χ n : - (Δ ⊢ᴮ{n} χ) → - Δ = fill Π (frml (SEP ϕ ψ)) → - (fill Π (frml ϕ,, frml ψ) ⊢ᴮ{n} χ). - Proof. - revert Π Δ χ. - induction n using lt_wf_ind. rename H into IHproves. - intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. - inversion PROOF; simplify_eq/= => Heq. - (* induction H => C' Heq; symmetry in Heq. *) - - (* raising the pf height *) - apply BI_Higher. - eapply IHproves; eauto. - - (* axiom *) - apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. - (* eapply BI_Sep_R; by econstructor. *) - - (* equivalence of bunches *) - simplify_eq/=. - destruct (bunch_equiv_fill _ _ _ H) as [C2 [-> HC2]]. - eapply BI_Equiv. - { apply HC2. } - eapply IHproves; eauto. - - (* weakening *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - apply BI_Weaken. - rewrite -fill_app. - eapply IHproves; eauto. - by apply bunch_decomp_correct, bunch_decomp_app. - * rewrite !fill_app/=. - by apply BI_Weaken. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Weaken. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* contraction *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]; last first. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Contr. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - + rename Π0 into C'. - destruct H1 as [C0 [HC0 ->]]. - apply bunch_decomp_correct in HC0. - simplify_eq/=. - assert (fill C' (fill C0 (frml ϕ,, frml ψ);, fill C0 (frml (SEP ϕ ψ))) ⊢ᴮ{ n0} χ) as IH1. - { specialize (IHproves n0 (lt_n_Sn _)). - set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml (SEP ϕ ψ)))] ++ C')%B). - specialize (IHproves C2 _ _ H). - revert IHproves. rewrite /C2 !fill_app /=. - eauto. } - rewrite fill_app. - apply BI_Contr. - set (C2 := (C0 ++ [CtxSemicR (fill C0 (frml ϕ,, frml ψ))] ++ C')%B). - replace (fill C' (fill C0 (frml ϕ,, frml ψ);, fill C0 (frml ϕ,, frml ψ)))%B - with (fill C2 (frml ϕ,, frml ψ))%B by rewrite fill_app//. - eapply IHproves; eauto. - rewrite /C2 fill_app//. - - (* box L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Box_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* box R *) - exfalso. - apply bunch_decomp_complete in Heq. - simplify_eq/=. - rename Δ0 into Δ. revert Π Heq. clear. - induction Δ as [ | | | Δ1 IH1 Δ2 IH2 | Δ1 IH1 Δ2 IH2] => Π /=; - inversion 1; simplify_eq/=; - solve [ by eapply IH1 | by eapply IH2 ]. - - (* emp R *) - exfalso. - apply bunch_decomp_complete in Heq. - inversion Heq. - - (* emp L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Emp_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* sep R *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* sep L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - by apply BI_Higher. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Sep_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* wand R *) - apply BI_Wand_R. - assert ((fill Π (frml ϕ,, frml ψ),, frml ϕ0) = - fill (Π ++ [CtxCommaL (frml ϕ0)]) (frml ϕ,, frml ψ))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* wand L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Wand_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Wand_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* bot L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_False_L. - - (* top R *) apply BI_True_R. - - (* top L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_True_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* conjR *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* conjL *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Conj_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* disj R 1 *) - eapply BI_Disj_R1. - eapply IHproves; eauto. - - (* disj R 2 *) - eapply BI_Disj_R2. - eapply IHproves; eauto. - - (* disj L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Disj_L. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* impl R *) - apply BI_Impl_R. - assert ((fill Π (frml ϕ,, frml ψ);, frml ϕ0) = - fill (Π ++ [CtxSemicL (frml ϕ0)]) (frml ϕ,, frml ψ))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Impl_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Impl_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - Qed. - - Lemma conj_l_inv' Δ Π ϕ ψ χ n : - (Δ ⊢ᴮ{n} χ) → - Δ = fill Π (frml (CONJ ϕ ψ)) → - (fill Π (frml ϕ;, frml ψ) ⊢ᴮ{n} χ). - Proof. - revert Π Δ χ. - induction n using lt_wf_ind. rename H into IHproves. - intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. - inversion PROOF; simplify_eq/= => Heq. - (* induction H => C' Heq; symmetry in Heq. *) - - (* raising the pf height *) - apply BI_Higher. - eapply IHproves; eauto. - - (* axiom *) - apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. - (* eapply BI_Sep_R; by econstructor. *) - - (* equivalence of bunches *) - simplify_eq/=. - destruct (bunch_equiv_fill _ _ _ H) as [C2 [-> HC2]]. - eapply BI_Equiv. - { apply HC2. } - eapply IHproves; eauto. - - (* weakening *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - apply BI_Weaken. - rewrite -fill_app. - eapply IHproves; eauto. - by apply bunch_decomp_correct, bunch_decomp_app. - * rewrite !fill_app/=. - by apply BI_Weaken. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Weaken. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* contraction *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]; last first. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Contr. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - + rename Π0 into C'. - destruct H1 as [C0 [HC0 ->]]. - apply bunch_decomp_correct in HC0. - simplify_eq/=. - assert (fill C' (fill C0 (frml ϕ;, frml ψ);, fill C0 (frml (CONJ ϕ ψ))) ⊢ᴮ{ n0} χ) as IH1. - { specialize (IHproves n0 (lt_n_Sn _)). - set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml (CONJ ϕ ψ)))] ++ C')%B). - specialize (IHproves C2 _ _ H). - revert IHproves. rewrite /C2 !fill_app /=. - eauto. } - rewrite fill_app. - apply BI_Contr. - set (C2 := (C0 ++ [CtxSemicR (fill C0 (frml ϕ;, frml ψ))] ++ C')%B). - replace (fill C' (fill C0 (frml ϕ;, frml ψ);, fill C0 (frml ϕ;, frml ψ)))%B - with (fill C2 (frml ϕ;, frml ψ))%B by rewrite fill_app//. - eapply IHproves; eauto. - rewrite /C2 fill_app//. - - (* box L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Box_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* box R *) - exfalso. - apply bunch_decomp_complete in Heq. - simplify_eq/=. - rename Δ0 into Δ. revert Π Heq. clear. - induction Δ as [ | | | Δ1 IH1 Δ2 IH2 | Δ1 IH1 Δ2 IH2] => Π /=; - inversion 1; simplify_eq/=; - solve [ by eapply IH1 | by eapply IH2 ]. - - (* emp R *) - exfalso. - apply bunch_decomp_complete in Heq. - inversion Heq. - - (* emp L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Emp_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* sep R *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* sep L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Sep_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* wand R *) - apply BI_Wand_R. - assert ((fill Π (frml ϕ;, frml ψ),, frml ϕ0) = - fill (Π ++ [CtxCommaL (frml ϕ0)]) (frml ϕ;, frml ψ))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* wand L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Wand_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Wand_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* bot L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_False_L. - - (* top R *) apply BI_True_R. - - (* top L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_True_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* conjR *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* conjL *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - by apply BI_Higher. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Conj_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* disj R 1 *) - eapply BI_Disj_R1. - eapply IHproves; eauto. - - (* disj R 2 *) - eapply BI_Disj_R2. - eapply IHproves; eauto. - - (* disj L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Disj_L. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* impl R *) - apply BI_Impl_R. - assert ((fill Π (frml ϕ;, frml ψ);, frml ϕ0) = - fill (Π ++ [CtxSemicL (frml ϕ0)]) (frml ϕ;, frml ψ))%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Impl_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Impl_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - Qed. - - Lemma top_l_inv' Δ Π ϕ ψ χ n : - (Δ ⊢ᴮ{n} χ) → - Δ = fill Π (frml TOP) → - (fill Π top ⊢ᴮ{n} χ). - Proof. - revert Π Δ χ. - induction n using lt_wf_ind. rename H into IHproves. - intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. - inversion PROOF; simplify_eq/= => Heq. - (* induction H => C' Heq; symmetry in Heq. *) - - (* raising the pf height *) - apply BI_Higher. - eapply IHproves; eauto. - - (* axiom *) - apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. - - (* equivalence of bunches *) - simplify_eq/=. - destruct (bunch_equiv_fill _ _ _ H) as [C2 [-> HC2]]. - eapply BI_Equiv. - { apply HC2. } - eapply IHproves; eauto. - - (* weakening *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - apply BI_Weaken. - rewrite -fill_app. - eapply IHproves; eauto. - by apply bunch_decomp_correct, bunch_decomp_app. - * rewrite !fill_app/=. - by apply BI_Weaken. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Weaken. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* contraction *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]; last first. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Contr. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - + rename Π0 into C'. - destruct H1 as [C0 [HC0 ->]]. - apply bunch_decomp_correct in HC0. - simplify_eq/=. - assert (fill C' (fill C0 top;, fill C0 (frml TOP)) ⊢ᴮ{ n0} χ) as IH1. - { specialize (IHproves n0 (lt_n_Sn _)). - set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml TOP))] ++ C')%B). - specialize (IHproves C2 _ _ H). - revert IHproves. rewrite /C2 !fill_app /=. - eauto. } - rewrite fill_app. - apply BI_Contr. - set (C2 := (C0 ++ [CtxSemicR (fill C0 top)] ++ C')%B). - replace (fill C' (fill C0 top;, fill C0 top))%B - with (fill C2 top)%B by rewrite fill_app//. - eapply IHproves; eauto. - rewrite /C2 fill_app//. - - (* box L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Box_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* box R *) - exfalso. - apply bunch_decomp_complete in Heq. - simplify_eq/=. - rename Δ0 into Δ. revert Π Heq. clear. - induction Δ as [ | | | Δ1 IH1 Δ2 IH2 | Δ1 IH1 Δ2 IH2] => Π /=; - inversion 1; simplify_eq/=; - solve [ by eapply IH1 | by eapply IH2 ]. - - (* emp R *) - exfalso. - apply bunch_decomp_complete in Heq. - inversion Heq. - - (* emp L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Emp_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* sep R *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* sep L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Sep_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* wand R *) - apply BI_Wand_R. - assert ((fill Π top,, frml ϕ0) = - fill (Π ++ [CtxCommaL (frml ϕ0)]) top)%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* wand L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Wand_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Wand_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* bot L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_False_L. - - (* top R *) apply BI_True_R. - - (* top L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - by eapply BI_Higher. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_True_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* conjR *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* conjL *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Conj_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* disj R 1 *) - eapply BI_Disj_R1. - eapply IHproves; eauto. - - (* disj R 2 *) - eapply BI_Disj_R2. - eapply IHproves; eauto. - - (* disj L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Disj_L. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* impl R *) - apply BI_Impl_R. - assert ((fill Π top;, frml ϕ0) = - fill (Π ++ [CtxSemicL (frml ϕ0)]) top)%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Impl_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Impl_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - Qed. - - Lemma emp_l_inv' Δ Π ϕ ψ χ n : - (Δ ⊢ᴮ{n} χ) → - Δ = fill Π (frml EMP) → - (fill Π empty ⊢ᴮ{n} χ). - Proof. - revert Π Δ χ. - induction n using lt_wf_ind. rename H into IHproves. - intros Π Δ χ PROOF Heq. symmetry in Heq. revert Heq. - inversion PROOF; simplify_eq/= => Heq. - (* induction H => C' Heq; symmetry in Heq. *) - - (* raising the pf height *) - apply BI_Higher. - eapply IHproves; eauto. - - (* axiom *) - apply fill_is_frml in Heq. destruct_and!; simplify_eq/=. - - (* equivalence of bunches *) - simplify_eq/=. - destruct (bunch_equiv_fill _ _ _ H) as [C2 [-> HC2]]. - eapply BI_Equiv. - { apply HC2. } - eapply IHproves; eauto. - - (* weakening *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - apply BI_Weaken. - rewrite -fill_app. - eapply IHproves; eauto. - by apply bunch_decomp_correct, bunch_decomp_app. - * rewrite !fill_app/=. - by apply BI_Weaken. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Weaken. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* contraction *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]; last first. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Contr. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - + rename Π0 into C'. - destruct H1 as [C0 [HC0 ->]]. - apply bunch_decomp_correct in HC0. - simplify_eq/=. - assert (fill C' (fill C0 empty;, fill C0 (frml EMP)) ⊢ᴮ{ n0} χ) as IH1. - { specialize (IHproves n0 (lt_n_Sn _)). - set (C2 := (C0 ++ [CtxSemicL (fill C0 (frml EMP))] ++ C')%B). - specialize (IHproves C2 _ _ H). - revert IHproves. rewrite /C2 !fill_app /=. - eauto. } - rewrite fill_app. - apply BI_Contr. - set (C2 := (C0 ++ [CtxSemicR (fill C0 empty)] ++ C')%B). - replace (fill C' (fill C0 empty;, fill C0 empty))%B - with (fill C2 empty)%B by rewrite fill_app//. - eapply IHproves; eauto. - rewrite /C2 fill_app//. - - (* box L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Box_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* box R *) - exfalso. - apply bunch_decomp_complete in Heq. - simplify_eq/=. - rename Δ0 into Δ. revert Π Heq. clear. - induction Δ as [ | | | Δ1 IH1 Δ2 IH2 | Δ1 IH1 Δ2 IH2] => Π /=; - inversion 1; simplify_eq/=; - solve [ by eapply IH1 | by eapply IH2 ]. - - (* emp R *) - exfalso. - apply bunch_decomp_complete in Heq. - inversion Heq. - - (* emp L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - by eapply BI_Higher. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Emp_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* sep R *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Sep_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* sep L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Sep_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* wand R *) - apply BI_Wand_R. - assert ((fill Π empty,, frml ϕ0) = - fill (Π ++ [CtxCommaL (frml ϕ0)]) empty)%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - (* wand L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Wand_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Wand_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* bot L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_False_L. - - (* true R *) apply BI_True_R. - - (* true L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_True_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* conjR *) - apply bunch_decomp_complete in Heq. - inversion Heq; simplify_eq/=. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - + rewrite fill_app /=. - eapply BI_Conj_R; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - - (* conjL *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Conj_L. - rewrite -HC0. - eapply IHproves; eauto. - apply bunch_decomp_correct. apply Hdec0. - - (* disj R 1 *) - eapply BI_Disj_R1. - eapply IHproves; eauto. - - (* disj R 2 *) - eapply BI_Disj_R2. - eapply IHproves; eauto. - - (* disj L *) - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - + destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Disj_L. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - * rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - - (* impl R *) - apply BI_Impl_R. - assert ((fill Π empty;, frml ϕ0) = - fill (Π ++ [CtxSemicL (frml ϕ0)]) empty)%B as ->. - { rewrite fill_app//. } - eapply IHproves; eauto. rewrite -Heq fill_app /= //. - - apply bunch_decomp_complete in Heq. - apply bunch_decomp_ctx in Heq. - destruct Heq as [H1 | H2]. - + destruct H1 as [C1 [HC0 HC]]. - inversion HC0; simplify_eq/=. - * rewrite !fill_app/=. - eapply BI_Impl_L; eauto. - eapply IHproves; eauto; first lia. - by apply bunch_decomp_correct. - * exfalso. inversion H5. - + rename Π0 into C'. - destruct H2 as (C0 & C1 & HC0 & HC1 & Hdec0). - rewrite -HC1. - apply BI_Impl_L; eauto. - rewrite -HC0. - eapply IHproves; eauto; first lia. - apply bunch_decomp_correct. apply Hdec0. - Qed. - -(** Derivable rules / inversion lemmas *) - -Lemma impl_r_inv Δ ϕ ψ : - (Δ ⊢ᴮ IMPL ϕ ψ) → - (Δ ;, frml ϕ ⊢ᴮ ψ)%B. -Proof. - intros [n H]%proves_provesN. - eapply provesN_proves. - by apply impl_r_inv'. -Qed. -Lemma wand_r_inv Δ ϕ ψ : - (Δ ⊢ᴮ WAND ϕ ψ) → - (Δ ,, frml ϕ ⊢ᴮ ψ)%B. -Proof. - intros [n H]%proves_provesN. - eapply provesN_proves. - by apply wand_r_inv'. -Qed. -Lemma sep_l_inv Π ϕ ψ χ : - (fill Π (frml (SEP ϕ ψ)) ⊢ᴮ χ) → - (fill Π (frml ϕ,, frml ψ) ⊢ᴮ χ). -Proof. - intros [n H]%proves_provesN. - eapply provesN_proves. - eapply sep_l_inv'; eauto. -Qed. -Lemma conj_l_inv Π ϕ ψ χ : - (fill Π (frml (CONJ ϕ ψ)) ⊢ᴮ χ) → - (fill Π (frml ϕ;, frml ψ) ⊢ᴮ χ). -Proof. - intros [n H]%proves_provesN. - eapply provesN_proves. - eapply conj_l_inv'; eauto. -Qed. - -Lemma box_l_inv Π Δ ϕ : - (fill Π (BOX <·> (BOX <·> Δ)) ⊢ᴮ ϕ) → - (fill Π (BOX <·> Δ) ⊢ᴮ ϕ). -Proof. - revert Π. induction Δ; simpl; eauto. - - intros Π [n H]%proves_provesN. - eapply provesN_proves. - eapply box_l_inv'; eauto. - - intros Π H1. - replace (fill Π (BOX <·> Δ1,, (BOX <·> Δ2)))%B - with (fill (CtxCommaR (BOX <·> Δ1)::Π) (BOX <·> Δ2)) by reflexivity. - apply IHΔ2. simpl. - replace (fill Π (BOX <·> Δ1,, BOX <·> (BOX <·> Δ2)))%B - with (fill (CtxCommaL (BOX <·> (BOX <·> Δ2))::Π) (BOX <·> Δ1)) by reflexivity. - apply IHΔ1. simpl. done. - - intros Π H1. - replace (fill Π (BOX <·> Δ1;, (BOX <·> Δ2)))%B - with (fill (CtxSemicR (BOX <·> Δ1)::Π) (BOX <·> Δ2)) by reflexivity. - apply IHΔ2. simpl. - replace (fill Π (BOX <·> Δ1;, BOX <·> (BOX <·> Δ2)))%B - with (fill (CtxSemicL (BOX <·> (BOX <·> Δ2))::Π) (BOX <·> Δ1)) by reflexivity. - apply IHΔ1. simpl. done. -Qed. - -Lemma collapse_l_inv Π Δ ϕ : - (fill Π (frml (collapse Δ)) ⊢ᴮ ϕ) → - (fill Π Δ ⊢ᴮ ϕ). -Proof. - revert Π. induction Δ; simpl; first done. - - intros Π [n H]%proves_provesN. - eapply provesN_proves. - eapply top_l_inv'; eauto. - - intros Π [n H]%proves_provesN. - eapply provesN_proves. - eapply emp_l_inv'; eauto. - - intros Π H1. - replace (fill Π (Δ1,, Δ2))%B - with (fill (CtxCommaR Δ1::Π) Δ2) by reflexivity. - apply IHΔ2. simpl. - replace (fill Π (Δ1,, frml (collapse Δ2)))%B - with (fill (CtxCommaL (frml (collapse Δ2))::Π) Δ1) by reflexivity. - apply IHΔ1. simpl. - by apply sep_l_inv. - - intros Π H1. - replace (fill Π (Δ1;, Δ2))%B - with (fill (CtxSemicR Δ1::Π) Δ2) by reflexivity. - apply IHΔ2. simpl. - replace (fill Π (Δ1;, frml (collapse Δ2)))%B - with (fill (CtxSemicL (frml (collapse Δ2))::Π) Δ1) by reflexivity. - apply IHΔ1. simpl. - by apply conj_l_inv. -Qed. - -End SeqcalcHeight. diff --git a/theories/seqcalc_s4.v b/theories/seqcalc_s4.v deleted file mode 100644 index 995f58d..0000000 --- a/theories/seqcalc_s4.v +++ /dev/null @@ -1,453 +0,0 @@ -(** BI + □ *) -From Coq Require Import ssreflect. -From stdpp Require Import prelude. -From bunched.algebra Require Import bi. - -Declare Scope bunch_scope. -Delimit Scope bunch_scope with B. - -(** * Syntax and sequence calculus for BI□ *) - -Definition atom := nat. - -(** ** Formulas and bunches *) -Inductive formula : Type := -| TOP -| EMP -| BOT -| ATOM (A : atom) -| CONJ (ϕ ψ : formula) -| DISJ (ϕ ψ : formula) -| SEP (ϕ ψ : formula) -| IMPL (ϕ ψ : formula) -| WAND (ϕ ψ : formula) -| BOX (ϕ : formula) -. - -Inductive bunch : Type := -| frml (ϕ : formula) -| top : bunch -| empty : bunch -| comma (Δ1 Δ2 : bunch) -| semic (Δ1 Δ2 : bunch) -. - -Notation "Δ ';,' Γ" := (semic Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. -Notation "Δ ',,' Γ" := (comma Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. - -(** "Collapse" internalizes the bunch as a formula. *) -Fixpoint collapse (Δ : bunch) : formula := - match Δ with - | top => TOP - | empty => EMP - | frml ϕ => ϕ - | (Δ ,, Δ')%B => SEP (collapse Δ) (collapse Δ') - | (Δ ;, Δ')%B => CONJ (collapse Δ) (collapse Δ') - end. - -Fixpoint bunch_map (f : formula → formula) (Δ : bunch) : bunch := - match Δ with - | top => top - | empty => empty - | frml ϕ => frml (f ϕ) - | (Δ ,, Δ') => (bunch_map f Δ,, bunch_map f Δ') - | (Δ ;, Δ') => (bunch_map f Δ;, bunch_map f Δ') - end%B. - -Infix "<·>" := bunch_map (at level 61, left associativity) : stdpp_scope. - -(** Bunched contexts with a hole *) -Inductive bunch_ctx_item : Type := -| CtxCommaL (Δ2 : bunch) (* Δ ↦ Δ , Δ2 *) -| CtxCommaR (Δ1 : bunch) (* Δ ↦ Δ1, Δ *) -| CtxSemicL (Δ2 : bunch) (* Δ ↦ Δ; Δ2 *) -| CtxSemicR (Δ1 : bunch) (* Δ ↦ Δ1; Δ *) -. - -Definition bunch_ctx := list bunch_ctx_item. - -Definition fill_item (C : bunch_ctx_item) (Δ : bunch) : bunch := - match C with - | CtxCommaL Δ2 => Δ ,, Δ2 - | CtxCommaR Δ1 => Δ1 ,, Δ - | CtxSemicL Δ2 => Δ ;, Δ2 - | CtxSemicR Δ1 => Δ1 ;, Δ - end%B. - -Definition fill (Π : bunch_ctx) (Δ : bunch) : bunch := - foldl (flip fill_item) Δ Π. - -(** ** Bunch equivalence *) -(** Equivalence on bunches is defined to be the least congruence - that satisfies the monoidal laws for (empty and comma) and (top - and semicolon). *) -Inductive bunch_equiv : bunch → bunch → Prop := -| BE_refl Δ : Δ =? Δ -| BE_sym Δ1 Δ2 : Δ1 =? Δ2 → Δ2 =? Δ1 -| BE_trans Δ1 Δ2 Δ3 : Δ1 =? Δ2 → Δ2 =? Δ3 → Δ1 =? Δ3 -| BE_cong C Δ1 Δ2 : Δ1 =? Δ2 → fill C Δ1 =? fill C Δ2 -| BE_comma_unit_l Δ : (empty ,, Δ)%B =? Δ -| BE_comma_comm Δ1 Δ2 : (Δ1 ,, Δ2)%B =? (Δ2 ,, Δ1)%B -| BE_comma_assoc Δ1 Δ2 Δ3 : (Δ1 ,, (Δ2 ,, Δ3))%B =? ((Δ1 ,, Δ2) ,, Δ3)%B -| BE_semic_unit_l Δ : (top ;, Δ)%B =? Δ -| BE_semic_comm Δ1 Δ2 : (Δ1 ;, Δ2)%B =? (Δ2 ;, Δ1)%B -| BE_semic_assoc Δ1 Δ2 Δ3 : (Δ1 ;, (Δ2 ;, Δ3))%B =? ((Δ1 ;, Δ2) ;, Δ3)%B -where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B). - -(** Register [bunch_equiv] as [(≡)] *) -Global Instance equiv_bunch_equiv : Equiv bunch := bunch_equiv. - -(** ** Sequent calculus itself *) -Reserved Notation "P ⊢ᴮ Q" (at level 99, Q at level 200, right associativity). -Inductive proves : bunch → formula → Prop := -(* structural *) -| BI_Axiom (a : atom) : frml (ATOM a) ⊢ᴮ ATOM a -| BI_Equiv Δ Δ' ϕ : - (Δ ≡ Δ') → (Δ ⊢ᴮ ϕ) → - Δ' ⊢ᴮ ϕ -| BI_Weaken C Δ Δ' ϕ : (fill C Δ ⊢ᴮ ϕ) → - fill C (Δ ;, Δ') ⊢ᴮ ϕ -| BI_Contr C Δ ϕ : (fill C (Δ ;, Δ) ⊢ᴮ ϕ) → - fill C Δ ⊢ᴮ ϕ -(* modalities *) -| BI_Box_L Π ϕ ψ : - (fill Π (frml ϕ) ⊢ᴮ ψ) → - fill Π (frml (BOX ϕ)) ⊢ᴮ ψ -| BI_Box_R Δ ϕ : - (BOX <·> Δ ⊢ᴮ ϕ) → - BOX <·> Δ ⊢ᴮ BOX ϕ -(* multiplicatives *) -| BI_Emp_R : - empty ⊢ᴮ EMP -| BI_Emp_L C ϕ : - (fill C empty ⊢ᴮ ϕ) → - fill C (frml EMP) ⊢ᴮ ϕ -| BI_Sep_R Δ Δ' ϕ ψ : - (Δ ⊢ᴮ ϕ) → - (Δ' ⊢ᴮ ψ) → - Δ ,, Δ' ⊢ᴮ SEP ϕ ψ -| BI_Sep_L C ϕ ψ χ : - (fill C (frml ϕ ,, frml ψ) ⊢ᴮ χ) → - fill C (frml (SEP ϕ ψ)) ⊢ᴮ χ -| BI_Wand_R Δ ϕ ψ : - (Δ ,, frml ϕ ⊢ᴮ ψ) → - Δ ⊢ᴮ WAND ϕ ψ -| BI_Wand_L C Δ ϕ ψ χ : - (Δ ⊢ᴮ ϕ) → - (fill C (frml ψ) ⊢ᴮ χ) → - fill C (Δ ,, frml (WAND ϕ ψ)) ⊢ᴮ χ -(* additives *) -| BI_False_L C ϕ : - fill C (frml BOT) ⊢ᴮ ϕ -| BI_True_R Δ : - Δ ⊢ᴮ TOP -| BI_True_L C ϕ : - (fill C top ⊢ᴮ ϕ) → - fill C (frml TOP) ⊢ᴮ ϕ -| BI_Conj_R Δ Δ' ϕ ψ : - (Δ ⊢ᴮ ϕ) → - (Δ' ⊢ᴮ ψ) → - Δ ;, Δ' ⊢ᴮ CONJ ϕ ψ -| BI_Conj_L C ϕ ψ χ : - (fill C (frml ϕ ;, frml ψ) ⊢ᴮ χ) → - fill C (frml (CONJ ϕ ψ)) ⊢ᴮ χ -| BI_Disj_R1 Δ ϕ ψ : - (Δ ⊢ᴮ ϕ) → - Δ ⊢ᴮ DISJ ϕ ψ -| BI_Disj_R2 Δ ϕ ψ : - (Δ ⊢ᴮ ψ) → - Δ ⊢ᴮ DISJ ϕ ψ -| BI_Disj_L Π ϕ ψ χ : - (fill Π (frml ϕ) ⊢ᴮ χ) → - (fill Π (frml ψ) ⊢ᴮ χ) → - fill Π (frml (DISJ ϕ ψ)) ⊢ᴮ χ -| BI_Impl_R Δ ϕ ψ : - (Δ ;, frml ϕ ⊢ᴮ ψ) → - Δ ⊢ᴮ IMPL ϕ ψ -| BI_Impl_L C Δ ϕ ψ χ : - (Δ ⊢ᴮ ϕ) → - (fill C (frml ψ) ⊢ᴮ χ) → - fill C (Δ ;, frml (IMPL ϕ ψ)) ⊢ᴮ χ -where "Δ ⊢ᴮ ϕ" := (proves Δ%B ϕ%B). - -(** ** Alternative representation of decomposition of bunches *) -(** We have an inductive type that characterizes when a bunch can be - decomposed into a context and a sub-bunch. This essentially gives an - us an inductive reasoning principle for equations [fill Π Δ = Δ']. *) -Inductive bunch_decomp : - bunch → bunch_ctx → bunch → Prop := -| decomp_id Δ : bunch_decomp Δ [] Δ -| decomp_comma_1 Δ1 Δ2 Π Δ : - bunch_decomp Δ1 Π Δ → - bunch_decomp (Δ1,,Δ2)%B (Π ++ [CtxCommaL Δ2]) Δ -| decomp_comma_2 Δ1 Δ2 Π Δ : - bunch_decomp Δ2 Π Δ → - bunch_decomp (Δ1,,Δ2)%B (Π ++ [CtxCommaR Δ1]) Δ -| decomp_semic_1 Δ1 Δ2 Π Δ : - bunch_decomp Δ1 Π Δ → - bunch_decomp (Δ1;,Δ2)%B (Π ++ [CtxSemicL Δ2]) Δ -| decomp_semic_2 Δ1 Δ2 Π Δ : - bunch_decomp Δ2 Π Δ → - bunch_decomp (Δ1;,Δ2)%B (Π ++ [CtxSemicR Δ1]) Δ. - -(** Auxiliary functions: map for bunch_ctx *) -Definition bunch_ctx_item_map (f : formula → formula) (F : bunch_ctx_item) := - match F with - | CtxCommaL Δ => CtxCommaL (f <·> Δ) - | CtxCommaR Δ => CtxCommaR (f <·> Δ) - | CtxSemicL Δ => CtxSemicL (f <·> Δ) - | CtxSemicR Δ => CtxSemicR (f <·> Δ) - end. - -Definition bunch_ctx_map (f : formula → formula) (Π : bunch_ctx) := map (bunch_ctx_item_map f) Π. - -(** * Properties *) - -Lemma fill_app (Π Π' : bunch_ctx) (Δ : bunch) : - fill (Π ++ Π') Δ = fill Π' (fill Π Δ). -Proof. by rewrite /fill foldl_app. Qed. - -(** Registering the right typeclasses for rewriting purposes. *) - -Global Instance equivalence_bunch_equiv : Equivalence ((≡@{bunch})). -Proof. - repeat split. - - intro x. econstructor. - - intros x y Hxy. by econstructor. - - intros x y z Hxy Hyz. by econstructor. -Qed. - -Global Instance comma_comm : Comm (≡) comma. -Proof. intros X Y. apply BE_comma_comm. Qed. -Global Instance semic_comm : Comm (≡) semic. -Proof. intros X Y. apply BE_semic_comm. Qed. -Global Instance comma_assoc : Assoc (≡) comma. -Proof. intros X Y Z. apply BE_comma_assoc. Qed. -Global Instance semic_assoc : Assoc (≡) semic. -Proof. intros X Y Z. apply BE_semic_assoc. Qed. -Global Instance comma_left_id : LeftId (≡) empty comma. -Proof. intros X. by econstructor. Qed. -Global Instance comma_right_id : RightId (≡) empty comma. -Proof. intros X. rewrite comm. by econstructor. Qed. -Global Instance semic_left_id : LeftId (≡) top semic. -Proof. intros X. by econstructor. Qed. -Global Instance semic_right_id : RightId (≡) top semic. -Proof. intros X. rewrite comm. by econstructor. Qed. - -Global Instance fill_proper C : Proper ((≡) ==> (≡)) (fill C). -Proof. intros X Y. apply BE_cong. Qed. - -Global Instance comma_proper : Proper ((≡) ==> (≡) ==> (≡)) comma. -Proof. - intros Δ1 Δ2 H Δ1' Δ2' H'. - change ((fill [CtxCommaL Δ1'] Δ1) ≡ (fill [CtxCommaL Δ2'] Δ2)). - etrans. - { eapply BE_cong; eauto. } - simpl. - change ((fill [CtxCommaR Δ2] Δ1') ≡ (fill [CtxCommaR Δ2] Δ2')). - eapply BE_cong; eauto. -Qed. - -Global Instance semic_proper : Proper ((≡) ==> (≡) ==> (≡)) semic. -Proof. - intros Δ1 Δ2 H Δ1' Δ2' H'. - change ((fill [CtxSemicL Δ1'] Δ1) ≡ (fill [CtxSemicL Δ2'] Δ2)). - etrans. - { eapply BE_cong; eauto. } - simpl. - change ((fill [CtxSemicR Δ2] Δ1') ≡ (fill [CtxSemicR Δ2] Δ2')). - eapply BE_cong; eauto. -Qed. -Global Instance proves_proper : Proper ((≡) ==> (=) ==> (≡)) proves. -Proof. - intros D1 D2 HD ϕ ? <-. - split; intros H. - - eapply BI_Equiv; eauto. - - eapply BI_Equiv; [ symmetry | ]; eauto. -Qed. - -(** [bunch_decomp Δ' Π Δ] completely characterizes [fill Π Δ = Δ'] *) -Lemma bunch_decomp_correct Δ Π Δ' : - bunch_decomp Δ Π Δ' → Δ = fill Π Δ'. -Proof. induction 1; rewrite ?fill_app /= //; try by f_equiv. Qed. - -Lemma bunch_decomp_complete' Π Δ' : - bunch_decomp (fill Π Δ') Π Δ'. -Proof. - revert Δ'. remember (reverse Π) as Πr. - revert Π HeqΠr. - induction Πr as [|HΠ Πr]=>Π HeqΠr. - { assert (Π = []) as ->. - { by eapply (inj reverse). } - simpl. intros. econstructor. } - intros Δ'. - assert (Π = reverse Πr ++ [HΠ]) as ->. - { by rewrite -reverse_cons HeqΠr reverse_involutive. } - rewrite fill_app /=. - revert Δ'. - induction HΠ=>Δ' /=; econstructor; eapply IHΠr; by rewrite reverse_involutive. -Qed. - -Lemma bunch_decomp_complete Δ Π Δ' : - (fill Π Δ' = Δ) → - bunch_decomp Δ Π Δ'. -Proof. intros <-. apply bunch_decomp_complete'. Qed. - -Lemma fill_is_frml Π Δ ϕ : - fill Π Δ = frml ϕ → - Π = [] ∧ Δ = frml ϕ. -Proof. - revert Δ. induction Π as [| F C IH]=>Δ; first by eauto. - destruct F ; simpl ; intros H1 ; - destruct (IH _ H1) as [HC HΔ] ; by simplify_eq/=. -Qed. - -Lemma bunch_decomp_app C C0 Δ Δ0 : - bunch_decomp Δ C0 Δ0 → - bunch_decomp (fill C Δ) (C0 ++ C) Δ0. -Proof. - revert Δ Δ0 C0. - induction C as [|F C]=>Δ Δ0 C0. - { simpl. by rewrite app_nil_r. } - intros HD. - replace (C0 ++ F :: C) with ((C0 ++ [F]) ++ C); last first. - { by rewrite -assoc. } - apply IHC. destruct F; simpl; by econstructor. -Qed. - -Lemma bunch_decomp_ctx C C' Δ ϕ : - bunch_decomp (fill C Δ) C' (frml ϕ) → - ((∃ C0, bunch_decomp Δ C0 (frml ϕ) ∧ C' = C0 ++ C) ∨ - (∃ (C0 C1 : bunch → bunch_ctx), - (∀ Δ Δ', fill (C0 Δ) Δ' = fill (C1 Δ') Δ) ∧ - (∀ Δ', fill (C1 Δ') Δ = fill C' Δ') ∧ - (∀ A, bunch_decomp (fill C A) (C0 A) (frml ϕ)))). -Proof. - revert Δ C'. - induction C as [|F C]=>Δ C'; simpl. - { remember (frml ϕ) as Γ1. intros Hdec. - left. eexists. rewrite right_id. split; done. } - simpl. intros Hdec. - destruct (IHC _ _ Hdec) as [IH|IH]. - - destruct IH as [C0 [HC0 HC]]. - destruct F; simpl in *. - + inversion HC0; simplify_eq/=. - * left. eexists; split; eauto. - rewrite -assoc //. - * right. - exists (λ A, (Π ++ [CtxCommaR A]) ++ C). - exists (λ A, ([CtxCommaL (fill Π A)] ++ C)). - repeat split. - { intros A B. by rewrite /= -!assoc /= !fill_app. } - { intros A. by rewrite /= -!assoc /= !fill_app. } - { intros A. apply bunch_decomp_app. by econstructor. } - + inversion HC0; simplify_eq/=. - * right. - exists (λ A, (Π ++ [CtxCommaL A]) ++ C). - exists (λ A, ([CtxCommaR (fill Π A)] ++ C)). - repeat split. - { intros A B. by rewrite /= -!assoc /= !fill_app. } - { intros A. by rewrite /= -!assoc /= !fill_app. } - { intros A. apply bunch_decomp_app. by econstructor. } - * left. eexists; split; eauto. - rewrite -assoc //. - + inversion HC0; simplify_eq/=. - * left. eexists; split; eauto. - rewrite -assoc //. - * right. - exists (λ A, (Π ++ [CtxSemicR A]) ++ C). - exists (λ A, ([CtxSemicL (fill Π A)] ++ C)). - repeat split. - { intros A B. by rewrite /= -!assoc /= !fill_app. } - { intros A. by rewrite /= -!assoc /= !fill_app. } - { intros A. apply bunch_decomp_app. by econstructor. } - + inversion HC0; simplify_eq/=. - * right. - exists (λ A, (Π ++ [CtxSemicL A]) ++ C). - exists (λ A, ([CtxSemicR (fill Π A)] ++ C)). - repeat split. - { intros A B. by rewrite /= -!assoc /= !fill_app. } - { intros A. by rewrite /= -!assoc /= !fill_app. } - { intros A. apply bunch_decomp_app. by econstructor. } - * left. eexists; split; eauto. - rewrite -assoc //. - - right. - destruct IH as (C0 & C1 & HC0 & HC1 & HC). - exists (λ A, C0 (fill_item F A)), (λ A, F::C1 A). repeat split. - { intros A B. simpl. rewrite -HC0 //. } - { intros B. rewrite -HC1 //. } - intros A. apply HC. -Qed. - -Lemma bunch_map_fill f Π Δ : - f <·> (fill Π Δ) = fill (bunch_ctx_map f Π) (f <·> Δ). -Proof. - revert Δ. induction Π as [|F Π IH] =>Δ/=//. - rewrite IH. f_equiv. by destruct F; simpl. -Qed. - -Global Instance bunch_map_proper f : Proper ((≡) ==> (≡)) (bunch_map f). -Proof. - intros Δ1 Δ2 HD. induction HD; simpl; eauto. - - etrans; eauto. - - rewrite !bunch_map_fill. by f_equiv. - - by rewrite left_id. - - by rewrite comm. - - by rewrite assoc. - - by rewrite left_id. - - by rewrite comm. - - by rewrite assoc. -Qed. - -Lemma bunch_decomp_box Δ Π ϕ : - bunch_decomp (BOX <·> Δ) Π (frml (BOX ϕ)) → - ∃ Π', Π = bunch_ctx_map BOX Π' ∧ bunch_decomp Δ Π' (frml ϕ). -Proof. - revert Π. induction Δ=>/= Π H1; try by inversion H1. - - inversion H1. simplify_eq/=. exists []. split; eauto. - econstructor. - - inversion H1 as [|ff |P1 |P1 P2 |aa]; simplify_eq/=. - + destruct (IHΔ1 _ H) as (Π'1 & -> & Hdec). - exists (Π'1 ++ [CtxCommaL Δ2]). - rewrite /bunch_ctx_map map_app /=. split; auto. - by econstructor. - + destruct (IHΔ2 _ H) as (Π'1 & -> & Hdec). - exists (Π'1 ++ [CtxCommaR Δ1]). - rewrite /bunch_ctx_map map_app /=. split; auto. - by econstructor. - - inversion H1 as [|ff |P1 |P1 P2 |aa]; simplify_eq/=. - + destruct (IHΔ1 _ H) as (Π'1 & -> & Hdec). - exists (Π'1 ++ [CtxSemicL Δ2]). - rewrite /bunch_ctx_map map_app /=. split; auto. - by econstructor. - + destruct (IHΔ2 _ H) as (Π'1 & -> & Hdec). - exists (Π'1 ++ [CtxSemicR Δ1]). - rewrite /bunch_ctx_map map_app /=. split; auto. - by econstructor. -Qed. - -(** Some convenient derived rules *) -Lemma BI_Boxes_L Π Δ ϕ : - (fill Π Δ ⊢ᴮ ϕ) → - (fill Π (BOX <·> Δ) ⊢ᴮ ϕ). -Proof. - revert Π. induction Δ=> Π IH /=; eauto. - - by apply BI_Box_L. - - apply (IHΔ1 ((CtxCommaL (bunch_map BOX Δ2))::Π)). simpl. - apply (IHΔ2 ((CtxCommaR Δ1)::Π)). done. - - apply (IHΔ1 ((CtxSemicL (bunch_map BOX Δ2))::Π)). simpl. - apply (IHΔ2 ((CtxSemicR Δ1)::Π)). done. -Qed. - -Lemma BI_Collapse_L Π Δ ϕ : - (fill Π Δ ⊢ᴮ ϕ) → - (fill Π (frml (collapse Δ)) ⊢ᴮ ϕ). -Proof. - revert Π. induction Δ=> Π IH /=; try by econstructor; eauto. - - apply BI_Sep_L. - apply (IHΔ1 ((CtxCommaL (frml (collapse Δ2)))::Π)). simpl. - apply (IHΔ2 ((CtxCommaR Δ1)::Π)). done. - - apply BI_Conj_L. - apply (IHΔ1 ((CtxSemicL (frml (collapse Δ2)))::Π)). simpl. - apply (IHΔ2 ((CtxSemicR Δ1)::Π)). done. -Qed. diff --git a/theories/syntax.v b/theories/syntax.v deleted file mode 100644 index a5573c9..0000000 --- a/theories/syntax.v +++ /dev/null @@ -1,153 +0,0 @@ -(* Formulas, bunches *) -From Coq Require Import ssreflect. -From stdpp Require Import prelude gmap fin_sets. -From bunched.algebra Require Import bi. - -Declare Scope bunch_scope. -Delimit Scope bunch_scope with B. - -(** * Generic syntax for bunches *) -Inductive sep := Comma | SemiC. - -Inductive bunch {formula : Type} : Type := -| frml (ϕ : formula) -| bnul (s : sep) -| bbin (s : sep) (Δ Γ : bunch) -. - -(* Definition semic {frml} (Δ Γ : @bunch frml) := bbin SemiC Δ Γ. *) -(* Definition comma {frml} (Δ Γ : @bunch frml) := bbin Comma Δ Γ. *) -(* Definition top {frml} : @bunch frml := bnul SemiC. *) -(* Definition empty {frml} : @bunch frml := bnul Comma. *) - -Notation "∅ₐ" := (bnul SemiC) : bunch_scope. -Notation "∅ₘ" := (bnul Comma) : bunch_scope. -Notation "Δ ';,' Γ" := (bbin SemiC Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. -Notation "Δ ',,' Γ" := (bbin Comma Δ%B Γ%B) (at level 80, right associativity) : bunch_scope. - -(** ** Bunched contexts with a hole *) -Inductive bunch_ctx_item {frml : Type} : Type := -| CtxL (s : sep) (Δ2 : @bunch frml) -| CtxR (s : sep) (Δ1 : @bunch frml) -. - -Definition CtxCommaL {frml} (Δ2 : bunch) : @bunch_ctx_item frml - := CtxL Comma Δ2. -Definition CtxSemicL {frml} (Δ2 : bunch) : @bunch_ctx_item frml - := CtxL SemiC Δ2. -Definition CtxCommaR {frml} (Δ1 : bunch) : @bunch_ctx_item frml - := CtxR Comma Δ1. -Definition CtxSemicR {frml} (Δ1 : bunch) : @bunch_ctx_item frml - := CtxR SemiC Δ1. - -Definition bunch_ctx {frml} := list (@bunch_ctx_item frml). - -Definition fill_item {frml} (F : @bunch_ctx_item frml) (Δ : bunch) : bunch := - match F with - | CtxL s Δ2 => bbin s Δ Δ2 - | CtxR s Δ1 => bbin s Δ1 Δ - end. - -Definition fill {frml} (Π : @bunch_ctx frml) (Δ : bunch) : bunch := - foldl (flip fill_item) Δ Π. - - -(** ** Bunch equivalence *) -(** Equivalence on bunches is defined to be the least congruence - that satisfies the monoidal laws for (empty and comma) and (top - and semicolon). *) -Inductive bunch_equiv {frml} : @bunch frml → @bunch frml → Prop := -| BE_refl Δ : Δ =? Δ -| BE_sym Δ1 Δ2 : Δ1 =? Δ2 → Δ2 =? Δ1 -| BE_trans Δ1 Δ2 Δ3 : Δ1 =? Δ2 → Δ2 =? Δ3 → Δ1 =? Δ3 -| BE_cong C Δ1 Δ2 : Δ1 =? Δ2 → fill C Δ1 =? fill C Δ2 -| BE_unit_l s Δ : bbin s (bnul s) Δ =? Δ -| BE_comm s Δ1 Δ2 : bbin s Δ1 Δ2 =? bbin s Δ2 Δ1 -| BE_assoc s Δ1 Δ2 Δ3 : bbin s Δ1 (bbin s Δ2 Δ3) =? bbin s (bbin s Δ1 Δ2) Δ3 -where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B). - -(** Register [bunch_equiv] as [(≡)] *) -#[export] Instance equiv_bunch_equiv frml : Equiv (@bunch frml) := bunch_equiv. - -(** * Properties *) - -#[export] Instance equivalence_bunch_equiv frml : Equivalence ((≡@{@bunch frml})). -Proof. - repeat split. - - intro x. econstructor. - - intros x y Hxy. by econstructor. - - intros x y z Hxy Hyz. by econstructor. -Qed. - -#[export] Instance bbin_comm frml s : Comm (≡@{@bunch frml}) (bbin s). -Proof. intros X Y. apply BE_comm. Qed. -#[export] Instance bbin_assoc frml s : Assoc (≡@{@bunch frml}) (bbin s). -Proof. intros X Y Z. apply BE_assoc. Qed. -#[export] Instance bbin_leftid frml s : LeftId (≡@{@bunch frml}) (bnul s) (bbin s). -Proof. intros X. apply BE_unit_l. Qed. -#[export] Instance bbin_rightid frml s : RightId (≡@{@bunch frml}) (bnul s) (bbin s). -Proof. intros X. rewrite comm. apply BE_unit_l. Qed. - -#[export] Instance fill_proper frml Π : Proper ((≡) ==> (≡@{@bunch frml})) (fill Π). -Proof. intros X Y. apply BE_cong. Qed. - -#[export] Instance bbin_proper frml s : Proper ((≡) ==> (≡) ==> (≡@{@bunch frml})) (bbin s). -Proof. - intros Δ1 Δ2 H Δ1' Δ2' H'. - change ((fill [CtxL s Δ1'] Δ1) ≡ (fill [CtxL s Δ2'] Δ2)). - etrans. - { eapply BE_cong; eauto. } - simpl. - change ((fill [CtxR s Δ2] Δ1') ≡ (fill [CtxR s Δ2] Δ2')). - eapply BE_cong; eauto. -Qed. - -Lemma fill_app {frml} (Π Π' : @bunch_ctx frml) (Δ : bunch) : - fill (Π ++ Π') Δ = fill Π' (fill Π Δ). -Proof. by rewrite /fill foldl_app. Qed. - - -(** * Formulas *) -Definition atom := nat. - -Inductive formula : Type := -| TOP -| EMP -| BOT -| ATOM (A : atom) -| CONJ (ϕ ψ : formula) -| DISJ (ϕ ψ : formula) -| SEP (ϕ ψ : formula) -| IMPL (ϕ ψ : formula) -| WAND (ϕ ψ : formula) -. - -(** "Collapse" internalizes the bunch as a formula. *) -Fixpoint collapse (Δ : @bunch formula) : formula := - match Δ with - | frml ϕ => ϕ - | ∅ₐ => TOP - | ∅ₘ => EMP - | Δ ,, Δ' => SEP (collapse Δ) (collapse Δ') - | Δ ;, Δ' => CONJ (collapse Δ) (collapse Δ') - end%B. - -Inductive collapse_gr : @bunch formula → formula → Prop := -| collapse_frml ϕ : collapse_gr (frml ϕ) ϕ -| collapse_top : collapse_gr ∅ₐ%B TOP -| collapse_emp : collapse_gr ∅ₘ%B EMP -| collapse_sep Δ1 Δ2 ϕ1 ϕ2 : - collapse_gr Δ1 ϕ1 → - collapse_gr Δ2 ϕ2 → - collapse_gr (Δ1 ,, Δ2)%B (SEP ϕ1 ϕ2) -| collapse_conj Δ1 Δ2 ϕ1 ϕ2 : - collapse_gr Δ1 ϕ1 → - collapse_gr Δ2 ϕ2 → - collapse_gr (Δ1 ;, Δ2)%B (CONJ ϕ1 ϕ2) -. - -Lemma collapse_gr_sound Δ : collapse_gr Δ (collapse Δ). -Proof. induction Δ; simpl; try destruct s; try by econstructor. Qed. - -Lemma collapse_gr_complete Δ ϕ : collapse_gr Δ ϕ → collapse Δ = ϕ. -Proof. induction 1; simpl; subst; eauto. Qed. diff --git a/theories/terms.v b/theories/terms.v index 10559ac..24e97e4 100644 --- a/theories/terms.v +++ b/theories/terms.v @@ -1,7 +1,7 @@ (* Bunched terms *) From Coq Require Import ssreflect. From bunched.algebra Require Import bi. -From bunched Require Import syntax interp prelude.sets. +From bunched Require Import bunches prelude.sets. From stdpp Require Import prelude base gmap functions. (** * Bunched terms *) @@ -195,10 +195,10 @@ Qed. ⟦ T(Δs) ⟧ = ⟦ T ⟧ (⟦ Δs ⟧) >> *) -Lemma bterm_ctx_alg_act {PROP : bi} `{!EqDecision V,!Countable V} - (T : bterm V) (Δs : V → bunch) (s : atom → PROP) : - bunch_interp s (bterm_ctx_act T Δs) = - bterm_alg_act T (bunch_interp s ∘ Δs). +Lemma bterm_ctx_alg_act {PROP : bi} {formula} `{!EqDecision V,!Countable V} + (T : bterm V) (Δs : V → bunch) (i : formula → PROP) : + bunch_interp i (bterm_ctx_act T Δs) = + bterm_alg_act T (bunch_interp i ∘ Δs). Proof. induction T; simpl. - reflexivity.