examples/tests/lemma_functions.mlw

   1 module LemmaFunction1
   2
   3   use int.Int
   4   use ref.Refint
   5
   6   function fact int : int
   7   axiom fact0 : fact 0 = 1
   8   axiom factn : forall n: int. n > 0 -> fact n = n * fact (n - 1)
   9
  10   let rec lemma f (n: int) : unit variant {n}
  11     requires { n >= 0 }
  12     ensures  { fact n >= 1 }
  13     =
  14     if n > 0 then f (n-1)
  15
  16   goal g: fact 42 >= 1
  17
  18 end
  19
  20 module LemmaFunction2
  21
  22   use int.Int
  23   use array.Array
  24   use array.ArraySum
  25
  26   let rec lemma sum_nonneg (a: array int) (l u: int) : unit
  27     requires { 0 <= l <= u <= length a }
  28     requires { forall i: int. 0 <= i < length a -> a[i] >= 0 }
  29     variant  { u-l }
  30     ensures  { sum a l u >= 0 }
  31   =
  32     if u > l then sum_nonneg a (l+1) u
  33
  34   goal g1:
  35     forall a: array int.
  36     (forall i: int. 0 <= i < length a -> a[i] >= 0) ->
  37     sum a 0 (length a) >= 0
  38
  39 end
  40
  41
  42
  43
  44 module M
  45
  46   use int.Int
  47
  48   type list 'a = Nil | Cons 'a (list 'a)
  49
  50   function length (l:list 'a) : int =
  51     match l with
  52     | Nil -> 0
  53     | Cons _ r -> 1 + length r
  54     end
  55
  56
  57   let rec lemma_length_non_neg (l:list 'a) : unit
  58     variant { l }
  59     ensures { length l >= 0 }
  60   =
  61     match l with
  62     | Nil -> ()
  63     | Cons _ r -> lemma_length_non_neg r
  64     end
  65
  66
  67   let rec toy_example(l:list 'a) : unit
  68     (* variant { l } does not work (not a sub-term) *)
  69     variant { length l }
  70     (* works if we add the "ghost lemma_length_non_neg" *)
  71   =
  72     match l with
  73     | Nil -> ()
  74     | Cons _ Nil -> ()
  75     | Cons x (Cons _ r) ->
  76       ghost lemma_length_non_neg l;
  77       toy_example (Cons x r)
  78     end
  79
  80 end