...
  View open merge request
Commits (7)
......@@ -998,7 +998,7 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif
COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
COQLIBS_FOR_DRIVERS_FILES =
COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
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_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
......
......@@ -102,6 +102,13 @@ theory int.ComputerDivision
end
theory for_drivers.ComputerOfEuclideanDivision
remove prop cdiv_cases_0
remove prop cdiv_cases_1
end
theory real.Real
......
(** Why3 driver for Colibri (with floating point support) *)
prelude ";; produced by colibri.drv ;;"
prelude "(set-logic QF_NIRABVFP)"
prelude "(set-info :smt-lib-version 2.6)"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
(* import "discrimination.gen" *)
theory BuiltIn
meta "select_inst_default" "all"
meta "select_lskept_default" "all"
meta "select_lsinst_default" "all"
meta "select_kept_default" "all"
end
transformation "inline_trivial"
transformation "eliminate_builtin"
(* transformation "detect_polymorphism" because eliminate algebraic
add polymorphism *)
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(* Prepare for counter-example query: get rid of some quantifiers
(makes it possible to query model values of the variables in
premises) and introduce counter-example projections. Note: does
nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_quantifiers"
transformation "discriminate"
transformation "encoding_smt"
transformation "abstract_quantifiers"
(** Extra theories supported by COLIBRI *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory int.ComputerDivision
syntax function div "(colibri_cdiv %1 %2)"
syntax function mod "(colibri_crem %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.Truncate
syntax function floor "(to_int %1)"
syntax function truncate "(to_int (colibri_truncate %1))"
syntax function ceil "(to_int (colibri_ceil %1))"
remove prop Floor_down
remove prop Floor_monotonic
end
theory real.FromInt
syntax function from_int "(to_real %1)"
end
theory real.Abs
syntax function abs "(colibri_abs_real %1)"
end
theory int.Abs
syntax function abs "(colibri_abs_int %1)"
end
theory real.PowerInt
syntax function power "(colibri_pow_real_int %1 %2)"
end
theory int.Power
syntax function power "(colibri_pow_int_int %1 %2)"
end
theory real.ExpLog
syntax function exp "(colibri_exp %1)"
(* syntax function log "(colibri_ln %1)" *)
end
theory real.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
theory int.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
(** TODO *)
(**
- colibri_floor
- colibri_abs_int
- colibri_abs_real
- colibri_truncate
- colibri_pow_real_int
- colibri_max
- colibri_min
- is_int
- to_int
- to_real
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name=".."/>
<path name=".."/>
<path name="stdlib"/>
<path name="for_drivers.mlw"/>
<theory name="ComputerOfEuclideanDivision" proved="true">
<goal name="VC cdiv_cases_0" expl="VC for cdiv_cases_0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC cdiv_cases_0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC cdiv_cases_0.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.7" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="1.88"/></proof>
</goal>
<goal name="VC cdiv_cases_0.8" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="VC cdiv_cases_0.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC cdiv_cases_0.12" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.13" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC cdiv_cases_1" expl="VC for cdiv_cases_1" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC cdiv_cases_1.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC cdiv_cases_1.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.7" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.8" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC cdiv_cases_1.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC cdiv_cases_1.12" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.13" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="cdiv_cases" proved="true">
<transf name="split_vc" proved="true" >
<goal name="cdiv_cases.0" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="cdiv_cases.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="cmod_cases" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="EuclideanOfComputerDivision" proved="true">
<goal name="VC cdiv_cases_0" expl="VC for cdiv_cases_0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC cdiv_cases_0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC cdiv_cases_0.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.7" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="1.80"/></proof>
</goal>
<goal name="VC cdiv_cases_0.8" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="VC cdiv_cases_0.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_0.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC cdiv_cases_0.12" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_0.13" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC cdiv_cases_1" expl="VC for cdiv_cases_1" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC cdiv_cases_1.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC cdiv_cases_1.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.5" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.7" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_1.8" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC cdiv_cases_1.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC cdiv_cases_1.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_1.14" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC cdiv_cases_1.15" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC cdiv_cases_2" expl="VC for cdiv_cases_2" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC cdiv_cases_2.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC cdiv_cases_2.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_2.5" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.7" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.8" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC cdiv_cases_2.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC cdiv_cases_2.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC cdiv_cases_2.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC cdiv_cases_2.14" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC cdiv_cases_2.15" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
<goal name="ediv_cases" proved="true">
<transf name="split_vc" proved="true" >
<goal name="ediv_cases.0" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ediv_cases.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ediv_cases.2" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="emod_cases" proved="true">
<transf name="split_vc" proved="true" >
<goal name="emod_cases.0" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="emod_cases.1" proved="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="emod_cases.2" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* 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:Numbers.BinNums.Z) (d:Numbers.BinNums.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:Numbers.BinNums.Z) (d:Numbers.BinNums.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.
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.
......@@ -135,6 +135,29 @@ version_old = "1.0"
driver = "cvc4"
command = "%e --lang=smt2 %f"
# COLIBRI with counterexamples
[ATP colibri-ce]
name = "COLIBRI"
alternative = "counterexamples"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# COLIBRI
[ATP colibri]
name = "COLIBRI"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# Psyche version 2.x
[ATP psyche]
name = "Psyche"
......
......@@ -34,5 +34,5 @@ let elim_less (d:decl) =
let () =
Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
~desc:"Abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context \
~desc:"Weaken quantifiers@ by replacing them by true or false in@ the@ axioms@ of@ the@ context \
and@ the@ goals."
theory ComputerOfEuclideanDivision
use int.Int
use int.Abs
use int.EuclideanDivision as ED
use int.ComputerDivision as CD
let lemma cdiv_cases_0 (n d:int)
requires { n >= 0 }
requires { d <> 0 }
ensures { CD.div n d = ED.div n d } =
assert { (ED.div n d) * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod n d) < abs d };
assert { 0 <= (CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d - ED.mod n d) < abs d };
assert { (ED.div n d - CD.div n d) * d = (CD.mod n d - ED.mod n d) };
if (ED.div n d - CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div n d - CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
let lemma cdiv_cases_1 (n d:int)
requires { n <= 0 }
requires { d <> 0 }
ensures { CD.div n d = - (ED.div (-n) d) } =
assert { -((ED.div (-n) d) * d + (ED.mod (-n) d)) = -(-n) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod (-n) d) < abs d };
assert { 0 <= -(CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d + ED.mod (-n) d) < abs d };
assert { (ED.div (-n) d + CD.div n d) * d + (CD.mod n d + ED.mod (-n) d) = 0 };
if (ED.div (-n) d + CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div (-n) d + CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
lemma cdiv_cases : forall n d:int [CD.div n d].
((n >= 0) -> (d > 0) -> CD.div n d = ED.div n d) /\
((n <= 0) -> (d > 0) -> CD.div n d = -(ED.div (-n) d)) /\
((n >= 0) -> (d < 0) -> CD.div n d = -(ED.div n (-d))) /\
((n <= 0) -> (d < 0) -> CD.div n d = ED.div (-n) (-d))
((n >= 0) -> (d <> 0) -> CD.div n d = ED.div n d) /\
((n <= 0) -> (d <> 0) -> CD.div n d = -(ED.div (-n) d))
lemma cmod_cases : forall n d:int [CD.mod n d].
((n >= 0) -> (d > 0) -> CD.mod n d = ED.mod n d) /\
((n <= 0) -> (d > 0) -> CD.mod n d = -(ED.mod (-n) d)) /\
((n >= 0) -> (d < 0) -> CD.mod n d = (ED.mod n (-d))) /\
((n <= 0) -> (d < 0) -> CD.mod n d = -(ED.mod (-n) (-d)))
((n >= 0) -> (d <> 0) -> CD.mod n d = ED.mod n d) /\
((n <= 0) -> (d <> 0) -> CD.mod n d = -(ED.mod (-n) d))
end
theory EuclideanOfComputerDivision
use int.Int
use int.Abs
use int.EuclideanDivision as ED
use int.ComputerDivision as CD
let lemma cdiv_cases_0 (n d:int)
requires { n >= 0 }
requires { d <> 0 }
ensures { CD.div n d = ED.div n d } =
assert { (ED.div n d) * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod n d) < abs d };
assert { 0 <= (CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d - ED.mod n d) < abs d };
assert { (ED.div n d - CD.div n d) * d = (CD.mod n d - ED.mod n d) };
if (ED.div n d - CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div n d - CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
let lemma cdiv_cases_1 (n d:int)
requires { n <= 0 }
requires { d > 0 }
ensures { CD.div n d - (if CD.mod n d = 0 then 0 else 1) = ED.div n d } =
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
if CD.mod n d = 0 then begin
()
end else begin
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d - 1) * d + (CD.mod n d + d) };
assert { abs d = d };
assert { 0 <= ED.mod n d < d };
assert { 0 < -(CD.mod n d) < d };
assert { 0 < CD.mod n d + d < d };
assert { -d < - CD.mod n d - d + ED.mod n d < d };
assert { (ED.div n d - (CD.div n d - 1)) * d + (- CD.mod n d - d + ED.mod n d) = 0 };
if (ED.div n d - (CD.div n d - 1)) > 0 then begin
absurd
end
else if (ED.div n d - (CD.div n d - 1)) < 0 then begin
absurd
end
else
()
end
let lemma cdiv_cases_2 (n d:int)
requires { n <= 0 }
requires { d < 0 }
ensures { CD.div n d + (if CD.mod n d = 0 then 0 else 1) = ED.div n d } =
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
if CD.mod n d = 0 then begin
()
end else begin
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d + 1) * d + (CD.mod n d - d) };
assert { abs d = -d };
assert { 0 <= ED.mod n d < -d };
assert { 0 < -(CD.mod n d) < -d };
assert { d < - CD.mod n d + d < 0 };
assert { d < - CD.mod n d + d + ED.mod n d < -d };
assert { (ED.div n d - (CD.div n d + 1)) * d + (- CD.mod n d + d + ED.mod n d) = 0 };
if (ED.div n d - (CD.div n d + 1)) > 0 then begin
absurd
end
else if (ED.div n d - (CD.div n d + 1)) < 0 then begin
absurd
end
else
()
end
lemma ediv_cases : forall n d:int [ED.div n d].
((n >= 0) -> (d <> 0) -> ED.div n d = CD.div n d) /\
((n <= 0) -> (d > 0) -> ED.div n d = CD.div n d - (if CD.mod n d = 0 then 0 else 1)) /\
((n <= 0) -> (d < 0) -> ED.div n d = CD.div n d + (if CD.mod n d = 0 then 0 else 1))
lemma emod_cases : forall n d:int [ED.mod n d].
((n >= 0) -> (d <> 0) -> ED.mod n d = CD.mod n d) /\
((n <= 0) -> (d > 0) -> ED.mod n d = CD.mod n d + (if CD.mod n d = 0 then 0 else d)) /\
((n <= 0) -> (d < 0) -> ED.mod n d = CD.mod n d - (if CD.mod n d = 0 then 0 else d))
end