Abs.v 1.12 KB
Newer Older
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
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
Require int.Int.

Notation abs := Zabs (only parsing).

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z -> ((abs x) = x)) /\
  ((~ (0%Z <= x)%Z) -> ((abs x) = (-x)%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x.
split ; intros H.
now apply Zabs_eq.
apply Zabs_non_eq.
apply Znot_gt_le.
contradict H.
apply Zlt_le_weak.
now apply Zgt_lt.
Qed.
(* DO NOT EDIT BELOW *)

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Lemma Abs_le : forall (x:Z) (y:Z), ((abs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
  (x <= y)%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
zify.
omega.
Qed.
(* DO NOT EDIT BELOW *)

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Lemma Abs_pos : forall (x:Z), (0%Z <= (abs x))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zabs_pos.
Qed.
(* DO NOT EDIT BELOW *)