diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-09 17:22:35 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-09 17:22:35 +0000 |
| commit | 770a0e7a4b6df754ead90c51334898dec5df4ebc (patch) | |
| tree | 2cb6af4fd6bee72c2992220def3427beb6056773 /theories/Bool | |
| parent | bd8b71db33fb9e40575713bc58ae39ccf9f68ab7 (diff) | |
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
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 6 |
1 files changed, 6 insertions, 0 deletions
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. |