Commit 15c368d5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove sum2bool.

parent 0c801b09
...@@ -135,20 +135,13 @@ Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit := ...@@ -135,20 +135,13 @@ Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
| _, _ => None | _, _ => None
end. 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 := Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with match op, l1, l2 with
| PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2) | PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2)
| MinusOp, 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) | LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 n2)
| LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 < n2) | LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 = n2) | EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2)
| _, _, _ => None | _, _, _ => None
end. end.
......
...@@ -101,7 +101,7 @@ Lemma wp_le E (n1 n2 : nat) P Q : ...@@ -101,7 +101,7 @@ Lemma wp_le E (n1 n2 : nat) P Q :
P wp E (BinOp LeOp (Lit n1) (Lit n2)) Q. P wp E (BinOp LeOp (Lit n1) (Lit n2)) Q.
Proof. Proof.
intros ? ?. rewrite -wp_bin_op //; []. intros ? ?. rewrite -wp_bin_op //; [].
destruct (decide _); by eauto with omega. destruct (bool_decide_reflect (n1 n2)); by eauto with omega.
Qed. Qed.
Lemma wp_lt E (n1 n2 : nat) P Q : Lemma wp_lt E (n1 n2 : nat) P Q :
...@@ -110,7 +110,7 @@ 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. P wp E (BinOp LtOp (Lit n1) (Lit n2)) Q.
Proof. Proof.
intros ? ?. rewrite -wp_bin_op //; []. intros ? ?. rewrite -wp_bin_op //; [].
destruct (decide _); by eauto with omega. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed. Qed.
Lemma wp_eq E (n1 n2 : nat) P Q : Lemma wp_eq E (n1 n2 : nat) P Q :
...@@ -119,7 +119,7 @@ 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. P wp E (BinOp EqOp (Lit n1) (Lit n2)) Q.
Proof. Proof.
intros ? ?. rewrite -wp_bin_op //; []. intros ? ?. rewrite -wp_bin_op //; [].
destruct (decide _); by eauto with omega. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
Qed. Qed.
End suger. End suger.
Supports Markdown
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