alternative version of rules_valid

co-dan · Jul 17, 2023 · 14103e9 · 14103e9
1 parent fec6390
commit 14103e9
Show file tree

Hide file tree

Showing 6 changed files with 56 additions and 24 deletions.
diff --git a/theories/algebra/from_closure.v b/theories/algebra/from_closure.v
@@ -507,6 +507,16 @@ Section FromClosure.
     apply bi.wand_intro_l. apply cl_unit.
   Qed.
 
+  Lemma C_elemof_pure (P : Prop) Δ : P → Δ ∈ (C_pure P).
+  Proof.
+    intros HP.
+    cut (True ⊢@{PM} CPred (C_pure P))%I.
+    - intros inc. specialize (inc Δ).
+      apply inc. done.
+    - trans (cl True)%I.
+      { apply (cl_unit _). }
+      apply cl_mono. intros ? ?. done.
+  Qed.
 
 End FromClosure.
 

diff --git a/theories/analytic_completion.v b/theories/analytic_completion.v
@@ -270,12 +270,13 @@ Proof.
   intros H1 Xs.
   rewrite - linearize_bterm_act_ren.
   rewrite H1. apply bi.exist_elim=>Ti.
-  destruct Ti as [Ti HTi]. simpl.
+  apply bi.pure_elim_l. intros HTi.
   apply elem_of_list_join in HTi.
   destruct HTi as [L [HTi HL]].
   apply elem_of_list_fmap_2 in HL.
   destruct HL as [Tz [-> HTz]].
-  apply (bi.exist_intro' _ _  (Tz ↾ HTz)).
+  apply (bi.exist_intro' _ _  Tz).
+  rewrite bi.pure_True // left_id.
   simpl in *. apply elem_of_elements in HTi.
   eapply transformed_premise_act_ren in HTi.
   by rewrite HTi.
@@ -290,7 +291,7 @@ Proof.
   intros H1 Xs.
   rewrite linearize_bterm_act.
   rewrite H1. apply bi.exist_elim=>Ti.
-  destruct Ti as [Ti HTi]. simpl.
+  apply bi.pure_elim_l. intros HTi.
   rewrite bterm_alg_act_disj_ren_inverse_transform.
   apply bi.exist_elim=>Tk. apply bi.pure_elim_l=>Htk.
   assert (Tk ∈ mjoin (fmap (elements ∘ transform_premise s) Ts)) as Tk'.
@@ -299,5 +300,6 @@ Proof.
     - by apply elem_of_elements.
     - rewrite list_fmap_compose.
       by do 2 apply elem_of_list_fmap_1. }
-  apply (bi.exist_intro' _ _  (Tk ↾ Tk')); done.
+  apply (bi.exist_intro' _ _  Tk).
+  rewrite bi.pure_True// left_id//.
 Qed.
diff --git a/theories/bunches.v b/theories/bunches.v
@@ -169,7 +169,7 @@ Section interp.
     | bbin sp Δ Δ' => sep_interp sp (bunch_interp Δ) (bunch_interp Δ')
     end%B%I.
 
-    Definition bunch_ctx_item_interp (F : bunch_ctx_item) : PROP → PROP :=
+  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
@@ -259,8 +259,32 @@ Section interp.
     destruct F as [[|] ? | [|] ?]; simpl; f_equiv; eauto.
   Qed.
 
+  Lemma bunch_ctx_item_interp_pure F P Q :
+    bunch_ctx_item_interp F (⌜P⌝ ∧ Q) ⊢ ⌜P⌝ ∧ bunch_ctx_item_interp F Q.
+  Proof.
+    destruct F as [[|] ? | [|] ?]; simpl.
+    - rewrite bi.sep_and_r. f_equiv.
+      apply bi.pure_sep_l.
+    - by rewrite assoc.
+    - rewrite bi.sep_and_l. f_equiv.
+      rewrite comm.
+      apply bi.pure_sep_l.
+    - rewrite assoc. rewrite (comm _ _ ⌜P⌝%I).
+      by rewrite assoc.
+  Qed.
+
+  Lemma bunch_ctx_interp_pure Π P Q :
+    bunch_ctx_interp Π (⌜P⌝ ∧ Q) ⊢ ⌜P⌝ ∧ bunch_ctx_interp Π Q.
+  Proof.
+    revert Q. induction Π as [|F Π]=>Q; first by simpl; auto.
+    rewrite !bunch_ctx_interp_cons.
+    rewrite bunch_ctx_item_interp_pure.
+    apply IHΠ.
+  Qed.
+
 End interp.
 
 Arguments sep_interp {_} _ _ _.
 Arguments bunch_interp {_ _} _ _.
