diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/micromega | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/micromega')
-rw-r--r-- | test-suite/micromega/csdp.cache | bin | 44878 -> 0 bytes | |||
-rw-r--r-- | test-suite/micromega/example.v | 10 | ||||
-rw-r--r-- | test-suite/micromega/square.v | 18 |
3 files changed, 14 insertions, 14 deletions
diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache Binary files differdeleted file mode 100644 index 645de69c..00000000 --- a/test-suite/micromega/csdp.cache +++ /dev/null diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index f424f0fc..d648c2e4 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -77,13 +77,13 @@ 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 -> - Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s). + Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s). Proof. intros. - generalize (Zabs_eq (C p t - D q t)). - generalize (Zabs_non_eq (C p t - D q t)). - generalize (Zabs_eq (C p s -D q s)). - generalize (Zabs_non_eq (C p s - D q s)). + 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. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 4c00ffe4..8767f687 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -9,17 +9,17 @@ Require Import ZArith Zwf Psatz QArith. Open Scope Z_scope. -Lemma Zabs_square : forall x, (Zabs x)^2 = x^2. +Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. intros ; case (Zabs_dec x) ; intros ; psatz Z 2. Qed. -Hint Resolve Zabs_pos Zabs_square. +Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. 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. +intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). +assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 + /\ Z.abs p^2 = p^2) by auto. 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. @@ -35,7 +35,7 @@ Lemma QnumZpower : forall x : Q, Qnum (x ^ 2)%Q = ((Qnum x) ^ 2) %Z. Proof. intros. destruct x. - cbv beta iota zeta delta - [Zmult]. + cbv beta iota zeta delta - [Z.mul]. ring. Qed. @@ -45,15 +45,15 @@ Proof. intros. destruct x. simpl. - unfold Zpower_pos. + unfold Z.pow_pos. simpl. - rewrite Pmult_1_r. + rewrite Pos.mul_1_r. reflexivity. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. - unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r. + unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r. intros HQeq. assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). |