lineardecision.mlw 19.1 KB
Newer Older
1 2
module LinearEquationsCoeffs

3 4 5 6
type a
function (+) a a : a
function ( *) a a : a
function (-_) a : a
7 8 9
function azero: a
function aone: a
predicate ale a a
10

11
clone algebra.OrderedUnitaryCommutativeRing as A with type t = a, function (+) = (+), function ( *) = ( *), function (-_) = (-_), constant zero = azero, constant one=aone, predicate (<=) = ale
12 13

type t
14
type vars = int -> a
15 16 17

exception Unknown

18
function interp t vars : a
19

20 21
val constant czero : t
val constant cone : t
22

23 24
axiom zero_def: forall y. interp czero y = azero
axiom one_def: forall y. interp cone y = aone
25

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42

val add (a b: t) : t
  ensures { forall v: vars. interp result v = interp a v + interp b v }
  raises  { Unknown -> true }

val mul (a b: t) : t
  ensures { forall v: vars. interp result v = interp a v * interp b v }

val opp (a:t) : t
  ensures { forall v: vars. interp result v = - (interp a v) }

val predicate eq (a b:t)
  ensures { result <-> forall y:vars. interp a y = interp b y }

axiom eq_def: forall a b: t. a=b -> eq a b

val inv (a:t) : t
43
  requires { not (eq a czero) }
44
  ensures { forall v: vars. interp result v * interp a v = aone }
45 46
  ensures { not (eq result czero) }
  raises { Unknown -> true }
47 48

val le (a b:t) : bool
49
  ensures { result -> forall y:vars. ale (interp a y) (interp b y) }
50 51 52
  raises  { Unknown -> true }


53
(*FIXME equality test, extensionality, specs for le and eq ? *)
54 55 56 57 58 59 60 61 62 63

end

module LinearEquationsDecision

use import int.Int

type coeff

clone LinearEquationsCoeffs as C with type t = coeff
64
type vars = C.vars
65

66
type expr = Term coeff int | Add expr expr | Cst coeff | UTerm int
67 68 69 70

let rec predicate valid_expr (e:expr)
  variant { e }
= match e with
71
  | Term _ i | UTerm i -> 0 <= i
72 73 74 75 76 77 78
  | Cst _ -> true
  | Add e1 e2 -> valid_expr e1 && valid_expr e2
  end

let rec predicate expr_bound (e:expr) (b:int)
  variant { e }
= match e with
79
  | Term _ i | UTerm i -> 0 <= i <= b
80 81 82 83
  | Cst _ -> true
  | Add e1 e2 -> expr_bound e1 b && expr_bound e2 b
  end

84
function interp (e:expr) (y:vars) (z:vars) : C.a
85
= match e with
86
  | UTerm v -> y v
87 88
  | Term c v -> C.( *) (C.interp c z) (y v)
  | Add e1 e2 -> C.(+) (interp e1 y z) (interp e2 y z)
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
  | Cst c -> C.interp c z
  end

use import bool.Bool
use import list.List

type equality = (expr, expr)
type context = list equality

let predicate valid_eq (eq:equality)
= match eq with (e1,e2) -> valid_expr e1 && valid_expr e2 end

let predicate eq_bound (eq:equality) (b:int)
= match eq with (e1,e2) -> expr_bound e1 b && expr_bound e2 b end

let rec predicate valid_ctx (ctx:context)
= match ctx with Nil -> true | Cons eq t -> valid_eq eq && valid_ctx t end

let rec predicate ctx_bound (ctx:context) (b:int)
= match ctx with Nil -> true | Cons eq t -> eq_bound eq b && ctx_bound t b end

let rec lemma expr_bound_w (e:expr) (b1 b2:int)
  requires { b1 <= b2 }
  requires { expr_bound e b1 }
  ensures  { expr_bound e b2 }
  variant  { e }
= match e with
  | Add e1 e2 -> expr_bound_w e1 b1 b2; expr_bound_w e2 b1 b2
  | Cst _ -> ()
  | Term _ _ -> ()
119
  | UTerm _ -> ()
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  end

lemma eq_bound_w: forall e:equality, b1 b2:int. eq_bound e b1 -> b1 <= b2 -> eq_bound e b2

