blob: 19bb5f809c93444a930707db955106a1c45651f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
Require Omega.
(* Submitted by Xavier Urbain 18 Jan 2002 *)
Lemma lem1 : (x,y:Z)
`-5 < x < 5` ->
`-5 < y` ->
`-5 < x+y+5`.
Proof.
Intros x y.
Omega.
Qed.
(* Proposed by Pierre Crégut *)
Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`.
Intro.
Omega.
Qed.
(* Proposed by Jean-Christophe Filliâtre *)
Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`.
Proof.
Intros.
Omega.
Qed.
(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
(* internal variable and a section variable (June 2001) *)
Section A.
Variable x,y : Z.
Hypothesis H : `x > y`.
Lemma lem4 : `x > y`.
Omega.
Qed.
End A.
(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
(* May 2002 *)
Section B.
Variables R1,R2,S1,S2,H,S:Z.
Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`.
Hypothesis J:`R1 < 0`->`S2 = S1-1`.
Hypothesis K:`R1 >= 0`->`R2 = R1`.
Hypothesis L:`R1 >= 0`->`S2 = S1`.
Hypothesis M:`H <= 2*S`.
Hypothesis N:`S < H`.
Lemma lem5 : `H > 0`.
Omega.
Qed.
End B.
|
