Further cleanup

Author: co-dan

theories/bunch_decomp.v

@@ -50,13 +50,23 @@ Lemma bunch_decomp_complete Δ Π Δ' :
   bunch_decomp Δ Π Δ'.
 Proof. intros <-. apply bunch_decomp_complete'. Qed.
 
+Lemma bunch_decomp_iff Δ Π Δ' :
+  (fill Π Δ' = Δ) ↔ bunch_decomp Δ Π Δ'.
+Proof.
+  split.
+  - apply bunch_decomp_complete.
+  - by symmetry; apply bunch_decomp_correct.
+Qed.
+
+(** * Properties of bunched contexts *)
+(** We prove several useful properties using the inductive system defined above. *)
+
 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/=.
+  intros H%bunch_decomp_iff.
+  inversion H; eauto.
 Qed.
 
 Lemma bunch_decomp_app C C0 Δ Δ0 :
@@ -72,72 +82,70 @@ Proof.
   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 ϕ)))).
+Lemma bunch_decomp_ctx Π Π' Δ ϕ :
+  bunch_decomp (fill Π Δ) Π' (frml ϕ) →
+  ((∃ Π0, bunch_decomp Δ Π0 (frml ϕ) ∧ Π' = Π0 ++ Π) ∨
+   (∃ (Π0 Π1 : bunch → bunch_ctx),
+       (∀ Δ Δ', fill (Π0 Δ) Δ' = fill (Π1 Δ') Δ) ∧
+       (∀ Δ', fill (Π1 Δ') Δ = fill Π' Δ') ∧
+       (∀ A, bunch_decomp (fill Π A) (Π0 A) (frml ϕ)))).
 Proof.
-  revert Δ C'.
-  induction C as [|F C]=>Δ C'; simpl.
+  revert Δ Π'.
+  induction Π as [|F Π]=>Δ Π'; 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 (IHΠ _ _ Hdec) as [IH|IH].
+  - destruct IH as [Π0 [HΠ0 HΠ]].
     destruct F; simpl in *.
-    + inversion HC0; simplify_eq/=.
+    + inversion HΠ0; simplify_eq/=.
       * left. eexists; split; eauto.
         rewrite -assoc //.
       * right.
-        exists (λ A, (Π ++ [CtxCommaR A]) ++ C).
-        exists (λ A, ([CtxCommaL (fill Π A)] ++ C)).
+        exists (λ A, (Π1 ++ [CtxCommaR A]) ++ Π).
+        exists (λ A, ([CtxCommaL (fill Π1 A)] ++ Π)).
         repeat split.
-        { intros A B. by rewrite /= -!assoc /= !fill_app. }
-        { intros A. by rewrite /= -!assoc /= !fill_app. }
+        { 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/=.
+    + inversion HΠ0; simplify_eq/=.
       * right.
-        exists (λ A, (Π ++ [CtxCommaL A]) ++ C).
-        exists (λ A, ([CtxCommaR (fill Π A)] ++ C)).
+        exists (λ A, (Π1 ++ [CtxCommaL A]) ++ Π).
+        exists (λ A, ([CtxCommaR (fill Π1 A)] ++ Π)).
         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/=.
+    + inversion HΠ0; simplify_eq/=.
       * left. eexists; split; eauto.
         rewrite -assoc //.
       * right.
-        exists (λ A, (Π ++ [CtxSemicR A]) ++ C).
-        exists (λ A, ([CtxSemicL (fill Π A)] ++ C)).
+        exists (λ A, (Π1 ++ [CtxSemicR A]) ++ Π).
+        exists (λ A, ([CtxSemicL (fill Π1 A)] ++ Π)).
         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/=.
+    + inversion HΠ0; simplify_eq/=.
       * right.
-        exists (λ A, (Π ++ [CtxSemicL A]) ++ C).
-        exists (λ A, ([CtxSemicR (fill Π A)] ++ C)).
+        exists (λ A, (Π1 ++ [CtxSemicL A]) ++ Π).
+        exists (λ A, ([CtxSemicR (fill Π1 A)] ++ Π)).
         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.
+    destruct IH as (Π0 & Π1 & HΠ0 & HΠ1 & HΠ).
+    exists (λ A, Π0 (fill_item F A)), (λ A, F::Π1 A). repeat split.
+    { intros A B. simpl. rewrite -HΠ0 //. }
+    { intros B. rewrite -HΠ1 //. }
+    intros A. apply HΠ.
 Qed.
 
-
-(* facts about terms *)
 Lemma bterm_ctx_act_decomp `{!EqDecision V, !Countable V} (T : bterm V)
   (Δs : V → bunch) ϕ Π :
   linear_bterm T →

theories/cutelim.v

@@ -206,9 +206,7 @@ Proof.
     by apply (HXY _).
 Qed.
 
-Program Definition C_impl (X Y : C) := {| CPred := PB_impl' X Y |}.
-
-Lemma is_heyting_impl (X Y Z : C) :
+Lemma has_heyting_impl (X Y Z : C) :
   ((X : PB) ⊢@{PB_alg} (PB_impl' Y Z : PB)) ↔
       ((X : PB) ∧ (Y : PB) ⊢@{PB_alg} (Z : PB))%I.
 Proof.
@@ -223,6 +221,8 @@ Proof.
     eexists _,_. split; eauto.
 Qed.
 
+Program Definition C_impl (X Y : C) := {| CPred := PB_impl' X Y |}.
+
 Program Definition C_alg : bi :=
   C_alg bunch comma formula Fint C_impl _ _ _ .
 Next Obligation.
@@ -232,15 +232,15 @@ Next Obligation.
   - intros Δ. simpl. intros H1 Δ' HX'.
     apply HY. apply H1. apply HX. apply HX'.
 Qed.
-Next Obligation. apply is_heyting_impl. Qed.
+Next Obligation. apply has_heyting_impl. Qed.
 
 (** * Interpretation in [C] and Okada's lemma *)
 Definition C_atom (a : atom) := Fint' (ATOM a).
 
 Definition inner_interp : formula → C := @formula_interp C_alg C_atom.
 
 (** We verify the Okada's property *)
-Lemma okada (A : formula) :
+Lemma okada_property (A : formula) :
   (frml A ∈ inner_interp A)
    ∧ (inner_interp A ⊢@{C_alg} Fint' A).
 Proof.
@@ -454,6 +454,19 @@ Proof.
       by f_equiv.
 Qed.
 
+Lemma blinterm_C_desc' `{!EqDecision V, !Countable V}
+      (T : bterm V) (TL : linear_bterm T)
+      (Xs : V → C_alg) :
+  bterm_alg_act (PROP:=C_alg) T Xs ≡ C_blinterm_interp T Xs.
+Proof.
+  apply bi.equiv_entails. split.
+  - by apply blinterm_C_desc.
+  - apply cl_adj; first apply _.
+    intros Δ. simpl.
+    destruct 1 as [Δs [Hd ->]].
+    by apply bterm_C_refl.
+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.
@@ -493,11 +506,11 @@ Proof.
     (bunch_interp C_atom (fill Γ (frml ψ)) ⊢@{C_alg} formula_interp C_atom ϕ) in H2.
   cut (@seq_interp C_alg C_atom (fill Γ Δ) ϕ).
   { simpl. intros H3.
-    destruct (okada ϕ) as [Hϕ1 Hϕ2].
+    destruct (okada_property ϕ) as [Hϕ1 Hϕ2].
     apply (Hϕ2 _). unfold inner_interp.
     apply H3. apply (C_collapse_inv _ [] (fill Γ Δ)). simpl.
     apply (bunch_interp_collapse C_alg C_atom).
-    apply okada. }
+    apply okada_property. }
   simpl. rewrite -H2.
   apply bunch_interp_fill_mono, H1.
 Qed.

theories/cutelim_s4.v

@@ -2,7 +2,7 @@
 From Coq Require Import ssreflect.
 From stdpp Require Import prelude.
 From bunched.algebra Require Import bi.
-From bunched Require Import seqcalc_s4 seqcalc_height_s4 interp_s4.
+From bunched Require Import seqcalc_height_s4 seqcalc_s4 interp_s4.
 
 (** The first algebra that we consider is a purely "combinatorial" one:
     predicates [(bunch/≡) → Prop] *)
@@ -284,7 +284,7 @@ Module Cl.
   Proof.
     destruct X as [X Xcl]. simpl.
     intros HX. rewrite Xcl.
-    intros ϕ Hϕ. eapply (Inversion.Box_L []).
+    intros ϕ Hϕ. eapply (box_l_inv []).
     by apply Hϕ.
   Qed.
 
@@ -334,7 +334,7 @@ Module Cl.
   Proof.
     destruct X as [X Xcl]. simpl.
     rewrite !Xcl. intros HX ϕ Hϕ.
-    simpl in HX. apply Inversion.Collapse_L.
+    simpl in HX. apply collapse_l_inv.
     by apply HX.
   Qed.
 
@@ -416,8 +416,8 @@ Module Cl.
       destruct Y as [Y Yc]. simpl.
       rewrite Yc. intros ψ Hψ.
       specialize (H ((Δ' ↾ HX), (ψ ↾ Hψ))). simpl in *.
-      apply Inversion.Impl_R in H.
-      by apply (Inversion.Collapse_L [CtxSemicR Δ]).
+      apply impl_r_inv in H.
+      by apply (collapse_l_inv [CtxSemicR Δ]).
   Qed.
 
   Definition C_emp : C := cl' PB_emp.
@@ -447,8 +447,8 @@ Module Cl.
       destruct Y as [Y Yc]. simpl.
       rewrite Yc. intros ψ Hψ.
       specialize (H ((Δ' ↾ HX), (ψ ↾ Hψ))). simpl in *.
-      apply Inversion.Wand_R in H.
-      by apply (Inversion.Collapse_L [CtxCommaR Δ]).
+      apply wand_r_inv in H.
+      by apply (collapse_l_inv [CtxCommaR Δ]).
   Qed.
 
   Program Definition PB_box (X: PB) : PB :=
@@ -605,8 +605,8 @@ Module Cl.
     intros Δ.
     destruct 1 as (Δ' & HD & HX).
     simpl. intros D1 H1 f Hf. rewrite HD.
-    rewrite comm. apply (Inversion.Collapse_L [CtxSemicR D1]). simpl.
-    apply Inversion.Impl_R. apply H1.
+    rewrite comm. apply (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.
     apply (C_collapse (Fint' f) [CtxSemicR D2]). simpl.
@@ -721,15 +721,6 @@ Module Cl.
       + intros HX1 Δ2 HD2.
         apply HY, HX1.
         by apply HX.
-    (* - intros X1 X2 HX; try apply _. *)
-    (*   apply discrete_iff. *)
-    (*   { apply _. } *)
-    (*   intros Δ. apply cl_proper. *)
-    (*   apply (@bi.pure_proper PB_alg). split. *)
-    (*   { intros H1 Δ' H2. apply HX. *)
-    (*     apply H1, H2. } *)
-    (*   { intros H1 Δ' H2. apply HX. *)
-    (*     apply H1, H2. } *)
     - intros ψ X Hψ Δ. simpl.
       intros HX ϕ Hs. apply Hs.
       done.
@@ -783,7 +774,7 @@ Definition C_atom (a : atom) := Fint' (ATOM a).
 Definition inner_interp : formula → C
   := formula_interp C_alg C_box C_atom.
 
-Lemma pas_de_deux (A : formula) :
+Lemma okada_property (A : formula) :
   ((inner_interp A) (frml A)) ∧ (inner_interp A ⊢@{C_alg} Fint' A).
 Proof.
   induction A; simpl.
@@ -887,15 +878,15 @@ Proof.
   simpl in H1, H2.
   cut (seq_interp C_alg C_box C_atom (fill Γ Δ) ϕ).
   { simpl. intros H3.
-    destruct (pas_de_deux ϕ) as [Hϕ1 Hϕ2].
+    destruct (okada_property ϕ) as [Hϕ1 Hϕ2].
     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). }
-    apply pas_de_deux. }
+    apply okada_property. }
   simpl. rewrite -H2.
   apply bunch_interp_fill_mono, H1.
 Qed.
 
-Print Assumptions cut.
+(* Print Assumptions cut. *)
 (*  ==> Closed under the global context *)