Coq: some work on bool simplification

This introduces some simplification of informative booleans, but tries
too hard to eliminate all of the existentials resulting in difficulties
in and/or trees.

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 943d850a..bd2c0fdb 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -64,6 +64,16 @@ Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P.
 destruct b; simpl; intuition.
 Qed.
 
+Definition and_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P /\ Q).
+refine (if l then if r then left _ else right _ else right _).
+all: tauto.
+Defined.
+
+Definition or_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P \/ Q).
+refine (if l then left _ else if r then left _ else right _).
+all: tauto.
+Defined.
+
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.