let rec lemma ctx_bound_w (l:context) (b1 b2:int)
  requires { ctx_bound l b1 }
  requires { b1 <= b2 }
  ensures  { ctx_bound l b2 }
  variant  { l }
= match l with Nil -> () | Cons _ t -> ctx_bound_w t b1 b2 end

function interp_eq (g:equality) (y:vars) (z:C.vars) : bool
  = match g with (g1, g2) -> interp g1 y z = interp g2 y z end

function interp_ctx (l: context) (g: equality) (y: vars) (z:C.vars) : bool
= match l with
  | Nil -> interp_eq g y z
137
  | Cons h t -> (interp_eq h y z) -> (interp_ctx t g y z)
138 139 140 141 142 143 144 145 146
  end

use import array.Array
use import matrix.Matrix

let apply_r (m: matrix coeff) (v: array coeff) : array coeff
  requires { v.length = m.columns }
  ensures  { result.length = m.rows }
  raises   { C.Unknown -> true }
147
= let r = Array.make m.rows C.czero in
148 149 150 151 152 153 154 155 156 157 158
  for i = 0 to m.rows - 1 do
    for j = 0 to m.columns - 1 do
      r[i] <- C.add r[i] (C.mul (get m i j) v[j]);
    done
  done;
  r

let apply_l (v: array coeff) (m: matrix coeff) : array coeff
  requires { v.length = m.rows }
  ensures  { result.length = m.columns }
  raises   { C.Unknown -> true }
159
= let r = Array.make m.columns C.czero in
160 161 162 163 164 165 166 167 168 169 170 171
  for j = 0 to m.columns - 1 do
    for i = 0 to m.rows - 1 do
      r[j] <- C.add r[j] (C.mul (get m i j) v[i]);
    done
  done;
  r

use import ref.Ref

let sprod (a b: array coeff) : coeff
  requires { a.length = b.length }
  raises   { C.Unknown -> true }
172
= let r = ref C.czero in
173 174 175 176 177 178 179 180 181 182 183 184
  for i = 0 to a.length - 1 do
    r := C.add !r (C.mul a[i] b[i]);
  done;
  !r

let m_append (m: matrix coeff) (v:array coeff) : matrix coeff
  requires { m.rows = v.length }
  ensures  { result.rows = m.rows }
  ensures  { result.columns = m.columns + 1 }
  ensures  { forall i j. 0 <= i < m.rows -> 0 <= j < m.columns ->
             result.elts i j = m.elts i j }
  ensures  { forall i. 0 <= i < m.rows -> result.elts i m.columns = v[i] }
185
= let r = Matrix.make m.rows (m.columns + 1) C.czero in
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
  for i = 0 to m.rows - 1 do
    invariant { forall k j. 0 <= k < i -> 0 <= j < m.columns ->
                r.elts k j = m.elts k j }
    invariant { forall k. 0 <= k < i -> r.elts k m.columns = v[k] }
    for j = 0 to m.columns - 1 do
      invariant { forall k j. 0 <= k < i -> 0 <= j < m.columns ->
                r.elts k j = m.elts k j }
      invariant { forall k. 0 <= k < i -> r.elts k m.columns = v[k] }
      invariant { forall l. 0 <= l < j -> r.elts i l = m.elts i l }
      set r i j (get m i j)
    done;
    set r i m.columns v[i]
  done;
  r

let v_append (v: array coeff) (c: coeff) : array coeff
  ensures { length result = length v + 1 }
  ensures { forall k. 0 <= k < v.length -> result[k] = v[k] }
  ensures { result[v.length] = c }
= let r = Array.make (v.length + 1) c in
  for i = 0 to v.length - 1 do
    invariant { forall k. 0 <= k < i -> r[k] = v[k] }
    invariant { r[v.length] = c }
    r[i] <- v[i]
  done;
  r

213
let predicate (==) (a b: array coeff)
214 215
  ensures { result = true -> length a = length b /\
            forall i. 0 <= i < length a -> C.eq a[i] b[i] }
216 217 218 219 220 221 222 223 224
=
  if length a <> length b then false
  else
    let r = ref true in
    for i = 0 to length a - 1 do
      invariant { !r = true -> forall j. 0 <= j < i -> C.eq a[j] b[j] }
      if not (C.eq a[i] b[i]) then r := false;
    done;
    !r
225 226 227 228 229 230 231 232 233 234

use import int.MinMax
use import list.Length

