Commit 24d6caf1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Complete the Coq realizations of theory real.

parent 62c66d4a
......@@ -61,6 +61,13 @@ Proof.
exact opp_IZR.
Qed.
(* Why3 goal *)
Lemma Injective :
forall (x:Z) (y:Z), ((BuiltIn.IZR x) = (BuiltIn.IZR y)) -> (x = y).
Proof.
exact eq_IZR.
Qed.
(* Why3 goal *)
Lemma Monotonic :
forall (x:Z) (y:Z), (x <= y)%Z -> ((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
......
......@@ -16,7 +16,10 @@ Require Reals.Rtrigo_def.
Require Reals.Rpower.
Require Reals.R_sqrt.
Require BuiltIn.
Require int.Int.
Require int.Power.
Require real.Real.
Require real.FromInt.
Require real.Square.
Require real.ExpLog.
......@@ -109,3 +112,17 @@ replace (5 / 10)%R with (/ 2)%R by field.
now apply Rpower_sqrt.
Qed.
(* Why3 goal *)
Lemma pow_from_int :
forall (x:Z) (y:Z), (0%Z < x)%Z -> (0%Z <= y)%Z ->
((Reals.Rpower.Rpower (BuiltIn.IZR x) (BuiltIn.IZR y)) =
(BuiltIn.IZR (int.Power.power x y))).
Proof.
intros x y h1 h2.
rewrite <- Z2Nat.id with (1 := h2).
rewrite <- pow_IZR.
rewrite <- INR_IZR_INZ.
apply Rpower_pow.
now apply IZR_lt.
Qed.
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