examples_in_progress/avl/monoid/monoid.mlw

   1
   2 module Monoid
   3
   4   type t
   5
   6   constant zero : t
   7   function op (a b:t) : t
   8
   9   axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c
  10   axiom neutral : forall x:t. op x zero = x = op zero x
  11
  12 end
  13
  14 module MonoidList
  15
  16   use list.Append
  17   clone import Monoid as M
  18
  19   (* Because definitions cannot be replicated via cloning. *)
  20   function sum (f:'a -> t) (l:list 'a) : t
  21   axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero
  22   axiom sum_def_cons : forall f:'a -> t,x,q.
  23     sum f (Cons x q) = op (f x) (sum f q)
  24
  25   let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit
  26     ensures { sum f (l ++ r) = op (sum f l) (sum f r) }
  27     variant { l }
  28   = match l with Cons _ q -> sum_append f q r | _ -> () end
  29
  30 end
  31
  32 module MonoidListDef
  33   use list.List
  34
  35   namespace M
  36     type t
  37     constant zero : t
  38     function op (a b:t) : t
  39   end
  40   function sum (f:'a -> M.t) (l:list 'a) : M.t = match l with
  41     | Nil -> M.zero
  42     | Cons x q -> M.op (f x) (sum f q)
  43     end
  44   clone export MonoidList with type M.t = M.t,constant M.zero = M.zero,
  45     function M.op = M.op,function sum = sum,
  46     goal sum_def_nil,goal sum_def_cons
  47
  48 end
  49
  50 module ComputableMonoid
  51
  52   use program_type.TypeParams
  53   clone export program_type.Type0
  54   clone export Monoid with type t = m
  55
  56   val zero () : t
  57     ensures { c result /\ result.m = zero }
  58
  59   val op (a b:t) : t
  60     requires { c a /\ c b }
  61     ensures { c result /\ result.m = op a.m b.m }
  62
  63 end
  64