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

1 files changed, 17 insertions, 81 deletions

diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 663395389..e66bc8ebf 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.