monoid.mlw 1.87 KB
 Martin Clochard committed Aug 29, 2014 1 2 3 4 5 6 7 `````` (** {1 Abstract monoids} Author: Martin Clochard *) (** {2 Abstract logic monoid} *) module Monoid `````` Andrei Paskevich committed Oct 22, 2014 8 `````` `````` Martin Clochard committed Aug 29, 2014 9 10 `````` (** Elements of the monoid. *) type t `````` Andrei Paskevich committed Oct 22, 2014 11 `````` `````` Martin Clochard committed Aug 29, 2014 12 13 14 15 `````` (** Neutral element. *) constant zero : t (** Composition law. *) function op (a b:t) : t `````` Andrei Paskevich committed Oct 22, 2014 16 `````` `````` Martin Clochard committed Aug 29, 2014 17 18 19 `````` (** Monoid properties. *) axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c axiom neutral : forall x:t. op x zero = x = op zero x `````` Andrei Paskevich committed Oct 22, 2014 20 `````` `````` Martin Clochard committed Aug 29, 2014 21 22 23 24 ``````end (** {2 Abstract monoid with aggregation} *) module MonoidSum `````` Andrei Paskevich committed Oct 22, 2014 25 `````` `````` Martin Clochard committed May 19, 2017 26 `````` use import seq.Seq `````` Andrei Paskevich committed Jun 14, 2018 27 `````` clone import Monoid as M with axiom . `````` Andrei Paskevich committed Oct 22, 2014 28 `````` `````` Martin Clochard committed May 19, 2017 29 30 31 32 33 34 `````` function agg (f:'a -> t) (s:seq 'a) : t axiom agg_empty : forall f:'a -> t. agg f empty = zero axiom agg_sing : forall f,s:seq 'a. length s = 1 -> agg f s = f s[0] axiom agg_cat : forall f,s1 s2:seq 'a. agg f (s1 ++ s2) = op (agg f s1) (agg f s2) `````` Andrei Paskevich committed Oct 22, 2014 35 `````` `````` Martin Clochard committed Aug 29, 2014 36 37 ``````end `````` Martin Clochard committed May 19, 2017 38 ``````(** {2 Definition of aggregation (refinement of MonoidSum} *) `````` Martin Clochard committed Aug 29, 2014 39 ``````module MonoidSumDef `````` Martin Clochard committed May 19, 2017 40 41 42 43 44 `````` use import seq.Seq use import seq.FreeMonoid (* TODO: do that refinement correctly ! *) `````` Andrei Paskevich committed Jun 14, 2018 45 `````` clone import Monoid as M with axiom . `````` Martin Clochard committed May 19, 2017 46 47 48 `````` let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t variant { length s } `````` Andrei Paskevich committed Jun 10, 2017 49 `````` = if length s = 0 then zero else op (f s[0]) (agg f s[1 ..]) `````` Martin Clochard committed May 19, 2017 50 51 52 53 54 55 `````` lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a) ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) } variant { length s1 } `````` Andrei Paskevich committed Jun 10, 2017 56 `````` = if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2 `````` Martin Clochard committed May 19, 2017 57 58 59 60 61 62 63 64 65 66 `````` clone MonoidSum as MS with type M.t = M.t, constant M.zero = M.zero, function M.op = M.op, goal M.assoc, goal M.neutral, function agg = agg, goal agg_empty, goal agg_sing, goal agg_cat `````` Andrei Paskevich committed Oct 22, 2014 67 `````` `````` Martin Clochard committed Aug 29, 2014 68 69 70 71 ``````end (** {2 Computable monoid} *) module ComputableMonoid `````` Andrei Paskevich committed Oct 22, 2014 72 `````` `````` Andrei Paskevich committed Jun 14, 2018 73 `````` clone export Monoid with axiom . `````` Andrei Paskevich committed Oct 22, 2014 74 `````` `````` Martin Clochard committed Aug 29, 2014 75 76 `````` (** Abstract routines computing operations in the monoid. *) val zero () : t ensures { result = zero } `````` Andrei Paskevich committed Oct 22, 2014 77 `````` `````` Martin Clochard committed Aug 29, 2014 78 `````` val op (a b:t) : t ensures { result = op a b } `````` Andrei Paskevich committed Oct 22, 2014 79 `````` `````` Martin Clochard committed Aug 29, 2014 80 ``end``