Commit 123dcce8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add some Coq realizations.

parent cb4f4a04
......@@ -839,10 +839,10 @@ endif
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Int
COQLIBS_INT_FILES = Abs EuclideanDivision Int MinMax
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
COQLIBS_REAL_FILES = Abs MinMax Real Square
COQLIBS_REAL_FILES = Abs FromInt MinMax Real Square
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL)
......
(* 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 int.Int.
Notation abs := Zabs (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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.
apply Zabs_non_eq.
apply Znot_gt_le.
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 *)
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 *)
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 *)
(* 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 int.Int.
Require int.Abs.
Definition div : Z -> Z -> Z.
(* YOU MAY EDIT THE CONTEXT BELOW *)
intros x y.
case (Z_le_dec 0 (Zmod x y)) ; intros H.
exact (Zdiv x y).
exact (Zdiv x y + 1)%Z.
Defined.
(* DO NOT EDIT BELOW *)
Definition mod1 : Z -> Z -> Z.
(* YOU MAY EDIT THE CONTEXT BELOW *)
intros x y.
exact (x - y * div x y)%Z.
Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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 Zy.
unfold mod1, div.
case Z_le_dec ; intros H ; ring.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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).
unfold div.
case Z_le_dec ; intros H.
split.
apply Z_div_pos with (2 := Hx).
now apply Zlt_gt.
destruct (Z_eq_dec y 1) as [H'|H'].
rewrite H', Zdiv_1_r.
apply Zle_refl.
rewrite <- (Zdiv_1_r x) at 2.
apply Zdiv_le_compat_l with (1 := Hx).
omega.
elim H.
apply Z_mod_lt.
now apply Zlt_gt.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y Zy.
zify.
assert (H1 := Z_mod_neg x y).
assert (H2 := Z_mod_lt x y).
unfold mod1, div.
case Z_le_dec ; intros H0.
rewrite Zmult_comm, <- Zmod_eq_full with (1 := Zy).
omega.
replace (x - y * (x / y + 1))%Z with (x - x / y * y - y)%Z by ring.
rewrite <- Zmod_eq_full with (1 := Zy).
omega.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x.
unfold mod1, div.
rewrite Zmod_1_r, Zdiv_1_r, Zmult_1_l.
apply Zminus_diag.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x.
unfold div.
now rewrite Zmod_1_r, Zdiv_1_r.
Qed.
(* DO NOT EDIT BELOW *)
(* 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 int.Int.
Notation min := Zmin (only parsing).
Notation max := Zmax (only parsing).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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 *)
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.
now left.
now right.
now left.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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 *)
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.
now left.
now left.
now right.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
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 *)
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 *)
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 *)
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 *)
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 *)
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 *)
(* 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 int.Int.
Require real.Real.
Definition from_int: Z -> R.
(* YOU MAY EDIT THE PROOF BELOW *)
exact IZR.
Defined.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Zero : ((from_int 0%Z) = 0%R).
(* YOU MAY EDIT THE PROOF BELOW *)
split.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma One : ((from_int 1%Z) = 1%R).
(* YOU MAY EDIT THE PROOF BELOW *)
split.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Add : forall (x:Z) (y:Z),
((from_int (x + y)%Z) = ((from_int x) + (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact plus_IZR.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Sub : forall (x:Z) (y:Z),
((from_int (x - y)%Z) = ((from_int x) - (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact minus_IZR.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Mul : forall (x:Z) (y:Z),
((from_int (x * y)%Z) = ((from_int x) * (from_int y))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact mult_IZR.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Lemma Neg : forall (x:Z), ((from_int (-x)%Z) = (-(from_int x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
exact opp_IZR.
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