Commit 6187ed56 authored by François Bobot's avatar François Bobot

Simplify euclidean to computer division

         make the proof using lemma function instead of coq
parent 496c821f
......@@ -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
......
This diff is collapsed.
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
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