Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.

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

5 files changed, 34 insertions, 91 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 8545429063..4ded2b8928 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -116,7 +116,10 @@ Qed.
 Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m.
 Proof.
 intro n; NZinduct m n.
-rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l.
+setoid_replace (n < n) with False using relation iff by
+  (apply -> neg_false; apply NZlt_irrefl).
+now setoid_replace (S n <= n) with False using relation iff by
+  (apply -> neg_false; apply NZnle_succ_l).
 intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ.
 rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m).
 rewrite or_cancel_r.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 35d929f0c1..d71f98057f 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -163,7 +163,9 @@ Proof.
 cases n.
 rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
 split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
-intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0.
+intro n. rewrite pred_succ.
+setoid_replace (S n == 0) with False using relation iff by
+  (apply -> neg_false; apply neq_succ_0).
 rewrite succ_inj_wd. tauto.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index f7abb82d8b..c109ff904a 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -99,7 +99,7 @@ intros n m p H; rewrite plus_comm in H; now apply plus_minus_eq_l.
 Qed.
 
 (* This could be proved by adding m to both sides. Then the proof would
-use plus_minus_assoc and le_minus_0, which is proven below. *)
+use plus_minus_assoc and minus_0_le, which is proven below. *)
 Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
 Proof.
 intros n m p H; double_induct n m.
@@ -134,12 +134,12 @@ intros m IH. rewrite minus_succ_r.
 apply le_trans with (n - m); [apply le_pred_l | assumption].
 Qed.
 
-Theorem le_minus_0 : forall n m : N, n <= m <-> n - m == 0.
+Theorem minus_0_le : forall n m : N, n - m == 0 <-> n <= m.
 Proof.
 double_induct n m.
-intro m; split; intro; [apply minus_0_l | apply le_0_l].
+intro m; split; intro; [apply le_0_l | apply minus_0_l].
 intro m; rewrite minus_0_r; split; intro H;
-[false_hyp H nle_succ_0 | false_hyp H neq_succ_0].
+[false_hyp H neq_succ_0 | false_hyp H nle_succ_0].
 intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ.
 Qed.
 
@@ -164,8 +164,8 @@ rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
 rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
 now apply <- plus_cancel_l.
 assert (H1 : S n <= m); [now apply -> lt_le_succ |].
-setoid_replace (S n - m) with 0 by now apply -> le_minus_0.
-setoid_replace ((S n * p) - m * p) with 0 by (apply -> le_minus_0; now apply times_le_mono_r).
+setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
+setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply times_le_mono_r).
 apply times_0_l.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 32912a73d6..a033d95a09 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -67,8 +67,10 @@ intros n m; induct n.
 (* The next command does not work with the axiom plus_0_l from NPlusSig *)
 rewrite plus_0_l. intuition reflexivity.
 intros n IH. rewrite plus_succ_l.
-rewrite_false (S (n + m) == 0) neq_succ_0.
-rewrite_false (S n == 0) neq_succ_0. tauto.
+setoid_replace (S (n + m) == 0) with False using relation iff by
+ (apply -> neg_false; apply neq_succ_0).
+setoid_replace (S n == 0) with False using relation iff by
+ (apply -> neg_false; apply neq_succ_0). tauto.
 Qed.
 
 Theorem plus_eq_succ :
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 6633953894..e66bc8ebfc 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -11,7 +11,7 @@
 (*i i*)
 
 Require Export Setoid.
