Update on theories/Numbers

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

2 files changed, 287 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v
new file mode 100644
index 0000000000..5c6e50c1db
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v
@@ -0,0 +1,114 @@
+Require Import NPlusOrder.
+Require Export ZPlusOrder.
+Require Export ZPairsPlus.
+
+Module NatPairsOrder (Import NPlusMod : NPlusSig)
+                     (Import NOrderModule : NOrderSig
+                        with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature.
+Module Import NPlusOrderPropertiesModule :=
+  NPlusOrderProperties NPlusMod NOrderModule.
+Module Export IntModule := NatPairsInt NPlusMod.
+Open Local Scope NatScope.
+
+Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1).
+Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1).
+
+Notation "x < y" := (lt x y) : IntScope.
+Notation "x <= y" := (le x y) : IntScope.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff; split; intro H.
+stepr (snd y1 + fst y2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption].
+stepl (snd y2 + fst x1) by apply plus_comm.
+stepr (fst y2 + snd x1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd x2) (fst x2)).
+now stepl (fst x1 + snd x2) by apply plus_comm.
+stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm.
+stepr (snd x1 + fst x2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry].
+stepl (snd x2 + fst y1) by apply plus_comm.
+stepr (fst x2 + snd y1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd y2) (fst y2)).
+now stepl (fst y1 + snd y2) by apply plus_comm.
+stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm.
+Qed.
+
+(* Below is a very long explanation why it would be useful to be
+able to use the fold tactic in hypotheses.
+We will prove the following statement not from scratch, like lt_wd,
+but expanding <= to < and == and then using lt_wd. The theorem we need
+to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z.
+To be able to express <= through < and ==, we need to expand <=%Int to
+<=%Nat, since we have not proved yet the properties of <=%Int. But
+then it would be convenient to fold back equalities from
+(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int.
+The reason is that we will need to show that (x1 == x2)%Int <->
+(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold
+equalities back to Int, then we could do simple rewriting, since we have
+already showed that ==%Int is an equivalence relation. On the other hand,
+if we leave equalities expanded to Nat, we will have to apply the
+transitivity of ==%Int by hand. *)
+
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff. do 2 rewrite le_lt.
+pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H.
+(* This is a remark about an extra level of definitions created by
+"with Module NBaseMod := NPlusMod.NBaseMod" constraint in the beginning
+of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
+that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since
+NPlusMod was imported first. On the other hand, the goal uses
+NOrderModule.NBaseMod.NDomainModule.E, or just NDomainModule.E, since le_lt
+theorem was proved in NOrderDomain module. (E without qualifiers refers to
+ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer,
+though, if the constraint "with Module NBaseMod := NPlusMod.NBaseMod" in the
+declaration of this functor would not create an extra level of definitions
+and there would be only one NDomainModule.E. *)
+replace NDomainModule.E with NPlusMod.NBaseMod.NDomainModule.E by reflexivity.
+fold (x1 == x2)%Int. fold (y1 == y2)%Int.
+assert (H1' : (x1 == y1)%Int); [exact H1 |].
+(* We do this instead of "fold (x1 == y1)%Int in H1" *)
+assert (H2' : (x2 == y2)%Int); [exact H2 |].
+rewrite H1'; rewrite H2'. reflexivity.
+Qed.
+
+Open Local Scope IntScope.
+
+Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *)
+Qed.
+
+Theorem lt_irr : forall n : Z, ~ (n < n).
+Proof.
+intros n; unfold lt, E; simpl. apply lt_irr.
+(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *)
+Qed.
+
+Theorem lt_S : forall n m, n < (S m) <-> n <= m.
+Proof.
+intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S.
+Qed.
+
+End NatPairsOrder.
+
+(* Since to define the order on integers we need both plus and order
+on natural numbers, we can export the properties of plus and order together *)
+Module NatPairsPlusOrderProperties (NPlusMod : NPlusSig)
+                                   (NOrderModule : NOrderSig
+                                     with Module NBaseMod := NPlusMod.NBaseMod).
+Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
+Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule.
+Module Export NatPairsPlusOrderPropertiesModule :=
+  ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
+End NatPairsPlusOrderProperties.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/QRewrite1.v b/theories/Numbers/QRewrite1.v
new file mode 100644
index 0000000000..a781411a29
--- /dev/null
+++ b/theories/Numbers/QRewrite1.v
@@ -0,0 +1,173 @@
+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); [apply H |];
+    assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2); [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) :=
+let H1 := fresh in
+  pose proof H as H1;
+  symmetry in H1;
+  qsetoid_rewrite H1;
+  clear H1.
+
+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 E_equiv : equiv nat E.
+
+Add Relation nat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Add Morphism plus with signature E ==> E ==> E as plus_morph. 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)).*)
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)