Commit f573ce6c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

A few more lemmas on division and square root

parent 4c0d93f7
......@@ -91,6 +91,30 @@ Qed.
(* Why3 assumption *)
Definition infix_sl(x:R) (y:R): R := (infix_as x (inv y)).
(* Why3 goal *)
Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_pl x y) z) = (infix_pl (infix_sl x z) (infix_sl y z))).
intros.
unfold infix_sl, infix_as, infix_pl.
field.
Qed.
(* Why3 goal *)
Lemma sub_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_mn x y) z) = (infix_mn (infix_sl x z) (infix_sl y z))).
intros.
unfold infix_sl, infix_as, infix_mn, infix_pl, prefix_mn.
field.
Qed.
(* Why3 goal *)
Lemma neg_div : forall (x:R) (y:R), (~ (y = 0%R)) -> ((infix_sl (prefix_mn x)
y) = (prefix_mn (infix_sl x y))).
intros.
unfold infix_sl, infix_as, prefix_mn.
field.
Qed.
(* Why3 goal *)
Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
((infix_sl (infix_as x y) z) = (infix_as x (infix_sl y z))).
......
......@@ -29,4 +29,17 @@ Lemma Square_sqrt : forall (x:R), (0%R <= x)%R -> ((sqrt (x * x)%R) = x).
exact sqrt_square.
Qed.
(* Why3 goal *)
Lemma Sqrt_mul : forall (x:R) (y:R), ((0%R <= x)%R /\ (0%R <= y)%R) ->
((sqrt (x * y)%R) = ((sqrt x) * (sqrt y))%R).
intros x y (hx & hy); now apply sqrt_mult.
Qed.
(* Why3 goal *)
Lemma Sqrt_le : forall (x:R) (y:R), ((0%R <= x)%R /\ (x <= y)%R) ->
((sqrt x) <= (sqrt y))%R.
intros x y (h1 & h2); apply sqrt_le_1; auto.
apply Rle_trans with x; auto.
Qed.
......@@ -137,6 +137,15 @@ theory Field
axiom Inverse : forall x:t. x <> zero -> x * inv x = one
function (/) (x y : t) : t = x * inv y
lemma add_div :
forall x y z : t. z <> zero -> (x+y)/z = x/z + y/z
lemma sub_div :
forall x y z : t. z <> zero -> (x-y)/z = x/z - y/z
lemma neg_div :
forall x y : t. y <> zero -> (-x)/y = -(x/y)
lemma assoc_mul_div: forall x y z:t.
(* todo: discard the hypothesis ? *)
z <> zero -> (x*y)/z = x*(y/z)
......
......@@ -193,6 +193,13 @@ theory Square
axiom Square_sqrt:
forall x:real. x >= 0.0 -> sqrt (x*x) = x
axiom Sqrt_mul:
forall x y:real. x >= 0.0 /\ y >= 0.0 ->
sqrt (x*y) = sqrt x * sqrt y
axiom Sqrt_le :
forall x y:real. 0.0 <= x <= y -> sqrt x <= sqrt y
end
(** {2 Exponential and Logarithm} *)
......
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