-Require Export Bool.
+(*Require Export Bool.*)
 (* Standard library. Export, not Import, because if a file
 importing the current file wants to use. e.g.,
 Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2,
@@ -31,13 +31,13 @@ Contents:
 
 (** Coercion from bool to Prop *)
 
-Definition eq_bool := (@eq bool).
+(*Definition eq_bool := (@eq bool).*)
 
 (*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*)
 (* This has been added to theories/Datatypes.v *)
-Coercion eq_true : bool >-> Sortclass.
+(*Coercion eq_true : bool >-> Sortclass.*)
 
-Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true.
+(*Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true.
 Proof.
 intro b; split; intro H. now inversion H. now rewrite H.
 Qed.
@@ -72,7 +72,7 @@ now rewrite H.
 destruct b1; destruct b2; simpl; try reflexivity.
 apply -> eq_true_unfold_neg. rewrite H. now intro.
 symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro.
-Qed.
+Qed.*)
 
 (** Extension of the tactics stepl and stepr to make them
 applicable to hypotheses *)
@@ -161,6 +161,9 @@ split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
 intros y H4; apply H3; [now apply <- H | now apply -> H].
 Qed.
 
+(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of
+morhisms and quatifiers *)
+
 Ltac solve_predicate_wd :=
 unfold predicate_wd;
 let x := fresh "x" in
@@ -168,6 +171,9 @@ let y := fresh "y" in
 let H := fresh "H" in
   intros x y H; qiff x y H.
 
+(* solve_relation_wd solves the goal [relation_wd R] for R consisting of
+morhisms and quatifiers *)
+
 Ltac solve_relation_wd :=
 unfold relation_wd, fun2_wd;
 let x1 := fresh "x" in
@@ -179,6 +185,7 @@ let H2 := fresh "H" in
   intros x1 y1 H1 x2 y2 H2;
   qsetoid_rewrite H1;
   qiff x2 y2 H2.
+
 (* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite
 uses qiff to take the formula apart in order to make it quantifier-free,
 and then qiff is called again and takes the formula apart for the second
@@ -191,6 +198,7 @@ We declare it to take the tactic that applies the induction theorem
 and not the induction theorem itself because the tactic may, for
 example, supply additional arguments, as does NZinduct_center in
 NZBase.v *)
+
 Ltac induction_maker n t :=
   try intros until n;
   pattern n; t; clear n;
@@ -244,77 +252,7 @@ Implicit Arguments prod_rel_equiv [A B].
 
 (** Miscellaneous *)
 
-Theorem neg_false : forall P : Prop, ~ P <-> (P <-> False).
-Proof.
-intro P; unfold not; split; intro H; [split; intro H1;
-[apply H; assumption | elim H1] | apply (proj1 H)].
-Qed.
-
-(* This tactic replaces P in the goal with False.
-The goal ~ P should be solvable by "apply H". *)
-Ltac rewrite_false P H :=
-setoid_replace P with False using relation iff;
-[| apply -> neg_false; apply H].
-
-Ltac rewrite_true P H :=
-setoid_replace P with True using relation iff;
-[| split; intro; [constructor | apply H]].
-
-(*Ltac symmetry Eq :=
-lazymatch Eq with
-| ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff;
-  [| split; intro; symmetry; assumption]
-| _ => fail Eq "does not have the form (E t1 t2)"
-end.*)
-(* This does not work because there already is a tactic "symmetry".
-Declaring "symmetry" a tactic notation does not work because it conflicts
-with "symmetry in": it thinks that "in" is a term. *)
-
-Theorem and_cancel_l : forall A B C : Prop,
-  (B -> A) -> (C -> A ) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
-Proof.
-intros; tauto.
-Qed.
-
-Theorem and_cancel_r : forall A B C : Prop,
-  (B -> A) -> (C -> A ) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
-Proof.
-intros; tauto.
-Qed.
-
-Theorem or_cancel_l : forall A B C : Prop,
-  (B -> ~A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
-Proof.
-intros; tauto.
-Qed.
-
-Theorem or_cancel_r : forall A B C : Prop,
-  (B -> ~A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
-Proof.
-intros; tauto.
-Qed.
-
-Theorem or_iff_compat_l : forall A B C : Prop,
-  (B <-> C) -> (A \/ B <-> A \/ C).
-Proof.
-intros; tauto.
-Qed.
-
-Theorem or_iff_compat_r : forall A B C : Prop,
-  (B <-> C) -> (B \/ A <-> C \/ A).
-Proof.
-intros; tauto.
-Qed.
-
-Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
-Proof.
-intros; tauto.
-Qed.
-
-Declare Left Step iff_stepl.
-Declare Right Step iff_trans.
-
-Definition comp_bool (x y : comparison) : bool :=
+(*Definition comp_bool (x y : comparison) : bool :=
 match x, y with
 | Lt, Lt => true
 | Eq, Eq => true
@@ -326,13 +264,11 @@ Theorem comp_bool_correct : forall x y : comparison,
   comp_bool x y <-> x = y.
 Proof.
 destruct x; destruct y; simpl; split; now intro.
-Qed.
-
-Definition LE_Set : forall A : Set, relation A := (@eq).
+Qed.*)
 
-Lemma eq_equiv : forall A : Set, equiv A (@LE_Set A).
+Lemma eq_equiv : forall A : Set, equiv A (@eq A).
 Proof.
-intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive.
+intro A; unfold equiv, reflexive, symmetric, transitive.
 repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
 (* It is interesting how the tactic split proves reflexivity *)
 Qed.