Skip to content
GitLab
Commit 6b4488e5 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Deghostify decision procedure on algebras 

More work than expected, todo see if it can be more efficient
parent 2cf07a7d
Expand all Hide whitespace changes
Inline Side-by-side
examples/in_progress/multiprecision/compute.mlw
View file @ 6b4488e5
......@@ -305,7 +305,7 @@ axiom ANonTrivial : A.zero <> one
(* A is an associative algebra over R *)
function ($) r a : a
val function ($) r a : a
axiom ExtDistSumA : forall r: r, x y: a. r $ (x + y) = r $ x + r $ y
......@@ -327,25 +327,38 @@ use import list.List
type r
type a
constant one : a
val constant rzero : r
val constant rone : r
val constant aone : a
val constant azero : a
val function rplus r r : r
val function rtimes r r : r
val function ropp r : r
val function aplus a a : a
val function atimes a a : a
val function aopp a : a
clone export AssocAlgebra with type r = r, type a = a, constant one = one
clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.( *) = rtimes, function R.(-_) = ropp, function (+) = aplus, function ( *) = atimes, function A.(-_) = aopp
axiom azero_def: azero = A.zero (* FIXME *)
type t = Var int | Add t t | Mul t t | Ext r t | Sub t t
type vars = int -> a
function asub (x y:a) : a
val function asub (x y:a) : a
axiom asub_def: forall x y: a. asub x y = x + (A.(-_) y)
axiom asub_def: forall x y: a. asub x y = aplus x (aopp y)
lemma ext_minone:
forall a: a. ($) (R.(-_) R.one) a = A.(-_) a
forall a: a. ($) (ropp rone) a = aopp a
function interp (x: t) (y: vars) : a =
let rec 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
| Add x1 x2 -> aplus (interp x1 y) (interp x2 y)
| Mul x1 x2 -> atimes (interp x1 y) (interp x2 y)
| Sub x1 x2 -> asub (interp x1 y) (interp x2 y)
| Ext r x -> ($) r (interp x y)
end
......@@ -357,16 +370,16 @@ predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y
type m = M r (list int)
type t' = list m
function mon (x: list int) (y: vars) : a =
let rec function mon (x: list int) (y: vars) : a =
match x with
| Nil -> one
| Cons x l -> y x * mon l y
| Nil -> aone
| Cons x l -> atimes (y x) (mon l y)
end
function interp' (x: t') (y: vars) : a =
let rec function interp' (x: t') (y: vars) : a =
match x with
| Nil -> zero
| Cons (M r m) l -> (($) r (mon m y)) + interp' l y end
| Nil -> azero
| Cons (M r m) l -> aplus (($) 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
......@@ -375,28 +388,29 @@ 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 }
ensures { mon (x1 ++ x2) y = atimes (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
interp' (Cons m x) y = aplus (interp' x y) (interp' (Cons m Nil) y)
let rec lemma interp_sum (x1 x2: t')
ensures { forall y: vars.
interp' (x1++x2) y = interp' x1 y + interp' x2 y }
interp' (x1++x2) y = aplus (interp' x1 y) (interp' x2 y) }
variant { x1 }
= match x1 with
| Nil -> ()
| Cons _ x -> interp_sum x x2 end
let ghost function append_mon (m1 m2:m)
let 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
= atimes (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) }
= match m1,m2 with M r1 l1, M r2 l2 -> M (rtimes 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 }
let rec function mul_mon (mon: m) (x:t'): t' (* mon*x *)
ensures { forall y. interp' result y =
atimes (interp' (Cons mon Nil) y) (interp' x y) }
= match x with
| Nil -> Nil
| Cons m l ->
......@@ -405,30 +419,30 @@ let rec ghost function mul_mon (mon: m) (x:t'): t' (* mon*x *)
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) }
let rec function mul_devel (x1 x2:t') : t'
ensures { forall y. interp' result y = atimes (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'
let rec function ext (c:r) (x:t') : t'
ensures { forall y. interp' result y = ($) c (interp' x y) }
= match x with
| Nil -> Nil
| Cons (M r m) l -> Cons (M (R.( *) c r) m) (ext c l) end
| Cons (M r m) l -> Cons (M (rtimes c r) m) (ext c l) end
lemma ext_sub:
forall x:t', y:vars. interp' (ext (R.(-_) R.one) x) y = A.(-_) (interp' x y)
forall x:t', y:vars. interp' (ext (ropp rone) x) y = aopp (interp' x y)
let rec ghost function conv (x:t) : t'
let rec 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
| Var v -> Cons (M rone (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)
| Sub x1 x2 -> (conv x1) ++ (ext (R.(-_) R.one) (conv x2))
| Sub x1 x2 -> (conv x1) ++ (ext (ropp rone) (conv x2))
end
......@@ -453,9 +467,9 @@ let rec function same (l1 l2: list int) : bool
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)
eq' (Cons (M r1 l1) (Cons (M r2 l2) l)) (Cons (M (rplus r1 r2) l1) l)
let rec ghost function insert_mon (m: m) (x: t') : t'
let rec function insert_mon (m: m) (x: t') : t'
ensures { eq' result (Cons m x) }
variant { length x }
= match m,x with
......@@ -463,7 +477,7 @@ let rec ghost function insert_mon (m: m) (x: t') : t'
| M r1 l1, Cons (M r2 l2) l ->
if same l1 l2
then
let s = R.(+) r1 r2 in
let s = rplus r1 r2 in
if eq0 s
then (assert { eq' l (Cons m x)
by eq' l (Cons (M s l1) l)
......@@ -473,7 +487,7 @@ let rec ghost function insert_mon (m: m) (x: t') : t'
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'
let rec function insertion_sort_mon (x:t') : t'
ensures { eq' result x }
variant { x }
= match x with
......@@ -481,11 +495,11 @@ let rec ghost function insertion_sort_mon (x:t') : t'
| Cons m l -> insert_mon m (insertion_sort_mon l)
end
let ghost function normalize' (x:t') : t'
let function normalize' (x:t') : t'
ensures { eq' result x }
= insertion_sort_mon x
let ghost function normalize (x:t) : t'
let function normalize (x:t) : t'
ensures { eq' result (conv x) }
= normalize' (conv x)
......@@ -499,6 +513,13 @@ let lemma norm' (x1 x2: t')
ensures { eq' x1 x2 }
= ()
let function norm_f (x1 x2: t) : bool
ensures { forall y: vars. result = true -> interp x1 y = interp x2 y }
= match normalize' (conv (Sub x1 x2)) with
| Nil -> true
| _ -> false
end
meta rewrite_def function interp
end
......@@ -509,13 +530,13 @@ use import int.Int
let predicate eq0_int (x:int) = x=0
let function ($) (x y:int) :int = x * y
let function ($$) (x y:int) :int = x * y
clone export AssocAlgebraDecision with type r = int, type a = int, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = Int.zero, constant one = Int.one, function (+) = (+), function A.(-_) = (-_), function ( *) = ( *), function ($) = ($), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = ( *), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = ( *), val ($) = ($$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
goal g: forall x y. x + y = y + x
goal h: forall x y z. x $ (y * z) = (x $ y) * z
goal h: forall x y z. x $$ (y * z) = (x $$ y) * z
end
theory InfMatrixGen
......@@ -636,12 +657,12 @@ module InfMatrix
type mat
function get mat int int : t
val function get mat int int : t
function row_zeros mat int : int
function col_zeros mat int : int
val function row_zeros mat int : int
val function col_zeros mat int : int
function create (rz: int -> int) (cz: int -> int) (f: int -> int -> t)
val function create (rz: int -> int) (cz: int -> int) (f: int -> int -> t)
: mat
axiom create_rowz:
......@@ -661,8 +682,8 @@ module InfMatrix
0 <= i -> 0 <= j -> (i >= cz j \/ j >= rz i) ->
get (create rz cz f) i j = tzero
function set (m: mat) (i j:int) (v:t) : mat =
if 0 <= i /\ 0 <= j
let ghost function set (m: mat) (i j:int) (v:t) : mat =
if 0 <= i && 0 <= j
then
create
(fun i1 -> if i1 = i then max (j+1) (row_zeros m i) else row_zeros m i1)
......@@ -692,7 +713,7 @@ module InfMatrix
forall rz cz: int -> int, f: int -> int -> t, i j: int.
in_bounds (create rz cz f) i j -> get (create rz cz f) i j = f i j
*)
function fcreate (r c: int) (f: int -> int -> t) : mat =
let ghost function fcreate (r c: int) (f: int -> int -> t) : mat =
create (fun _ -> max 0 c) (fun _ -> max 0 r) f
lemma fcreate_get_ib:
......@@ -745,10 +766,10 @@ module Sum_extended
by forall y. c <= y < d -> sumf f2 a b y = ha y }
end
let ghost sum_ext (f g: int -> int) (a b: int) : unit
requires {forall i. a <= i < b -> f i = g i }
ensures { sum f a b = sum g a b }
= ()
let ghost sum_ext (f g: int -> int) (a b: int) : unit
requires { forall i. a <= i < b -> f i = g i }
ensures { sum f a b = sum g a b }
= ()
end
......@@ -824,17 +845,19 @@ module InfIntMatrix
use import int.Int (*FIXME needed so i < i+1 ?*)
(* Zero matrix *)
constant zerof : int -> int -> int = fun _ _ -> 0
let constant zerof : int -> int -> int = fun _ _ -> 0
constant mzero : mat = fcreate 0 0 zerof
val constant mzero : mat
function zerorc (r c: int) : mat = fcreate r c zerof
axiom mzero_def: mzero = fcreate 0 0 zerof (*FIXME*)
let ghost function zerorc (r c: int) : mat = fcreate r c zerof
(* Identity matrix *)
constant idf : int -> int -> int = fun x y -> if x = y then 1 else 0
let constant idf : int -> int -> int = fun x y -> if x = y then 1 else 0
constant id : mat = create (fun i -> i+1) (fun j -> j+1) idf
let constant id : mat = create (fun i -> i+1) (fun j -> j+1) idf
lemma id_def:
forall i. 0 <= i -> get id i i = 1
......@@ -843,14 +866,17 @@ module InfIntMatrix
(* Matrix addition *)
function add2f (a b: mat) : int -> int -> int =
let ghost function add2f (a b: mat) : int -> int -> int =
fun x y -> get a x y + get b x y
function add (a b: mat) : mat =
function f_add (a b: mat) : mat =
create (fun i -> max (row_zeros a i) (row_zeros b i))
(fun j -> max (col_zeros a j) (col_zeros b j))
(add2f a b)
val function add (a b: mat) : mat
ensures { result = f_add a b }
lemma add_get:
forall a b: mat, i j: int. 0 <= i -> 0 <= j ->
get (add a b) i j = get a i j + get b i j
......@@ -877,10 +903,13 @@ module InfIntMatrix
function opp2f (a: mat) : int -> int -> int =
fun x y -> - get a x y
function opp (a: mat) : mat =
function f_opp (a: mat) : mat =
create (row_zeros a) (col_zeros a) (opp2f a)
function sub (a b: mat) : mat = add a (opp b)
val function opp (a: mat) : mat
ensures { result = f_opp a }
let function sub (a b: mat) : mat = add a (opp b)
lemma sub_size:
forall a b: mat, r c: int. size a r c -> size b r c -> size (sub a b) r c
......@@ -929,11 +958,14 @@ module InfIntMatrix
so i >= col_zeros a k
so get a i k = 0
function mul (a b: mat) : mat =
function f_mul (a b: mat) : mat =
create (fun i -> maxf (fun k -> row_zeros b k) 0 (row_zeros a i))
(fun j -> maxf (fun k -> col_zeros a k) 0 (col_zeros b j))
(mul_cell a b)
val function mul (a b: mat) : mat
ensures { result = f_mul a b }
let lemma mul_sizes (m1 m2: mat) (m n p: int)
requires { size m1 m n /\ size m2 n p }
requires { 0 < m /\ 0 < n /\ 0 < p }
......@@ -967,7 +999,8 @@ module InfIntMatrix
= 0 + (get id i i)*(get m i j) + 0
= get m i j)
/\ (forall i j. 0 <= i -> 0 <= j -> not (in_bounds m i j)
-> mul_cell id m i j
-> (forall k. 0 <= k < mul_cell_bound id m i j -> mul_atom id m i j k = 0)
so mul_cell id m i j
= sum (fun k -> mul_atom id m i j k) 0 (mul_cell_bound id m i j)
= 0 = get m i j))
......@@ -1004,7 +1037,9 @@ module InfIntMatrix
+ sum (ft1 k) (mul_cell_bound a b i k) m_a_bc
= sumf ft1 0 (mul_cell_bound a b i k) k
+ sum (ft1 k) (mul_cell_bound a b i k) m_a_bc
so forall l. l >= mul_cell_bound a b i k -> ft1 k l = 0
so (forall l. l >= mul_cell_bound a b i k ->
mul_atom a b i k l = 0
so ft1 k l = 0)
so sum (ft1 k) (mul_cell_bound a b i k) m_a_bc = 0 };
assert { forall k. 0 <= k < m_ab_c ->
mul_atom ab c i j k = sumf ft1 0 m_a_bc k
......@@ -1034,7 +1069,9 @@ module InfIntMatrix
+ sum (ft2 k) (mul_cell_bound b c k j) m_ab_c
= sumf ft2 0 (mul_cell_bound b c k j) k
+ sum (ft2 k) (mul_cell_bound b c k j) m_ab_c
so forall l. l >= mul_cell_bound b c k j -> ft2 k l = 0
so (forall l. l >= mul_cell_bound b c k j ->
mul_atom b c k j l = 0
so ft2 k l = 0)
so sum (ft2 k) (mul_cell_bound b c k j) m_ab_c = 0 };
assert { forall k. 0 <= k < m_a_bc ->
mul_atom a bc i j k = sumf ft2 0 m_ab_c k
......@@ -1092,9 +1129,12 @@ module InfIntMatrix
function extf (c: int) (a: mat): int -> int -> int =
fun x y -> c * (get a x y)
function extp (c: int) (a: mat) : mat =
function f_extp (c: int) (a: mat) : mat =
create (fun i -> row_zeros a i) (fun j -> col_zeros a j) (extf c a)
val function extp (c: int) (a: mat) : mat
ensures { result = f_extp c a }
lemma ext_iso:
forall m: mat, r: int. extp r m === m
......@@ -1153,7 +1193,7 @@ use import int.Int
let predicate eq0_int (x:int) = x = 0
clone export AssocAlgebraDecision with type r = int, type a = mat, constant R.zero = Int.zero, constant R.one = Int.one, function R.(+) = (+), function R.(-_) = (-_), function R.(*) = (*),constant A.zero = mzero, constant one = id, function (+) = add, function A.(-_) = opp, function ( *) = mul, function asub = sub, function ($) = extp, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, goal A.Mul_distr_l, goal A.Mul_distr_r, goal asub_def, goal A.Inv_def_l, goal A.Inv_def_r
clone export AssocAlgebraDecision with type r = int, type a = mat, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = ( *), val azero = mzero, val aone = id, val aplus = add, val aopp = opp, val atimes = mul, val asub = sub, val ($) = extp, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, goal A.Mul_distr_l, goal A.Mul_distr_r, goal asub_def, goal A.Inv_def_l, goal A.Inv_def_r
end
......@@ -1365,4 +1405,4 @@ module MatrixTests
assert { s22 = c22 };
paste_quarters s11 s12 s21 s22
end
end
\ No newline at end of file
end
Supports Markdown
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