Commit 59586b88 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix axioms of int.Exponentiation and realize it in Coq.

Remove axioms from int.Power realization.
parent 4325b20b
......@@ -866,7 +866,8 @@ endif
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax Power
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
......@@ -939,7 +940,7 @@ clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_INT_ALL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Definition unit := unit.
Parameter fib: Z -> Z.
Axiom fib0 : ((fib 0%Z) = 0%Z).
Axiom fib1 : ((fib 1%Z) = 1%Z).
......@@ -33,33 +18,49 @@ Axiom fib1 : ((fib 1%Z) = 1%Z).
Axiom fibn : forall (n:Z), (2%Z <= n)%Z ->
((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z).
(* Why3 assumption *)
Inductive t :=
| mk_t : Z -> Z -> Z -> Z -> t .
Axiom t_WhyType : WhyType t.
Existing Instance t_WhyType.
Definition a11(u:t): Z := match u with
| (mk_t a111 _ _ _) => a111
(* Why3 assumption *)
Definition a22(v:t): Z := match v with
| (mk_t x x1 x2 x3) => x3
end.
Definition a12(u:t): Z := match u with
| (mk_t _ a121 _ _) => a121
(* Why3 assumption *)
Definition a21(v:t): Z := match v with
| (mk_t x x1 x2 x3) => x2
end.
Definition a21(u:t): Z := match u with
| (mk_t _ _ a211 _) => a211
(* Why3 assumption *)
Definition a12(v:t): Z := match v with
| (mk_t x x1 x2 x3) => x1
end.
Definition a22(u:t): Z := match u with
| (mk_t _ _ _ a221) => a221
(* Why3 assumption *)
Definition a11(v:t): Z := match v with
| (mk_t x x1 x2 x3) => x
end.
(* Why3 assumption *)
Definition mult(x:t) (y:t): t :=
(mk_t (((a11 x) * (a11 y))%Z + ((a12 x) * (a21 y))%Z)%Z
(((a11 x) * (a12 y))%Z + ((a12 x) * (a22 y))%Z)%Z
(((a21 x) * (a11 y))%Z + ((a22 x) * (a21 y))%Z)%Z
(((a21 x) * (a12 y))%Z + ((a22 x) * (a22 y))%Z)%Z).
Parameter power: t -> Z -> t.
Axiom Assoc : forall (x:t) (y:t) (z:t), ((mult (mult x y) z) = (mult x
(mult y z))).
Axiom Unit_def_l : forall (x:t), ((mult (mk_t 1%Z 0%Z 0%Z 1%Z) x) = x).
Axiom Unit_def_r : forall (x:t), ((mult x (mk_t 1%Z 0%Z 0%Z 1%Z)) = x).
Axiom Comm : forall (x:t) (y:t), ((mult x y) = (mult y x)).
Parameter power: t -> Z -> t.
Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
......@@ -68,29 +69,30 @@ Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
Axiom Power_1 : forall (x:t), ((power x 1%Z) = x).
Axiom Power_sum : forall (x:t) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((power x (n + m)%Z) = (mult (power x n) (power x m))).
Axiom Power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = (mult (power x n) (power x m)))).
Axiom Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n * m)%Z) = (power (power x n) m))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Axiom Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z -> ((power (mult x
y) n) = (mult (power x n) (power y n))).
(* Why3 goal *)
Theorem WP_parameter_logfib : forall (n:Z), (0%Z <= n)%Z -> ((~ (n = 0%Z)) ->
((((0%Z <= n)%Z /\ ((int.EuclideanDivision.div n 2%Z) < n)%Z) /\
((((0%Z <= n)%Z /\ ((int.EuclideanDivision.div n 2%Z) < n)%Z) /\
(0%Z <= (int.EuclideanDivision.div n 2%Z))%Z) -> forall (result:Z)
(result1:Z), ((power (mk_t 1%Z 1%Z 1%Z 0%Z) (int.EuclideanDivision.div n
2%Z)) = (mk_t (result + result1)%Z result1 result1 result)) ->
((((int.EuclideanDivision.mod1 n 2%Z) = 0%Z) -> match (
((result * result)%Z + (result1 * result1)%Z)%Z,
(result1 * (result + (result + result1)%Z)%Z)%Z) with
| (a, b) => ((power (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a + b)%Z b b a))
end) /\ ((~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> match (
(result1 * (result + (result + result1)%Z)%Z)%Z,
(((result + result1)%Z * (result + result1)%Z)%Z + (result1 * result1)%Z)%Z) with
| (a, b) => ((power (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a + b)%Z b b a))
end)))).
((((int.EuclideanDivision.mod1 n 2%Z) = 0%Z) -> let a :=
((result * result)%Z + (result1 * result1)%Z)%Z in let b :=
(result1 * (result + (result + result1)%Z)%Z)%Z in ((power (mk_t 1%Z 1%Z
1%Z 0%Z) n) = (mk_t (a + b)%Z b b a))) /\
((~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> let a :=
(result1 * (result + (result + result1)%Z)%Z)%Z in let b :=
(((result + result1)%Z * (result + result1)%Z)%Z + (result1 * result1)%Z)%Z in
((power (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a + b)%Z b b a)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
Import EuclideanDivision.
intros.
......@@ -100,11 +102,10 @@ intuition.
rewrite H4 in H3.
rewrite H3.
replace (2 * div n 2 + 0)%Z with (div n 2 + div n 2)%Z by omega.
rewrite Power_sum.
rewrite Power_sum by exact H5.
rewrite H2; simpl.
unfold mult; simpl.
apply f_equal4; ring.
intuition.
generalize (Mod_bound n 2 h)%Z.
simpl.
......@@ -114,14 +115,12 @@ rewrite h' in H3.
rewrite H3.
replace (2 * div n 2 + 1)%Z with ((div n 2 + div n 2) + 1)%Z by omega.
rewrite Power_s.
rewrite Power_sum.
rewrite Power_sum by exact H5.
rewrite H2; simpl.
unfold mult at 2; simpl.
unfold mult.
apply f_equal4; unfold a11, a12, a21, a22; try ring.
intuition.
omega.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
......@@ -12,16 +12,17 @@ Require int.Power.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Implicit Arguments contents.
Import int.ComputerDivision.
Import Power.
......@@ -43,10 +44,10 @@ rewrite h5; clear h5.
intros.
rewrite <- h3; clear h3.
rewrite H0 at 2. clear H0.
rewrite Power_sum. 2:omega.
replace (2 * (e / 2))%Z with (e/2 + e/2)%Z by omega.
rewrite Power_sum. 2:omega.
rewrite Power_mult2. 2:omega.
rewrite Power_sum by omega.
replace (2 * (e / 2))%Z with (e/2 + e/2)%Z by ring.
rewrite Power_sum by apply H.
rewrite Power_mult2 by apply H.
rewrite Power_1.
ring.
Qed.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Section Exponentiation.
(* Why3 goal *)
Variable t : Type.
Hypothesis t_WhyType : WhyType t.
Existing Instance t_WhyType.
(* Why3 goal *)
Variable one: t.
(* Why3 goal *)
Variable infix_as: t -> t -> t.
(* Why3 goal *)
Hypothesis Assoc : forall (x:t) (y:t) (z:t), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))).
(* Why3 goal *)
Hypothesis Unit_def_l : forall (x:t), ((infix_as one x) = x).
(* Why3 goal *)
Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x).
(* Why3 goal *)
Hypothesis Comm : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)).
(* Why3 goal *)
Definition power: t -> Z -> t.
intros x n.
exact (iter_nat (Zabs_nat n) t (fun acc => infix_as x acc) one).
Defined.
(* Why3 goal *)
Lemma Power_0 : forall (x:t), ((power x 0%Z) = one).
Proof.
easy.
Qed.
(* Why3 goal *)
Lemma Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (infix_as x (power x n))).
Proof.
intros x n h1.
unfold power.
fold (Zsucc n).
now rewrite Zabs_nat_Zsucc.
Qed.
(* Why3 goal *)
Lemma Power_1 : forall (x:t), ((power x 1%Z) = x).
Proof.
exact Unit_def_r.
Qed.
(* Why3 goal *)
Lemma Power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = (infix_as (power x n) (power x m)))).
Proof.
intros x n m Hn Hm.
revert n Hn.
apply natlike_ind.
apply sym_eq, Unit_def_l.
intros n Hn IHn.
replace (Zsucc n + m)%Z with ((n + m) + 1)%Z by ring.
rewrite Power_s by auto with zarith.
rewrite IHn.
now rewrite <- Assoc, <- Power_s.
Qed.
(* Why3 goal *)
Lemma Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n * m)%Z) = (power (power x n) m))).
Proof.
intros x n m Hn Hm.
revert m Hm.
apply natlike_ind.
now rewrite Zmult_0_r, 2!Power_0.
intros m Hm IHm.
replace (n * Zsucc m)%Z with (n * m + n)%Z by ring.
rewrite Power_sum by auto with zarith.
rewrite IHm.
now rewrite Comm, <- Power_s.
Qed.
(* Why3 goal *)
Lemma Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z ->
((power (infix_as x y) n) = (infix_as (power x n) (power y n))).
Proof.
intros x y.
apply natlike_ind.
apply sym_eq.
rewrite 3!Power_0.
apply Unit_def_r.
intros n Hn IHn.
unfold Zsucc.
rewrite 3!(Power_s _ _ Hn).
rewrite IHn.
now rewrite Assoc, <- (Assoc y), (Comm y), 2!Assoc.
Qed.
End Exponentiation.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require Import Exponentiation.
(* Why3 goal *)
Definition power: Z -> Z -> Z.
Admitted.
Notation power := Zpower.
Lemma power_is_exponentiation :
forall x n, (0 <= n)%Z -> power x n = Exponentiation.power _ 1%Z Zmult x n.
Proof.
intros x [|n|n] H.
easy.
2: now elim H.
unfold Exponentiation.power, power, Zpower_pos.
now rewrite iter_nat_of_P.
Qed.
(* Why3 goal *)
Lemma Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
Proof.
intros x.
Admitted.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma Power_s : forall (x:Z) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (x * (power x n))%Z).
Proof.
intros x n h1.
Admitted.
rewrite Zpower_exp.
change (power x 1) with (x * 1)%Z.
ring.
now apply Zle_ge.
easy.
Qed.
(* Why3 goal *)
Lemma Power_1 : forall (x:Z), ((power x 1%Z) = x).
intros x.
Admitted.
Proof.
exact Zmult_1_r.
Qed.
(* Why3 goal *)
Lemma Power_sum : forall (x:Z) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((power x (n + m)%Z) = ((power x n) * (power x m))%Z).
intros x n m (Hn, Hm).
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring.
replace (n+n0)%Z with ((n+n0-1)+1)%Z by omega.
rewrite Power_s; auto with zarith.
replace (n+n0-1)%Z with (n+(n0-1))%Z by omega.
rewrite Hind; auto with zarith.
replace (power x n0) with (power x ((n0-1)+1)%Z).
rewrite (Power_s x (n0-1)%Z).
ring.
omega.
apply f_equal2; auto.
omega.
Lemma Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
Proof.
intros x n m Hn Hm.
now apply Zpower_exp; apply Zle_ge.
Qed.
(* Why3 goal *)
Lemma Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n * m)%Z) = (power (power x n) m))).
Proof.
intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
subst n0; rewrite Power_0; ring_simplify (n * 0)%Z.
apply Power_0.
replace (n*n0)%Z with (n*(n0-1)+n)%Z by ring.
rewrite Power_sum; auto with zarith.
rewrite Hind; auto with zarith.
rewrite <- (Power_1 (power x n)) at 2.
rewrite <- Power_sum; auto with zarith.
ring_simplify (n0 - 1 + 1)%Z; auto.
rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult ; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
Proof.
intros x y n Hn.
generalize Hn.
pattern n.
apply natlike_ind; auto.
intros; do 3 rewrite Power_0.
omega.
intros.
replace (Zsucc x0) with (x0+1)%Z by omega.
rewrite Power_s.
2:omega.
rewrite (Power_s x x0).
rewrite (Power_s y x0).
rewrite H0.
ring.
omega.
omega.
omega.
rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
Qed.
......@@ -190,6 +190,7 @@ theory Exponentiation
type t
constant one : t
function (*) t t : t
clone algebra.CommutativeMonoid with type t = t, constant unit = one, function op = (*)
function power t int : t
......@@ -199,7 +200,7 @@ theory Exponentiation
lemma Power_1 : forall x : t. power x 1 = x
lemma Power_sum : forall x: t, n m: int. n >= 0 /\ m >= 0 ->
lemma Power_sum : forall x: t, n m: int. 0 <= n -> 0 <= m ->
power x (n+m) = power x n * power x m
lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
......@@ -216,8 +217,10 @@ theory Power
use import Int
clone export
Exponentiation with type t = int, constant one = one, function (*) = (*)
clone export Exponentiation with type t = int, constant one = one,
function (*) = (*), goal CommutativeMonoid.Assoc,
goal CommutativeMonoid.Unit_def_l, goal CommutativeMonoid.Unit_def_r,
goal CommutativeMonoid.Comm.Comm
end
......
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