From 2fd45fa939ddae7cdb31ee0495e622e6e6a6235f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 20 Feb 2019 09:55:19 +0000
Subject: 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.

---
 lib/coq/Sail2_values.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib/coq/Sail2_values.v')

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.
-- 
cgit v1.2.3


From 3e59f95ce23e24c5ccfa9e0475f0a3d4a070e318 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 28 Feb 2019 17:04:31 +0000
Subject: Coq: remove unused library definitions

---
 lib/coq/Sail2_values.v | 35 -----------------------------------
 1 file changed, 35 deletions(-)

(limited to 'lib/coq/Sail2_values.v')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index bd2c0fdb..1b5da853 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -45,35 +45,6 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
-(* The informative boolean type. *)
-
-Definition Bool (P : Prop) : Type := {P} + {~P}.
-
-Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P.
-refine (if sumbool_of_bool b then left _ else right _);
-destruct H; subst;
-intuition.
-Defined.
-
-Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false.
-
-Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P.
-destruct b; simpl; intuition.
-Qed.
-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.
@@ -1123,11 +1094,6 @@ Ltac extract_properties :=
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
     change (projT1 (existT _ x Hx)) with x in * end.
-(* We could also destruct any remaining Bools, if necessary. *)
-Ltac extract_Bool_props :=
-  repeat match goal with
-  | H:projBool _ = true |- _ => rewrite projBool_true in H
-  | H:projBool _ = false |- _ => rewrite projBool_false in H end.
 (* TODO: hyps, too? *)
 Ltac reduce_list_lengths :=
   repeat match goal with |- context [length_list ?X] => 
@@ -1193,7 +1159,6 @@ Ltac prepare_for_solver :=
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
  split_cases;
  extract_properties;
- extract_Bool_props;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  destruct_exists;
-- 
cgit v1.2.3


From 576fb915bc281ea8e59eba896e3404d2f85e918c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Mar 2019 10:41:33 +0000
Subject: Coq: add a little bit of boolean solving Just enough for RISC-V to go
 through

---
 lib/coq/Sail2_values.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib/coq/Sail2_values.v')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 1b5da853..e6c5e786 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1208,6 +1208,14 @@ prepare_for_solver;
  | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
+   (* Booleans - and_boolMP *)
+ | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => 
+     constructor; intros l r H1 H2;
+     solve [exists l; destruct l; intuition | exists r; destruct l; intuition]
+   end
+ | match goal with |- context [@eq _ _ _] =>
+     constructor; intuition
+   end
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get
-- 
cgit v1.2.3