← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/micromega/rexample.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/micromega/rexample.v
 
1
(************************************************************************)
 
2
(*                                                                      *)
 
3
(* Micromega: A reflexive tactic using the Positivstellensatz           *)
 
4
(*                                                                      *)
 
5
(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
 
6
(*                                                                      *)
 
7
(************************************************************************)
 
8
 
 
9
Require Import Psatz.
 
10
Require Import Reals.
 
11
Require Import Ring_normalize.
 
12
 
 
13
Open Scope R_scope.
 
14
 
 
15
Lemma yplus_minus : forall x y, 
 
16
  0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 
17
Proof.
 
18
  intros.
 
19
  psatzl R.
 
20
Qed.
 
21
 
 
22
(* Other (simple) examples *)
 
23
 
 
24
Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
 
25
Proof.
 
26
  intros.
 
27
  psatzl R.
 
28
Qed.
 
29
 
 
30
 
 
31
Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 
32
Proof.
 
33
  intros ; psatzl R.
 
34
Qed.
 
35
 
 
36
 
 
37
Lemma vcgen_25 : forall   
 
38
  (n : R)
 
39
  (m : R)
 
40
  (jt : R)
 
41
  (j : R)
 
42
  (it : R)
 
43
  (i : R)
 
44
  (H0 : 1 * it + (-2%R  ) * i + (-1%R  ) = 0)
 
45
  (H :  1 * jt + (-2  ) * j + (-1  ) = 0)
 
46
  (H1 : 1 * n + (-10  ) = 0)
 
47
  (H2 : 0 <= (-4028  )  * i + (6222  ) * j + (705  )  * m + (-16674  ))
 
48
  (H3 : 0 <= (-418  ) * i + (651  ) * j + (94  ) * m + (-1866  ))
 
49
  (H4 : 0 <= (-209  ) * i + (302  ) * j + (47  ) * m + (-839  ))
 
50
  (H5 : 0 <= (-1  ) * i + 1 * j + (-1  ))
 
51
  (H6 : 0 <= (-1  ) * j + 1 * m + (0  ))
 
52
  (H7 : 0 <= (1  ) * j + (5  ) * m + (-27  ))
 
53
  (H8 : 0 <= (2  ) * j + (-1  ) * m + (2  ))
 
54
  (H9 : 0 <= (7  ) * j + (10  ) * m + (-74  ))
 
55
  (H10 : 0 <= (18  ) * j + (-139  ) * m + (1188  ))
 
56
  (H11 : 0 <= 1  * i + (0  ))
 
57
  (H13 : 0 <= (121  )  * i + (810  )  * j + (-7465  ) * m + (64350  )),
 
58
  (( 1 ) = (-2  ) * i + it).
 
59
Proof.
 
60
  intros.
 
61
  psatzl R.
 
62
Qed.
 
63
 
 
64
Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 
65
Proof.
 
66
  intros.
 
67
  psatz R 2.
 
68
Qed.
 
69
 
 
70
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.
 
71
Proof.
 
72
  intros ; psatz R.
 
73
Qed.
 
74
 
 
75
Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 
76
intros; split_Rabs; psatzl R.
 
77
Qed.
 
 
b'\\ No newline at end of file'