Commit 3d744048 by François Bobot

### Add algorithms for computational real operations

` - addition, subtraction, division, square-root`
parent e5b91996
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 ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!