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.

2 files changed, 24 insertions, 0 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index bd0d7750..dc00fdd3 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -61,6 +61,20 @@ Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad
 Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E :=
  l >>= (fun l => if l then returnm true else r).
 
+Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E.
+refine (
+ l >>= (fun l => if l then r >>= fun r => if r then returnm (left _) else returnm (right _) else returnm (right _))
+).
+all: tauto.
+Defined.
+
+Definition or_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P \/ Q)) E.
+refine (
+ l >>= (fun l => if l then returnm (left _) else r >>= fun r => if r then returnm (left _) else returnm (right _))
+).
+all: tauto.
+Defined.
+
 (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E :=
 match b with
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.