Abs.v 1.68 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 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Require Import Rbasic_fun.
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
Require real.Real.
Definition abs: R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rabs.
Defined.
(* DO NOT EDIT BELOW *)


(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((abs x) = x)) /\
  ((~ (0%R <= x)%R) -> ((abs x) = (-x)%R)).
(* YOU MAY EDIT THE PROOF BELOW *)
split ; intros H.
apply Rabs_right.
now apply Rle_ge.
apply Rabs_left.
now apply Rnot_le_lt.
Qed.
(* DO NOT EDIT BELOW *)

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Lemma Abs_le : forall (x:R) (y:R), ((abs x) <= y)%R <-> (((-y)%R <= x)%R /\
  (x <= y)%R).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
unfold abs, Rabs.
case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]).
rewrite <- (Ropp_involutive x).
now apply Ropp_le_contravar.
apply Rlt_le.
apply Rlt_le_trans with (1 := H).
apply Rle_trans with (2 := H0).
rewrite <- Ropp_0.
apply Ropp_le_contravar.
now apply Rlt_le.
rewrite <- (Ropp_involutive y).
now apply Ropp_le_contravar.
apply Rge_le in H.
apply Rle_trans with (2 := H).
apply Rle_trans with (Ropp x).
now apply Ropp_le_contravar.
rewrite <- Ropp_0.
now apply Ropp_le_contravar.
exact H0.
exact H1.
Qed.
(* DO NOT EDIT BELOW *)

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

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