let rec function max_var (e:expr) : int
  variant { e }
  requires { valid_expr e }
  ensures { 0 <= result }
  ensures { expr_bound e result }
= match e with
235
  | Term _ i | UTerm i -> i
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
  | Cst _ -> 0
  | Add e1 e2 -> max (max_var e1) (max_var e2)
  end

let function max_var_e (e:equality) : int
  requires { valid_eq e }
  ensures { 0 <= result }
  ensures { eq_bound e result }
= match e with (e1,e2) -> max (max_var e1) (max_var e2) end

let rec function max_var_ctx (l:context) : int
  variant { l }
  requires { valid_ctx l }
  ensures { 0 <= result }
  ensures { ctx_bound l result }
= match l with
  | Nil -> 0
  | Cons e t -> max (max_var_e e) (max_var_ctx t)
  end

let rec function opp_expr (e:expr) : expr
257
 (* ensures { forall y z. interp result y z = C.(-_) (interp e y z) }*)
258 259 260 261 262
  ensures { forall b. expr_bound e b -> expr_bound result b }
  variant { e }
= match e with
  | Cst c -> Cst (C.opp c)
  | Term c j -> Term (C.opp c) j
263
  | UTerm j -> Term (C.opp C.cone) j
264 265 266 267 268
  | Add e1 e2 -> Add (opp_expr e1) (opp_expr e2)
  end

predicate no_cst (e:expr)
= match e with
269 270
  | Cst c -> C.eq c C.czero
  | Term _ _ | UTerm _ -> true
271 272 273
  | Add e1 e2 -> no_cst e1 && no_cst e2
  end

274 275 276 277
(*TODO put this back in norm_eq*)
let rec norm_eq_aux (ex acc_e:expr) (acc_c:coeff) : (expr, coeff)
  requires { no_cst acc_e }
  returns { (rex, rc) -> forall y z.
278 279 280
              C.(+) (interp rex y z) (interp (Cst rc) y z)
            = C.(+) (interp ex y z)
                    (C.(+) (interp acc_e y z) (interp (Cst acc_c) y z)) }
281 282 283 284 285 286 287 288 289 290 291 292
  returns { (rex, _) -> no_cst rex }
  returns { (rex, _) -> forall b:int. expr_bound ex b /\ expr_bound acc_e b
                        -> expr_bound rex b }
  raises  { C.Unknown -> true }
  variant { ex }
= match ex with
  | Cst c -> acc_e, (C.add c acc_c)
  | Term _ _ | UTerm _ -> (Add acc_e ex, acc_c)
  | Add e1 e2 -> let ae, ac = norm_eq_aux e1 acc_e acc_c in
                 norm_eq_aux e2 ae ac
  end

293
let norm_eq (e:equality) : (expr, coeff)
294 295
 (* returns { (ex, c) -> forall y z.
            interp_eq e y z -> interp_eq (ex, Cst c) y z }*)
296 297 298 299 300 301 302
  returns { (ex, _) -> no_cst ex }
  returns { (ex, _) -> forall b:int. eq_bound e b -> expr_bound ex b }
  raises  { C.Unknown -> true }
= match e with
  | (e1, e2) ->
    let s = Add e1 (opp_expr e2) in
    assert { forall b. eq_bound e b -> expr_bound s b };
303
    match norm_eq_aux s (Cst C.czero) C.czero with
304 305 306 307 308 309 310 311 312
      (e, c) -> e, C.opp c
    end
  end

(*TODO: predicate that says that matrices a, b represent the context*)

let transpose (m:matrix coeff) : matrix coeff
  ensures { result.rows = m.columns /\ result.columns = m.rows }
=
313
  let r = Matrix.make m.columns m.rows C.czero in
314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
  for i = 0 to m.rows - 1 do
    for j = 0 to m.columns - 1 do
      set r j i (get m i j)
    done
  done;
  r

let swap_rows (m:matrix coeff) (i1 i2: int) : unit
  requires { 0 <= i1 < m.rows /\ 0 <= i2 < m.rows }
= for j = 0 to m.columns - 1 do
    let c = get m i1 j in
    set m i1 j (get m i2 j);
    set m i2 j c
  done

let mul_row (m:matrix coeff) (i: int) (c: coeff) : unit
  requires { 0 <= i < m.rows }
