fix bunch_decomp_box

co-dan · Jul 24, 2023 · 3fa1cb2 · 3fa1cb2
1 parent 2c435dd
commit 3fa1cb2
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 9 deletions.
diff --git a/theories/s4/seqcalc.v b/theories/s4/seqcalc.v
@@ -103,20 +103,22 @@ Qed.
 
 Lemma bunch_decomp_box Δ Π ϕ :
   bunch_decomp (BOX <$> Δ) Π (frml (BOX ϕ)) →
-  ∃ Π', Π = bunch_ctx_map BOX Π' ∧ bunch_decomp Δ Π' (frml ϕ).
+  ∃ Π', (∀ Γ, fill Π (BOX <$> Γ) =  BOX <$> fill Π' Γ) ∧ 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).
+    + destruct (IHΔ1 _ H1') as (Π'1 & HΠ'1 & Hdec).
       exists (Π'1 ++ [CtxL s Δ2]).
-      rewrite /bunch_ctx_map map_app /=. split; auto.
-        by econstructor.
-    + destruct (IHΔ2 _ H1') as (Π'1 & -> & Hdec).
+      split; last by econstructor.
+      intros Γ. rewrite !fill_app /=.
+      rewrite HΠ'1 //.
+    + destruct (IHΔ2 _ H1') as (Π'1 & HΠ'1 & Hdec).
       exists (Π'1 ++ [CtxR s Δ1]).
-      rewrite /bunch_ctx_map map_app /=. split; auto.
-        by econstructor.
+      split; last by econstructor.
+      intros Γ. rewrite !fill_app /=.
+      rewrite HΠ'1 //.
 Qed.
 
 (** Some convenient derived rules *)

diff --git a/theories/s4/seqcalc_height.v b/theories/s4/seqcalc_height.v
@@ -538,9 +538,9 @@ Section SeqcalcHeight.
     - (* box R *)
       apply bunch_decomp_complete in Heq.
       apply bunch_decomp_box in Heq.
-      destruct Heq as (Π' & -> & ->%bunch_decomp_correct).
+      destruct Heq as (Π' & HΠ' & ->%bunch_decomp_correct).
       change (frml (BOX ϕ)) with (BOX <$> (frml ϕ)).
-      rewrite -(bunch_map_fill BOX). apply BI_Box_R.
+      rewrite HΠ'. apply BI_Box_R.
       rewrite bunch_map_fill /=. eapply IHproves; eauto.
       rewrite bunch_map_fill //.
     - (* emp R *)