- Another bug in get_sort_family_of (sort-polymorphism of constants and

  inductive types was not taken into account).
- Virtually extended tauto to 
  - support arbitrary-length disjunctions and conjunctions,
  - support arbitrary complex forms of disjunctions and
    conjunctions when in the contravariant of an implicative hypothesis,
  - stick with the purely propositional fragment and not apply reflexivity.
  This is virtual in the sense that it is not activated since it breaks 
  compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a 
  way that is closer to the intuitive meaning (forbid dependencies 
  between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
  definition; modified tauto.ml4 so that it works with the current and
  the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.



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

6 files changed, 46 insertions, 51 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 1f8d13973b..4c3b2ff849 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -60,45 +60,38 @@ Hint Resolve lt_div2: arith.
 
 (** Properties related to the parity *)
 
-Lemma even_odd_div2 :
-  forall n,
-    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
+with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
 Proof.
-  intro n. pattern n in |- *. apply ind_0_1_SS.
-  (* n  = 0 *)
-  split. split; auto with arith. 
-  split. intro H. inversion H.
-  intro H.  absurd (S (div2 0) = div2 1); auto with arith.
-  (* n = 1 *)
-  split. split. intro. inversion H. inversion H1.
-  intro H.  absurd (div2 1 = div2 2).
-  simpl in |- *. discriminate. assumption.
-  split; auto with arith.
-  (* n = (S (S n')) *)
-  intros. decompose [and] H. unfold iff in H0, H1.
-  decompose [and] H0. decompose [and] H1. clear H H0 H1.
-  split; split; auto with arith.
-  intro H. inversion H. inversion H1.
-  change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
-  intro H. inversion H. inversion H1.
-  change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
+  destruct n; intro H.
+    (* 0 *) trivial.
+    (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial.
+  destruct n; intro.
+    (* 0 *) inversion H.
+    (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
 Qed.
 
-(** Specializations *)
-
-Lemma even_div2 : forall n, even n -> div2 n = div2 (S n).
-Proof fun n => proj1 (proj1 (even_odd_div2 n)).
+Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
+with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Proof.
+  destruct n; intro H.
+    (* 0 *) constructor.
+    (* S n *) constructor. apply div2_odd. rewrite H. trivial.
+  destruct n; intro H.
+    (* 0 *) discriminate.
+    (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+Qed.
 
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n.
-Proof fun n => proj2 (proj1 (even_odd_div2 n)).
+Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
-Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
-Proof fun n => proj1 (proj2 (even_odd_div2 n)).
+Lemma even_odd_div2 :
+  forall n,
+    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Proof.
+  auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+Qed.
 
-Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
-Proof fun n => proj2 (proj2 (even_odd_div2 n)).
 
-Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
 (** Properties related to the double ([2n]) *)
 
@@ -132,8 +125,7 @@ Proof.
   split; split; auto with arith.
   intro H. inversion H. inversion H1.
   (* n = (S (S n')) *)
-  intros. decompose [and] H. unfold iff in H0, H1.
-  decompose [and] H0. decompose [and] H1. clear H H0 H1.
+  intros. destruct H as ((IH1,IH2),(IH3,IH4)).
   split; split.
   intro H. inversion H. inversion H1.
   simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
@@ -142,8 +134,6 @@ Proof.
   simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
   simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 Qed.
-
-
 (** Specializations *)
 
 Lemma even_double : forall n, even n -> n = double (div2 n).
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 24efa44ef9..7938beda7e 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -30,7 +30,7 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
 
  Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x.
  Proof.
- unfold In; compute; auto.
+ unfold In; compute; auto with extcore.
  Qed.
 
  Lemma Subset_Included : forall s s',  s[<=]s'  <-> Included _ (!!s) (!!s').
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b01b80630b..a91fd0480b 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -150,6 +150,16 @@ Proof.
 intros; tauto.
 Qed.
 
+Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
+Proof.
+intros A B []; split; trivial.
+Qed.
+
+Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
+Proof.
+intros; tauto.
+Qed.
+
 (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
     either [P] and [Q], or [~P] and [Q] *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 0e8b4ab1f0..2e0fe42b68 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -139,18 +139,6 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
     proofs "in one step" *)
 
 Ltac easy :=
-(*
-  let rec use_hyp H :=
-    match type of H with
-    | _ /\ _ => 
-    | _ => solve [inversion H] 
-    end
-  with destruct_hyp H :=
-    match type of H with
-    | _ /\ _ => case H; do_intro; do_intro
-    | _ => idtac
-    end
-*)
   let rec use_hyp H :=
     match type of H with
     | _ /\ _ => exact H || destruct_hyp H
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 6f793ce2fa..6129128de0 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -80,6 +80,13 @@ Proof.
 unfold decidable; tauto.
 Qed.
 
+Theorem not_iff : 
+  forall A B:Prop, decidable A -> decidable B -> 
+    ~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B).
+Proof.
+unfold decidable; tauto.
+Qed.
+
 (** Results formulated with iff, used in FSetDecide. 
     Negation are expanded since it is unclear whether setoid rewrite 
     will always perform conversion. *)    
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index b704f3d378..d9d848f0db 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -393,10 +393,10 @@ Theorem Ncompare_n_Sm :
 Proof.
 intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto.
 destruct p; simpl; intros; discriminate.
-pose proof (proj1 (Pcompare_p_Sq p q));
+pose proof (Pcompare_p_Sq p q) as (?,_).
 assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
 intros H; destruct H; discriminate.
-pose proof (proj2 (Pcompare_p_Sq p q));
+pose proof (Pcompare_p_Sq p q) as (_,?);
 assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
 Qed.