331
  requires { not (C.eq c C.czero) }
332 333 334 335 336 337 338 339 340 341 342 343 344 345
= for j = 0 to m.columns - 1 do
    set m i j (C.mul c (get m i j))
  done

let addmul_row (m:matrix coeff) (src dst: int) (c: coeff) : unit
  requires { 0 <= src < m.rows /\ 0 <= dst < m.rows }
  raises   { C.Unknown -> true }
= for j = 0 to m.columns - 1 do
    set m dst j (C.add (get m dst j) (C.mul c (get m src j)))
  done

use import ref.Refint
use import option.Option

346
(*TODO this goes inside gauss_jordan*)
347 348 349 350
val breakpoint (a: matrix coeff) : unit writes { a }

let a_breakpoint (v:array coeff) : unit
  = any unit
351

352 353 354 355 356 357 358 359
let gauss_jordan (a: matrix coeff) : option (array coeff)
  (*AX=B, a=(A|B), result=X*)
  returns { Some r -> Array.length r = a.columns - 1 | None -> true }
  requires { 1 <= a.rows /\ 1 <= a.columns }
  raises { C.Unknown -> true }
=
  let n = a.rows in
  let m = a.columns in
360 361 362 363 364 365 366 367 368 369 370
  let rec find_nonz (i j:int)
    requires { 0 <= i <= n }
    requires { 0 <= j < m }
    variant { n-i }
    ensures { i <= result <= n }
    ensures { result < n -> not (C.eq (a.elts result j) C.czero) }
    = if i >= n then n
    else
      if C.eq (get a i j) C.czero
      then find_nonz (i+1) j
      else i in
371 372 373 374 375 376 377 378
  let pivots = Array.make n 0 in
  let r = ref (-1) in
  for j = 0 to m-1 do
    invariant { -1 <= !r < n }
    invariant { forall i. 0 <= i <= !r -> 0 <= pivots[i] }
    invariant { forall i1 i2: int. 0 <= i1 < i2 <= !r -> pivots[i1] < pivots[i2] }
    invariant { !r >= 0 -> pivots[!r] < j }
    label Start in
379
    let k = find_nonz (!r+1) j in
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
    if k < n
    then begin
      incr r;
      pivots[!r] <- j;
      mul_row a k (C.inv(get a k j));
      if k <> !r then swap_rows a k !r;
      for i = 0 to n-1 do
        if i <> !r
        then addmul_row a !r i (C.opp(get a i j))
      done;
    end
  done;
  if !r < 0 then None (* matrix is all zeroes *)
  else if pivots[!r] >= m-1 then None (*pivot on last column, no solution*)
  else begin
395
    let v = Array.make (m-1) C.czero in
396 397 398
    for i = 0 to !r do
      v[pivots[i]] <- get a i (m-1)
    done;
399
   (* a_breakpoint v;*)
400 401 402
    Some v
  end

403

404 405 406
let linear_decision (l: context) (g: equality) : bool
  requires { valid_ctx l }
  requires { valid_eq g }
407
  ensures { forall y z. result -> interp_ctx l g y z }
408 409 410
  raises  { C.Unknown -> true }
=
  let nv = max (max_var_e g) (max_var_ctx l) in
411 412 413
  let a = Matrix.make (length l) (nv+1) C.czero in
  let b = Array.make (length l) C.czero in      (* ax = b *)
  let v = Array.make (nv+1) C.czero in          (* goal *)
414
  (*v[0] <- any coeff;*)
415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
  let rec fill_expr (ex: expr) (i:int): unit
    variant { ex }
    requires { no_cst ex }
    raises  { C.Unknown -> true }
    requires { 0 <= i < length l }
    requires { expr_bound ex nv }
  = match ex with
    | Cst c -> if C.eq c C.czero then () else absurd
    | Term c j -> set a i j (C.add (get a i j) c)
    | UTerm j -> set a i j (C.add (get a i j) C.cone)
    | Add e1 e2 -> fill_expr e1 i; fill_expr e2 i
    end in
  let rec fill_ctx (ctx:context) (i:int) : unit
    requires { ctx_bound ctx nv }
    variant { length l - i }
    requires { length l - i = length ctx }
    requires { 0 <= i <= length l }
    raises  { C.Unknown -> true }
  = match ctx with
    | Nil -> ()
    | Cons e t ->
      assert { i < length l };
      let ex, c = norm_eq e in
      if (not (C.eq c C.czero)) then b[i] <- C.add b[i] c;
      fill_expr ex i;
      fill_ctx t (i+1)
    end in
  let rec fill_goal (ex:expr) : unit
    requires { expr_bound ex nv }
    variant { ex }
    requires { no_cst ex }
    raises { C.Unknown -> true }
  = match ex with
    | Cst c -> if C.eq c C.czero then () else absurd
    | Term c j -> v[j] <- C.add v[j] c
    | UTerm j -> v[j] <- C.add v[j] C.cone
    | Add e1 e2 -> fill_goal e1; fill_goal e2
