Define bunched equivalence in two steps

co-dan · Jul 27, 2023 · 332c680 · 332c680
1 parent 276ae21
commit 332c680
Show file tree

Hide file tree

Showing 5 changed files with 189 additions and 553 deletions.
diff --git a/theories/bunch_decomp.v b/theories/bunch_decomp.v
@@ -162,3 +162,152 @@ Proof.
         rewrite fn_lookup_insert_ne//.
       * apply HH.
 Qed.
+
+Local Lemma bunch_equiv_fill_1 {formula} (Δ : @bunch formula) C ϕ :
+  fill C (frml ϕ) =? Δ →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  intros Heq.
+  remember (fill C (frml ϕ)) as Y.
+  revert C 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 ++ C). 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 rtsc_lr. }
+      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 (Π ++ [CtxR s Δ2]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+    * exists (Π ++ [CtxL s Δ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 (Π ++ [CtxL s Δ2;CtxL s Δ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 ++ [CtxR s Δ1;CtxL s Δ3])%B. split.
+         { rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+      ** exists (Π0 ++ [CtxR s (bbin s Δ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 {formula} (Δ : @bunch formula) C ϕ :
+  Δ =? fill C (frml ϕ) →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  intros Heq.
+  remember (fill C (frml ϕ)) as Y.
+  revert C 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 ++ C). 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 rtsc_lr. }
+      by rewrite HC2.
+  + exists (C' ++ [CtxR s (bnul s)]%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 (Π ++ [CtxR s Δ1]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+    * exists (Π ++ [CtxL s Δ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 ++ [CtxL s (bbin s Δ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 ++ [CtxL s Δ3;CtxR s Δ1])%B. split.
+         { simpl. rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+    * exists (Π ++ [CtxR s Δ2;CtxR s Δ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 {formula} Δ C (ϕ : formula) :
+  Δ ≡ (fill C (frml ϕ)) →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  revert Δ. eapply rtc_ind_l.
+  { exists C. 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.
diff --git a/theories/bunches.v b/theories/bunches.v
@@ -72,50 +72,49 @@ Definition bunch_ctx_map {A B} (f : A → B) (Π : @bunch_ctx A) := map (bunch_c
 (** 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
+Inductive bunch_equiv_step {frml} : @bunch frml → @bunch frml → Prop :=
 | 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).
+where "Δ =? Γ" := (bunch_equiv_step Δ%B Γ%B).
+
+Definition bunch_equiv {frml} := rtsc (@bunch_equiv_step frml).
 
 (** 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.
+Proof. apply _. Qed.
 
 #[export] Instance bbin_comm frml s : Comm (≡@{@bunch frml}) (bbin s).
-Proof. intros X Y. apply BE_comm. Qed.
+Proof. intros X Y. apply rtsc_rl. apply BE_comm. Qed.
 #[export] Instance bbin_assoc frml s : Assoc (≡@{@bunch frml}) (bbin s).
-Proof. intros X Y Z. apply BE_assoc. Qed.
+Proof. intros X Y Z. apply rtsc_lr. 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.
+Proof. intros X. apply rtsc_lr. 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.
+Proof. intros X. rewrite comm. apply rtsc_lr. apply BE_unit_l. Qed.
 
 #[export] Instance fill_proper frml Π : Proper ((≡) ==> (≡@{@bunch frml})) (fill Π).
-Proof. intros X Y. apply BE_cong. Qed.
+Proof.
+  intros X Y.
+  eapply rtc_congruence. clear X Y.
+  intros X Y. apply sc_congruence. clear X Y.
+  intros X Y ?. by econstructor.
+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. }
+  { eapply fill_proper; eauto. }
   simpl.
   change ((fill [CtxR s Δ2] Δ1') ≡ (fill [CtxR s Δ2] Δ2')).
-  eapply BE_cong; eauto.
+  eapply fill_proper; eauto.
 Qed.
 
 Lemma fill_app {frml} (Π Π' : @bunch_ctx frml) (Δ : bunch) :
@@ -129,16 +128,26 @@ Proof.
   rewrite IH. f_equiv. by destruct F; simpl.
 Qed.
 
-Global Instance bunch_map_proper {A B} (f : A → B) : Proper ((≡) ==> (≡@{bunch})) (fmap f).
+Lemma bunch_map_proper' {A B} (f : A → B) : Proper ((bunch_equiv_step) ==> (≡@{bunch})) (fmap f).
 Proof.
-  intros Δ1 Δ2 HD. induction HD; simpl; eauto.
-  - etrans; eauto.
-  - rewrite !bunch_map_fill. by f_equiv.
+  intros Δ1 Δ2 HD.
+  induction HD; simpl.
+  - rewrite !bunch_map_fill; by f_equiv.
   - by rewrite left_id.
   - by rewrite comm.
   - by rewrite assoc.
 Qed.
 
+#[global] Instance bunch_map_proper {A B} (f : A → B) : Proper ((≡) ==> (≡@{bunch})) (fmap f).
+Proof.
+  intros Δ1 Δ2 HD.
+  induction HD as [|Δ1 Δ2 Δ3 HD1 HD]; first done.
+  etrans; last by apply IHHD.
+  destruct HD1 as [HD1 | HD1].
+  - by apply bunch_map_proper'.
+  - symmetry. by apply bunch_map_proper'.
+Qed.
+
 Section interp.
   Variable (PROP : bi).
   Context {formula : Type}.
@@ -237,10 +246,9 @@ Section interp.
       apply (IHΠ (λ i, bunch_interp Δ1 ∧ P i)%I).
   Qed.
 
-  Global Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp.
+  Lemma bunch_interp_proper' : Proper ((bunch_equiv_step) ==> (≡)) 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.
@@ -251,6 +259,13 @@ Section interp.
     - simpl. destruct s; by rewrite assoc.
   Qed.
 
+  #[global] Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp.
+  Proof.
+    intros Δ1 Δ2. induction 1 as [|Δ1 Δ2 Δ3 HD1 HD]; first done.
+    etrans; last by eassumption.
+    destruct HD1; [| symmetry]; by apply bunch_interp_proper'.
+  Qed.
+
   Global Instance bunch_ctx_interp_mono Π : Proper ((⊢) ==> (⊢)) (bunch_ctx_interp Π).
   Proof.
     induction Π as [|F Π]=>P1 P2 HP; first by simpl; auto.

diff --git a/theories/s4/cutelim.v b/theories/s4/cutelim.v
@@ -310,7 +310,7 @@ Qed.
 Lemma box_true : True ⊢@{C_alg} C_box (True : C_alg).
 Proof.
   apply cl_adj. { apply _. } intros Δ _.
-  rewrite -(BE_unit_l _ Δ).
+  rewrite -(left_id ∅ₐ%B _ Δ).
   apply C_weaken. apply (cl_unit _ _ _).
   simpl. exists ∅ₐ%B. simpl. split; auto.
   apply (cl_unit _ _ _). done.