Commit d8c37c5c authored by MARCHE Claude's avatar MARCHE Claude

fixed generation of headers for Coq realizations

parent 4c401f16
......@@ -88,3 +88,4 @@ intros a a_WT l.
rewrite 2!Length.length_std.
now rewrite List.rev_length.
Qed.
......@@ -326,3 +326,4 @@ assert (occ v m (i+1) n >= 1)%Z.
omega.
generalize (Hocc v); omega.
Qed.
......@@ -47,3 +47,4 @@ generalize (map.Occ.occ_exists v a1 l u H).
intros (j, (hj1,hj2)).
exists j; intuition.
Qed.
......@@ -267,3 +267,4 @@ replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
rewrite <- h0. trivial. omega. omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring. assumption.
Qed.
......@@ -95,3 +95,4 @@ apply Z.gcd_unique.
rewrite coprime_is_Zrel_prime in h1.
now apply Znumtheory.rel_prime_div with (2:=h2).
Qed.
......@@ -226,3 +226,4 @@ elim H.
now apply -> even_divides.
exact H0.
Qed.
......@@ -158,3 +158,4 @@ apply Zgcd_is_pos.
apply Zis_gcd_mult.
apply Zgcd_is_gcd.
Qed.
......@@ -122,3 +122,4 @@ Proof.
intros k.
now exists k.
Qed.
......@@ -189,3 +189,4 @@ apply proj2 in Pp.
apply Pp.
omega.
Qed.
......@@ -82,3 +82,4 @@ intros x y z.
replace (x - z)%R with ((x - y) + (y - z))%R by ring.
apply Rabs_triang.
Qed.
......@@ -69,3 +69,4 @@ Definition log2 (x:R): R := ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
(* Why3 assumption *)
Definition log10 (x:R): R :=
((Reals.Rpower.ln x) / (Reals.Rpower.ln 10%R))%R.
......@@ -52,3 +52,4 @@ Lemma Neg : forall (x:Z),
((Reals.Raxioms.IZR (-x)%Z) = (-(Reals.Raxioms.IZR x))%R).
exact opp_IZR.
Qed.
......@@ -117,3 +117,4 @@ apply eq_sym, Rmax_left.
apply Rmax_case ; now apply Rlt_le.
now apply Rlt_le.
Qed.
......@@ -113,3 +113,4 @@ apply Hind; omega.
replace 1%R with (1*1)%R by auto with real.
apply Rmult_le_compat; auto with real.
Qed.
......@@ -91,3 +91,4 @@ intros x h1.
replace (5 / 10)%R with (/ 2)%R by field.
now apply Rpower_sqrt.
Qed.
......@@ -235,3 +235,4 @@ Proof.
intros x y z H Zz.
now apply Rmult_le_compat_r.
Qed.
......@@ -14,3 +14,4 @@
Require Import BuiltIn.
Require BuiltIn.
Require real.Real.
......@@ -57,3 +57,4 @@ Lemma Sqrt_le : forall (x:R) (y:R), ((0%R <= x)%R /\ (x <= y)%R) ->
intros x y (h1 & h2); apply sqrt_le_1; auto.
apply Rle_trans with x; auto.
Qed.
......@@ -194,3 +194,4 @@ Proof.
intros x.
apply atan_right_inv.
Qed.
......@@ -243,3 +243,4 @@ Lemma all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem x
Proof.
now intros a a_WT x.
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