1 files changed, 82 insertions, 0 deletions
diff --git a/src/ReflectFacts.v b/src/ReflectFacts.v
new file mode 100644
index 0000000..404ecc8
--- /dev/null
+++ b/src/ReflectFacts.v
@@ -0,0 +1,82 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import
+        Bool ZArith BVList Logic.
+
+Local Coercion is_true : bool >-> Sortclass.
+
+Section ReflectFacts.
+
+Infix "-->" := implb (at level 60, right associativity) : bool_scope.
+
+Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).
+Proof.
+ intros; destruct H; intuition.
+ discriminate H.
+Qed.
+
+Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b.
+Proof.
+ intros.
+ destr_bool; constructor; try now apply H.
+ unfold not. intros. apply H in H0. destruct H. easy.
+Qed.
+
+Lemma reflect_dec : forall P b, reflect P b -> {P} + {~P}.
+Proof. intros; destruct H; [now left | now right]. Qed.
+
+ Lemma implyP : forall (b1 b2: bool), reflect (b1 -> b2) (b1 --> b2).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
+ Qed.
+
+ Lemma iffP : forall (b1 b2: bool), reflect (b1 <-> b2) (eqb b1 b2).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
+ Qed.
+
+ Lemma implyP2 : forall (b1 b2 b3: bool), reflect (b1 -> b2 -> b3) (b1 --> b2 --> b3).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
+ Qed.
+
+ Lemma andP : forall (b1 b2: bool), reflect (b1 /\ b2) (b1 && b2).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
+ Qed.
+
+ Lemma orP : forall (b1 b2: bool), reflect (b1 \/ b2) (b1 || b2).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *.
+        destruct H1 as [H1a | H1b ]; easy. left. easy. left. easy.
+        right. easy.
+ Qed.
+
+ Lemma negP : forall (b: bool), reflect (~ b) (negb b).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b; intros; try easy; try compute in *.
+        contradict H0. easy.
+ Qed.
+
+ Lemma eqP : forall (b1 b2: bool), reflect (b1 = b2) (Bool.eqb b1 b2).
+ Proof. intros; apply iff_reflect; split;
+        case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
+ Qed.
+
+ Lemma FalseB : (false = true) <-> False.
+ Proof. split; auto. discriminate. Qed.
+
+ Lemma TrueB : (true = true) <-> True.
+ Proof. split; auto. Qed.
+
+End ReflectFacts.