Commit 5459fb63 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add realization of real.Abs.

parent ff115c6a
(* 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 *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment