...
  View open merge request
Commits (1)
This diff is collapsed.
This diff is collapsed.
...@@ -16,3 +16,4 @@ toy_compiler ...@@ -16,3 +16,4 @@ toy_compiler
vstte10_max_sum vstte10_max_sum
warshall_algorithm warshall_algorithm
zeros zeros
creal
...@@ -70,6 +70,15 @@ Lemma Exp_log : ...@@ -70,6 +70,15 @@ Lemma Exp_log :
exact exp_ln. exact exp_ln.
Qed. Qed.
(* Why3 goal *)
Lemma log_lt :
forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
(0%R < x)%R /\ (x < y)%R -> ((Reals.Rpower.ln x) < (Reals.Rpower.ln y))%R.
Proof.
intros x y (h1,h2).
exact (ln_increasing x y h1 h2).
Qed.
(* Why3 assumption *) (* Why3 assumption *)
Definition log2 (x:Reals.Rdefinitions.R) : Reals.Rdefinitions.R := Definition log2 (x:Reals.Rdefinitions.R) : Reals.Rdefinitions.R :=
((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R. ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
......
...@@ -67,3 +67,15 @@ intros x y (h1 & h2); apply sqrt_le_1; auto. ...@@ -67,3 +67,15 @@ intros x y (h1 & h2); apply sqrt_le_1; auto.
apply Rle_trans with x; auto. apply Rle_trans with x; auto.
Qed. Qed.
(* Why3 goal *)
Lemma Sqrt_lt :
forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
(0%R <= x)%R /\ (x < y)%R ->
((Reals.R_sqrt.sqrt x) < (Reals.R_sqrt.sqrt y))%R.
Proof.
intros x y (h1 & h2).
apply sqrt_lt_1; auto.
apply Rlt_le.
apply Rle_lt_trans with x; auto.
Qed.
...@@ -225,6 +225,10 @@ why3_vc Sqrt_le ...@@ -225,6 +225,10 @@ why3_vc Sqrt_le
using assms using assms
by auto by auto
why3_vc Sqrt_lt
using assms
by auto
why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult) why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult)
why3_vc Sqrt_square why3_vc Sqrt_square
...@@ -264,6 +268,10 @@ why3_vc Log_one by auto ...@@ -264,6 +268,10 @@ why3_vc Log_one by auto
why3_vc Exp_zero by auto why3_vc Exp_zero by auto
why3_vc Log_lt
using assms
by auto
why3_end why3_end
section {* Power of a real to an integer *} section {* Power of a real to an integer *}
......
...@@ -12,8 +12,8 @@ c2410d334c7e0852086bb13cae1189f601f3b1c6 real/Abs.xml ...@@ -12,8 +12,8 @@ c2410d334c7e0852086bb13cae1189f601f3b1c6 real/Abs.xml
da70a842eac8ff6687f1d119c309be4c227976ff real/MinMax.xml da70a842eac8ff6687f1d119c309be4c227976ff real/MinMax.xml
3cc6bd97503e596fae70c51ef1d5401a62114b94 real/FromInt.xml 3cc6bd97503e596fae70c51ef1d5401a62114b94 real/FromInt.xml
62beb9d22a9b5a94aaa55b8865e49320f5c776ff real/Truncate.xml 62beb9d22a9b5a94aaa55b8865e49320f5c776ff real/Truncate.xml
9ec1794c5e35cee3bc4d71a42be74fc89fb342fb real/Square.xml d2d3b1ce73c33b7c4a035c7b6040501aeec328fa real/Square.xml
6dc1b60c6ee9c4740643b7b5242808fadb22eae0 real/ExpLog.xml 5743213b73ad4549137da958ec3c1f1086fd0c75 real/ExpLog.xml
4194b7f0b6769a256bc38c0327d81a8e33264d21 real/Trigonometry.xml 4194b7f0b6769a256bc38c0327d81a8e33264d21 real/Trigonometry.xml
da4b981eb0a086bafef4994a856470521dc76f3a real/PowerInt.xml da4b981eb0a086bafef4994a856470521dc76f3a real/PowerInt.xml
23fc6a0ffa09725c78addb8391ed82ee08090d30 number/Divisibility.xml 23fc6a0ffa09725c78addb8391ed82ee08090d30 number/Divisibility.xml
......
...@@ -220,6 +220,9 @@ module Square ...@@ -220,6 +220,9 @@ module Square
axiom Sqrt_le : axiom Sqrt_le :
forall x y:real. 0.0 <= x <= y -> sqrt x <= sqrt y forall x y:real. 0.0 <= x <= y -> sqrt x <= sqrt y
axiom Sqrt_lt :
forall x y:real. 0.0 <= x < y -> sqrt x < sqrt y
end end
(** {2 Exponential and Logarithm} *) (** {2 Exponential and Logarithm} *)
...@@ -243,6 +246,8 @@ module ExpLog ...@@ -243,6 +246,8 @@ module ExpLog
axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x
axiom log_lt: forall x y:real. 0. < x < y -> log x < log y
function log2 (x : real) : real = log x / log 2.0 function log2 (x : real) : real = log x / log 2.0
function log10 (x : real) : real = log x / log 10.0 function log10 (x : real) : real = log x / log 10.0
......