A generic preprocessing tactic zify for (r)omega

------------------------------------------------ 

See file PreOmega for more details and/or test-suite/succes/*Omega*.v

The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.

Integration with omega and romega:
 (r)omega : the earlier tactics, 100% compatible 
 (r)omega with * : full zify applied before the (r)omega run
 (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, 
   applies only specific parts of zify (btw "with Z" means take advantage 
   of Zmax, Zmin, Zabs and Zsgn). 

As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it. 

For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.

Even though zify is designed to help (r)omega, I think it might be 
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet. 


Side-effects: 

- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated, 
  and this operation will be justified by means of decidability, it helps
  to have as little as possible in the conclusion. 






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

1 files changed, 127 insertions, 0 deletions

diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
new file mode 100644
index 000000000..550edca50
--- /dev/null
+++ b/test-suite/success/ROmegaPre.v
@@ -0,0 +1,127 @@
+Require Import ZArith Nnat ROmega.
+Open Scope Z_scope.
+
+(** Test of the zify preprocessor for (R)Omega *)
+
+(* More details in file PreOmega.v
+ 
+   (r)omega with Z        : starts with zify_op
+   (r)omega with nat      : starts with zify_nat
+   (r)omega with positive : starts with zify_positive
+   (r)omega with N        : starts with uses zify_N
+   (r)omega with *        : starts zify (a saturation of the others)
+*)
+
+(* zify_op *)
+
+Goal forall a:Z, Zmax a a = a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b = Zmax b a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+intros.
+zify.
+intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
+Qed.
+
+Goal forall a:Z, Zabs a = a -> a >= 0.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+intros.
+romega with *.
+Qed.
+
+(* zify_nat *)
+
+Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
+intros.
+romega with *.
+Qed.
+(* 2000 instead of 200: works, but quite slow *)
+
+Goal forall m: nat, (m*m>=0)%nat.
+intros.
+romega with *.
+Qed.
+
+(* zify_positive *)
+
+Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m*m>=1)%positive.
+intros.
+romega with *.
+Qed.
+
+(* zify_N *)
+
+Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<1)%N -> (m=0)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m*m>=0)%N.
+intros.
+romega with *.
+Qed.
+
+(* mix of datatypes *)
+
+Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+intros.
+romega with *.
+Qed.
+
+