Maybe working version of mergableenv?

theories/examples/comparison/barrier.v

@@ -138,8 +138,7 @@ Section proof.
   Proof.
     iStepsS. iLöb as "IH".
     wp_lam. iStepsS; try iSmash.
-    - destruct (decide (z = x2)) as [-> | Hneq]; iSmash.
-    - iRevert "H4"; iSmash.
+    destruct (decide (z = x2)) as [-> | Hneq]; iSmash.
   Qed. 
   (* we need reverts in some places to detect extra inequalities: at some places we have 3 tickets and mergablepersist does not get all currently *)
 

theories/steps/introduce_hyp.v

@@ -42,29 +42,59 @@ End mergable.
 Section mergable_env. (* WIP *)
   Context {PROP : bi}.
 
-  Class MergableEnv (Δ : envs PROP) (P : PROP) (M : PROP) :=
-    mergable_env : (of_envs Δ) ∗ P ⊢ <pers> M.
+  Class MergableEnv (Δ : envs PROP) (P : PROP) (M : option PROP) :=
+    mergable_env : (of_envs Δ) ∗ P ⊢ <pers> default emp M.
 
   Instance mergable_env_base Δ P : 
-    MergableEnv Δ P True | 999.
+    MergableEnv Δ P None | 999.
   Proof. rewrite /MergableEnv; eauto. Qed.
 
-  Instance mergable_env_cons Δ P C mi p P2 P3 M PR :
+  Global Instance mergable_env_base2 C0 C1 P P0 mP0 P1 mP1 Δ :
+    TCOr (TCAnd (MergablePersist P C0) $
+          TCAnd (C0 false empty_hyp_first P0) $
+                 TCEq mP0 (Some P0)) 
+         (TCAnd (TCEq C0 (λ _ _ _, True)) $
+          TCAnd (TCEq P0 bi_emp) $
+                 TCEq mP0 None) →    
+    TCOr (TCAnd (MergablePersist P C1) $
+          TCAnd (C1 false empty_hyp_last P1) $
+                 TCEq mP1 (Some P1)) 
+         (TCAnd (TCEq C1 (λ _ _ _, True)) $
+          TCAnd (TCEq P1 bi_emp) $
+                 TCEq mP1 None) →
+    MergableEnv Δ P (match mP1 with 
+                     | Some H1 => Some $ match mP0 with | Some H0 => H0 ∧ H1 | _ => H1 end
+                     | None => mP0
+                     end)%I | 999.
+  Proof.
+    rewrite /MergableEnv.
+    move => [[HPC0 [/HPC0 /= HC0 ->]]|[_ [_ ->]]] [[HPC1 [/HPC1 /= HC1 ->]]|[_ [_ ->]]] /=.
+    - iIntros "[_ HP]". iSplit.
+      * iApply HC0. iFrame. rewrite empty_hyp_first_eq //.
+      * iApply HC1. iFrame. rewrite empty_hyp_last_eq //.
+    - iIntros "[_ HP]".
+      iApply HC0. iFrame. rewrite empty_hyp_first_eq //.
+    - iIntros "[_ HP]".
+      iApply HC1. iFrame. rewrite empty_hyp_last_eq //.
+    - eauto.
+  Qed.
+
+  Global Instance mergable_env_cons Δ P C i p P2 P3 M :
     MergablePersist P C →
-    FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2 →
-    MergableEnv (envs_option_delete true mi p Δ) P M →
-    MakeAnd M P3 PR →
-    MergableEnv Δ P PR | 100.
+    FindInContext Δ (λ p P2, C p P2 P3) i p P2 →
+    MergableEnv (envs_delete true i p Δ) P M →
+    MergableEnv Δ P (Some $ match M with | Some M' => M' ∧ P3 | _ => P3 end)%I | 100.
   Proof.
     rewrite /MergablePersist /MergableEnv /MakeAnd => HCP HΔ.
