diff options
Diffstat (limited to 'plugins/omega/OmegaLemmas.v')
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 269 |
1 files changed, 117 insertions, 152 deletions
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index ec9faedd..1872f576 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -6,234 +6,192 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: OmegaLemmas.v 12337 2009-09-17 15:58:14Z glondu $ i*) - -Require Import ZArith_base. -Open Local Scope Z_scope. +Require Import BinInt Znat. +Local Open Scope Z_scope. (** Factorization lemmas *) -Theorem Zred_factor0 : forall n:Z, n = n * 1. - intro x; rewrite (Zmult_1_r x); reflexivity. +Theorem Zred_factor0 n : n = n * 1. +Proof. + now Z.nzsimpl. Qed. -Theorem Zred_factor1 : forall n:Z, n + n = n * 2. +Theorem Zred_factor1 n : n + n = n * 2. Proof. - exact Zplus_diag_eq_mult_2. + rewrite Z.mul_comm. apply Z.add_diag. Qed. -Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m). +Theorem Zred_factor2 n m : n + n * m = n * (1 + m). Proof. - intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; trivial with arith. + rewrite Z.mul_add_distr_l; now Z.nzsimpl. Qed. -Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). +Theorem Zred_factor3 n m : n * m + n = n * (1 + m). Proof. - intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; - trivial with arith. + now Z.nzsimpl. Qed. -Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p). +Theorem Zred_factor4 n m p : n * m + n * p = n * (m + p). Proof. - intros x y z; symmetry in |- *; apply Zmult_plus_distr_r. + symmetry; apply Z.mul_add_distr_l. Qed. -Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m. +Theorem Zred_factor5 n m : n * 0 + m = m. Proof. - intros x y; rewrite <- Zmult_0_r_reverse; auto with arith. + now Z.nzsimpl. Qed. -Theorem Zred_factor6 : forall n:Z, n = n + 0. +Theorem Zred_factor6 n : n = n + 0. Proof. - intro; rewrite Zplus_0_r; trivial with arith. + now Z.nzsimpl. Qed. (** Other specific variants of theorems dedicated for the Omega tactic *) Lemma new_var : forall x : Z, exists y : Z, x = y. -intros x; exists x; trivial with arith. +Proof. +intros x; now exists x. Qed. -Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y. -intros x y H; rewrite H; auto with arith. +Lemma OMEGA1 x y : x = y -> 0 <= x -> 0 <= y. +Proof. +now intros ->. Qed. -Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y. -exact Zplus_le_0_compat. +Lemma OMEGA2 x y : 0 <= x -> 0 <= y -> 0 <= x + y. +Proof. +Z.order_pos. Qed. -Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0. - -intros x y k H1 H2 H3; apply (Zmult_integral_l k); - [ unfold not in |- *; intros H4; absurd (k > 0); - [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate - | assumption ] - | rewrite <- H2; assumption ]. +Lemma OMEGA3 x y k : k > 0 -> x = y * k -> x = 0 -> y = 0. +Proof. +intros LT -> EQ. apply Z.mul_eq_0 in EQ. destruct EQ; now subst. Qed. -Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0. - -unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0); - [ intros H4; cut (0 <= z * y + x); - [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6; - absurd (z * y + x > 0); - [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate - | apply Zle_gt_trans with x; - [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x); - apply Zplus_le_compat_r; rewrite Zmult_comm; - generalize H4; unfold Zgt in |- *; case y; - [ simpl in |- *; intros H7; discriminate H7 - | intros p H7; rewrite <- (Zmult_0_r (Zpos p)); - unfold Zle in |- *; rewrite Zcompare_mult_compat; - exact H6 - | simpl in |- *; intros p H7; discriminate H7 ] - | assumption ] ] - | rewrite H3; unfold Zle in |- *; simpl in |- *; discriminate ] - | apply Zgt_trans with x; [ assumption | assumption ] ]. +Lemma OMEGA4 x y z : x > 0 -> y > x -> z * y + x <> 0. +Proof. +Z.swap_greater. intros Hx Hxy. +rewrite Z.add_move_0_l, <- Z.mul_opp_l. +destruct (Z.lt_trichotomy (-z) 1) as [LT|[->|GT]]. +- intro. revert LT. apply Z.le_ngt, (Z.le_succ_l 0). + apply Z.mul_pos_cancel_r with y; Z.order. +- Z.nzsimpl. Z.order. +- rewrite (Z.mul_lt_mono_pos_r y), Z.mul_1_l in GT; Z.order. Qed. -Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0. - -intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith. +Lemma OMEGA5 x y z : x = 0 -> y = 0 -> x + y * z = 0. +Proof. +now intros -> ->. Qed. -Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z. - -intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption. +Lemma OMEGA6 x y z : 0 <= x -> y = 0 -> 0 <= x + y * z. +Proof. +intros H ->. now Z.nzsimpl. Qed. -Lemma OMEGA7 : - forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t. - -intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat; - apply Zmult_gt_0_le_0_compat; assumption. +Lemma OMEGA7 x y z t : + z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t. +Proof. +intros. Z.swap_greater. Z.order_pos. Qed. -Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0. - -intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1); - [ intros H4; absurd (0 < x); - [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y; - rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r; - assumption - | assumption ] - | intros H4; rewrite H4; trivial with arith ]. +Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0. +Proof. +intros H1 H2 H3. rewrite <- Z.opp_nonpos_nonneg in H2. Z.order. Qed. -Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0. - -intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l; - rewrite Zplus_0_r; assumption. +Lemma OMEGA9 x y z t : y = 0 -> x = z -> y + (- x + z) * t = 0. +Proof. +intros. subst. now rewrite Z.add_opp_diag_l. Qed. -Lemma OMEGA10 : - forall v c1 c2 l1 l2 k1 k2 : Z, +Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 : (v * c1 + l1) * k1 + (v * c2 + l2) * k2 = v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2). - -intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; - rewrite (Zplus_permute (l1 * k1) (v * c2 * k2)); trivial with arith. +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +rewrite <- !Z.add_assoc. f_equal. apply Z.add_shuffle3. Qed. -Lemma OMEGA11 : - forall v1 c1 l1 l2 k1 : Z, +Lemma OMEGA11 v1 c1 l1 l2 k1 : (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2). - -intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; - trivial with arith. +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +now rewrite Z.add_assoc. Qed. -Lemma OMEGA12 : - forall v2 c2 l1 l2 k2 : Z, +Lemma OMEGA12 v2 c2 l1 l2 k2 : l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2). - -intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; - rewrite Zplus_permute; trivial with arith. +Proof. +rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. +apply Z.add_shuffle3. Qed. -Lemma OMEGA13 : - forall (v l1 l2 : Z) (x : positive), +Lemma OMEGA13 (v l1 l2 : Z) (x : positive) : v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2. - -intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1); - rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r; - rewrite <- Zopp_neg; rewrite (Zplus_comm (- Zneg x) (Zneg x)); - rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r; - trivial with arith. +Proof. + rewrite Z.add_shuffle1. + rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r. + now Z.nzsimpl. Qed. -Lemma OMEGA14 : - forall (v l1 l2 : Z) (x : positive), +Lemma OMEGA14 (v l1 l2 : Z) (x : positive) : v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2. - -intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1); - rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r; - rewrite <- Zopp_neg; rewrite Zplus_opp_r; rewrite Zmult_0_r; - rewrite Zplus_0_r; trivial with arith. +Proof. + rewrite Z.add_shuffle1. + rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r. + now Z.nzsimpl. Qed. -Lemma OMEGA15 : - forall v c1 c2 l1 l2 k2 : Z, - v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2). -intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; - rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith. +Lemma OMEGA15 v c1 c2 l1 l2 k2 : + v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2). +Proof. + rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. + apply Z.add_shuffle1. Qed. -Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k. - -intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r; - repeat rewrite Zmult_assoc; repeat elim Zplus_assoc; - trivial with arith. +Lemma OMEGA16 v c l k : (v * c + l) * k = v * (c * k) + l * k. +Proof. + now rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc. Qed. -Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0. - -unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; - apply Zplus_reg_l with (y * z); rewrite Zplus_comm; - rewrite H3; rewrite H2; auto with arith. +Lemma OMEGA17 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0. +Proof. + unfold Zne, not. intros NE EQ. subst. now Z.nzsimpl. Qed. -Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0. - -unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1; - rewrite H3; auto with arith. +Lemma OMEGA18 x y k : x = y * k -> Zne x 0 -> Zne y 0. +Proof. + unfold Zne, not. intros. subst; auto. Qed. -Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1. - -unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x); - [ intros H1; elim Zle_lt_or_eq with (1 := H1); - [ intros H2; left; change (0 <= Zpred x) in |- *; apply Zsucc_le_reg; - rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption - | intros H2; absurd (x = 0); auto with arith ] - | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm; - apply Zle_left; apply Zsucc_le_reg; simpl in |- *; - apply Zlt_le_succ; auto with arith ]. +Lemma OMEGA19 x : Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1. +Proof. + unfold Zne. intros Hx. apply Z.lt_gt_cases in Hx. + destruct Hx as [LT|GT]. + - right. change (-1) with (-(1)). + rewrite Z.mul_opp_r, <- Z.opp_add_distr. Z.nzsimpl. + rewrite Z.opp_nonneg_nonpos. now apply Z.le_succ_l. + - left. now apply Z.lt_le_pred. Qed. -Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0. - -unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3; - simpl in H3; rewrite Zplus_0_r in H3; trivial with arith. +Lemma OMEGA20 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0. +Proof. + unfold Zne, not. intros H1 H2 H3; apply H1; rewrite H2 in H3; + simpl in H3; rewrite Z.add_0_r in H3; trivial with arith. Qed. Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop) - (H : P (y + x)) := eq_ind_r P H (Zplus_comm x y). + (H : P (y + x)) := eq_ind_r P H (Z.add_comm x y). Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop) (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p). Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop) - (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p). + (H : P (n + m + p)) := eq_ind_r P H (Z.add_assoc n m p). Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop) - (H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p). + (H : P (m + (n + p))) := eq_ind_r P H (Z.add_shuffle3 n m p). Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop) (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) := @@ -261,24 +219,24 @@ Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop) (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x). Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop) - (H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x). + (H : P (x * -1)) := eq_ind_r P H (Z.opp_eq_mul_m1 x). Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop) - (H : P (y * x)) := eq_ind_r P H (Zmult_comm x y). + (H : P (y * x)) := eq_ind_r P H (Z.mul_comm x y). Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop) - (H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y). + (H : P (- x + - y)) := eq_ind_r P H (Z.opp_add_distr x y). Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) := - eq_ind_r P H (Zopp_involutive x). + eq_ind_r P H (Z.opp_involutive x). Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop) (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y). Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop) - (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p). + (H : P (n * p + m * p)) := eq_ind_r P H (Z.mul_add_distr_r n m p). Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop) - (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y). + (H : P (x * - y)) := eq_ind_r P H (Z.mul_opp_comm x y). Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop) (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p). @@ -300,3 +258,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x). + +Theorem intro_Z : + forall n:nat, exists y : Z, Z.of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros n; exists (Z.of_nat n); split; trivial. + rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. +Qed. |