Proper Cuts

This is a small functional programming exercise. Given a list l, build the list of all cuts of l, a cut being a pair of lists (l1, l2) such that l is the concatenation of l1 and l2.

Author: Mário Pereira (NOVA LINCS) with slight modifications by Jean-Christophe Filliâtre (CNRS)

module ProperCut

  use list.List, list.Append
  use list.Mem, list.Distinct

  predicate injective (f: 'a -> 'b) =
    forall x x'. x <> x' -> f x <> f x'

A map function in the style of OCaml List.map. Other than just specifying that map f l is the point-wise projection of the elements in l, we also state that an injective function f preserves the property of no repeated elements in the result list r.

  let rec function map (f: 'a -> 'b) (l: list 'a) : (r: list 'b)
    ensures  { forall y. mem y r <-> (exists x. mem x l && y = f x) }
    ensures  { distinct l -> injective f -> distinct r }
    variant  { l }
  = match l with
    | Nil      -> Nil
    | Cons x s -> Cons (f x) (map f s)
    end

  predicate cut (l1 l2: list 'a) (l: list 'a) =
    l1 ++ l2 = l

  type cut_list 'a = list (list 'a, list 'a)

  predicate proper_cuts (c: cut_list 'a) (l: list 'a) =
    distinct c && (forall l1 l2. mem (l1, l2) c <-> cut l1 l2 l)

  scope Harness

    constant le : list int = Nil
    constant ce : cut_list int = (Cons (Nil, Nil) Nil)
    goal Ge : proper_cuts ce le

    constant l3 : list int = Cons 3 Nil
    constant c3 : list (list int, list int) =
      Cons (Nil, Cons 3 Nil) (Cons (Cons 3 Nil, Nil) Nil)
    goal G3 : proper_cuts c3 l3

  end

  let function cons (x: 'a) : (f: (list 'a, list 'a) -> (list 'a, list 'a))
    ensures { injective f }
    ensures { forall l l1 l2. mem (l1, l2) (map f l) <->
              exists s1. l1 = Cons x s1 && mem (s1, l2) l }
  = fun l -> let (l1,l2) = l in (Cons x l1, l2)

  let rec proper_cuts (l: list 'a) : (r: cut_list 'a)
    variant { l }
    ensures { proper_cuts r l }
  = match l with
    | Nil ->
        Cons (Nil, Nil) Nil
    | Cons x r ->
        (* First, compute the cuts of the tail list `r` *)
        let pr = proper_cuts r in
        (* Then, inject `x` in `pr` using `map` and `cons` defined before *)
        let r  = map (cons x) pr in
        (* Finally, add the `(Nil, r)` as the remaining cut of `l` *)
        Cons (Nil, l) r
    end

end