452
    end in
453
  fill_ctx l 0;
454
  let (ex, d) = norm_eq g in
455 456 457
  fill_goal ex;
  (*let show (a: matrix coeff) (b v: array coeff) (d: coeff) = breakpoint a in
  show a b v d;*)
458 459 460 461 462 463 464 465
  let ab = m_append a b in
  let cd = v_append v d in
  let ab' = transpose ab in
  match gauss_jordan (m_append ab' cd) with
    | Some r -> apply_l r a == v && C.eq (sprod r b) d
    | None -> false
  end

466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
(* forall eq in list interp_eq  est vraie -> interp_eq (toute combinaison linéaire) est vraie *)

end
module RationalCoeffs

use import int.Int
use import real.RealInfix
use import real.FromInt
use import int.Abs

meta coercion function from_int

type t = (int, int)
type rvars = int -> real

function of_int (n:int) : t = (n,1)
(*meta coercion function of_int*)


let constant rzero = (0,1)
let constant rone = (1,1)

function rinterp (t:t) (v:rvars) : real
= match t with
490
  | (n,d) ->  from_int n /. from_int d (*todo if d = 1 then n...*)
491 492 493 494 495 496 497 498 499
  end

use import int.ComputerDivision
use import ref.Ref
use import number.Gcd

let gcd (x:int) (y:int)
  requires { x >= 0 /\ y >= 0 }
  ensures { result = gcd x y }
500
  ensures { x > 0 -> result > 0 }
501
  =
502
  let ghost ox = x in
503 504 505 506 507 508
  let x = ref x in let y = ref y in
  label Pre in
  while (!y > 0) do
     invariant { !x >= 0 /\ !y >= 0 }
     invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
     variant { !y }
509
     invariant { ox > 0 -> !x > 0 }
510 511 512 513 514
     let r = mod !x !y in let ghost q = div !x !y in
     assert { r = !x - q * !y };
     x := !y; y := r;
  done;
  !x
515
(*
516 517 518 519
let simp (t:t) : t
  ensures { forall v:rvars. rinterp result v = rinterp t v }
= match t with
  | (n,d) ->
520 521 522 523 524 525 526 527
    let g = gcd (abs n) (abs d) in
    if g > 1
    then
      let n', d' = (div n g, div d g) in
      assert { n = g * n' /\ d = g * d' };
      assert { n /. d = n' /. d' };
      (n', d')
    else (n, d)
528
  end
529
*)
530 531
let radd (a b:t)
= match (a,b) with
532
  | (n1,d1), (n2,d2) -> (*simp*) ((n1*d2 + n2*d1),(d1*d2))
533 534 535 536
  end

let rmul (a b:t)
= match (a,b) with
537
  | (n1,d1), (n2, d2) -> (*simp*) (n1*n2, d1*d2)
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566
  end

let ropp (a:t)
= match a with
  | (n,d) -> (-n, d)
  end

let predicate req (a b:t)
= match (a,b) with
  | (n1,d1), (n2,d2) -> n1 * d2 = n2 * d1
  end

let rinv a
= match a with
  | (n,d) -> (d,n)
  end

let function rle (a b:t)
= match (a,b) with
  | (n1,d1), (n2,d2) -> n1 * d2 <= n2 * d1
  end

predicate (<=) (a b:t) = rle a b

end

module LinearDecisionRational

use import RationalCoeffs
567 568 569
use import real.RealInfix
use import real.FromInt

570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), type coeff = t, function C.interp=rinterp, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, lemma C.eq_def, val C.le=rle(*, goal ZeroLessOne, goal C.CompatOrderAdd, goal C.CompatOrderMult, goal C.Unitary, goal C.NonTrivialRing, goal C.Mul_distr_l, goal C.Mul_distr_r, goal C.Inv_def_l, goal C.Inv_def_r, goal C.MulAssoc.Assoc, goal C.Assoc, goal C.MulComm.Comm, goal C.Comm, goal C.Unit_def_l, goal C.Unit_def_r*)