-    apply (ficext_satisfies) in HΔ as HC.
-    apply (findinextcontext_spec true) in HΔ.
-    rewrite HΔ => {HΔ}.
-    rewrite -assoc => HΔ <-.
-    iIntros "(HP2 & HΔ & HP)".
-    iSplit.
+    apply (fic_satisfies) in HΔ as HC. simpl in HC.
+    apply (findincontext_spec true) in HΔ.
+    rewrite HΔ => {HΔ}. set (Δ' := envs_delete true i p Δ).
+    rewrite -assoc => HΔ.
+    iIntros "(HP2 & HΔ & HP)". cbn.
+    destruct M as [M'|]; first iSplit.
     - iClear "HP2". iApply HΔ. by iFrame.
     - iClear "HΔ". iApply HCP => //. by iFrame.
+    - iClear "HΔ". iApply HCP => //. by iFrame.
   Qed.
 
 End mergable_env.
@@ -249,12 +279,17 @@ Section coq_tactics.
     done.
   Qed.
 
-  Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' R P3 :
-    MergableEnv Δ P1 P3 →
+  Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' R mP3 :
+    MergableEnv Δ P1 mP3 →
     TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
         (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
     match envs_add_fresh a j P1' Δ with
-    | Some Δ' => envs_entails Δ' $ IntroduceHyp (□ P3)%I R
+    | Some Δ' => 
+      match mP3 with
+      | None => envs_entails Δ' R
+      | Some P3 =>
+        envs_entails Δ' $ IntroduceHyp (□ P3)%I R
+      end
     | _ => False
     end →
     envs_entails Δ $ IntroduceHyp P1 R.
@@ -266,9 +301,11 @@ Section coq_tactics.
     { revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
       unfold bi_intuitionistically.
       rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
+    destruct mP3 as [P3|]; last first.
+    { rewrite envs_add_fresh_sound // -HΔR. rewrite -HP1_ent. by iApply "HΔ'". }
     iAssert (□ P3)%I as "#HP3"; last first. (* 'iEnough' *)
     { rewrite (envs_add_fresh_sound Δ) //.
-      rewrite HP1_ent.
+      rewrite -HP1_ent.
       iSpecialize ("HΔ'" with "HP1"). 
       by iApply (HΔR with "HΔ'"). }
     iCombine "HΔ' HP1" as "H".
@@ -494,11 +531,14 @@ Ltac introduceHypStep namer_tac :=
       |introduceHypPure
       |notypeclasses refine (tac_introduce_hyp_merge_consume _ _ _ _ _ _ _ _ _ _); 
         [iSolveTC | register_delete namer_tac; simpl ]
-      | let j := namer_tac NameTac.GetName Δ P in first
+      | let j := namer_tac NameTac.GetName Δ P in 
+        notypeclasses refine (tac_introduce_hyp_merge_env j _ _ _ _ _ _ _ _ _);
+        [iSolveTC | iSolveTC | simpl]
+        (*first
         [notypeclasses refine (tac_introduce_hyp_merge_persist j _ _ _ _ _ _ _ _ _ _ _ _ _);
           [iSolveTC | iSolveTC | simpl ]
         |notypeclasses refine (tac_introduce_hyp_not_mergable j _ _ _ _ _ _ _);
-          [iSolveTC | simpl ] ]
+          [iSolveTC | simpl ] ] *)
       ]
     end
   end.

theories/util_instances.v

@@ -753,8 +753,9 @@ Global Hint Extern 4 (FindInContext ?Δ ?PTC ?k ?r ?R) =>
       [let hole := eval cbn beta in (PTC p Q) in eassert hole by iSolveTC ; unify i j; unify R Q
       |find Γ i p]
     end in
+  let Δ' := eval cbn [envs_option_delete envs_delete env_delete ident_beq string_beq ascii_beq beq] in Δ in
   first [
-    is_evar k; match Δ with | Envs ?Γp ?Γs _ => first [unify r false; find Γs k false | unify r true; find Γp k true]; split; [pm_reflexivity|done] end
+    is_evar k; match Δ' with | Envs ?Γp ?Γs _ => first [unify r false; find Γs k false | unify r true; find Γp k true]; split; [pm_reflexivity|done] end
     | split; [pm_reflexivity|iSolveTC]
   ] : typeclass_instances.