 ### [Realization] The realizations ask to prove that the coq driver is correct

``` - use the syntax of the driver for the own realization of a theory
- add a *_def lemma for defined logics with syntax
- add comments that inform which syntax is used for declared logic```
parent 6fa633ef
 ... ... @@ -6,9 +6,6 @@ time "why3cpulimit time : %s s" (* À discuter *) (*transformation "simplify_recursive_definition"*) transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_non_struct_recursion" transformation "eliminate_if" ... ...
 ... ... @@ -5,5 +5,7 @@ prelude "(* Beware! Only edit allowed sections below *)" printer "coq-realize" filename "%t.v" transformation "inline_trivial" import "coq-common.gen"
 ... ... @@ -5,6 +5,9 @@ prelude "(* Beware! Only edit allowed sections below *)" printer "coq" filename "%f_%t_%g.v" transformation "inline_trivial" transformation "eliminate_builtin" import "coq-common.gen" theory real.Trigonometry ... ...
 ... ... @@ -5,6 +5,9 @@ prelude "(* Beware! Only edit allowed sections below *)" printer "coq" filename "%f_%t_%g.v" transformation "inline_trivial" transformation "eliminate_builtin" import "coq-common.gen" theory real.Trigonometry ... ...
 ... ... @@ -4,12 +4,12 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 goal *) Notation abs := Zabs (only parsing). (* Why3 comment *) (* abs is replaced with (Zabs x) by the coq driver *) (* Why3 goal *) Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z -> ((abs x) = x)) /\ ((~ (0%Z <= x)%Z) -> ((abs x) = (-x)%Z)). Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z -> ((Zabs x) = x)) /\ ((~ (0%Z <= x)%Z) -> ((Zabs x) = (-x)%Z)). intros x. split ; intros H. now apply Zabs_eq. ... ... @@ -21,7 +21,7 @@ now apply Zgt_lt. Qed. (* Why3 goal *) Lemma Abs_le : forall (x:Z) (y:Z), ((abs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ Lemma Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z). intros x y. zify. ... ... @@ -29,7 +29,7 @@ omega. Qed. (* Why3 goal *) Lemma Abs_pos : forall (x:Z), (0%Z <= (abs x))%Z. Lemma Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. exact Zabs_pos. Qed. ... ...
 ... ... @@ -6,22 +6,22 @@ Require BuiltIn. Require int.Int. Require int.Abs. (* Why3 goal *) Notation div := ZOdiv (only parsing). (* Why3 comment *) (* div is replaced with (ZOdiv x x1) by the coq driver *) (* Why3 goal *) Notation mod1 := ZOmod (only parsing). (* Why3 comment *) (* mod1 is replaced with (ZOmod x x1) by the coq driver *) (* Why3 goal *) Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z). intros x y _. apply ZO_div_mod_eq. Qed. (* 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). ((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z). intros x y (Hx,Hy). split. apply ZO_div_pos with (1 := Hx). ... ... @@ -38,7 +38,7 @@ Qed. (* 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). (((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z). 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)) _). ... ... @@ -52,7 +52,7 @@ Qed. (* 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. (0%Z <= (ZOdiv x y))%Z. intros x y (Hx, Hy). apply ZO_div_pos with (1 := Hx). now apply Zlt_le_weak. ... ... @@ -60,7 +60,7 @@ Qed. (* 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. ((ZOdiv x y) <= 0%Z)%Z. intros x y (Hx, Hy). generalize (ZO_div_pos (-x) y). rewrite ZOdiv_opp_l. ... ... @@ -69,21 +69,21 @@ Qed. (* Why3 goal *) Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (mod1 x y))%Z. (0%Z <= (ZOmod x y))%Z. intros x y (Hx, Zy). now apply ZOmod_lt_pos. Qed. (* Why3 goal *) Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((mod1 x y) <= 0%Z)%Z. ((ZOmod x y) <= 0%Z)%Z. intros x y (Hx, Zy). now apply ZOmod_lt_neg. Qed. (* Why3 goal *) Lemma Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((Zabs ((div x y) * y)%Z) <= (Zabs x))%Z. ((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z. intros x y Zy. rewrite Zmult_comm. zify. ... ... @@ -93,30 +93,30 @@ omega. Qed. (* Why3 goal *) Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x). Lemma Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x). exact ZOdiv_1_r. Qed. (* Why3 goal *) Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z). Lemma Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z). exact ZOmod_1_r. Qed. (* Why3 goal *) Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z). Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOdiv x y) = 0%Z). exact ZOdiv_small. Qed. (* Why3 goal *) Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((mod1 x y) = x). Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOmod x y) = x). exact ZOmod_small. Qed. (* 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). (0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z). intros x y z (Hx&Hy&Hz). rewrite (Zplus_comm y). rewrite <- ZO_div_plus. ... ... @@ -131,7 +131,7 @@ Qed. (* 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)). (0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)). intros x y z (Hx&Hy&Hz). rewrite Zplus_comm, Zmult_comm. apply ZO_mod_plus. ... ...
 ... ... @@ -3,32 +3,29 @@ Require Import BuiltIn. Require BuiltIn. (* Why3 comment *) (* infix_ls is replaced with (x < x1)%Z by the coq driver *) (* Why3 goal *) Notation infix_ls := Zlt (only parsing). Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ (x = y)). exact Zle_lt_or_eq_iff. Qed. (* Why3 assumption *) Definition infix_lseq(x:Z) (y:Z): Prop := (infix_ls x y) \/ (x = y). Lemma infix_lseq_Zle : forall x y, infix_lseq x y <-> Zle x y. Proof. intros x y. apply iff_sym. apply Zle_lt_or_eq_iff. Qed. (* Why3 goal *) Notation infix_pl := Zplus (only parsing). (* Why3 comment *) (* infix_pl is replaced with (x + x1)%Z by the coq driver *) (* Why3 goal *) Notation prefix_mn := Zopp (only parsing). (* Why3 comment *) (* prefix_mn is replaced with (-x)%Z by the coq driver *) (* Why3 goal *) Notation infix_as := Zmult (only parsing). (* Why3 comment *) (* infix_as is replaced with (x * x1)%Z by the coq driver *) (* 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))). Lemma Assoc : forall (x:Z) (y:Z) (z:Z), (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z). Proof. intros x y z. apply sym_eq. ... ... @@ -36,38 +33,38 @@ apply Zplus_assoc. Qed. (* Why3 goal *) Lemma Unit_def_l : forall (x:Z), ((infix_pl 0%Z x) = x). Lemma Unit_def_l : forall (x:Z), ((0%Z + x)%Z = x). Proof. exact Zplus_0_l. Qed. (* Why3 goal *) Lemma Unit_def_r : forall (x:Z), ((infix_pl x 0%Z) = x). Lemma Unit_def_r : forall (x:Z), ((x + 0%Z)%Z = x). Proof. exact Zplus_0_r. Qed. (* Why3 goal *) Lemma Inv_def_l : forall (x:Z), ((infix_pl (prefix_mn x) x) = 0%Z). Lemma Inv_def_l : forall (x:Z), (((-x)%Z + x)%Z = 0%Z). Proof. exact Zplus_opp_l. Qed. (* Why3 goal *) Lemma Inv_def_r : forall (x:Z), ((infix_pl x (prefix_mn x)) = 0%Z). Lemma Inv_def_r : forall (x:Z), ((x + (-x)%Z)%Z = 0%Z). Proof. exact Zplus_opp_r. Qed. (* Why3 goal *) Lemma Comm : forall (x:Z) (y:Z), ((infix_pl x y) = (infix_pl y x)). Lemma Comm : forall (x:Z) (y:Z), ((x + y)%Z = (y + x)%Z). Proof. exact Zplus_comm. Qed. (* 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))). Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z), (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z). Proof. intros x y z. apply sym_eq. ... ... @@ -75,32 +72,35 @@ apply Zmult_assoc. Qed. (* Why3 goal *) Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z), ((infix_as x (infix_pl y z)) = (infix_pl (infix_as x y) (infix_as x z))). Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z), ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z). Proof. intros x y z. apply Zmult_plus_distr_r. Qed. (* Why3 goal *) Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z), ((infix_as (infix_pl y z) x) = (infix_pl (infix_as y x) (infix_as z x))). Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z), (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z). Proof. intros x y z. apply Zmult_plus_distr_l. Qed. (* Why3 assumption *) Definition infix_mn(x:Z) (y:Z): Z := (infix_pl x (prefix_mn y)). (* Why3 goal *) Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z). reflexivity. Qed. (* Why3 goal *) Lemma Comm1 : forall (x:Z) (y:Z), ((infix_as x y) = (infix_as y x)). Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z). Proof. exact Zmult_comm. Qed. (* Why3 goal *) Lemma Unitary : forall (x:Z), ((infix_as 1%Z x) = x). Lemma Unitary : forall (x:Z), ((1%Z * x)%Z = x). Proof. exact Zmult_1_l. Qed. ... ... @@ -112,68 +112,55 @@ discriminate. Qed. (* Why3 goal *) Lemma Refl : forall (x:Z), (infix_lseq x x). Lemma Refl : forall (x:Z), (x <= x)%Z. Proof. intros x. apply infix_lseq_Zle. apply Zle_refl. Qed. (* Why3 goal *) Lemma Trans : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) -> ((infix_lseq y z) -> (infix_lseq x z)). Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z -> (x <= z)%Z). Proof. intros x y z H1 H2. apply infix_lseq_Zle. apply Zle_trans with y ; now apply infix_lseq_Zle. exact Zle_trans. Qed. (* Why3 goal *) Lemma Antisymm : forall (x:Z) (y:Z), (infix_lseq x y) -> ((infix_lseq y x) -> (x = y)). Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> ((y <= x)%Z -> (x = y)). Proof. intros x y H1 H2. apply Zle_antisym ; now apply infix_lseq_Zle. exact Zle_antisym. Qed. (* Why3 goal *) Lemma Total : forall (x:Z) (y:Z), (infix_lseq x y) \/ (infix_lseq y x). Lemma Total : forall (x:Z) (y:Z), (x <= y)%Z \/ (y <= x)%Z. Proof. intros x y. destruct (Zle_or_lt x y) as [H|H]. left. now apply infix_lseq_Zle. assumption. right. apply infix_lseq_Zle. now apply Zlt_le_weak. Qed. (* Why3 goal *) Lemma ZeroLessOne : (infix_lseq 0%Z 1%Z). Lemma ZeroLessOne : (0%Z <= 1%Z)%Z. Proof. apply Zle_lt_or_eq_iff. 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)). Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((x + z)%Z <= (y + z)%Z)%Z. Proof. intros x y z H. apply infix_lseq_Zle. apply Zplus_le_compat_r. now apply infix_lseq_Zle. exact Zplus_le_compat_r. Qed. (* 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))). Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z). Proof. intros x y z H1 H2. apply infix_lseq_Zle. apply Zmult_le_compat_r ; now apply infix_lseq_Zle. exact Zmult_le_compat_r. Qed.
 ... ... @@ -4,22 +4,22 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 goal *) Notation min := Zmin (only parsing). (* Why3 comment *) (* min is replaced with (Zmin x x1) by the coq driver *) (* Why3 goal *) Notation max := Zmax (only parsing). (* Why3 comment *) (* max is replaced with (Zmax x x1) by the coq driver *) (* Why3 goal *) Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (max x y))%Z /\ (y <= (max x y))%Z. Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\ (y <= (Zmax x y))%Z. split. apply Zle_max_l. apply Zle_max_r. Qed. (* Why3 goal *) Lemma Max_is_some : forall (x:Z) (y:Z), ((max x y) = x) \/ ((max x y) = y). Lemma Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y). intros x y. unfold Zmax. case Zcompare. ... ... @@ -29,15 +29,15 @@ now left. Qed. (* Why3 goal *) Lemma Min_is_le : forall (x:Z) (y:Z), ((min x y) <= x)%Z /\ ((min x y) <= y)%Z. Lemma Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\ ((Zmin x y) <= y)%Z. split. apply Zle_min_l. apply Zle_min_r. Qed. (* Why3 goal *) Lemma Min_is_some : forall (x:Z) (y:Z), ((min x y) = x) \/ ((min x y) = y). Lemma Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y). intros x y. unfold Zmin. case Zcompare. ... ... @@ -47,33 +47,33 @@ now right. Qed. (* Why3 goal *) Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((max x y) = x). Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x). exact Zmax_l. Qed. (* Why3 goal *) Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((max x y) = y). Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y). exact Zmax_r. Qed. (* Why3 goal *) Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((min x y) = x). Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x). exact Zmin_l. Qed. (* Why3 goal *) Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((min x y) = y). Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y). exact Zmin_r. Qed. (* Why3 goal *) Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((max x y) = (max y x)). Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)). intros x y _. apply Zmax_comm. Qed. (* Why3 goal *) Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((min x y) = (min y x)). Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)). intros x y _. apply Zmin_comm. Qed. ... ...
 ... ... @@ -5,14 +5,12 @@ Require Import Rbasic_fun. Require BuiltIn. Require real.Real. (* Why3 goal *) Definition abs: R -> R. exact Rabs. Defined. (* Why3 comment *) (* abs is replaced with (Rabs x) by the coq driver *) (* Why3 goal *) Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((abs x) = x)) /\ ((~ (0%R <= x)%R) -> ((abs x) = (-x)%R)). Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((Rabs x) = x)) /\ ((~ (0%R <= x)%R) -> ((Rabs x) = (-x)%R)). split ; intros H. apply Rabs_right. now apply Rle_ge. ... ... @@ -21,10 +19,10 @@ now apply Rnot_le_lt. Qed. (* 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), ((Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\ (x <= y)%R). intros x y. unfold abs, Rabs. unfold Rabs. case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]). rewrite <- (Ropp_involutive x). now apply Ropp_le_contravar. ... ... @@ -47,25 +45,25 @@ exact H1. Qed. (* Why3 goal *) Lemma Abs_pos : forall (x:R), (0%R <= (abs x))%R. Lemma Abs_pos : forall (x:R), (0%R <= (Rabs x))%R. exact Rabs_pos. Qed. (* Why3 goal *) Lemma Abs_sum : forall (x:R) (y:R), ((abs (x + y)%R) <= ((abs x) + (abs y))%R)%R. ((Rabs (x + y)%R) <= ((Rabs x) + (Rabs 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). ((Rabs (x * y)%R) = ((Rabs x) * (Rabs y))%R). exact Rabs_mult. Qed. (* Why3 goal *) Lemma triangular_inequality : forall (x:R) (y:R) (z:R),