examples/verifythis_2016_matrix_multiplication/sum_extended.mlw

   1 module Sum_extended
   2
   3   use int.Int
   4   use int.Sum
   5
   6   function addf (f g:int -> int) : int -> int = fun x -> f x + g x
   7
   8   function smulf (f:int -> int) (l:int) : int -> int = fun x -> l * f x
   9
  10   let rec lemma sum_mult (f:int -> int) (a b l:int) : unit
  11     ensures { sum (smulf f l) a b = l * sum f a b }
  12     variant { b - a }
  13   = if b > a then sum_mult f a (b-1) l
  14
  15
  16   let rec lemma sum_add (f g:int -> int) (a b:int) : unit
  17     ensures { sum (addf f g) a b = sum f a b + sum g a b }
  18     variant { b - a }
  19   = if b > a then sum_add f g a (b-1)
  20
  21
  22   function sumf (f:int -> int -> int) (a b:int) : int -> int = fun x -> sum (f x) a b
  23
  24   let rec lemma fubini (f1 f2: int -> int -> int) (a b c d: int) : unit
  25     requires { forall x y. a <= x < b /\ c <= y < d -> f1 x y = f2 y x }
  26     ensures  { sum (sumf f1 c d) a b = sum (sumf f2 a b) c d }
  27     variant  { b - a }
  28   = if b <= a
  29     then assert { forall x. sumf f2 a b x = 0 }
  30     else begin
  31       fubini f1 f2 a (b-1) c d;
  32       assert { let ha = addf (sumf f2 a (b-1)) (f1 (b-1)) in
  33         sum (sumf f2 a b) c d = sum ha c d
  34         by forall y. c <= y < d -> sumf f2 a b y = ha y }
  35     end
  36
  37    let ghost sum_ext (f g: int -> int) (a b: int) : unit
  38      requires {forall i. a <= i < b -> f i = g i }
  39      ensures  { sum f a b  = sum g a b }
  40    = ()
  41
  42 end