mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
87 lines
2.9 KiB
Plaintext
87 lines
2.9 KiB
Plaintext
|
|
(** {1 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)
|
|
|
|
(** The list of all cuts for a list `l` must respect two conditions:
|
|
1. there are no duplicate elements in the list;
|
|
2. a pair `(l1, l2)` belongs to the cut list if is a valid cut
|
|
of `l` (soundness);
|
|
3. if a pair `(l1, l2)` is a cut of `l`, then it belongs to the list `l`
|
|
(completness). *)
|
|
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
|
|
|
|
(** A specialized function `cons` to be used as the argument of `map`. For any
|
|
pair `(l1, l2)` it returns `(x::l1, l2)`. *)
|
|
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)
|
|
|
|
(** The main function `proper_cuts` *)
|
|
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
|