diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index bc42c6564..66ab6f1c8 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -54,21 +54,22 @@ Qed. Lemma not_true_is_false : forall b:bool, b <> true -> b = false. Proof. - destruct b. - intros. - red in H; elim H. - reflexivity. - intros abs. - reflexivity. + destruct b; intuition. Qed. Lemma not_false_is_true : forall b:bool, b <> false -> b = true. Proof. - destruct b. - intros. - reflexivity. - intro H; red in H; elim H. - reflexivity. + destruct b; intuition. +Qed. + +Lemma not_true_iff_false : forall b, b <> true <-> b = false. +Proof. + destruct b; intuition. +Qed. + +Lemma not_false_iff_true : forall b, b <> false <-> b = true. +Proof. + destruct b; intuition. Qed. (**********************) @@ -547,6 +548,13 @@ Proof. intros b1 b2; case b1; case b2; intuition. Qed. +Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true). +Proof. + split. + intros; subst; intuition. + apply eq_true_iff_eq. +Qed. + Notation bool_1 := eq_true_iff_eq (only parsing). (* Compatibility *) Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true. |