Finished the propert version of from_predicated_sem_pred_expr2

7 files changed, 316 insertions, 44 deletions

diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v
index 2169306..24a29a3 100644
--- a/src/common/NonEmpty.v
+++ b/src/common/NonEmpty.v
@@ -326,3 +326,15 @@ Proof.
   - constructor.
   - clear H. inv H1; intuition (constructor; auto).
 Qed.
+
+Lemma In_map2 :
+  forall A B (f: A -> B) n (x: B),
+    In x (map f n) ->
+    exists y, In y n /\ x = f y.
+Proof.
+  induction n; inversion 1; subst; cbn in *.
+  - inv H. exists a; split; auto. constructor.
+  - clear H. inv H1.
+    + exists a; split; auto; constructor; tauto.
+    + exploit IHn; eauto; simplify. exists x0; split; auto; constructor; tauto.
+Qed.
diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v
index fdd7dcb..5ec9200 100644
--- a/src/hls/AbstrSemIdent.v
+++ b/src/hls/AbstrSemIdent.v
@@ -1065,16 +1065,14 @@ Proof.
         eapply H3; eauto.
       * constructor; eauto. constructor. left.
         replace true with (negb false) by auto. now apply sem_pexpr_negate.
-        eapply IHpe; auto. eapply predicated_cons; eauto.
+        eauto using predicated_cons.
     + intros * HPREDS **; cbn in *; unfold "→"; repeat destr. inv Heqp. inv H0.
       * constructor. left. constructor. replace false with (negb true) by auto. now apply sem_pexpr_negate.
         constructor; auto.
-      * constructor. right.
-        eapply IHpe; eauto.
-        eapply predicated_cons; eauto.
+      * constructor. right. eauto using predicated_cons.
 Qed.
 
-Lemma from_predicated_sem_pred_expr2:
+Lemma from_predicated_sem_pred_expr2':
   forall preds ps pe b b',
     (forall x, sem_pexpr ctx (get_forest_p' x preds) (ps !! x)) ->
     predicated_mutexcl pe ->
@@ -1095,29 +1093,105 @@ Proof.
       * eapply sem_pred_det; eauto. reflexivity.
       * replace false with (negb true) in H4 by auto. apply sem_pexpr_negate2 in H4.
         eapply sem_pexpr_det in H4; eauto; [discriminate|reflexivity].
-    + inv H1.
-      * exploit from_predicated_sem_pred_expr_true.
-        instantiate (2 := pe). instantiate (1 := preds).
-        intros.
-        assert (NE.In x (NE.cons (p, p0) pe)) by (constructor; tauto).
-        inv H.
-        assert ((p, p0) <> x).
-        { unfold not; intros. subst. inv H4. contradiction. }
-        specialize (H3 _ _ ltac:(constructor; left; auto) H2 H).
-        destruct x; cbn in *.
-        eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H7; eauto.
-        apply negb_inj; cbn.
-        rewrite <- eval_predf_negate.
-        eapply H3; eauto.
-        intros. eapply sem_pexpr_det in H0; now try eapply H1.
-      * eapply IHpe; auto. eapply predicated_cons; eauto.
-    + inv H4. inv H2; inv H1.
+    + inv H1; eauto using predicated_cons.
+      exploit from_predicated_sem_pred_expr_true.
+      instantiate (2 := pe). instantiate (1 := preds).
+      intros.
+      assert (NE.In x (NE.cons (p, p0) pe)) by (constructor; tauto).
+      inv H.
+      assert ((p, p0) <> x).
+      { unfold not; intros. subst. inv H4. contradiction. }
+      specialize (H3 _ _ ltac:(constructor; left; auto) H2 H).
+      destruct x; cbn in *.
+      eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H7; eauto.
+      apply negb_inj; cbn.
+      rewrite <- eval_predf_negate.
+      eapply H3; eauto.
+      intros. eapply sem_pexpr_det in H0; now try eapply H1.      
+    + inv H4. inv H2; inv H1; eauto using predicated_cons.
       * replace true with (negb false) in H0 by auto.
         apply sem_pexpr_negate2 in H0.
         eapply sem_pexpr_det in H0; now try apply H8.
-      * eapply IHpe; eauto. eapply predicated_cons; eauto.
       * inv H0. eapply sem_pred_det in H9; now eauto.
-      * eapply IHpe; eauto. eapply predicated_cons; eauto.
+Qed.
+
+Lemma from_predicated_inv_exists_true :
+  forall ps pe,
+    eval_predf ps (from_predicated_inv pe) = true ->
+    exists y, NE.In y pe /\ (eval_predf ps (fst y) = true).
+Proof.
+  induction pe; cbn -[eval_predf]; intros; repeat destr; inv Heqp.
+  - exists (p, p0); intuition constructor.
+  - rewrite eval_predf_Por in H. apply orb_prop in H. inv H.
+    + exists (p, p0); intuition constructor; tauto.
+    + exploit IHpe; auto; simplify.
+      exists x; intuition constructor; tauto.
+Qed.
+
+Lemma from_predicated_sem_pred_expr2:
+  forall preds ps pe b,
+    (forall x, sem_pexpr ctx (get_forest_p' x preds) (ps !! x)) ->
+    predicated_mutexcl pe ->
+    sem_pexpr ctx (from_predicated true preds pe) b ->
+    eval_predf ps (from_predicated_inv pe) = true ->
+    sem_pred_expr preds sem_pred ctx pe b.
+Proof.
+  induction pe.
+  - cbn -[eval_predf]; intros; repeat destr. inv Heqp. inv H1. inv H6.
+    + replace true with (negb false) in H1 by auto.
+      apply sem_pexpr_negate2 in H1.
+      eapply sem_pexpr_eval_inv in H1; eauto.
+      now rewrite H1 in H2.
+    + inv H1. constructor; auto. eapply sem_pexpr_eval; eauto.
+    + inv H7. constructor; auto. eapply sem_pexpr_eval; eauto.
+  - cbn -[eval_predf]; intros; repeat destr. inv Heqp.
+    rewrite eval_predf_Por in H2. apply orb_prop in H2. inv H2.
+    + inv H1. inv H6.
+      * inv H1. inv H6. constructor; eauto using sem_pexpr_eval.
+      * (* contradiction, because eval_predf p true means that all other
+        implications in H1 are false, therefore sem_pexpr will evaluate to
+        true. *)
+        exploit from_predicated_sem_pred_expr_true.
+        -- instantiate (2 := pe). instantiate (1 := preds).
+           intros. destruct x.
+           assert (HIN1: NE.In (p, p0) (NE.cons (p, p0) pe))
+             by (intuition constructor; tauto).
+           assert (HIN2: NE.In (p1, p2) (NE.cons (p, p0) pe))
+             by (intuition constructor; tauto).
+           assert (HNEQ: (p, p0) <> (p1, p2)).
+           { unfold not; inversion 1; subst. clear H4. inv H0. inv H5. contradiction. }
+           cbn. eapply sem_pexpr_eval; eauto.
+           symmetry. rewrite <- negb_involutive. symmetry.
+           rewrite <- eval_predf_negate. rewrite <- negb_involutive.
+           f_equal; cbn.
+           inv H0. specialize (H4 _ _ HIN1 HIN2 HNEQ). cbn in H4.
+           eapply H4; auto.
+        -- intros. eapply sem_pexpr_det in H1; now eauto.
+      * inv H5. inv H2.
+        -- eapply sem_pexpr_negate2' in H1. eapply sem_pexpr_eval_inv in H; eauto.
+           now rewrite H in H3.
+        -- inv H1. constructor; eauto using sem_pexpr_eval.
+    + assert (eval_predf ps p = false).
+      { case_eq (eval_predf ps p); auto; intros HCASE; exfalso.
+        exploit from_predicated_inv_exists_true; eauto; simplify.
+        destruct x; cbn -[eval_predf] in *.
+        assert (HNEQ: (p, p0) <> (p1, p2)).
+        { unfold not; intros. inv H4. inv H0. inv H6. contradiction. }
+        assert (HIN2: NE.In (p1, p2) (NE.cons (p, p0) pe))
+          by (intuition constructor; tauto).
+        assert (HIN1: NE.In (p, p0) (NE.cons (p, p0) pe))
+          by (intuition constructor; tauto).
+        inv H0. specialize (H4 _ _ HIN1 HIN2 HNEQ). eapply H4 in HCASE. cbn in HCASE.
+        rewrite negate_correct in HCASE. now setoid_rewrite H5 in HCASE.
+      }
+      inv H1. inv H7.
+      * inv H1.
+        apply sem_pexpr_negate2' in H6. eapply sem_pexpr_eval_inv in H6; eauto.
+        now rewrite H2 in H6.
+      * eapply sem_pred_expr_cons_false;
+          eauto using sem_pexpr_eval, predicated_cons.
+      * inv H6. inv H4; eapply sem_pred_expr_cons_false;
+          eauto using sem_pexpr_eval, predicated_cons.
 Qed.
 
 End PROOF.
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 91b0450..c1c5fdb 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -193,6 +193,12 @@ Fixpoint from_predicated (b: bool) (f: PTree.t pred_pexpr) (a: predicated pred_e
            (from_predicated b f r)
   end.
 
+Fixpoint from_predicated_inv (a: predicated pred_expression): pred_op :=
+  match a with
+  | NE.singleton (p, e) => p
+  | (p, e) ::| r => Por p (from_predicated_inv r)
+  end.
+
 #[local] Open Scope monad_scope.
 
 Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) :=
@@ -262,12 +268,15 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
                                    (merge (list_translation rl f))) (f #r Mem)));
       Some (pred, f #r Mem <- pruned)
   | RBsetpred p' c args p =>
+      let predicated := seq_app
+        (pred_ret (PEsetpred c))
+        (merge (list_translation args f)) in
       let new_pred :=
         (from_pred_op f.(forest_preds) (dfltp p' ∧ pred)
-           → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c))
-                                                  (merge (list_translation args f))))
+           → from_predicated true f.(forest_preds) predicated)
         ∧ (from_pred_op f.(forest_preds) (¬ (dfltp p') ∨ ¬ pred) → (f #p p))
       in
+      do _ <- assert_ (check_mutexcl predicated);
       do _ <- assert_ (predicated_not_in_forest p f);
       do _ <- assert_ (is_initial_pred_and_notin f p pred);
       Some (pred, f #p p <- new_pred)
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 5a18efe..676c96d 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -93,10 +93,25 @@ Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list
   | RBexit p c => lst
   end.
 
+Definition remember_expr_p (f : forest) (lst: list (option pred_op * predicated pred_expression)) (i : instr):
+    list (option pred_op * predicated pred_expression) :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => lst
+  | RBload  p chunk addr rl r => lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p => (p', seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) :: lst
+  | RBexit p c => lst
+  end.
+
 Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
   let '(p, f, l, lm) := s in
   Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
 
+Definition update'' (s: pred_op * forest * list pred_expr * list pred_expr * list (option pred_op * predicated pred_expression)) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list (option pred_op * predicated pred_expression)) :=
+  let '(p, f, l, lm, lp) := s in
+  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i).
+
 Lemma equiv_update:
   forall i p f l lm p' f' l' lm',
     mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -357,14 +372,16 @@ Proof.
   assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
     by now inv H0.
   inversion_clear HPRED' as [? ? ? HPRED].
-  destruct ti as [is_trs is_tps is_tm]. destr. inv H4. inv H1.
+  destruct ti as [is_trs is_tps is_tm]. do 2 destr. inv H4. inv H1.
   pose proof H as YH. specialize (YH src). rewrite forest_pred_gss in YH.
   inv YH; try inv H3.
   + inv H1. inv H6. replace false with (negb true) in H4 by auto.
     replace false with (negb true) in H8 by auto.
     eapply sem_pexpr_negate2 in H4. eapply sem_pexpr_negate2 in H8.
     destruct i.
-    exploit from_predicated_sem_pred_expr2; eauto; intros.
+    exploit from_predicated_sem_pred_expr2.
+    3: { eauto. }
+    3: {  }
     exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify.
     inv H3. inv H15. clear H13.
     exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H3.
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v
index 2dbdf12..0a09c23 100644
--- a/src/hls/GiblePargenproofCommon.v
+++ b/src/hls/GiblePargenproofCommon.v
@@ -233,11 +233,148 @@ Proof.
   - intros. cbn in H. eapply andb_prop in H. inv H. eapply IHa in H0.
     unfold predicated_not_inP in *; intros. inv H. inv H3; cbn in *; eauto.
     unfold not; intros. eapply predin_PredIn in H. now rewrite H in H1.
-Qed.
-    
+Qed.    
 
 Lemma truthy_dec:
   forall ps a, truthy ps a \/ falsy ps a.
 Proof.
   destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto).
 Qed.
+
+Definition all_mutexcl (f: forest) : Prop :=
+  forall x, predicated_mutexcl (f #r x).
+
+(* Lemma map_mutexcl' : *)
+(*   forall A B (x: predicated A) (f: (pred_op * A) -> (pred_op * B)), *)
+(*     predicated_mutexcl x -> *)
+(*     (forall a pop, fst (f (pop, a)) ⇒ pop) -> *)
+(*     (forall a b, f a = f b -> a = b) -> *)
+(*     predicated_mutexcl (NE.map f x). *)
+(* Proof. *)
+(*   induction x; cbn; intros. *)
+(*   - cbn. repeat constructor; intros. inv H2. inv H3. contradiction. *)
+(*   - constructor. intros. *)
+(*     assert (exists x0', x0 = f x0') by admit. *)
+(*     assert (exists y', y = f y') by admit. *)
+(*     simplify. unfold "⇒" in *; intros. *)
+(*     destruct x2, x1. *)
+(*     eapply H0 in H5. *)
+(*     inv H. *)
+(*     specialize (H6 (p, a0) (p0, a1)). *)
+(*     assert ((fst (p, a0)) ⇒ ¬ (fst (p0, a1))) by admit. *)
+(*     unfold "⇒" in H; simplify. *)
+(*     apply H in H5. *)
+
+Lemma map_deep_simplify :
+  forall A x (eqd: forall a b: pred_op * A, {a = b} + {a <> b}),
+    predicated_mutexcl x ->
+    predicated_mutexcl
+      (GiblePargenproofEquiv.NE.map (fun x : Predicate.pred_op * A => (deep_simplify peq (fst x), snd x)) x).
+Proof.
+  intros. inv H.
+  assert (forall x0 y : pred_op * A,
+  GiblePargenproofEquiv.NE.In x0
+    (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) ->
+  GiblePargenproofEquiv.NE.In y
+    (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) ->
+  x0 <> y -> fst x0 ⇒ ¬ fst y).
+  { intros. exploit NE.In_map2. eapply H. simplify.
+    exploit NE.In_map2. eapply H2. simplify.
+    specialize (H0 _ _ H4 H5).
+    destruct (eqd x1 x0); subst; try contradiction.
+    apply H0 in n.
+    unfold "⇒" in *; intros. rewrite negate_correct.
+    rewrite deep_simplify_correct. rewrite <- negate_correct. apply n.
+    erewrite <- deep_simplify_correct; eassumption. }
+  constructor; auto.
+  generalize dependent x. induction x; crush; [constructor|].
+  inv H1.
+  assert (forall x0 y, GiblePargenproofEquiv.NE.In x0 x -> GiblePargenproofEquiv.NE.In y x -> x0 <> y -> fst x0 ⇒ ¬ fst y).
+  { intros. eapply H0; auto; constructor; tauto. }
+  assert (forall x0 y : pred_op * A,
+    GiblePargenproofEquiv.NE.In x0
+      (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) ->
+    GiblePargenproofEquiv.NE.In y
+      (GiblePargenproofEquiv.NE.map (fun x1 : Predicate.pred_op * A => (deep_simplify peq (fst x1), snd x1)) x) ->
+    x0 <> y -> fst x0 ⇒ ¬ fst y).
+  { intros. eapply H; auto; constructor; tauto. }
+  constructor; eauto.
+  unfold not; intros.
+  Abort.
+
+Lemma prune_predicated_mutexcl :
+  forall A (x: predicated A) y,
+    predicated_mutexcl x ->
+    prune_predicated x = Some y ->
+    predicated_mutexcl y.
+Proof.
+  unfold prune_predicated; intros.
+  Admitted.
+#[local] Hint Resolve prune_predicated_mutexcl : mte.
+
+Lemma app_predicated_mutexcl :
+  forall A p (x: predicated A) y,
+    predicated_mutexcl x ->
+    predicated_mutexcl y ->
+    predicated_mutexcl (app_predicated p x y).
+Proof. Admitted.
+#[local] Hint Resolve app_predicated_mutexcl : mte.
+
+Lemma seq_app_predicated_mutexcl :
+  forall A B (f: predicated (A -> B)) y,
+    predicated_mutexcl f ->
+    predicated_mutexcl y ->
+    predicated_mutexcl (seq_app f y).
+Proof. Admitted.
+#[local] Hint Resolve seq_app_predicated_mutexcl : mte.
+
+Lemma all_predicated_mutexcl:
+  forall f l,
+    all_mutexcl f ->
+    predicated_mutexcl (merge (list_translation l f)).
+Proof. Admitted.
+#[local] Hint Resolve all_predicated_mutexcl : mte.
+
+Lemma flap2_predicated_mutexcl :
+  forall A B C (f: predicated (A -> B -> C)) x y,
+    predicated_mutexcl f ->
+    predicated_mutexcl (flap2 f x y).
+Proof. Admitted.
+#[local] Hint Resolve flap2_predicated_mutexcl : mte.
+
+Lemma all_mutexcl_set :
+  forall f n r,
+    all_mutexcl f ->
+    predicated_mutexcl n ->
+    all_mutexcl f #r r <- n.
+Proof.
+  unfold all_mutexcl; intros.
+  destruct (resource_eq x r); subst.
+  { now rewrite forest_reg_gss. }
+  now rewrite forest_reg_gso by auto.
+Qed.
+#[local] Hint Resolve all_mutexcl_set : mte.
+
+Lemma pred_ret_mutexcl :
+  forall A (a: A), predicated_mutexcl (pred_ret a).
+Proof.
+  unfold pred_ret. repeat constructor; intros. inv H. inv H0. contradiction.
+Qed.
+#[local] Hint Resolve pred_ret_mutexcl : mte.
+
+Lemma all_mutexcl_maintained :
+  forall f p p' f' i,
+    all_mutexcl f ->
+    update (p, f) i = Some (p', f') ->
+    all_mutexcl f'.
+Proof.
+  destruct i; cbn -[seq_app]; intros; unfold Option.bind in *; repeat destr; inv H0.
+  - trivial.
+  - apply prune_predicated_mutexcl in Heqo1; auto with mte.
+  - apply prune_predicated_mutexcl in Heqo0; auto with mte.
+  - apply prune_predicated_mutexcl in Heqo0; auto with mte.
+    apply app_predicated_mutexcl; auto with mte.
+  - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto.
+  - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn.
+    fold (get_forest x f). auto.
+Qed.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index a1bfa0c..9e58981 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -890,6 +890,24 @@ Section SEM_PRED_EXEC.
       + destruct b; try discriminate. constructor; eauto.
   Qed.
 
+  Lemma sem_pexpr_negate2' :
+    forall p b,
+      sem_pexpr ctx (¬ p) b ->
+      sem_pexpr ctx p (negb b).
+  Proof.
+    intros. rewrite <- negb_involutive in H.
+    auto using sem_pexpr_negate2.
+  Qed.
+
+  Lemma sem_pexpr_negate' :
+    forall p b,
+      sem_pexpr ctx p (negb b) ->
+      sem_pexpr ctx (¬ p) b.
+  Proof.
+    intros. rewrite <- negb_involutive.
+    auto using sem_pexpr_negate.
+  Qed.
+
   Lemma sem_pexpr_evaluable :
     forall f_p ps,
       (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v
index d340477..3d0f7d5 100644
--- a/src/hls/GiblePargenproofForward.v
+++ b/src/hls/GiblePargenproofForward.v
@@ -374,6 +374,7 @@ all be evaluable.
 
   Lemma sem_update_Isetpred:
     forall A (ctx: @ctx A) f pr p0 c args b rs m,
+      predicated_mutexcl (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) ->
       valid_mem (ctx_mem ctx) m ->
       sem ctx f (mk_instr_state rs pr m, None) ->
       Op.eval_condition c rs ## args m = Some b ->
@@ -381,7 +382,9 @@ all be evaluable.
       sem_pexpr ctx
       (from_predicated true (forest_preds f) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) b.
   Proof.
-    intros. eapply from_predicated_sem_pred_expr.
+    intros * HPREDMUT **. eapply from_predicated_sem_pred_expr.
+    { inv H0. inv H10. eassumption. }
+    { auto. }
     pose proof (sem_merge_list _ ctx f rs pr m args H0).
     apply sem_pred_expr_ident2 in H3; simplify.
     eapply sem_pred_expr_seq_app_val; [eauto| |].
@@ -402,7 +405,7 @@ all be evaluable.
   Proof.
     intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED.
     pose proof SEM as SEM2.
-    inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. destr.
+    inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. repeat destr.
     inversion_clear PRUNE.
     rename Heqo into PRUNE.
     inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
@@ -413,11 +416,12 @@ all be evaluable.
     + constructor; intros. destruct (peq x pred); subst.
       * rewrite Regmap.gss.
         rewrite forest_pred_gss.
-        cbn [update] in *. unfold Option.bind in *. destr. destr. inv UPD.
+        cbn [update] in *. unfold Option.bind in *. repeat destr. inv UPD.
         replace b with (b && true) by eauto with bool.
         apply sem_pexpr_Pand.
         destruct b. constructor. right.
         eapply sem_update_Isetpred; eauto.
+        { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. }
         constructor. constructor. replace false with (negb true) by auto.
         apply sem_pexpr_negate. inv TRUTHY. constructor.
         cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto.
@@ -425,6 +429,7 @@ all be evaluable.
         apply sem_pexpr_negate.
         eapply sem_pexpr_eval. inv PRED. eauto. auto.
         eapply sem_update_Isetpred; eauto.
+        { unfold assert_ in Heqo. destr. auto using check_mutexcl_correct. }
         constructor. constructor. constructor.
         replace true with (negb false) by auto. apply sem_pexpr_negate.
         eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf].
@@ -503,10 +508,10 @@ all be evaluable.
         eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto.
         rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
       * inv H3. auto.
-    - unfold Option.bind in *. destr. destr. inv H2.
+    - unfold Option.bind in *. repeat destr. inv H2.
       constructor.
       * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in.
-        inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
+        inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
       * constructor. intros. destruct (peq x pred); subst.
         rewrite forest_pred_gss. replace (ps !! pred) with (true && ps !! pred) by auto.
         assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) p0 ∧ from_pred_op (forest_preds f) p')) true).
@@ -521,9 +526,9 @@ all be evaluable.
         }
         rewrite forest_pred_gso by auto. inv H3. inv H9. auto.
       * rewrite forest_pred_reg. apply sem_pred_not_in. inv H3. auto.
-        apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
+        apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
       * apply sem_pred_not_in. inv H3; auto. cbn.
-        apply pred_not_in_forest_exitP. unfold assert_ in Heqo. now destr.
+        apply pred_not_in_forest_exitP. unfold assert_ in Heqo0. now destr.
     - unfold Option.bind in *. destr. inv H2. inv H3. constructor.
       * constructor. inv H8. auto.
       * constructor. intros. inv H9. eauto.
@@ -578,10 +583,10 @@ all be evaluable.
         eapply sem_pred_expr_app_predicated_false. inv H1. auto. inv H1. inv H8. eauto.
         rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool.
       * inv H1. auto.
-    - unfold Option.bind in *. destr. destr. inv H0. split; [|solve [auto]].
+    - unfold Option.bind in *. repeat destr. inv H0. split; [|solve [auto]].
       constructor.
       * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in.
-        inv H1. inv H7. auto. apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
+        inv H1. inv H7. auto. apply pred_not_in_forestP. unfold assert_ in Heqo1. now destr.
       * constructor. intros. destruct (peq x p0); subst.
         rewrite forest_pred_gss. replace (ps !! p0) with (true && ps !! p0) by auto.
         assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) (dfltp o) ∧ from_pred_op (forest_preds f) p')) true).
@@ -596,9 +601,9 @@ all be evaluable.
         }
         rewrite forest_pred_gso by auto. inv H1. inv H8. auto.
       * rewrite forest_pred_reg. apply sem_pred_not_in. inv H1. auto.
-        apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
+        apply pred_not_in_forestP. unfold assert_ in Heqo1. now destr.
       * apply sem_pred_not_in. inv H1; auto. cbn.
-        apply pred_not_in_forest_exitP. unfold assert_ in Heqo0. now destr.
+        apply pred_not_in_forest_exitP. unfold assert_ in Heqo1. now destr.
     - unfold Option.bind in *. destr. inv H0. inv H1. split.
       -- constructor.
          * constructor. inv H7. auto.
@@ -742,9 +747,9 @@ all be evaluable.
   Proof.
     intros * UPD STEP EVAL. destruct instr; cbn [update] in UPD;
       try solve [unfold Option.bind in *; try destr; inv UPD; inv STEP; auto].
-    - unfold Option.bind in *. destr. destr. inv UPD. inv STEP; auto. cbn [is_ps] in *.
-      unfold is_initial_pred_and_notin in Heqo1. unfold assert_ in Heqo1. destr. destr.
-      destr. destr. destr. destr. subst. assert (~ PredIn p2 next_p).
+    - unfold Option.bind in *. repeat destr. inv UPD. inv STEP; auto. cbn [is_ps] in *.
+      unfold is_initial_pred_and_notin in Heqo2. unfold assert_ in Heqo2. repeat destr.
+      subst. assert (~ PredIn p2 next_p).
       unfold not; intros. apply negb_true_iff in Heqb0. apply not_true_iff_false in Heqb0.
       apply Heqb0. now apply predin_PredIn. rewrite eval_predf_not_PredIn; auto.
     - unfold Option.bind in *. destr. inv UPD. inv STEP. inv H3. cbn.