Commit 940b18ef authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update some Coq realizations with the new script format.

Note: they are stable with respect to the following command.
why3 --realize -D drivers/coq-realize.drv -T toto.Titi -o lib/coq/toto/
parent 78aea783
...@@ -3,38 +3,26 @@ ...@@ -3,38 +3,26 @@
Require Import ZArith. Require Import ZArith.
Require Import Rbase. Require Import Rbase.
Require Import Rbasic_fun. 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. Require real.Real.
(* Why3 goal *)
Definition abs: R -> R. Definition abs: R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rabs. exact Rabs.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((abs x) = x)) /\ Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((abs x) = x)) /\
((~ (0%R <= x)%R) -> ((abs x) = (-x)%R)). ((~ (0%R <= x)%R) -> ((abs x) = (-x)%R)).
(* YOU MAY EDIT THE PROOF BELOW *)
split ; intros H. split ; intros H.
apply Rabs_right. apply Rabs_right.
now apply Rle_ge. now apply Rle_ge.
apply Rabs_left. apply Rabs_left.
now apply Rnot_le_lt. now apply Rnot_le_lt.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Abs_le : forall (x:R) (y:R), ((abs x) <= y)%R <-> (((-y)%R <= x)%R /\ Lemma Abs_le : forall (x:R) (y:R), ((abs x) <= y)%R <-> (((-y)%R <= x)%R /\
(x <= y)%R). (x <= y)%R).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y. intros x y.
unfold abs, Rabs. unfold abs, Rabs.
case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]). case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]).
...@@ -57,16 +45,30 @@ now apply Ropp_le_contravar. ...@@ -57,16 +45,30 @@ now apply Ropp_le_contravar.
exact H0. exact H0.
exact H1. exact H1.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Abs_pos : forall (x:R), (0%R <= (abs x))%R. Lemma Abs_pos : forall (x:R), (0%R <= (abs x))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rabs_pos. exact Rabs_pos.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Abs_sum : forall (x:R) (y:R),
((abs (x + y)%R) <= ((abs x) + (abs y))%R)%R.
exact Rabs_triang.
Qed.
(* Why3 goal *)
Lemma Abs_prod : forall (x:R) (y:R),
((abs (x * y)%R) = ((abs x) * (abs y))%R).
exact Rabs_mult.
Qed.
(* Why3 goal *)
Lemma triangular_inequality : forall (x:R) (y:R) (z:R),
((abs (x - z)%R) <= ((abs (x - y)%R) + (abs (y - z)%R))%R)%R.
intros x y z.
replace (x - z)%R with ((x - y) + (y - z))%R by ring.
apply Rabs_triang.
Qed.
...@@ -2,78 +2,45 @@ ...@@ -2,78 +2,45 @@
(* Beware! Only edit allowed sections below *) (* Beware! Only edit allowed sections below *)
Require Import ZArith. Require Import ZArith.
Require Import Rbase. 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. Require int.Int.
Require real.Real. Require real.Real.
(* Why3 goal *)
Definition from_int: Z -> R. Definition from_int: Z -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact IZR. exact IZR.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Zero : ((from_int 0%Z) = 0%R). Lemma Zero : ((from_int 0%Z) = 0%R).
(* YOU MAY EDIT THE PROOF BELOW *)
split. split.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma One : ((from_int 1%Z) = 1%R). Lemma One : ((from_int 1%Z) = 1%R).
(* YOU MAY EDIT THE PROOF BELOW *)
split. split.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Add : forall (x:Z) (y:Z), Lemma Add : forall (x:Z) (y:Z),
((from_int (x + y)%Z) = ((from_int x) + (from_int y))%R). ((from_int (x + y)%Z) = ((from_int x) + (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact plus_IZR. exact plus_IZR.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Sub : forall (x:Z) (y:Z), Lemma Sub : forall (x:Z) (y:Z),
((from_int (x - y)%Z) = ((from_int x) - (from_int y))%R). ((from_int (x - y)%Z) = ((from_int x) - (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact minus_IZR. exact minus_IZR.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mul : forall (x:Z) (y:Z), Lemma Mul : forall (x:Z) (y:Z),
((from_int (x * y)%Z) = ((from_int x) * (from_int y))%R). ((from_int (x * y)%Z) = ((from_int x) * (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact mult_IZR. exact mult_IZR.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Neg : forall (x:Z), ((from_int (-x)%Z) = (-(from_int x))%R). Lemma Neg : forall (x:Z), ((from_int (-x)%Z) = (-(from_int x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact opp_IZR. exact opp_IZR.
Qed. Qed.
(* DO NOT EDIT BELOW *)
...@@ -2,264 +2,165 @@ ...@@ -2,264 +2,165 @@
(* Beware! Only edit allowed sections below *) (* Beware! Only edit allowed sections below *)
Require Import ZArith. Require Import ZArith.
Require Import Rbase. Require Import Rbase.
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
(* Why3 goal *)
Definition infix_ls: R -> R -> Prop. Definition infix_ls: R -> R -> Prop.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rlt. exact Rlt.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* Why3 assumption *)
Definition infix_lseq(x:R) (y:R): Prop := (infix_ls x y) \/ (x = y). Definition infix_lseq(x:R) (y:R): Prop := (infix_ls x y) \/ (x = y).
(* Why3 goal *)
Definition infix_pl: R -> R -> R. Definition infix_pl: R -> R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rplus. exact Rplus.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Definition prefix_mn: R -> R. Definition prefix_mn: R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Ropp. exact Ropp.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Definition infix_as: R -> R -> R. Definition infix_as: R -> R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmult. exact Rmult.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Unit_def : forall (x:R), ((infix_pl x 0%R) = x). Lemma Unit_def : forall (x:R), ((infix_pl x 0%R) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rplus_0_r. exact Rplus_0_r.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Assoc : forall (x:R) (y:R) (z:R), ((infix_pl (infix_pl x y) Lemma Assoc : forall (x:R) (y:R) (z:R), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))). z) = (infix_pl x (infix_pl y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rplus_assoc. exact Rplus_assoc.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Inv_def : forall (x:R), ((infix_pl x (prefix_mn x)) = 0%R). Lemma Inv_def : forall (x:R), ((infix_pl x (prefix_mn x)) = 0%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rplus_opp_r. exact Rplus_opp_r.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Comm : forall (x:R) (y:R), ((infix_pl x y) = (infix_pl y x)). Lemma Comm : forall (x:R) (y:R), ((infix_pl x y) = (infix_pl y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rplus_comm. exact Rplus_comm.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Assoc1 : forall (x:R) (y:R) (z:R), ((infix_as (infix_as x y) Lemma Assoc1 : forall (x:R) (y:R) (z:R), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))). z) = (infix_as x (infix_as y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmult_assoc. exact Rmult_assoc.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mul_distr : forall (x:R) (y:R) (z:R), ((infix_as x (infix_pl y Lemma Mul_distr : forall (x:R) (y:R) (z:R), ((infix_as x (infix_pl y
z)) = (infix_pl (infix_as x y) (infix_as x z))). z)) = (infix_pl (infix_as x y) (infix_as x z))).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmult_plus_distr_l. exact Rmult_plus_distr_l.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* Why3 assumption *)
Definition infix_mn(x:R) (y:R): R := (infix_pl x (prefix_mn y)). Definition infix_mn(x:R) (y:R): R := (infix_pl x (prefix_mn y)).
(* YOU MAY EDIT THE CONTEXT BELOW *) (* Why3 goal *)
(* DO NOT EDIT BELOW *)
Lemma Comm1 : forall (x:R) (y:R), ((infix_as x y) = (infix_as y x)). Lemma Comm1 : forall (x:R) (y:R), ((infix_as x y) = (infix_as y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmult_comm. exact Rmult_comm.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Unitary : forall (x:R), ((infix_as 1%R x) = x). Lemma Unitary : forall (x:R), ((infix_as 1%R x) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rmult_1_l. exact Rmult_1_l.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma NonTrivialRing : ~ (0%R = 1%R). Lemma NonTrivialRing : ~ (0%R = 1%R).
(* YOU MAY EDIT THE PROOF BELOW *)
apply not_eq_sym. apply not_eq_sym.
exact R1_neq_R0. exact R1_neq_R0.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Definition inv: R -> R. Definition inv: R -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rinv. exact Rinv.
Defined. Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Inverse : forall (x:R), (~ (x = 0%R)) -> ((infix_as x (inv x)) = 1%R). Lemma Inverse : forall (x:R), (~ (x = 0%R)) -> ((infix_as x (inv x)) = 1%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rinv_r. exact Rinv_r.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* Why3 assumption *)
Definition infix_sl(x:R) (y:R): R := (infix_as x (inv y)). Definition infix_sl(x:R) (y:R): R := (infix_as x (inv y)).
(* YOU MAY EDIT THE CONTEXT BELOW *) (* Why3 goal *)
(* DO NOT EDIT BELOW *)
Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> 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))). ((infix_sl (infix_as x y) z) = (infix_as x (infix_sl y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z _. intros x y z _.
apply Rmult_assoc. apply Rmult_assoc.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ 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 = 0%R)) -> ((infix_sl (infix_sl x y) z) = (infix_sl x (infix_as y
z))). z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z (Zy, Zz). intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv. unfold infix_sl, infix_as, inv.
rewrite Rmult_assoc. rewrite Rmult_assoc.
now rewrite Rinv_mult_distr. now rewrite Rinv_mult_distr.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ 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) ~ (z = 0%R)) -> ((infix_sl x (infix_sl y z)) = (infix_sl (infix_as x z)
y)). y)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z (Zy, Zz). intros x y z (Zy, Zz).
unfold infix_sl, infix_as, inv. unfold infix_sl, infix_as, inv.
field. field.
now split. now split.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Refl : forall (x:R), (infix_lseq x x). Lemma Refl : forall (x:R), (infix_lseq x x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rle_refl. exact Rle_refl.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Trans : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> ((infix_lseq y Lemma Trans : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)). z) -> (infix_lseq x z)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rle_trans. exact Rle_trans.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Antisymm : forall (x:R) (y:R), (infix_lseq x y) -> ((infix_lseq y x) -> Lemma Antisymm : forall (x:R) (y:R), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)). (x = y)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Rle_antisym. exact Rle_antisym.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Total : forall (x:R) (y:R), (infix_lseq x y) \/ (infix_lseq y x). Lemma Total : forall (x:R) (y:R), (infix_lseq x y) \/ (infix_lseq y x).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y. intros x y.
destruct (Rle_or_lt x y) as [H|H]. destruct (Rle_or_lt x y) as [H|H].
now left. now left.
right. right.
now apply Rlt_le. now apply Rlt_le.
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *) (* Why3 goal *)
Lemma ZeroLessOne : (infix_lseq 0%R 1%R).
exact Rle_0_1.
Qed.
(* Why3 goal *)
Lemma CompatOrderAdd : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> Lemma CompatOrderAdd : forall (x:R) (y:R) (z:R), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)). (infix_lseq (infix_pl x z) (infix_pl y z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z. intros x y z.
exact (Rplus_le_compat_r z x y). exact (Rplus_le_compat_r z x y).
Qed. Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (infix_lseq x y) -> 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))). ((infix_lseq 0%R z) -> (infix_lseq (infix_as x z) (infix_as y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z H Zz. intros x y z H Zz.
now apply Rmult_le_compat_r. now apply Rmult_le_compat_r.
Qed. 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