Commit ff115c6a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add realization of real.MinMax and commit missed parts of real.Real.

Note that the files are compiled with: coqc -R . '' real/toto.v
parent 72b12557
(* 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 real.Real.
(* no editable section? *)
Require Import Rbasic_fun.
Definition min: R -> R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmin.
Defined.
(* DO NOT EDIT BELOW *)
Definition max: R -> R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmax.
Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Max_is_ge : forall (x:R) (y:R), (x <= (max x y))%R /\ (y <= (max x
y))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
split.
apply Rmax_l.
apply Rmax_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Max_is_some : forall (x:R) (y:R), ((max x y) = x) \/ ((max x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
destruct (Rle_or_lt x y) as [H|H].
right.
now apply Rmax_right.
left.
apply Rmax_left.
now apply Rlt_le.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Min_is_le : forall (x:R) (y:R), ((min x y) <= x)%R /\ ((min x
y) <= y)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
split.
apply Rmin_l.
apply Rmin_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Min_is_some : forall (x:R) (y:R), ((min x y) = x) \/ ((min x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
destruct (Rle_or_lt x y) as [H|H].
left.
now apply Rmin_left.
right.
apply Rmin_right.
now apply Rlt_le.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -157,7 +157,7 @@ Definition infix_sl(x:R) (y:R): R := (infix_as x (inv y)).
Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_as x y) z) = (infix_as x (infix_sl y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z Zz.
intros x y z _.
apply Rmult_assoc.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -170,8 +170,10 @@ Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
~ (z = 0%R)) -> ((infix_sl (infix_sl x y) z) = (infix_sl x (infix_as y
z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv.
rewrite Rmult_assoc.
now rewrite Rinv_mult_distr.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -183,8 +185,10 @@ Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
~ (z = 0%R)) -> ((infix_sl x (infix_sl y z)) = (infix_sl (infix_as x z)
y)).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv.
field.
now split.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -194,8 +198,7 @@ Qed.
Lemma Refl : forall (x:R), (infix_lseq x x).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
exact Rle_refl.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -206,8 +209,7 @@ Qed.
Lemma Trans : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
exact Rle_trans.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -218,8 +220,7 @@ Qed.
Lemma Antisymm : forall (x:R) (y:R), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
exact Rle_antisym.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -229,8 +230,11 @@ Qed.
Lemma Total : forall (x:R) (y:R), (infix_lseq x y) \/ (infix_lseq y x).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros x y.
destruct (Rle_or_lt x y) as [H|H].
now left.
right.
now apply Rlt_le.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -241,8 +245,8 @@ Qed.
Lemma CompatOrderAdd : forall (x:R) (y:R) (z:R), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros x y z.
exact (Rplus_le_compat_r z x y).
Qed.
(* DO NOT EDIT BELOW *)
......@@ -253,8 +257,8 @@ Qed.
Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (infix_lseq x y) ->
((infix_lseq 0%R z) -> (infix_lseq (infix_as x z) (infix_as y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intros x y z H Zz.
now apply Rmult_le_compat_r.
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