...
  View open merge request
Commits (1)
This diff is collapsed.
This diff is collapsed.
......@@ -16,3 +16,4 @@ toy_compiler
vstte10_max_sum
warshall_algorithm
zeros
creal
......@@ -70,6 +70,15 @@ Lemma Exp_log :
exact exp_ln.
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 *)
Definition log2 (x:Reals.Rdefinitions.R) : Reals.Rdefinitions.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.
apply Rle_trans with x; auto.
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
using assms
by auto
why3_vc Sqrt_lt
using assms
by auto
why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult)
why3_vc Sqrt_square
......@@ -264,6 +268,10 @@ why3_vc Log_one by auto
why3_vc Exp_zero by auto
why3_vc Log_lt
using assms
by auto
why3_end
section {* Power of a real to an integer *}
......
......@@ -12,8 +12,8 @@ c2410d334c7e0852086bb13cae1189f601f3b1c6 real/Abs.xml
da70a842eac8ff6687f1d119c309be4c227976ff real/MinMax.xml
3cc6bd97503e596fae70c51ef1d5401a62114b94 real/FromInt.xml
62beb9d22a9b5a94aaa55b8865e49320f5c776ff real/Truncate.xml
9ec1794c5e35cee3bc4d71a42be74fc89fb342fb real/Square.xml
6dc1b60c6ee9c4740643b7b5242808fadb22eae0 real/ExpLog.xml
d2d3b1ce73c33b7c4a035c7b6040501aeec328fa real/Square.xml
5743213b73ad4549137da958ec3c1f1086fd0c75 real/ExpLog.xml
4194b7f0b6769a256bc38c0327d81a8e33264d21 real/Trigonometry.xml
da4b981eb0a086bafef4994a856470521dc76f3a real/PowerInt.xml
23fc6a0ffa09725c78addb8391ed82ee08090d30 number/Divisibility.xml
......
......@@ -220,6 +220,9 @@ module Square
axiom Sqrt_le :
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
(** {2 Exponential and Logarithm} *)
......@@ -243,6 +246,8 @@ module ExpLog
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 log10 (x : real) : real = log x / log 10.0
......