decProp

Author: Tragicus

theories/Corelib/ssr/ssrbool.v

@@ -303,6 +303,12 @@ Abbreviation reflect := Datatypes.reflect.
 Abbreviation ReflectT := Datatypes.ReflectT.
 Abbreviation ReflectF := Datatypes.ReflectF.
 
+Structure decProp := DecProp {
+  prop :> Prop;
+  propb :> bool;
+  propbP : reflect prop propb
+  }.
+
 Reserved Notation "~~ b" (at level 35, right associativity).
 Reserved Notation "b ==> c" (at level 55, right associativity).
 Reserved Notation "b1 (+) b2" (at level 50, left associativity).
@@ -649,37 +655,34 @@ End BoolIf.
 
 Section ReflectCore.
 
-Variables (P Q : Prop) (b c : bool).
-
-Hypothesis Hb : reflect P b.
+Variables (P : decProp) (Q : Prop) (b : bool).
 
-Lemma introNTF : (if c then ~ P else P) -> ~~ b = c.
-Proof. by case c; case Hb. Qed.
+Lemma introNTF : (if b then ~ P else P) -> ~~ P = b.
+Proof. by case b; case (propbP P). Qed.
 
-Lemma introTF : (if c then P else ~ P) -> b = c.
-Proof. by case c; case Hb. Qed.
+Lemma introTF : (if b then P : Prop else ~ P) -> P = b :> bool.
+Proof. by case b; case (propbP P). Qed.
 
-Lemma elimNTF : ~~ b = c -> if c then ~ P else P.
-Proof. by move <-; case Hb. Qed.
+Lemma elimNTF : ~~ P = b -> if b then ~ P else P.
+Proof. by move <-; case (propbP P). Qed.
 
-Lemma elimTF : b = c -> if c then P else ~ P.
-Proof. by move <-; case Hb. Qed.
+Lemma elimTF : P = b :> bool -> if b then P : Prop else ~ P.
+Proof. by move <-; case (propbP P). Qed.
 
-Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
-Proof. by case Hb; auto. Qed.
+Lemma equivPif : (Q -> P) -> (P -> Q) -> if P then Q else ~ Q.
+Proof. by case (propbP P); auto. Qed.
 
-Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
-Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed.
+Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if P then ~ Q else Q.
+Proof. by case (propbP P) => [? _ H ? | ? H _]; case: H. Qed.
 
 End ReflectCore.
 
 (**  Internal negated reflection lemmas  **)
 Section ReflectNegCore.
 
-Variables (P Q : Prop) (b c : bool).
-Hypothesis Hb : reflect P (~~ b).
+Variables (P : decProp) (Q : Prop) (b : bool).
 
-Lemma introTFn : (if c then ~ P else P) -> b = c.
+Lemma introTFn : (if ~~ b then ~ P else P) -> P = b :> bool.
 Proof. by move/(introNTF Hb) <-; case b. Qed.
 
 Lemma elimTFn : b = c -> if c then ~ P else P.