Commit d4fbc21f authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Decision procedure on algebras

parent 06da7413
......@@ -77,21 +77,13 @@ let ghost function append_mon (m1 m2:m)
let rec ghost function mul_mon (x:t') (mon:m) : t'
ensures { forall y.
interp' result y = C.( *) (interp' x y) (interp' (Cons mon Nil) y) } =
match x with
interp' result y = C.( *) (interp' x y) (interp' (Cons mon Nil) y) }
= match x with
| Nil -> Nil
| Cons m r ->
let mr = append_mon m mon in
let lr = mul_mon r mon in
let res = Cons mr lr in
assert { forall y. interp' res y
= C.(+) (interp' (Cons mr Nil) y) (interp' lr y)
= C.(+) (C.( *) (interp' (Cons m Nil) y) (interp' (Cons mon Nil) y))
(C.( *) (interp' r y) (interp' (Cons mon Nil) y))
= C.( *) (C.(+) (interp' (Cons m Nil) y) (interp' r y))
(interp' (Cons mon Nil) y)
= C.( *) (interp' x y) (interp' (Cons mon Nil) y) };
res
Cons mr lr
end
let rec ghost function mul_devel (x1 x2:t') : t'
......@@ -253,7 +245,7 @@ constant x9 : t = Mul x3 x3
constant x10 : t = Mul x4 x4
meta "compute_max_steps" 0x10000000
(*
goal d: eq' (conv z1) (conv z2)
goal d': eq' (conv z1) (conv z2) by normalize (conv z1) = normalize (conv z2)
......@@ -285,6 +277,8 @@ constant g6 : t = Mul g4 x5
goal devel_6 : eq g3 g4
goal devel_conv_6: eq' (conv g3) (conv g4)
goal devel_conv_6_norm: eq' (conv g3) (conv g4) by normalize (conv g3) = normalize (conv g4)
*)
(*
goal devel_7 : eq g5 g6
goal devel_conv_7: eq' (conv g5) (conv g6)
......@@ -292,4 +286,217 @@ goal devel_conv_7_norm: eq' (conv g5) (conv g6) by normalize (conv g5) = normali
*)
end
module AssocAlgebra
type r
type a
function (+) a a : a
function ( *) a a : a
clone algebra.UnitaryCommutativeRing as R with type t = r
clone algebra.Ring as A with type t = a, function (+) = (+), function (*) = (*)
constant one : a
constant zero : a = A.zero
axiom AUnitary : forall x:a. one * x = x * one = x
axiom ANonTrivial : A.zero <> one
(* A is an associative algebra over R *)
function (@) r a : a
axiom ExtDistSumA : forall r: r, x y: a. r @ (x + y) = r @ x + r @ y
axiom ExtDistSumR : forall r s: r, x: a. (R.(+) r s)@x = r@x + s@x
axiom AssocMulExt : forall r s: r, x: a. (R.( *) r s)@x = r@(s@x)
axiom UnitExt : forall x: a. R.one @ x = x
axiom CommMulExt : forall r: r, x y: a. r@(x*y) = (r@x)*y = x*(r@y)
val predicate eq0 (r: r) ensures { result <-> r = R.zero }
end
module AssocAlgebraDecision
use import int.Int
use import list.List
use import AssocAlgebra as AA
type t = Var int | Add t t | Mul t t | Ext r t
type vars = int -> a
function interp (x: t) (y: vars) : a =
match x with
| Var n -> y n
| Add x1 x2 -> interp x1 y + interp x2 y
| Mul x1 x2 -> interp x1 y * interp x2 y
| Ext r x -> AA.(@) r (interp x y)
end
predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y
(** Conversion to sum of monomials *)
type m = M r (list int)
type t' = list m
function mon (x: list int) (y: vars) : a =
match x with
| Nil -> AA.one
| Cons x l -> y x * mon l y
end
function interp' (x: t') (y: vars) : a =
match x with
| Nil -> AA.zero
| Cons (M r m) l -> (AA.(@) r (mon m y)) + interp' l y end
predicate eq_mon (m1 m2: list int) = forall y: vars. mon m1 y = mon m2 y
predicate eq' (x1 x2: t') = forall y: vars. interp' x1 y = interp' x2 y
use import list.Append
use import list.Length
let rec lemma mon_append (x1 x2: list int) (y: vars)
ensures { mon (x1 ++ x2) y = mon x1 y * mon x2 y }
variant { x1 }
= match x1 with Nil -> () | Cons _ x -> mon_append x x2 y end
lemma interp_cons : forall m:m, x:t', y:vars.
interp' (Cons m x) y = interp' x y + interp' (Cons m Nil) y
let rec lemma interp_sum (x1 x2: t') (y: vars)
ensures { interp' (x1++x2) y = interp' x1 y + interp' x2 y }
variant { x1 }
= match x1 with
| Nil -> ()
| Cons _ x -> interp_sum x x2 y end
let ghost function append_mon (m1 m2:m)
ensures { forall y. interp' (Cons result Nil) y
= interp' (Cons m1 Nil) y * interp' (Cons m2 Nil) y }
= match m1,m2 with M r1 l1, M r2 l2 -> M (R.( *) r1 r2) (l1 ++ l2) end
let rec ghost function mul_mon (mon: m) (x:t'): t' (* mon*x *)
ensures { forall y. interp' result y = interp' (Cons mon Nil) y * interp' x y }
= match x with
| Nil -> Nil
| Cons m l ->
let mr = append_mon mon m in
let lr = mul_mon mon l in
Cons mr lr
end
let rec ghost function mul_devel (x1 x2:t') : t'
ensures { forall y. interp' result y = (interp' x1 y) * (interp' x2 y) }
= match x1 with
| Nil -> Nil
| Cons (M r m) l -> mul_mon (M r m) x2 ++ mul_devel l x2
end
let rec ghost function ext (c:r) (x:t') : t'
ensures { forall y. interp' result y = AA.(@) c (interp' x y) }
= match x with
| Nil -> Nil
| Cons (M r m) l -> Cons (M (R.( *) c r) m) (ext c l) end
let rec ghost function conv (x:t) : t'
ensures { forall y. interp x y = interp' result y }
= match x with
| Var v -> Cons (M R.one (Cons v Nil)) Nil
| Add x1 x2 -> (conv x1) ++ (conv x2)
| Mul x1 x2 -> mul_devel (conv x1) (conv x2)
| Ext r x -> ext r (conv x)
end
(** Normalisation *)
(*lexicographic order on monomials with variables sorted using sort_mons*)
let rec function le_mon (x1 x2: list int) : bool
= (length x1 < length x2) ||
((length x1 = length x2) &&
match x1, x2 with
| Nil, _ -> true
| _, Nil -> false
| Cons v1 r1, Cons v2 r2 -> v1 <= v2 && le_mon r1 r2
end)
let rec function same (l1 l2: list int) : bool
ensures { result -> eq_mon l1 l2 }
= match l1, l2 with
| Nil, Nil -> true
| Nil, _ | _, Nil -> false
| Cons x1 l1, Cons x2 l2 -> x1 = x2 && same l1 l2
end
lemma squash_append: forall r1 r2: r, l1 l2: list int, l: t'. same l1 l2 ->
eq' (Cons (M r1 l1) (Cons (M r2 l2) l)) (Cons (M (R.(+) r1 r2) l1) l)
let rec ghost function insert_mon (m: m) (x: t') : t'
ensures { eq' result (Cons m x) }
variant { length x }
= match m,x with
| _,Nil -> Cons m Nil
| M r1 l1, Cons (M r2 l2) l ->
if same l1 l2
then
let s = R.(+) r1 r2 in
if eq0 s
then (assert { eq' l (Cons m x)
by eq' l (Cons (M s l1) l)
so eq' (Cons (M s l1) l) (Cons m x)};
l)
else Cons (M s l1) l
else if le_mon l1 l2 then Cons m x else Cons (M r2 l2) (insert_mon m l)
end
let rec ghost function insertion_sort_mon (x:t') : t'
ensures { eq' result x }
variant { x }
= match x with
| Nil -> Nil
| Cons m l -> insert_mon m (insertion_sort_mon l)
end
let ghost function normalize (x:t') : t'
ensures { eq' result x }
= insertion_sort_mon x
lemma norm: forall x1 x2: t, y:vars.
normalize (conv x1) = normalize (conv x2) -> interp x1 y = interp x2 y
lemma norm': forall x1 x2: t'. normalize x1 = normalize x2 -> eq' x1 x2
end
module Matrix
use import int.Int
use import matrices.Matrix
use import matrices.MatrixArithmetic
use import matrices.BlockMul
function extf (c: int) (a:mat int) : int -> int -> int =
fun x y -> c * (get a x y)
function ext (c: int) (a:mat int) : mat int =
create (rows a) (cols a) (extf c a)
constant d : int
axiom DimNonNeg : d >= 0
constant zero11 : mat int = zero d d
constant one11 : mat int = create d d (fun _ _ -> 1)
let predicate eq0_int (x:int) = x=0
clone export AssocAlgebra with type r = int, type a = mat int, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = zero11, constant one = one11, function (+) = add, function A.(-_) = opp, function ( *) = mul, function (@) = ext, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int
use import AssocAlgebraDecision
end
\ No newline at end of file
......@@ -6,8 +6,9 @@
<prover id="1" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../compute.mlw" expanded="true">
<theory name="UnitaryCommutativeRingDecision" sum="b60d85f83e2113a07e31fb9ff218971f" expanded="true">
<theory name="UnitaryCommutativeRingDecision" sum="f010a5ed2c748e31ccaccc0292b55495">
<goal name="VC mon_append" expl="VC for mon_append">
<proof prover="0" timelimit="15"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
......@@ -29,28 +30,15 @@
</goal>
<goal name="VC mul_mon" expl="VC for mul_mon">
<transf name="split_goal_wp">
<goal name="VC mul_mon.1" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC mul_mon.1.1" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC mul_mon.1.2" expl="assertion">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC mul_mon.1.3" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC mul_mon.1.4" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<goal name="VC mul_mon.1" expl="postcondition">
<transf name="simplify_trivial_quantification">
<goal name="VC mul_mon.1.1" expl="VC for mul_mon">
<proof prover="1"><result status="valid" time="0.31"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_mon.2" expl="postcondition">
<transf name="compute_in_goal">
<goal name="VC mul_mon.2.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.49" steps="34"/></proof>
</goal>
</transf>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -156,11 +144,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC insert_mon.3.2" expl="postcondition">
<transf name="compute_in_goal">
<goal name="VC insert_mon.3.2.1" expl="postcondition">
<proof prover="2"><result status="valid" time="3.00"/></proof>
</goal>
</transf>
<proof prover="2"><result status="valid" time="0.81"/></proof>
</goal>
</transf>
</goal>
......@@ -176,7 +160,7 @@
<proof prover="0" timelimit="15"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
</theory>
<theory name="Tests" sum="6dff474baec302c419f4992d0bd1a6cf">
<theory name="Tests" sum="1f065f37e7ef4cf469e13a7cf28b7627">
<goal name="VC eq0_int" expl="VC for eq0_int">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......@@ -198,171 +182,179 @@
<goal name="VC eq0" expl="VC for eq0">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="d" expl="">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal">
<goal name="d.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</theory>
<theory name="AssocAlgebra" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AssocAlgebraDecision" sum="bee23ddea5475b0e934c7a637429ecf5">
<goal name="VC mon_append" expl="VC for mon_append">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="d&apos;" expl="">
<goal name="interp_cons" expl="">
<proof prover="1"><result status="valid" time="1.11"/></proof>
<transf name="compute_in_goal">
<goal name="d&apos;.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="interp_cons.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_1" expl="">
<transf name="compute_in_goal">
<goal name="devel_1.1" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
</transf>
<goal name="VC interp_sum" expl="VC for interp_sum">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="devel_2" expl="">
<transf name="compute_in_goal">
<goal name="devel_2.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
<goal name="VC append_mon" expl="VC for append_mon">
<proof prover="2" timelimit="1" memlimit="1000"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="devel_3" expl="">
<transf name="compute_in_goal">
<goal name="devel_3.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="VC mul_mon" expl="VC for mul_mon">
<transf name="split_goal_wp">
<goal name="VC mul_mon.1" expl="postcondition">
<transf name="simplify_trivial_quantification">
<goal name="VC mul_mon.1.1" expl="VC for mul_mon">
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="devel_4" expl="">
<transf name="compute_in_goal">
<goal name="devel_4.1" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<goal name="VC mul_mon.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_5" expl="">
<transf name="compute_in_goal">
<goal name="devel_5.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<goal name="VC mul_devel" expl="VC for mul_devel">
<transf name="split_goal_wp">
<goal name="VC mul_devel.1" expl="postcondition">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_1" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_1.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="VC mul_devel.2" expl="postcondition">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_2" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_2.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="VC ext" expl="VC for ext">
<transf name="split_goal_wp">
<goal name="VC ext.1" expl="postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_3" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_3.1" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
<goal name="VC ext.2" expl="postcondition">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_4" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_4.1" expl="">
<proof prover="0"><result status="valid" time="3.62" steps="6"/></proof>
<goal name="VC conv" expl="VC for conv">
<transf name="split_goal_wp">
<goal name="VC conv.1" expl="postcondition">
<proof prover="1"><result status="valid" time="1.19"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_5" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_5.1" expl="">
<proof prover="0"><result status="valid" time="1.87" steps="6"/></proof>
<goal name="VC conv.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_1_norm" expl="">
<transf name="split_goal_wp">
<goal name="devel_conv_1_norm.1" expl="">
<transf name="compute_in_goal">
</transf>
<goal name="VC conv.3" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="devel_conv_1_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<goal name="VC conv.4" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_2_norm" expl="">
<transf name="split_goal_wp">
<goal name="devel_conv_2_norm.1" expl="">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="devel_conv_2_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
<goal name="VC le_mon" expl="VC for le_mon">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC same" expl="VC for same">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="squash_append" expl="">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<transf name="compute_in_goal">
<goal name="squash_append.1" expl="">
<proof prover="0"><result status="valid" time="0.14" steps="669"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_3_norm" expl="">
<goal name="VC insert_mon" expl="VC for insert_mon">
<transf name="split_goal_wp">
<goal name="devel_conv_3_norm.1" expl="">
<transf name="compute_in_goal">
<goal name="VC insert_mon.1" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC insert_mon.1.1" expl="VC for insert_mon">
<transf name="compute_in_goal">
<goal name="VC insert_mon.1.1.1" expl="VC for insert_mon">
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
<goal name="VC insert_mon.1.2" expl="VC for insert_mon">
<proof prover="0"><result status="valid" time="0.04" steps="26"/></proof>
</goal>
<goal name="VC insert_mon.1.3" expl="VC for insert_mon">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_3_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
<goal name="VC insert_mon.2" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_4_norm" expl="">
<transf name="split_goal_wp">
<goal name="devel_conv_4_norm.1" expl="">
<transf name="compute_in_goal">
<goal name="VC insert_mon.3" expl="postcondition">
<transf name="split_goal_wp">
<goal name="VC insert_mon.3.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC insert_mon.3.2" expl="postcondition">
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_4_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_5_norm" expl="">
<goal name="VC insertion_sort_mon" expl="VC for insertion_sort_mon">
<transf name="split_goal_wp">
<goal name="devel_conv_5_norm.1" expl="">
<transf name="compute_in_goal">
</transf>
<goal name="VC insertion_sort_mon.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="devel_conv_5_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
<goal name="VC insertion_sort_mon.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_6" expl="">
<transf name="compute_in_goal">
<goal name="devel_6.1" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
</transf>
<goal name="VC normalize" expl="VC for normalize">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="devel_conv_6" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_6.1" expl="">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
<goal name="norm" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="devel_conv_6_norm" expl="">
<transf name="split_goal_wp">
<goal name="devel_conv_6_norm.1" expl="">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="devel_conv_6_norm.2" expl="">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>