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, 176 insertions, 29 deletions

diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 27f31bf83..d9fb4e97c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinPos.
@@ -17,6 +17,7 @@ Require Import Zcompare.
 Require Import Zorder.
 Require Import Decidable.
 Require Import Peano_dec.
+Require Import Min Max Zmin Zmax.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
@@ -26,6 +27,8 @@ Definition neq (x y:nat) := x <> y.
 (************************************************)
 (** Properties of the injection from nat into Z *)
 
+(** Injection and successor *)
+
 Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
   intro y; induction y as [| n H];
@@ -33,25 +36,12 @@ Proof.
       | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
 	rewrite Zpos_succ_morphism; trivial with arith ].
 Qed.
- 
-Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
-Proof.
-  intro x; induction x as [| n H]; intro y; destruct y as [| m];
-    [ simpl in |- *; trivial with arith
-      | simpl in |- *; trivial with arith
-      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
-      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
-	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
-	  trivial with arith ].
-Qed.
 
-Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+(** Injection and equality. *)
+
+Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H];
-    [ simpl in |- *; trivial with arith
-      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
-	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
-	  trivial with arith ].
+  intros x y H; rewrite H; trivial with arith.
 Qed.
 
 Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
@@ -66,6 +56,24 @@ Proof.
 	    intros E; rewrite E; auto with arith ].
 Qed. 
 
+Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Proof.
+  intros x y H.
+  destruct (eq_nat_dec x y) as [H'|H']; auto.
+  elimtype False.
+  exact (inj_neq _ _ H' H).
+Qed.
+
+Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
+Proof.
+ split; [apply inj_eq | apply inj_eq_rev].
+Qed.
+
+
+(** Injection and order relations: *)
+
+(** One way ... *)
+
 Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
 Proof.
   intros x y; intros H; elim H;
@@ -81,29 +89,100 @@ Proof.
     exact H.
 Qed.
 
+Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Proof.
+  intros x y H; apply Zle_ge; apply inj_le; apply H.
+Qed.
+
 Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
 Proof.
   intros x y H; apply Zlt_gt; apply inj_lt; exact H.
 Qed.
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+(** The other way ... *)
+
+Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
 Proof.
-  intros x y H; apply Zle_ge; apply inj_le; apply H.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_lt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
 Qed.
 
-Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
+Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
 Proof.
-  intros x y H; rewrite H; trivial with arith.
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_le _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
 Qed.
 
-Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
 Proof.
-  intros x; exists (Z_of_nat x); split;
-    [ trivial with arith
-      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
-	unfold Zle in |- *; elim x; intros; simpl in |- *; 
-          discriminate ].
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_gt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
+Qed.
+
+Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
+Proof.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_ge _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
+Qed.
+
+(* Both ways ... *)
+
+Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
+Proof.
+ split; [apply inj_le | apply inj_le_rev].
+Qed.
+
+Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
+Proof.
+ split; [apply inj_lt | apply inj_lt_rev].
+Qed.
+
+Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
+Proof.
+ split; [apply inj_ge | apply inj_ge_rev].
+Qed.
+
+Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
+Proof.
+ split; [apply inj_gt | apply inj_gt_rev].
+Qed.
+
+(** Injection and usual operations *)
+ 
+Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H]; intro y; destruct y as [| m];
+    [ simpl in |- *; trivial with arith
+      | simpl in |- *; trivial with arith
+      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
+      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
+	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
+	  trivial with arith ].
+Qed.
+
+Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H];
+    [ simpl in |- *; trivial with arith
+      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
+	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
+	  trivial with arith ].
 Qed.
 
 Theorem inj_minus1 :
@@ -121,6 +200,46 @@ Proof.
     [ trivial with arith | apply gt_not_le; assumption ].
 Qed.
 
+Theorem inj_minus : forall n m:nat, 
+ Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
+Proof.
+ intros.
+ rewrite Zmax_comm.
+ unfold Zmax.
+ destruct (le_lt_dec m n) as [H|H].
+
+ rewrite (inj_minus1 _ _ H).
+ assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)).
+ unfold Zle in H'.
+ rewrite <- Zcompare_antisym in H'.
+ destruct Zcompare; simpl in *; intuition.
+
+ rewrite (inj_minus2 _ _ H).
+ assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)).
+ rewrite Zplus_opp_r in H'.
+ unfold Zminus; rewrite H'; auto.
+Qed.
+
+Theorem inj_min : forall n m:nat, 
+  Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl min.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_min_distr; f_equal; auto.
+Qed.
+
+Theorem inj_max : forall n m:nat, 
+  Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl max.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_max_distr; f_equal; auto.
+Qed.
+
+(** Composition of injections **)
+
 Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
   forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
 Proof.
@@ -136,3 +255,31 @@ Proof.
   rewrite inj_plus; repeat rewrite <- H.
   rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
+
+Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
+Proof.
+destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+(** Misc *)
+
+Theorem intro_Z :
+  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+  intros x; exists (Z_of_nat x); split;
+    [ trivial with arith
+      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
+	unfold Zle in |- *; elim x; intros; simpl in |- *; 
+          discriminate ].
+Qed.
+
+Lemma Zpos_P_of_succ_nat : forall n:nat, 
+ Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Proof.
+  intros.
+  unfold Z_of_nat.
+  destruct n.
+  simpl; auto.
+  simpl (P_of_succ_nat (S n)).
+  apply Zpos_succ_morphism.
+Qed.