From 15c368d501c2ad9eb1fcbf49fb3f935c8bf0cd2a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 20:51:56 +0100
Subject: [PATCH] Remove sum2bool.

---
 heap_lang/heap_lang.v | 13 +++----------
 heap_lang/sugar.v     |  6 +++---
 2 files changed, 6 insertions(+), 13 deletions(-)

diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index f9660593d..99cfccfd2 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -135,20 +135,13 @@ Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
   | _, _ => None
   end.
 
-(* FIXME RJ I am *sure* this already exists somewhere... but I can't find it. *)
-Definition sum2bool {A B} (x : { A } + { B }) : bool :=
-  match x with
-  | left _ => true
-  | right _ => false
-  end.
-
 Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   match op, l1, l2 with
   | PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2)
   | MinusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 - n2)
-  | LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 ≤ n2)
-  | LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 < n2)
-  | EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 = n2)
+  | LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 ≤ n2)
+  | LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2)
+  | EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2)
   | _, _, _ => None
   end.
 
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index d2f4d46e6..98555157f 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -101,7 +101,7 @@ Lemma wp_le E (n1 n2 : nat) P Q :
   P ⊑ wp E (BinOp LeOp (Lit n1) (Lit n2)) Q.
 Proof.
   intros ? ?. rewrite -wp_bin_op //; [].
-  destruct (decide _); by eauto with omega.
+  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
 Qed.
 
 Lemma wp_lt E (n1 n2 : nat) P Q :
@@ -110,7 +110,7 @@ Lemma wp_lt E (n1 n2 : nat) P Q :
   P ⊑ wp E (BinOp LtOp (Lit n1) (Lit n2)) Q.
 Proof.
   intros ? ?. rewrite -wp_bin_op //; [].
-  destruct (decide _); by eauto with omega.
+  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
 Qed.
 
 Lemma wp_eq E (n1 n2 : nat) P Q :
@@ -119,7 +119,7 @@ Lemma wp_eq E (n1 n2 : nat) P Q :
   P ⊑ wp E (BinOp EqOp (Lit n1) (Lit n2)) Q.
 Proof.
   intros ? ?. rewrite -wp_bin_op //; [].
-  destruct (decide _); by eauto with omega.
+  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
 Qed.
 
 End suger.
-- 
GitLab