fix minor issues

theories/logrel/F_mu_ref_conc/binary/examples/fact.v

@@ -86,7 +86,7 @@ Section fact_equiv.
       iExists (#nv _); iFrame; eauto. }
     generalize 1%Z as l => l.
     iLöb as "IH" forall (n l).
-    destruct (decide (n = 0)) as [->|].
+    destruct (decide (n = 0)%Z) as [->|].
     - iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl; asimpl.
       rewrite fact_acc_body_unfold.
@@ -117,12 +117,14 @@ Section fact_equiv.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
       iApply wp_value. simpl.
-      destruct Z.eq_dec; first lia.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
       simpl.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
-      destruct Z.eq_dec; first lia.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       asimpl.
       iApply (wp_bind (fill [BinOpRCtx _ (#nv _)])).
@@ -201,12 +203,14 @@ Section fact_equiv.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
       iApply wp_value. simpl.
-      destruct Z.eq_dec; first done.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
       simpl.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
-      destruct Z.eq_dec; first done.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       iMod (do_step_pure _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
               with "[$Hj]") as "Hj"; eauto.

theories/logrel/F_mu_ref_conc/lang.v

@@ -94,22 +94,18 @@ Module F_mu_ref_conc.
     | Add => λ a b, #nv(a + b)
     | Sub => λ a b, #nv(a - b)
     | Mult => λ a b, #nv(a * b)
-    | Eq => λ a b, if (Z.eq_dec a b) then #♭v true else #♭v false
-    | Le => λ a b, if (Z.le_dec a b) then #♭v true else #♭v false
-    | Lt => λ a b, if (Z.lt_dec a b) then #♭v true else #♭v false
+    | Eq => λ a b, #♭v (bool_decide (a = b))
+    | Le => λ a b, #♭v (bool_decide (a ≤ b)%Z)
+    | Lt => λ a b, #♭v (bool_decide (a < b)%Z)
     end.
 
   Definition binop_eval (op : binop) : val → val → option val :=
     match op with
     | Eq => λ a b, Some (#♭v (bool_decide (a = b)))
     | _ => λ a b,
-        match a with
-        | IntV an =>
-            match b with
-            | IntV bn => Some (int_binop_eval op an bn)
-            | _ => None
-            end
-        | _ => None
+        match a, b with
+        | IntV an, IntV bn => Some (int_binop_eval op an bn)
+        | _, _ => None
         end
     end.
 

theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v

@@ -102,7 +102,9 @@ Section symbol_nat_sem_typ.
       iModIntro.
       simpl.
       iApply wp_pure_step_later; auto. iIntros "!> _".
-      simpl. destruct Z.lt_dec; last lia.
+      simpl.
+      destruct (decide (m < t)%Z); last lia.
+      rewrite bool_decide_eq_true_2; last done.
       iApply wp_value.
       iApply wp_pure_step_later; auto. iIntros "!> _".
       iApply wp_value; eauto.

theories/logrel/F_mu_ref_conc/wp_rules.v

@@ -142,7 +142,15 @@ Section lang_rules.
 
   Local Ltac solve_exec_safe :=
     intros; subst; do 3 eexists; econstructor; simpl; eauto.
-  Local Ltac solve_exec_puredet := simpl; intros; by inv_base_step.
+  Local Ltac solve_exec_puredet :=
+    simpl; intros;
+      by inv_base_step;
+      repeat match goal with
+          |- context [bool_decide ?A] =>
+            destruct (decide A);
+            [rewrite (bool_decide_eq_true_2 A); last done|
+             rewrite (bool_decide_eq_false_2 A); last done]
+        end; simplify_eq/=; auto.
   Local Ltac solve_pure_exec :=
     unfold IntoVal in *;
     repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
@@ -202,31 +210,10 @@ Section lang_rules.
 
   Global Instance wp_int_binop op a b :
     PureExec True 1 (BinOp op (#n a) (#n b)) (of_val (int_binop_eval op a b)).
-  Proof.
-    destruct op;
-      (unfold IntoVal in *;
-      repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
-       intros ?; apply nsteps_once, pure_base_step_pure_step;
-       constructor; [solve_exec_safe |try solve_exec_puredet]); [].
-    intros; simpl in *; inv_base_step.
-    destruct Z.eq_dec as [->|];
-      [rewrite bool_decide_eq_true_2; done|
-       rewrite bool_decide_eq_false_2; eauto with congruence].
-  Qed.
+  Proof. destruct op; solve_pure_exec. Qed.
 
   Global Instance wp_Eq_binop `{!AsVal e1} `{!AsVal e2} :
     PureExec True 1 (BinOp Eq e1 e2) (#♭ (bool_decide (e1 = e2))).
-  Proof.
-    unfold IntoVal in *;
-      repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
-       intros ?; apply nsteps_once, pure_base_step_pure_step;
-       constructor; [solve_exec_safe |]; [].
-    intros; simpl in *; inv_base_step.
-    match goal with |- context[ bool_decide (?A = ?B)] =>
-    destruct (decide (A = B)) as [->|] end;
-    [rewrite !bool_decide_eq_true_2; done|
-       rewrite !bool_decide_eq_false_2; eauto].
-    intros ?%of_val_inj; done.
-  Qed.
+  Proof. solve_pure_exec. Qed.
 
 End lang_rules.