Added the automatic generation of the boolean equality if possible and the

decidability of the usual equality
Major changes:
 * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v 
 * added 2 files:
    * toplevel/ind_tables.ml* : tables where the boolean eqs and the
        decidability proofs are stored
    * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically
        generated from inductives types (currently boolean eq & decidability )
 * improvement of injection: if the decidability have been correctly computed,
   injection can now break the equalities over dependant pair

How to use:
 Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
 Scheme Equality for I. tries to create the equality for the already declared
type I




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 912192b26..3525908ab 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -51,6 +51,23 @@ Definition negb (b:bool) := if b then false else true.
 Infix "||" := orb (at level 50, left associativity) : bool_scope.
 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
 
+(*******************************)
+(** * Properties of [andb]     *)
+(*******************************)
+
+Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
+Proof.
+  destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+Qed.
+Hint Resolve andb_prop: bool v62.
+
+Lemma andb_true_intro :
+  forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+Hint Resolve andb_true_intro: bool v62.
+
 (** Interpretation of booleans as propositions *)
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.