+Arguments bunch_ctx_interp {_ _} _ _ _.
 
diff --git a/theories/cutelim.v b/theories/cutelim.v
@@ -466,9 +466,10 @@ Proof.
 Qed.
 
 (** All the simple structural rules are valid in [C] *)
-Lemma C_extensions (Ts : list (bterm nat)) (T : bterm nat) :
-    (Ts, T) ∈ M.rules → rule_valid C_alg Ts T.
+Lemma C_extensions s :
+    s ∈ M.rules → rule_valid s C_alg.
 Proof.
+  destruct s as [Ts T].
   intros Hs. unfold rule_valid.
   intros Xs.
   trans (bterm_alg_act (PROP:=C_alg) T
@@ -484,9 +485,11 @@ Proof.
   destruct H1 as (Δs & HΔs & H1).
   rewrite H1. eapply (BI_Simple_Ext []); eauto.
   intros Ti HTi. simpl. apply (Hϕ _).
-  exists (Ti ↾ HTi). simpl. eapply bterm_C_refl.
-  intros i. specialize (HΔs i). revert HΔs.
-  simpl. generalize (Xs i)=>X. apply X.
+  exists Ti. split.
+  - by apply C_elemof_pure.
+  - eapply bterm_C_refl.
+    intros i. specialize (HΔs i). revert HΔs.
+    simpl. generalize (Xs i)=>X. apply X.
 Qed.
 
 (** * Cut admissibility *)

diff --git a/theories/seqcalc.v b/theories/seqcalc.v
@@ -159,16 +159,10 @@ Proof.
 Qed.
 
 (** * Interpretation *)
-(** Associated with the set of rules:
-     when is the set of rules is valid in an algebra? *)
-Definition rule_valid (PROP : bi) (Ts : list bterm) (T : bterm) :=
-  ∀ (Xs : nat → PROP),
-    bterm_alg_act T Xs ⊢
-       ∃ Ti' : {Ti : bterm | Ti ∈ Ts }, bterm_alg_act (proj1_sig Ti') Xs.
 
 (** Sequent calculus is sound w.r.t. the BI algebras. *)
 Theorem seq_interp_sound {PROP : bi} (s : atom → PROP) Δ ϕ :
-  (∀ Ts T, (Ts, T) ∈ rules → rule_valid PROP Ts T) →
+  (∀ s, s ∈ rules → rule_valid s PROP) →
   (Δ ⊢ᴮ ϕ) →
   seq_interp s Δ ϕ.
 Proof.
@@ -180,16 +174,17 @@ Proof.
       by rewrite bi.and_elim_l.
   - apply bunch_interp_fill_mono; simpl.
     apply bi.and_intro; eauto.
-  - assert (rule_valid PROP Ts T) as HH.
+  - assert (rule_valid (Ts,T) PROP) as HH.
     { eapply Hrules; auto. }
     specialize (HH (bunch_interp (formula_interp s) ∘ Δs)).
     rewrite bunch_ctx_interp_decomp.
     rewrite bterm_ctx_alg_act.
     rewrite HH.
     rewrite bunch_ctx_interp_exist.
-    apply bi.exist_elim=>Ti'.
-    destruct Ti' as [Ti HTi].
+    apply bi.exist_elim=>Ti.
     rewrite -bterm_ctx_alg_act.
+    rewrite bunch_ctx_interp_pure.
+    apply bi.pure_elim_l. intros HTi.
     rewrite -bunch_ctx_interp_decomp.
     by apply H1.
   - by rewrite IHproves1 IHproves2.
@@ -207,7 +202,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 (formula_interp s) Π (∃ (x : bool), if x then bunch_interp (formula_interp s) (frml ϕ) else bunch_interp (formula_interp s) (frml ψ))).
+    trans (bunch_ctx_interp (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/terms.v b/theories/terms.v
@@ -125,9 +125,7 @@ Definition structural_rule := (list (bterm nat) * bterm nat)%type.
 Definition is_analytical (s : structural_rule) := linear_bterm (snd s).
 Definition rule_valid (s : structural_rule) (PROP : bi) : Prop :=
   ∀ (Xs : nat → PROP),
-    bterm_alg_act (snd s) Xs ⊢
-       ∃ Ti' : {Ti : bterm nat | Ti ∈ fst s }, bterm_alg_act (proj1_sig Ti') Xs.
-
+    bterm_alg_act (snd s) Xs ⊢ ∃ Ti, ⌜Ti ∈ fst s⌝ ∧ bterm_alg_act Ti Xs.
 
 (** * Properties *)