end

module LinearDecisionInt

use import int.Int

function id (t:int) (v:int -> int) : int = t
let predicate eq (a b:int) = a=b

exception Unknown
let inv (t:int) : int
  ensures { forall v: int -> int. id result v * id t v = one }
  ensures { not (eq result zero) }
  raises { Unknown -> true }
= raise Unknown

clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), type coeff = int, function C.interp = id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = zero, val C.cone = one, lemma C.zero_def, lemma C.one_def, val C.add = (+), val C.mul = ( *), val C.opp = (-_), val C.eq = eq, val C.inv = inv, lemma C.eq_def, val C.le = (<=)(*, goal ZeroLessOne, goal C.CompatOrderAdd, goal C.CompatOrderMult, goal C.Unitary, goal C.NonTrivialRing, goal C.Mul_distr_l, goal C.Mul_distr_r, goal C.Inv_def_l, goal C.Inv_def_r, goal C.MulAssoc.Assoc, goal C.Assoc, goal C.MulComm.Comm, goal C.Comm, goal C.Unit_def_l, goal C.Unit_def_r*)


use import real.FromInt

axiom from_int_ext: forall x y: int. from_int x = from_int y -> x = y
(*FIXME put this in real.why ?*)

use import RationalCoeffs
use LinearDecisionRational as R
use import list.List
let function m (x:int) : (int, int)
  ensures { forall z. rinterp result z = from_int x }
  = (x,1)

val function m_y (y:int->int): (int -> real)
  ensures { forall i. result i = from_int (y i) }
605

606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639
let rec function m_expr (e:expr) : R.expr
  ensures { forall y z. R.interp result (m_y y) (m_y z) = from_int (interp e y z) }
  ensures { valid_expr e -> R.valid_expr result }
= match e with
  | Cst c -> R.Cst (m c)
  | Add e1 e2 -> R.Add (m_expr e1) (m_expr e2)
  | Term c n -> R.Term (m c) n
  | UTerm n -> R.UTerm n
  end

let function m_eq (eq:equality) : R.equality
  ensures { forall y z. R.interp_eq result (m_y y) (m_y z)
                        <-> interp_eq eq y z }
  ensures { valid_eq eq -> R.valid_eq result }
= match eq with (e1,e2) -> (m_expr e1, m_expr e2) end

let rec function m_ctx (ctx:context) : R.context
  ensures { forall y z g. R.interp_ctx result (m_eq g) (m_y y) (m_y z) <->
                        interp_ctx ctx g y z }
  ensures { valid_ctx ctx -> R.valid_ctx result }
  variant { ctx }
= match ctx with
  | Nil -> Nil
  | Cons h t ->
    let r = Cons (m_eq h) (m_ctx t) in
    r
    end

let int_decision (l: context) (g: equality) : bool
  requires { valid_ctx l }
  requires { valid_eq g }
  ensures { forall y z. result -> interp_ctx l g y z }
  (*raises  { R.Unknown -> true } ??? *)
= R.linear_decision (m_ctx l) (m_eq g)
640 641 642

end

643 644

module Test
645 646 647 648 649 650 651 652 653 654 655 656 657

use import RationalCoeffs
use import LinearDecisionRational
use import int.Int
use import real.RealInfix
use import real.FromInt

meta coercion function from_int

goal g: forall x y: real.
        (from_int 3 /. from_int 1) *. x +. (from_int 2/. from_int 1) *. y = (from_int 21/. from_int 1) ->
        (from_int 7 /. from_int 1) *. x +. (from_int 4/. from_int 1) *. y = (from_int 47/. from_int 1) ->
        x = (from_int 5 /. from_int 1)
658 659 660 661 662 663 664 665 666 667 668 669
end

module TestInt

use import LinearDecisionInt
use import int.Int

goal g: forall x y:int.
     3 * x + 2 * y = 21 ->
     7 * x + 4 * y = 47 ->
     x = 5

670
end