From 770a0e7a4b6df754ead90c51334898dec5df4ebc Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 9 Feb 2008 17:22:35 +0000 Subject: Major revision of FSetAVL: more Function, including some non-structural ones NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0d674ebf9..652ac955e 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -308,6 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62. (** * Properties of [andb] *) (*******************************) +Lemma andb_true_iff : + forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; destruct b2; intuition. +Qed. + Lemma andb_true_eq : forall a b:bool, true = a && b -> true = a /\ true = b. Proof. -- cgit v1.2.3