From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/micromega/example.v | 22 +++++++++++----------- test-suite/micromega/heap3_vcgen_25.v | 2 +- test-suite/micromega/qexample.v | 4 ++-- test-suite/micromega/rexample.v | 4 ++-- test-suite/micromega/square.v | 4 ++-- test-suite/micromega/zomicron.v | 4 ++-- 6 files changed, 20 insertions(+), 20 deletions(-) (limited to 'test-suite/micromega') diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index 5cb103953..f424f0fcc 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -19,7 +19,7 @@ Lemma not_so_easy : forall x n : Z, 2*x + 1 <= 2 *n -> x <= n-1. Proof. intros. - lia. + lia. Qed. @@ -27,19 +27,19 @@ Qed. Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0. Proof. - intros. + intros. psatz Z 2. Qed. -Lemma Zdiscr: forall a b c x, +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, +Lemma plus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -48,20 +48,20 @@ Qed. -Lemma mplus_minus : forall x y, +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 -> +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: +(* Motivating example from: Expressiveness + Automation + Soundness: Towards COmbining SMT Solvers and Interactive Proof Assistants *) Parameter rho : Z. Parameter rho_ge : rho >= 0. @@ -76,7 +76,7 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop := 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 -> + rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D -> Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s). Proof. intros. @@ -194,8 +194,8 @@ 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 >= 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. @@ -323,7 +323,7 @@ Proof. Qed. -Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> +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. diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v index 0298303f5..efb5c7fd5 100644 --- a/test-suite/micromega/heap3_vcgen_25.v +++ b/test-suite/micromega/heap3_vcgen_25.v @@ -11,7 +11,7 @@ Require Import Psatz. Open Scope Z_scope. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : Z) (m : Z) (jt : Z) diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 1fa250e09..c9c779f90 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -10,7 +10,7 @@ Require Import Psatz. Require Import QArith. Require Import Ring_normalize. -Lemma plus_minus : forall x y, +Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. @@ -37,7 +37,7 @@ Qed. Open Scope Z_scope. Open Scope Q_scope. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : Q) (m : Q) (jt : Q) diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index d7386a4ec..c957add69 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -12,7 +12,7 @@ Require Import Ring_normalize. Open Scope R_scope. -Lemma yplus_minus : forall x y, +Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -34,7 +34,7 @@ Proof. Qed. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : R) (m : R) (jt : R) diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index b78bba25c..4c00ffe4a 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -20,7 +20,7 @@ Proof. intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p). assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2 /\ Zabs p^2 = p^2) by auto. -assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by +assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. intros n IHn p [Hn [Hp Heq]]. @@ -55,7 +55,7 @@ Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r. intros HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 60c16a998..3b2460233 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -24,7 +24,7 @@ Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x Proof. intros ; intuition auto. lia. -Qed. +Qed. Lemma compact_proof : forall z, (z < 0) -> @@ -32,5 +32,5 @@ Lemma compact_proof : forall z, (0 >= z \/ 0 < z) -> False. Proof. intros. - lia. + lia. Qed. \ No newline at end of file -- cgit v1.2.3