Commit 54f46f3b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update some additional Coq realizations now that notations are supported.

parent 47fb5a4c
......@@ -979,7 +979,7 @@ clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
update-coq: bin/why3
#for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
#for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......
......@@ -2,19 +2,14 @@
(* 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.
(* Why3 goal *)
Notation abs := Zabs (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
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.
......@@ -24,29 +19,18 @@ 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 *)
(* Why3 goal *)
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 *)
(* Why3 goal *)
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 *)
......@@ -3,34 +3,25 @@
Require Import ZArith.
Require Import Rbase.
Require Import ZOdiv.
(*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.Abs.
(* Why3 goal *)
Notation div := ZOdiv (only parsing).
(* Why3 goal *)
Notation mod1 := ZOmod (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
y))%Z + (mod1 x y))%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y _.
apply ZO_div_mod_eq.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx,Hy).
split.
apply ZO_div_pos with (1 := Hx).
......@@ -44,15 +35,10 @@ apply ZO_div_lt with (1 := H').
omega.
now rewrite <- H', ZOdiv_0_l.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (mod1 x y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y Zy.
destruct (Zle_or_lt 0 x) as [Hx|Hx].
refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
......@@ -63,66 +49,41 @@ clear -Zy ; zify ; omega.
apply ZOmod_lt_neg with (2 := Zy).
now apply Zlt_le_weak.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (div x y))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx, Hy).
apply ZO_div_pos with (1 := Hx).
now apply Zlt_le_weak.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((div x y) <= 0%Z)%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx, Hy).
generalize (ZO_div_pos (-x) y).
rewrite ZOdiv_opp_l.
omega.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (mod1 x y))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx, Zy).
now apply ZOmod_lt_pos.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((mod1 x y) <= 0%Z)%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx, Zy).
now apply ZOmod_lt_neg.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((div x y) * y)%Z) <= (Zabs x))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y Zy.
rewrite Zmult_comm.
zify.
......@@ -130,57 +91,32 @@ generalize (ZO_mult_div_le x y).
generalize (ZO_mult_div_ge x y).
omega.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact ZOdiv_1_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
exact ZOmod_1_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
y) = 0%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
exact ZOdiv_small.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((mod1 x
y) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact ZOmod_small.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z (Hx&Hy&Hz).
rewrite (Zplus_comm y).
rewrite <- ZO_div_plus.
......@@ -192,15 +128,10 @@ now apply Zlt_le_weak.
intros H.
now rewrite H in Hx.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z (Hx&Hy&Hz).
rewrite Zplus_comm, Zmult_comm.
apply ZO_mod_plus.
......@@ -209,6 +140,5 @@ apply Zplus_le_0_compat with (1 := Hz).
apply Zmult_le_0_compat with (1 := Hy).
now apply Zlt_le_weak.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,11 +2,11 @@
(* 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".*)
(* Why3 goal *)
Notation infix_ls := Zlt (only parsing).
(* Why3 assumption *)
Definition infix_lseq(x:Z) (y:Z): Prop := (infix_ls x y) \/ (x = y).
Lemma infix_lseq_Zle :
......@@ -17,156 +17,96 @@ apply iff_Symmetric.
apply Zle_lt_or_eq_iff.
Qed.
(* Why3 goal *)
Notation infix_pl := Zplus (only parsing).
(* Why3 goal *)
Notation prefix_mn := Zopp (only parsing).
(* Why3 goal *)
Notation infix_as := Zmult (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Unit_def : forall (x:Z), ((infix_pl x 0%Z) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zplus_0_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Assoc : forall (x:Z) (y:Z) (z:Z), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z.
apply sym_eq.
apply Zplus_assoc.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Inv_def : forall (x:Z), ((infix_pl x (prefix_mn x)) = 0%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zplus_opp_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Comm : forall (x:Z) (y:Z), ((infix_pl x y) = (infix_pl y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zplus_comm.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z.
apply sym_eq.
apply Zmult_assoc.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Mul_distr : forall (x:Z) (y:Z) (z:Z), ((infix_as x (infix_pl y
z)) = (infix_pl (infix_as x y) (infix_as x z))).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmult_plus_distr_r.
Qed.
(* DO NOT EDIT BELOW *)
(* Why3 assumption *)
Definition infix_mn(x:Z) (y:Z): Z := (infix_pl x (prefix_mn y)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Comm1 : forall (x:Z) (y:Z), ((infix_as x y) = (infix_as y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmult_comm.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Unitary : forall (x:Z), ((infix_as 1%Z x) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmult_1_l.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma NonTrivialRing : ~ (0%Z = 1%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
discriminate.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Refl : forall (x:Z), (infix_lseq x x).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x.
apply infix_lseq_Zle.
apply Zle_refl.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Trans : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z H1 H2.
apply infix_lseq_Zle.
apply Zle_trans with y ;
now apply infix_lseq_Zle.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Antisymm : forall (x:Z) (y:Z), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y H1 H2.
apply Zle_antisym ;
now apply infix_lseq_Zle.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Total : forall (x:Z) (y:Z), (infix_lseq x y) \/ (infix_lseq y x).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
destruct (Zle_or_lt x y) as [H|H].
left.
......@@ -175,34 +115,28 @@ right.
apply infix_lseq_Zle.
now apply Zlt_le_weak.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma ZeroLessOne : (infix_lseq 0%Z 1%Z).
now left.
Qed.
(* Why3 goal *)
Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z H.
apply infix_lseq_Zle.
apply Zplus_le_compat_r.
now apply infix_lseq_Zle.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
((infix_lseq 0%Z z) -> (infix_lseq (infix_as x z) (infix_as y z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y z H1 H2.
apply infix_lseq_Zle.
apply Zmult_le_compat_r ;
now apply infix_lseq_Zle.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,33 +2,24 @@
(* 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.
(* Why3 goal *)
Notation min := Zmin (only parsing).
(* Why3 goal *)
Notation max := Zmax (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (max x y))%Z /\ (y <= (max x
y))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
split.
apply Zle_max_l.
apply Zle_max_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Max_is_some : forall (x:Z) (y:Z), ((max x y) = x) \/ ((max x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
unfold Zmax.
case Zcompare.
......@@ -36,27 +27,17 @@ now left.
now right.
now left.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Min_is_le : forall (x:Z) (y:Z), ((min x y) <= x)%Z /\ ((min x
y) <= y)%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
split.
apply Zle_min_l.
apply Zle_min_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Min_is_some : forall (x:Z) (y:Z), ((min x y) = x) \/ ((min x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y.
unfold Zmin.
case Zcompare.
......@@ -64,68 +45,37 @@ now left.
now left.
now right.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((max x y) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmax_l.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((max x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmax_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((min x y) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmin_l.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((min x y) = y).
(* YOU MAY EDIT THE PROOF BELOW *)
exact Zmin_r.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((max x y) = (max y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y _.
apply Zmax_comm.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((min x y) = (min y x)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y _.
apply Zmin_comm.
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