diff options
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | theories/Numbers/QRewrite.v | 195 |
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)).*) - |