examples/proper_cuts.mlw

   1
   2 (** {1 Proper Cuts}
   3
   4     This is a small functional programming exercise.
   5     Given a list `l`, build the list of all cuts of `l`,
   6     a cut being a pair of lists `(l1, l2)` such that `l`
   7     is the concatenation of `l1` and `l2`.
   8
   9     Author: Mário Pereira (NOVA LINCS)
  10     with slight modifications by Jean-Christophe Filliâtre (CNRS)
  11 *)
  12
  13 module ProperCut
  14
  15   use list.List, list.Append
  16   use list.Mem, list.Distinct
  17
  18   predicate injective (f: 'a -> 'b) =
  19     forall x x'. x <> x' -> f x <> f x'
  20
  21   (** A `map` function in the style of OCaml `List.map`. Other than just
  22       specifying that `map f l` is the point-wise projection of the elements in
  23       `l`, we also state that an injective function `f` preserves the
  24       property of no repeated elements in the result list `r`. *)
  25
  26   let rec function map (f: 'a -> 'b) (l: list 'a) : (r: list 'b)
  27     ensures  { forall y. mem y r <-> (exists x. mem x l && y = f x) }
  28     ensures  { distinct l -> injective f -> distinct r }
  29     variant  { l }
  30   = match l with
  31     | Nil      -> Nil
  32     | Cons x s -> Cons (f x) (map f s)
  33     end
  34
  35   predicate cut (l1 l2: list 'a) (l: list 'a) =
  36     l1 ++ l2 = l
  37
  38   type cut_list 'a = list (list 'a, list 'a)
  39
  40   (** The list of all cuts for a list `l` must respect two conditions:
  41         1. there are no duplicate elements in the list;
  42         2. a pair `(l1, l2)` belongs to the cut list if is a valid cut
  43            of `l` (soundness);
  44         3. if a pair `(l1, l2)` is a cut of `l`, then it belongs to the list `l`
  45            (completness). *)
  46   predicate proper_cuts (c: cut_list 'a) (l: list 'a) =
  47     distinct c && (forall l1 l2. mem (l1, l2) c <-> cut l1 l2 l)
  48
  49   scope Harness
  50
  51     constant le : list int = Nil
  52     constant ce : cut_list int = (Cons (Nil, Nil) Nil)
  53     goal Ge : proper_cuts ce le
  54
  55     constant l3 : list int = Cons 3 Nil
  56     constant c3 : list (list int, list int) =
  57       Cons (Nil, Cons 3 Nil) (Cons (Cons 3 Nil, Nil) Nil)
  58     goal G3 : proper_cuts c3 l3
  59
  60   end
  61
  62   (** A specialized function `cons` to be used as the argument of `map`. For any
  63       pair `(l1, l2)` it returns `(x::l1, l2)`.  *)
  64   let function cons (x: 'a) : (f: (list 'a, list 'a) -> (list 'a, list 'a))
  65     ensures { injective f }
  66     ensures { forall l l1 l2. mem (l1, l2) (map f l) <->
  67               exists s1. l1 = Cons x s1 && mem (s1, l2) l }
  68   = fun l -> let (l1,l2) = l in (Cons x l1, l2)
  69
  70   (** The main function `proper_cuts` *)
  71   let rec proper_cuts (l: list 'a) : (r: cut_list 'a)
  72     variant { l }
  73     ensures { proper_cuts r l }
  74   = match l with
  75     | Nil ->
  76         Cons (Nil, Nil) Nil
  77     | Cons x r ->
  78         (* First, compute the cuts of the tail list `r` *)
  79         let pr = proper_cuts r in
  80         (* Then, inject `x` in `pr` using `map` and `cons` defined before *)
  81         let r  = map (cons x) pr in
  82         (* Finally, add the `(Nil, r)` as the remaining cut of `l` *)
  83         Cons (Nil, l) r
  84     end
  85
  86 end