From b144625268ac41a2532eaa185b4118ba1aaf8ea5 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 15 Feb 2024 20:27:50 +0100
Subject: [PATCH] fix minor issues
---
.../F_mu_ref_conc/binary/examples/fact.v | 14 +++++---
theories/logrel/F_mu_ref_conc/lang.v | 16 ++++-----
.../F_mu_ref_conc/unary/examples/symbol_nat.v | 4 ++-
theories/logrel/F_mu_ref_conc/wp_rules.v | 35 ++++++-------------
4 files changed, 29 insertions(+), 40 deletions(-)
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/fact.v b/theories/logrel/F_mu_ref_conc/binary/examples/fact.v
index cd9a5aac..dd010401 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/fact.v
+++ b/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.
diff --git a/theories/logrel/F_mu_ref_conc/lang.v b/theories/logrel/F_mu_ref_conc/lang.v
index 79c2317f..2c8303f1 100644
--- a/theories/logrel/F_mu_ref_conc/lang.v
+++ b/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.
diff --git a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
index d8f4b605..f33cd53b 100644
--- a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
+++ b/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.
diff --git a/theories/logrel/F_mu_ref_conc/wp_rules.v b/theories/logrel/F_mu_ref_conc/wp_rules.v
index 6f72ab43..08f811f2 100644
--- a/theories/logrel/F_mu_ref_conc/wp_rules.v
+++ b/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.
--
GitLab