QRewrite is now obsolete. It was containing manual ltac stuff

for helping rewriting under Quantifiers and binders, but Matthieu's
setoid rewrite now has the same kind of capabilities by default. 



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

2 files changed, 1 insertions, 196 deletions

diff --git a/Makefile.common b/Makefile.common
index d821373097..c7b7559e94 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -651,7 +651,7 @@ REALSVO:=$(REALSBASEVO) $(REALS_$(REALS))
 ALLREALS:=$(REALSBASEVO) $(REALS_all)
 
 NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \
- QRewrite.vo	NumPrelude.vo	BigNumPrelude.vo )
+ NumPrelude.vo	BigNumPrelude.vo )
 
 CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \
  CyclicAxioms.vo NZCyclic.vo )
diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v
deleted file mode 100644
index 49e0b3e787..0000000000
--- a/theories/Numbers/QRewrite.v
+++ /dev/null
@@ -1,195 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Import List.
-Require Import Setoid.
-
-(** An attempt to extend setoid rewrite to formulas with quantifiers *)
-
-(* The following algorithm was explained to me by Bruno Barras.
-
-In the future, we need to prove that some predicates are
-well-defined w.r.t. a setoid relation, i.e., we need to prove theorems
-of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it
-makes sense to do induction only on predicates P that satisfy this
-property. Ideally, such goal should be proved by saying "intros x y H;
-rewrite H; reflexivity".
-
-Such predicates P may contain quantifiers besides setoid morphisms.
-Unfortunately, the tactic "rewrite" (which in this case stands for
-"setoid_rewrite") currently cannot handle universal quantifiers as well
-as lambda abstractions, which are part of the existential quantifier
-notation (recall that "exists x, P" stands for "ex (fun x => p)").
-
-Therefore, to prove that P x <-> P y, we proceed as follows. Suppose
-that P x is C[forall z, A[x,z]] where C is a context, i.e., a term with
-a hole. We assume that the hole of C does not occur inside another
-quantifier, i.e., that forall z, A[x,z] is a top-level quantifier in P.
-The notation A[x,z] means that x and z occur freely in A. We prove that
-forall z, A[x,z] <-> forall z, A[y,z]. To do this, we show that
-forall z, A[x,z] <-> A[y,z]. After performing "intro z", this goal is
-handled recursively, until no more quantifiers are left in A.
-
-After we obtain the goal
-
-H : x == y
-H1 : forall z, A[x,z] <-> forall z, A[y,z]
-=================================
-C[forall z, A[x,z]] <-> C[forall z, A[y,z]]
-
-we say "rewrite H1". The tactic setoid_rewrite can handle this because
-"forall z" is a top-level quantifier. Repeating this for other
-quantifier subformulas in P, we make them all identical in P x and P y.
-After that, saying "rewrite H" solves the goal.
-
-The job of deriving P x <-> P y from x == y is done by the tactic
-qmorphism x y below. *)
-
-Section Quantifiers.
-
-Variable A : Set.
-
-Theorem exists_morph : forall P1 P2 : A -> Prop,
-  (forall x : A, P1 x <-> P2 x) -> (ex P1 <-> ex P2).
-Proof.
-(intros P1 P2 H; split; intro H1; destruct H1 as [x H1];
-exists x); [now rewrite <- H | now rewrite H].
-Qed.
-
-Theorem forall_morph : forall P1 P2 : A -> Prop,
-  (forall x : A, P1 x <-> P2 x) -> ((forall x : A, P1 x) <-> (forall x : A, P2 x)).
-Proof.
-(intros P1 P2 H; split; intros H1 x); [now apply -> H | now apply <- H].
-Qed.
-
-End Quantifiers.
-
-(* replace x by y in t *)
-Ltac repl x y t :=
-match t with
-| context C [x] => let t' := (context C [y]) in repl x y t'
-| _ => t
-end.
-
-(* The tactic qiff x y H solves the goal P[x] <-> P[y] from H : E x y
-where E is a registered setoid relation, P may contain quantifiers,
-and x and y are arbitrary terms *)
-Ltac qiff x y H :=
-match goal with
-| |- ?P <-> ?P => reflexivity
-(* The clause above is needed because if the goal is trivial, i.e., x
-and y do not occur in P, "setoid_replace x with y" below would produce
-an error. *)
-| |- context [ex ?P] =>
-  lazymatch P with
-  | context [x] =>
-    let P' := repl x y P in
-      setoid_replace (ex P) with (ex P') using relation iff;
-      [qiff x y H | apply exists_morph; intro; qiff x y H]
-  end
-| |- context [forall z, @?P z] =>
-  lazymatch P with
-  | context [x] =>
-    let P' := repl x y P in
-      setoid_replace (forall z, P z) with (forall z, P' z) using relation iff;
-      [qiff x y H | apply forall_morph; intro; qiff x y H]
-  end
-| _ => setoid_rewrite H; reflexivity
-end.
-
-Ltac qsetoid_rewrite H :=
-lazymatch (type of H) with
-| ?E ?t1 ?t2 =>
-  lazymatch goal with
-  | |- (fun x => @?G x) t1 =>
-    let H1 := fresh in
-    let H2 := fresh in
-    let x1 := fresh "x" in
-    let x2 := fresh "x" in
-    set (x1 := t1); set (x2 := t2);
-    assert (H1 : E x1 x2) by apply H;
-    assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2) by qiff x1 x2 H1;
-    unfold x1 in *; unfold x2 in *; apply <- H2;
-    clear H1 H2 x1 x2
-  | _ => pattern t1; qsetoid_rewrite H
-  end
-| _ => fail "The type of" H "does not have the form (E t1 t2)"
-end.
-
-Tactic Notation "qsetoid_rewrite" "<-" constr(H) :=
-match goal with
-| |- ?G =>
-  let H1 := fresh in
-    pose proof H as H1;
-    symmetry in H1; (* symmetry unfolds the beta-redex in the goal (!), so we have to restore the goal *)
-    change G;
-    qsetoid_rewrite H1;
-    clear H1
-end.
-
-Tactic Notation "qsetoid_replace" constr(t1) "with" constr(t2)
-                "using" "relation" constr(E) :=
-let H := fresh in
-lazymatch goal with
-| |- ?G =>
-  cut (E t1 t2); [intro H; change G; qsetoid_rewrite H; clear H |]
-end.
-
-(* For testing *)
-
-(*Parameter E : nat -> nat -> Prop.
-Axiom eq_equiv : equiv nat E.
-
-Add Relation nat E
- reflexivity proved by (proj1 eq_equiv)
- symmetry proved by (proj2 (proj2 eq_equiv))
- transitivity proved by (proj1 (proj2 eq_equiv))
-as eq_rel.
-
-Notation "x == y" := (E x y) (at level 70).
-
-Parameter P : nat -> nat.
-Add Morphism S with signature E ==> E as S_morph. Admitted.
-Add Morphism P with signature E ==> E as P_morph. Admitted.
-Add Morphism plus with signature E ==> E ==> E as plus_morph. Admitted.
-
-Theorem Zplus_pred : forall n m : nat, P n + m == P (n + m).
-Proof.
-intros n m.
-cut (forall n : nat, S (P n) == n). intro H.
-pattern n at 2.
-qsetoid_rewrite <- (H n).
-Admitted.
-
-Goal forall x, x == x + x ->
-  (exists y, forall z, y == y + z -> exists u, x == u) /\ x == 0.
-intros x H1. pattern x at 1.
-qsetoid_rewrite H1. qsetoid_rewrite <- H1.
-Admitted.*)
-
-(* For the extension that deals with multiple equalities. The idea is
-to give qiff a list of hypothesis instead of just one H. *)
-
-(*Inductive EqList : Type :=
-| eqnil : EqList
-| eqcons : forall A : Prop, A -> EqList -> EqList.
-
-Implicit Arguments eqcons [A].
-
-Ltac ra L :=
-lazymatch L with
-| eqnil => reflexivity
-| eqcons ?H ?T => rewrite H; ra T
-end.
-
-ra (eqcons H0 (eqcons H1 eqnil)).*)
-