|
(************************************************************************)
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
Require Import ZArith.
Require Import Psatz.
Open Scope Z_scope.
Require Import ZMicromega.
Require Import VarMap.
Lemma not_so_easy : forall x n : Z,
2*x + 1 <= 2 *n -> x <= n-1.
Proof.
intros.
psatz Z 2.
Qed.
(* From Laurent Théry *)
Goal forall (x y : Z), x = 0 -> x * y = 0.
Proof.
intros.
psatz Z 2.
Qed.
Goal forall (x y : Z), x = 0 -> x * y = 0.
Proof.
intros.
psatz Z 2.
Qed.
Goal forall (x y : Z), 2*x = 0 -> x * y = 0.
Proof.
intros.
psatz Z 2.
Qed.
Goal forall (x y: Z), - x*x >= 0 -> x * y = 0.
Proof.
intros.
psatz Z 4.
Qed.
Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
Proof.
intros.
psatz Z 2.
Qed.
Lemma Zdiscr: forall a b c x,
a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
Proof.
intros ; psatz Z 4.
Qed.
Lemma plus_minus : forall x y,
0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y.
Proof.
intros.
psatz Z 1.
Qed.
Lemma mplus_minus : forall x y,
x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma pol3: forall x y, 0 <= x + y ->
x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
Proof.
intros; psatz Z 4.
Qed.
(* Motivating example from: Expressiveness + Automation + Soundness:
Towards COmbining SMT Solvers and Interactive Proof Assistants *)
Parameter rho : Z.
Parameter rho_ge : rho >= 0.
Parameter correct : Z -> Z -> Prop.
Definition rbound1 (C:Z -> Z -> Z) : Prop :=
forall p s t, correct p t /\ s <= t -> C p t - C p s <= (1-rho)*(t-s).
Definition rbound2 (C:Z -> Z -> Z) : Prop :=
forall p s t, correct p t /\ s <= t -> (1-rho)*(t-s) <= C p t - C p s.
Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t /\ correct q t /\
rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D ->
Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s).
Proof.
intros.
generalize (Z.abs_eq (C p t - D q t)).
generalize (Z.abs_neq (C p t - D q t)).
generalize (Z.abs_eq (C p s -D q s)).
generalize (Z.abs_neq (C p s - D q s)).
unfold rbound2 in H.
unfold rbound1 in H.
intuition.
generalize (H6 _ _ _ (conj H H4)).
generalize (H7 _ _ _ (conj H H4)).
generalize (H8 _ _ _ (conj H H4)).
generalize (H10 _ _ _ (conj H H4)).
generalize (H6 _ _ _ (conj H5 H4)).
generalize (H7 _ _ _ (conj H5 H4)).
generalize (H8 _ _ _ (conj H5 H4)).
generalize (H10 _ _ _ (conj H5 H4)).
generalize rho_ge.
zify; intuition subst ; psatz Z 2.
Qed.
(* Rule of signs *)
Lemma sign_pos_pos: forall x y,
x > 0 -> y > 0 -> x*y > 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_pos_zero: forall x y,
x > 0 -> y = 0 -> x*y = 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_pos_neg: forall x y,
x > 0 -> y < 0 -> x*y < 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_zero_pos: forall x y,
x = 0 -> y > 0 -> x*y = 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_zero_neg: forall x y,
x = 0 -> y < 0 -> x*y = 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_neg_pos: forall x y,
x < 0 -> y > 0 -> x*y < 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_neg_zero: forall x y,
x < 0 -> y = 0 -> x*y = 0.
Proof.
intros; psatz Z 2.
Qed.
Lemma sign_neg_neg: forall x y,
x < 0 -> y < 0 -> x*y > 0.
Proof.
intros; psatz Z 2.
Qed.
(* Other (simple) examples *)
Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
Proof.
intros.
psatz Z 2.
Qed.
Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 -> False.
Proof.
intros ; psatz Z 2.
Qed.
(* Found in Parrilo's talk *)
(* BUG?: certificate with **very** big coefficients *)
Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
Proof.
intros.
psatz Z 2.
Qed.
(* from hol_light/Examples/sos.ml *)
Lemma hol_light1 : forall a1 a2 b1 b2,
a1 >= 0 -> a2 >= 0 ->
(a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) ->
(a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
Proof.
intros ; psatz Z 4.
Qed.
Lemma hol_light2 : forall x a,
3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
Proof.
intros ; psatz Z 2.
Qed.
Lemma hol_light3 : forall b a c x,
b ^ 2 < 4 * a * c -> (a * x ^2 + b * x + c = 0) -> False.
Proof.
intros ; psatz Z 4.
Qed.
Lemma hol_light4 : forall a c b x,
a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
Proof.
intros ; psatz Z 4.
Qed.
Lemma hol_light5 : forall x y,
0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1
-> x ^ 2 + y ^ 2 < 1 \/
(x - 1) ^ 2 + y ^ 2 < 1 \/
x ^ 2 + (y - 1) ^ 2 < 1 \/
(x - 1) ^ 2 + (y - 1) ^ 2 < 1.
Proof.
intros; psatz Z 3.
Qed.
Lemma hol_light7 : forall x y z,
0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
-> x * y + x * z + y * z >= 3 * x * y * z.
Proof.
intros ; psatz Z 3.
Qed.
Lemma hol_light8 : forall x y z,
x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
Proof.
intros ; psatz Z 2.
Qed.
Lemma hol_light9 : forall w x y z,
w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
-> (w + x + y + z) ^ 2 <= 4.
Proof.
intros; psatz Z 2.
Qed.
Lemma hol_light10 : forall x y,
x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
Proof.
intros ; psatz Z 2.
Qed.
Lemma hol_light11 : forall x y,
x > 1 /\ y > 1 -> x * y > x + y - 1.
Proof.
intros ; psatz Z 2.
Qed.
Lemma hol_light12: forall x y z,
2 <= x /\ x <= 125841 / 50000 /\
2 <= y /\ y <= 125841 / 50000 /\
2 <= z /\ z <= 125841 / 50000
-> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= 0.
Proof.
intros x y z ; set (e:= (125841 / 50000)).
compute in e.
unfold e ; intros ; psatz Z 2.
Qed.
Lemma hol_light14 : forall x y z,
2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
-> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
Proof.
intros ;psatz Z 2.
Qed.
(* ------------------------------------------------------------------------- *)
(* Inequality from sci.math (see "Leon-Sotelo, por favor"). *)
(* ------------------------------------------------------------------------- *)
Lemma hol_light16 : forall x y,
0 <= x /\ 0 <= y /\ (x * y = 1)
-> x + y <= x ^ 2 + y ^ 2.
Proof.
intros ; psatz Z 2.
Qed.
Lemma hol_light17 : forall x y,
0 <= x /\ 0 <= y /\ (x * y = 1)
-> x * y * (x + y) <= x ^ 2 + y ^ 2.
Proof.
intros ; psatz Z 3.
Qed.
Lemma hol_light18 : forall x y,
0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
Proof.
intros ; psatz Z 4.
Qed.
(* ------------------------------------------------------------------------- *)
(* Some examples over integers and natural numbers. *)
(* ------------------------------------------------------------------------- *)
Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
Proof.
intros.
psatz Z 2.
Qed.
Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
-> (x1 + y1 = x2 + y2).
Proof.
intros.
psatz Z 2.
Qed.
Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
Proof.
intros.
psatz Z 1.
Qed.
Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
Proof.
intros.
generalize (motzkin' x y).
psatz Z 8.
Qed.
(** Other tests *)
Goal forall x y z n,
y >= z /\ y = n \/ ~ y >= z /\ z = n ->
x >= y /\
(x >= z /\ (x >= n /\ x = x \/ ~ x >= n /\ x = n) \/
~ x >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)) \/
~ x >= y /\
(y >= z /\ (x >= n /\ y = x \/ ~ x >= n /\ y = n) \/
~ y >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)).
Proof.
intros.
psatz Z 2.
Qed.
(** Incompeteness: require manual case split *)
Goal forall (z0 z z1 z2 z3 z5 :Z)
(H8 : 0 <= z2)
(H5 : z5 > 0)
(H0 : z0 > 0)
(H9 : z2 < z0)
(H1 : z0 * z5 > 0)
(H10 : 0 <= z1 * z0 + z0 * z5 - 1 - z0 * z5 * z)
(H11 : z1 * z0 + z0 * z5 - 1 - z0 * z5 * z < z0 * z5)
(H6 : 0 <= z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3)
(H7 : z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3 < z0 * z5)
(C : z > z3), False.
Proof.
intros.
assert (z1 - z5 * z3 - 1 < 0) by psatz Z 3.
psatz Z 3.
Qed.
Goal forall
(d sz x n : Z)
(GE : sz * x - sz * d >=1 )
(R : sz + d * sz - sz * x >= 1),
False.
Proof.
intros.
assert (x - d >= 1) by psatz Z 3.
psatz Z 3.
Qed.
Goal forall x6 x8 x9 x10 x11 x12 x13 x14,
x6 >= 0 ->
-x6 + x8 + x9 + -x10 >= 1 ->
x8 >= 0 ->
x11 >= 0 ->
-x11 + x12 + x13 + -x14 >= 1 ->
x6 + -4*x8 + -2*x9 + 3*x10 + x11 + -4*x12 + -2*x13 + 3*x14 >= -5 ->
x10 >= 0 ->
x14 >= 0 ->
x12 >= 0 ->
x8 + -x10 + x12 + -x14 >= 1 ->
False.
Proof.
intros.
psatz Z 1.
Qed.
Goal forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
x2 + -1*x4 >= 0 ->
-2*x2 + x4 >= -1 ->
x1 + x3 + x4 + -1*x7 + -1*x11 >= 1 ->
-1*x2 + x8 + x10 >= 0 ->
-2*x3 + -2*x4 + x5 + 2*x6 + x9 >= -1 ->
-2*x1 + 3*x3 + x4 + -1*x7 + -1*x11 >= 0 ->
-2*x1 + x3 + x4 + -1*x8 + -1*x10 + 2*x12 >= 0 ->
-2*x2 + x3 + x4 + -1*x7 + -1*x11 + 2*x12 >= 0 ->
-2*x2 + x3 + 3*x4 + -1*x8 + -1*x10 >= 0 ->
2*x2 + -1*x3 + -1*x4 + x5 + 2*x6 + -2*x8 + x9 + -2*x10 >= 0 ->
x1 + -2*x3 + x7 + x11 + -2*x12 >= 0 ->
False.
Proof.
intros.
psatz Z 1.
Qed.
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
