From c5f077f5680951fff590082effa0e2843706962e Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Nov 2009 16:43:52 +0000 Subject: Numbers: finish files NStrongRec and NDefOps - NStrongRec provides a "strong" recursor based on the usual one: recursive calls can be done here on any lower value. See binary log in NDefOps for an example of use. - NDefOps contains alternative definitions of usual operators (add, mul, ltb, pow, even, half, log) via usual or strong recursor, and proofs of correctness and/or of equivalence with axiomatized operators. These files were in the archive but not being compiled, some proofs of correction for functions defined there were missing. By the way, some more iff-style lemmas in Bool. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'theories/Bool') 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. -- cgit v1.2.3