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

Infinite matrices definitions

parent df04199d
......@@ -305,14 +305,14 @@ axiom ANonTrivial : A.zero <> one
(* A is an associative algebra over R *)
function (@) r a : a
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)
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 }
......@@ -320,9 +320,16 @@ end
module AssocAlgebraDecision
use import int.Int
use import list.List
use import AssocAlgebra as AA
type r
type a
constant one : a
clone export AssocAlgebra with type r = r, type a = a, constant one = one
type t = Var int | Add t t | Mul t t | Ext r t
type vars = int -> a
......@@ -332,7 +339,7 @@ function interp (x: t) (y: vars) : a =
| 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)
| Ext r x -> ($) r (interp x y)
end
predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y
......@@ -344,14 +351,14 @@ type t' = list m
function mon (x: list int) (y: vars) : a =
match x with
| Nil -> AA.one
| Nil -> 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
| Nil -> zero
| Cons (M r m) l -> (($) 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
......@@ -397,7 +404,7 @@ let rec ghost function mul_devel (x1 x2:t') : t'
end
let rec ghost function ext (c:r) (x:t') : t'
ensures { forall y. interp' result y = AA.(@) c (interp' x y) }
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
......@@ -461,23 +468,27 @@ 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 ghost function normalize' (x:t') : t'
ensures { eq' result x }
= insertion_sort_mon x
let ghost function normalize (x:t) : t'
ensures { eq' result (conv x) }
= normalize' (conv x)
let lemma norm (x1 x2: t) (y:vars)
requires { normalize (conv x1) = normalize (conv x2) }
requires { normalize x1 = normalize x2 }
ensures { interp x1 y = interp x2 y }
= ()
let lemma norm' (x1 x2: t')
requires { normalize x1 = normalize x2 }
requires { normalize' x1 = normalize' x2 }
ensures { eq' x1 x2 }
= ()
meta reify_target function interp
goal g: forall x y. x * y = y * x
meta reify_target function interp
meta reify_normalize function normalize
end
......@@ -487,25 +498,346 @@ use import int.Int
let predicate eq0_int (x:int) = x=0
clone export AssocAlgebra 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
use import AssocAlgebraDecision
let function ($) (x y:int) :int = x * y
meta reify_target function interp
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
goal g: forall x y. x * y = y * x
goal g: forall x y. x + y = y + x
goal h: forall x y z. x $ (y * z) = (x $ y) * z
end
module Matrix
theory InfMatrixGen
use import int.Int
type mat 'a
clone algebra.UnitaryCommutativeRing as F
function get (mat F.t) int int : F.t
function set (mat F.t) int int F.t : mat F.t
function row_zeros (mat F.t) int : int
function col_zeros (mat F.t) int : int
axiom row_zeros_def:
forall m: mat F.t, i j: int. 0 <= i -> j >= row_zeros m i -> get m i j = F.zero
axiom col_zeros_def:
forall m: mat F.t, i j: int. 0 <= j -> i >= col_zeros m j -> get m i j = F.zero
(*FIXME should be invariants*)
axiom set_def_changed:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
get (set m i j v) i j = v
axiom set_def_unchanged:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
forall i' j': int. 0 <= i' -> 0 <= j' -> (i <> i' \/ j <> j') ->
get (set m i j v) i' j' = get m i' j'
axiom set_def_rowz_changed:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
j >= row_zeros m i -> row_zeros (set m i j v) i = j+1
axiom set_def_colz_changed:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
i >= col_zeros m j -> col_zeros (set m i j v) j = i+1
axiom set_def_rowz_unchanged:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
j < row_zeros m i -> row_zeros (set m i j v) i = row_zeros m i
axiom set_def_colz_unchanged:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
i < col_zeros m j -> col_zeros (set m i j v) j = col_zeros m j
axiom set_def_other_rowz:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
forall i': int. 0 <= i' -> i <> i' ->
row_zeros (set m i j v) i' = row_zeros m i'
axiom set_def_other_colz:
forall m: mat F.t, i j: int, v: F.t. 0 <= i -> 0 <= j ->
forall j': int. 0 <= j' -> j <> j' ->
col_zeros (set m i j v) j' = col_zeros m j'
predicate (==) (m1 m2: mat F.t) =
forall i j: int. 0 <= i -> 0 <= j -> get m1 i j = get m2 i j
axiom extensionality:
forall m1 m2: mat F.t. m1 == m2 -> m1 = m2
predicate (===) (m1 m2: mat F.t) =
forall i j: int. 0 <= i -> 0 <= j ->
row_zeros m1 i = row_zeros m2 i /\ col_zeros m1 j = col_zeros m2 j
predicate size (m: mat F.t) (r c: int) =
forall i j. 0 <= i -> 0 <= j -> row_zeros m i = c /\ col_zeros m j = r
end
module InfMatrix
use HighOrd
type t
constant tzero: t
clone export algebra.UnitaryCommutativeRing with type t = t, constant zero = tzero
use import int.Int
clone export relations.MinMax with type t = int, predicate le = (<=)
type mat
function get mat int int : t
function row_zeros mat int : int
function col_zeros mat int : int
function create (rz: int -> int) (cz: int -> int) (f: int -> int -> t)
: mat
axiom create_rowz:
forall rz cz: int -> int, f: int -> int -> t, i: int.
0 <= i -> row_zeros (create rz cz f) i = rz i
axiom create_colz:
forall rz cz: int -> int, f: int -> int -> t, j: int.
0 <= j -> col_zeros (create rz cz f) j = cz j
axiom create_get_ib:
forall rz cz: int -> int, f: int -> int -> t, i j: int.
0 <= i < cz j -> 0 <= j < rz i -> get (create rz cz f) i j = f i j
axiom create_get_oob:
forall rz cz: int -> int, f: int -> int -> t, i j: int.
0 <= i -> 0 <= j -> (i >= cz j \/ j >= rz i) ->
get (create rz cz f) i j = tzero
function fcreate (r c: int) (f: int -> int -> t) : mat =
create (fun _ -> c) (fun _ -> r) f
lemma fcreate_get_ib:
forall r c i j: int, f: int -> int -> t.
0 <= i < r -> 0 <= j < c -> get (fcreate r c f) i j = f i j
lemma fcreate_get_oob:
forall r c i j: int, f: int -> int -> t.
0 <= i -> 0 <= j -> (i >= r \/ j >= c) -> get (fcreate r c f) i j = tzero
function set (m: mat) (i j:int) (v:t) : mat =
create
(fun i1 -> if i1 = i then max (j+1) (row_zeros m i) else row_zeros m i1)
(fun j1 -> if j1 = j then max (i+1) (col_zeros m j) else col_zeros m j1)
(fun i1 j1 -> if i1 = i && j1 = j then v else get m i1 j1)
clone export InfMatrixGen with type mat 'a = mat,
type F.t = t,
function get = get,
function set = set,
function row_zeros = row_zeros,
function col_zeros = col_zeros,
lemma set_def_changed,
lemma set_def_unchanged,
lemma set_def_colz_changed,
lemma set_def_colz_unchanged,
lemma set_def_rowz_changed,
lemma set_def_rowz_unchanged,
lemma set_def_other_rowz,
lemma set_def_other_colz
lemma fcreate_size:
forall r c: int, f: int -> int -> t. size (fcreate r c f) r c
end
theory MaxFun
use import int.Int
use import int.MinMax
(* maximum of a function over an interval; always at least 0 *)
let rec function maxf (f: int -> int) (a b: int) : int
variant { b - a }
= if b <= a then zero else max (maxf f a (b - 1)) (f (b-1))
let rec lemma maxf_nonneg (f: int -> int) (a b: int)
requires { a <= b }
ensures { maxf f a b >= 0 }
variant { b - a }
= if a = b then () else maxf_nonneg f a (b-1)
let rec lemma maxf_larger (f: int -> int) (a b i: int)
requires { a <= i < b }
variant { b - a }
ensures { maxf f a b >= f i }
= if i = b-1 then () else maxf_larger f a (b-1) i
let rec lemma max_left (f: int -> int) (a b: int)
requires { a < b }
ensures { maxf f a b = max (f a) (maxf f (a+1) b) }
variant { b - a }
= if a = b-1 then () else max_left f a (b-1)
let rec lemma max_ext (f g: int -> int) (a b: int)
requires { a < b }
variant { b - a }
requires { forall i. a <= i < b -> f i = g i }
ensures { maxf f a b = maxf g a b }
= if a = b-1 then () else max_ext f g a (b-1)
let rec lemma max_decomp (f: int -> int) (a b c: int)
requires { a <= b <= c }
variant { c - b }
ensures { maxf f a c = max (maxf f a b) (maxf f b c) }
= if b = c
then assert { maxf f a c = max (maxf f a b) (maxf f b c)
by maxf f b c = 0
so maxf f a b >= 0 }
else begin
max_decomp f a b (c-1);
assert { maxf f a c = max (maxf f a b) (maxf f b c)
by maxf f a c = max (maxf f a (c-1)) (f (c-1))
so maxf f b c = max (maxf f b (c-1)) (f (c-1))
so maxf f a c = max (max (maxf f a b) (maxf f b (c-1))) (f (c-1))
= max (maxf f a b) (maxf f b c) }
end
end
module InfIntMatrix
use import int.Int
clone export InfMatrix with type t = int, constant tzero = zero
use import int.Sum
use import int.Int (*FIXME needed so i < i+1 ?*)
(* Zero matrix *)
constant zerof : int -> int -> int = fun _ _ -> 0
constant zero : mat = fcreate 0 0 zerof
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
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
function idrc (r c: int) : mat = fcreate r c idf
(* Matrix addition *)
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 =
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)
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
lemma add_sizes:
forall a b: mat. a === b -> a === add a b === b
lemma zero_neutral:
forall a. add a zero = a by add a zero == a
(* Matrix additive inverse *)
function opp2f (a: mat) : int -> int -> int =
fun x y -> - get a x y
function opp (a: mat) : mat =
create (row_zeros a) (col_zeros a) (opp2f a)
function sub (a b: mat) : mat = add a (opp b)
lemma opp_involutive:
forall m. opp (opp m) = m by opp (opp m) == m
(* Matrix multiplication *)
function mul_atom (a b: mat) (i j: int) : int -> int =
fun k -> get a i k * get b k j
lemma atom_oob:
forall a b: mat, i j k: int. 0 <= i -> 0 <= j ->
k >= row_zeros a i \/ k >= col_zeros b j -> mul_atom a b i j k = 0
by if k >= row_zeros a i then get a i k = 0
else k >= col_zeros b j so get b k j = 0
function mul_cell_bound (a b: mat) (i j: int) : int
= min (row_zeros a i) (col_zeros b j)
function mul_cell (a b: mat) : int -> int -> int =
fun i j -> sum (mul_atom a b i j) 0 (mul_cell_bound a b i j)
use import MaxFun
lemma cell_oob_r:
forall a b: mat, i j: int.
j >= maxf (fun k -> row_zeros b k) 0 (row_zeros a i) ->
mul_cell a b i j = 0
by forall k. 0 <= k < mul_cell_bound a b i j ->
mul_atom a b i j k = 0
by 0 <= k < row_zeros a i
so j >= row_zeros b k
so get b k j = 0
lemma cell_oob_c:
forall a b: mat, i j: int.
i >= maxf (fun k -> col_zeros a k) 0 (col_zeros b j) ->
mul_cell a b i j = 0
by forall k. 0 <= k < mul_cell_bound a b i j ->
mul_atom a b i j k = 0
by 0 <= k < col_zeros b j
so i >= col_zeros a k
so get a i k = 0
function 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)
lemma mul_sizes:
forall m1 m2: mat, m n p: int.
size m1 m n -> size m2 n p -> size (mul m1 m2) m p
lemma id_neutral_r:
forall m: mat. mul m id = m by mul m id == m
lemma id_neutral_l:
forall m: mat. mul id m = m by mul id m == m
end
(*
use import int.MinMax
use import matrices.Matrix
use import matrices.MatrixArithmetic
use import matrices.BlockMul
constant d : int
axiom DimNonNeg : d >= 0
......@@ -523,7 +855,7 @@ constant one11 : mat int = create d d (fun x y -> if x=y then 1 else 0)
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, 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 = 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, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
predicate quarters (a a11 a12 a21 a22: mat int) =
(rows a11 = rows a12 = rows a21 = rows a22 = cols a11 = cols a12 = cols a21 = cols a22) /\
......@@ -542,7 +874,7 @@ let lemma naive_blocks (a b c a11 a12 a21 a22 b11 b12 b21 b22 c11 c12 c21 c22: m
ensures { c = mul a b }
=
()
end
use import AssocAlgebraDecision
end
\ No newline at end of file
*)
\ No newline at end of file
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