Commit 88e22fa8 authored by Dan Frumin's avatar Dan Frumin

Get rid of `Peano.nat.eq_nat_dec` in favour of `decide`.

`decide` works much better because of the general lemmas and tacitcs
parent 59d1cab3
......@@ -107,7 +107,7 @@ Module lang.
match op,v1,v2 with
| Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b))
| Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
| Eq, LitV (Nat a), LitV (Nat b) => Some $ if eq_nat_dec a b then LitV (Bool true) else LitV (Bool false)
| Eq, LitV (Nat a), LitV (Nat b) => Some $ if decide (a = b) then LitV (Bool true) else LitV (Bool false)
| Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
| Eq, LitV (Loc l1), LitV (Loc l2) => Some $ if decide (l1 = l2) then LitV (Bool true) else LitV (Bool false)
| Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false)
......
......@@ -133,13 +133,13 @@ Section namegen_refinement.
iDestruct (bij_agree with "HB Hln Hl'n'") as %Hag.
destruct (decide (l = l')) as [->|Hll].
+ assert (n = n') as -> by (apply Hag; auto).
destruct (PeanoNat.Nat.eq_dec n' n'); last congruence.
case_decide; last by contradiction.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _,_; iFrame. }
iApply bin_log_related_bool.
+ assert (n n') as Hnn'.
{ intros Hnn. apply Hll. by apply Hag. }
destruct (PeanoNat.Nat.eq_dec n n'); first congruence.
case_decide; first by contradiction.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _,_; iFrame. }
iApply bin_log_related_bool.
......
......@@ -227,12 +227,10 @@ Section refinement.
iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
destruct (decide (n = o)); simplify_eq; rel_op_l.
rel_op_l.
case_decide; subst; rel_if_l.
(* The ticket is called out *)
* replace (if PeanoNat.Nat.eq_dec o o then LitV true else LitV false) with #true; last first.
{ (* TODO :( *) case_match; congruence. }
rel_if_l.
unlock lock.acquire.
* unlock lock.acquire.
rel_rec_r.
destruct b.
{ iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
......@@ -243,10 +241,7 @@ Section refinement.
iApply "Hpool". iExists _,_,_; by iFrame. }
iApply bin_log_related_unit.
* replace (if PeanoNat.Nat.eq_dec n o then LitV true else LitV false) with #false; last first.
{ (* TODO :( *) case_match; congruence. }
rel_if_l.
iMod ("Hcl" with "[-Hticket]") as "_".
* iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
rel_rec_l.
......
......@@ -282,8 +282,7 @@ Section masked.
rel_op_l; eauto.
rel_op_r; eauto.
value_case.
destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; eauto.
destruct op; simpl in Hopv'; simplify_eq/=; try case_match; eauto.
Qed.
Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment