Commit 5971a083 authored by François Bobot's avatar François Bobot

[Realize] ComputerofEuclidianDivision

parent 6689cec7
...@@ -938,7 +938,9 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64 ...@@ -938,7 +938,9 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES)) COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif endif
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
drivers/coq-realizations.aux: Makefile drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@' $(SHOW) 'Generate $@'
...@@ -969,9 +971,11 @@ drivers/coq-realizations.aux: Makefile ...@@ -969,9 +971,11 @@ drivers/coq-realizations.aux: Makefile
echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \ echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \ for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \ echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FOR_DRIVER_FILES); do \
echo 'theory for_driver.'"$$f"' meta "realized_theory" "for_driver.'"$$f"'", "" end'; done; \
) > $@ ) > $@
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float update-coq-for-drivers
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
...@@ -1009,6 +1013,9 @@ update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux ...@@ -1009,6 +1013,9 @@ update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
update-coq-for-drivers: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/for_drivers.why
for f in $(COQLIBS_FOR_DRIVERS_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T for_drivers.$$f -o $(GENERATED_PREFIX_COQ)/for_drivers/; done
ifeq (@enable_coq_support@,yes) ifeq (@enable_coq_support@,yes)
......
...@@ -53,4 +53,7 @@ theory ComputerDivTest ...@@ -53,4 +53,7 @@ theory ComputerDivTest
goal smoke5 : div_m1_m2 = -1 goal smoke5 : div_m1_m2 = -1
goal smoke6 : mod_m1_m2 = 1 goal smoke6 : mod_m1_m2 = 1
end goal div_pos_neg: forall x y. x>=0 -> y<0 -> div x y <= 0
\ No newline at end of file
end
...@@ -338,7 +338,7 @@ ...@@ -338,7 +338,7 @@
<proof prover="26"><result status="timeout" time="1.00"/></proof> <proof prover="26"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ComputerDivTest" sum="a20f961d6e8e381a10b2bd458c94d3f3" expanded="true"> <theory name="ComputerDivTest" sum="d74573be376d2c764268607b65efce26" expanded="true">
<goal name="ok1" expl=""> <goal name="ok1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
...@@ -647,6 +647,9 @@ ...@@ -647,6 +647,9 @@
<proof prover="25"><result status="unknown" time="0.14"/></proof> <proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof> <proof prover="26"><result status="timeout" time="1.00"/></proof>
</goal> </goal>
<goal name="div_pos_neg" expl="" expanded="true">
<proof prover="11" timelimit="50" edited="div-ComputerDivTest-div_pos_neg_2.why" obsolete="true"><undone/></proof>
</goal>
</theory> </theory>
</file> </file>
</why3session> </why3session>
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Lemma on_pos_euclidean_is_div:
forall n d, (int.EuclideanDivision.div n (Zpos d)) = Zdiv n (Zpos d).
intros n d.
unfold EuclideanDivision.div.
assert (0 < Z.pos d)%Z by reflexivity.
destruct (Z.mod_pos_bound n (Zpos d) H).
case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* reflexivity.
* destruct (H2 H0).
Qed.
(* Why3 goal *)
Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n
(-d)%Z))%Z))) /\ ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z
(-d)%Z)))))).
intros n d.
destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
rewrite Z.mul_1_l.
reflexivity.
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
destruct (Z.pos n / Z.pos d)%Z;reflexivity.
Qed.
(* Why3 goal *)
Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z)))) /\
((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
(-d)%Z))%Z))))).
intros n d.
unfold int.EuclideanDivision.mod1.
SearchAbout Z.rem Z.quot.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d).
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
intuition.
+ rewrite H1.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_r.
omega.
+ rewrite H1.
rewrite Z.mul_opp_r.
rewrite Z.mul_opp_l.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_l.
omega.
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