list.mlw

(** {1 Polymorphic Lists} *)

(** {2 Basic theory of polymorphic lists} *)

module List

  type list 'a = Nil | Cons 'a (list 'a)

  let predicate is_nil (l:list 'a)
    ensures { result <-> l = Nil }
  =
    match l with Nil -> true | Cons _ _ -> false end

end

(** {2 Length of a list} *)

module Length

  use int.Int
  use List

  let rec function length (l: list 'a) : int =
    match l with
    | Nil      -> 0
    | Cons _ r -> 1 + length r
    end

  lemma Length_nonnegative: forall l: list 'a. length l >= 0
  meta "remove_unused:dependency" lemma Length_nonnegative, function length

  lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil
  meta "remove_unused:dependency" lemma Length_nil, function length

end

(** {2 Membership in a list} *)

module Mem
  use List

  predicate mem (x: 'a) (l: list 'a) = match l with
    | Nil      -> false
    | Cons y r -> x = y \/ mem x r
    end

end

(** {2 Quantifiers on lists} *)

module Quant

  use List
  use Mem

  let rec function for_all (p: 'a -> bool) (l:list 'a) : bool
    ensures { result <-> forall x. mem x l -> p x }
  =
    match l with
    | Nil -> true
    | Cons x r -> p x && for_all p r
    end

  let rec function for_some (p: 'a -> bool) (l:list 'a) : bool
    ensures { result <-> exists x. mem x l /\ p x }
  =
    match l with
    | Nil -> false
    | Cons x r -> p x || for_some p r
    end

  let function mem (eq:'a -> 'a -> bool) (x:'a) (l:list 'a) : bool
    ensures  { result <-> exists y. mem y l /\ eq x y }
  =
    for_some (eq x) l

end


module Elements

  use set.Fset
  use List
  use Mem

  function elements (l: list 'a) : fset 'a =
    match l with
    | Nil -> empty
    | Cons x r -> add x (elements r)
    end

  lemma elements_mem:
    forall x: 'a, l: list 'a. mem x l <-> Fset.mem x (elements l)

end

(** {2 Nth element of a list} *)

module Nth

  use List
  use option.Option
  use int.Int

  let rec function nth (n: int) (l: list 'a) : option 'a =
    match l with
    | Nil      -> None
    | Cons x r -> if n = 0 then Some x else nth (n - 1) r
    end

end

module NthNoOpt

  use List
  use int.Int

  function nth (n: int) (l: list 'a) : 'a

  axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x
  meta "remove_unused:dependency" axiom nth_cons_0, function nth

  axiom nth_cons_n: forall x:'a, r:list 'a, n:int.
    n > 0 -> nth n (Cons x r) = nth (n-1) r
  meta "remove_unused:dependency" axiom nth_cons_n, function nth

end

module NthLength

  use int.Int
  use option.Option
  use List
  use export Nth
  use export Length

  lemma nth_none_1:
     forall l: list 'a, i: int. i < 0 -> nth i l = None
  meta "remove_unused:dependency" lemma nth_none_1, function nth

  lemma nth_none_2:
     forall l: list 'a, i: int. i >= length l -> nth i l = None
  meta "remove_unused:dependency" lemma nth_none_2, function nth

  lemma nth_none_3:
     forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= length l
  meta "remove_unused:dependency" lemma nth_none_3, function nth

end

(** {2 Head and tail} *)

module HdTl

  use List
  use option.Option

  let function hd (l: list 'a) : option 'a = match l with
    | Nil      -> None
    | Cons h _ -> Some h
  end

  let function tl (l: list 'a) : option (list 'a) = match l with
    | Nil      -> None
    | Cons _ t -> Some t
  end

end

module HdTlNoOpt

  use List

  function hd (l: list 'a) : 'a

  axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x
  meta "remove_unused:dependency" axiom hd_cons, function hd

  function tl (l: list 'a) : list 'a

  axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r
  meta "remove_unused:dependency" axiom tl_cons, function tl

end

(** {2 Relation between head, tail, and nth} *)

module NthHdTl

  use int.Int
  use option.Option
  use List
  use Nth
  use HdTl

  lemma Nth_tl:
    forall l1 l2: list 'a. tl l1 = Some l2 ->
    forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1
  meta "remove_unused:dependency" lemma Nth_tl, function nth

  lemma Nth0_head:
    forall l: list 'a. nth 0 l = hd l
  meta "remove_unused:dependency" lemma Nth0_head, function nth

end

(** {2 Appending two lists} *)

module Append

  use List

  let rec function (++) (l1 l2: list 'a) : list 'a =
    match l1 with
    | Nil -> l2
    | Cons x1 r1 -> Cons x1 (r1 ++ l2)
    end

  lemma Append_assoc:
    forall l1 [@induction] l2 l3: list 'a.
    l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
  meta "remove_unused:dependency" lemma Append_assoc, function (++)

  lemma Append_l_nil:
    forall l: list 'a. l ++ Nil = l
  meta "remove_unused:dependency" lemma Append_l_nil, function (++)

  use Length
  use int.Int

  lemma Append_length:
    forall l1 [@induction] l2: list 'a. length (l1 ++ l2) = length l1 + length l2
  meta "remove_unused:dependency" lemma Append_length, function (++)

  use Mem

  lemma mem_append:
    forall x: 'a, l1 [@induction] l2: list 'a.
    mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2
  meta "remove_unused:dependency" lemma mem_append, function (++)

  lemma mem_decomp:
    forall x: 'a, l: list 'a.
    mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2
  meta "remove_unused:dependency" lemma mem_decomp, function (++)

end

module NthLengthAppend

  use int.Int
  use List
  use export NthLength
  use export Append

  lemma nth_append_1:
    forall l1 l2: list 'a, i: int.
    i < length l1 -> nth i (l1 ++ l2) = nth i l1
  meta "remove_unused:dependency" lemma nth_append_1, function nth

  lemma nth_append_2:
    forall l1 [@induction] l2: list 'a, i: int.
    length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2
  meta "remove_unused:dependency" lemma nth_append_2, function nth

end

(** {2 Reversing a list} *)

module Reverse

  use List
  use Append

  let rec function reverse (l: list 'a) : list 'a =
    match l with
    | Nil      -> Nil
    | Cons x r -> reverse r ++ Cons x Nil
    end

  lemma reverse_append:
    forall l1 l2: list 'a, x: 'a.
    (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2)
  meta "remove_unused:dependency" lemma reverse_append, function reverse

  lemma reverse_cons:
    forall l: list 'a, x: 'a.
    reverse (Cons x l) = reverse l ++ Cons x Nil
  meta "remove_unused:dependency" lemma reverse_cons, function reverse


  lemma cons_reverse:
    forall l: list 'a, x: 'a.
    Cons x (reverse l) = reverse (l ++ Cons x Nil)
  meta "remove_unused:dependency" lemma cons_reverse, function reverse

  lemma reverse_reverse:
    forall l: list 'a. reverse (reverse l) = l
  meta "remove_unused:dependency" lemma reverse_reverse, function reverse

  use Mem

  lemma reverse_mem:
    forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)
  meta "remove_unused:dependency" lemma reverse_mem, function reverse

  use Length

  lemma Reverse_length:
    forall l: list 'a. length (reverse l) = length l
  meta "remove_unused:dependency" lemma Reverse_length, function reverse

end

(** {2 Reverse append} *)

module RevAppend

  use List

  let rec function rev_append (s t: list 'a) : list 'a =
    match s with
    | Cons x r -> rev_append r (Cons x t)
    | Nil -> t
    end

  use Append

  lemma rev_append_append_l:
    forall r [@induction] s t: list 'a.
      rev_append (r ++ s) t = rev_append s (rev_append r t)
  meta "remove_unused:dependency" lemma rev_append_append_l, function rev_append

  use int.Int
  use Length

  lemma rev_append_length:
    forall s [@induction] t: list 'a.
      length (rev_append s t) = length s + length t
  meta "remove_unused:dependency" lemma rev_append_length, function rev_append

  use Reverse

  lemma rev_append_def:
    forall r [@induction] s: list 'a. rev_append r s = reverse r ++ s
  meta "remove_unused:dependency" lemma rev_append_def, function rev_append

  lemma rev_append_append_r:
    forall r s t: list 'a.
      rev_append r (s ++ t) = rev_append (rev_append s r) t
  meta "remove_unused:dependency" lemma rev_append_append_r, function rev_append

end

(** {2 Zip} *)

module Combine

  use List

  let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b)
  = match x, y with
    | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y)
    | _ -> Nil
    end

end

(** {2 Sorted lists for some order as parameter} *)

module Sorted

  use List

  type t
  predicate le t t
  clone relations.Transitive with
    type t = t, predicate rel = le, axiom Trans

  inductive sorted (l: list t) =
    | Sorted_Nil:
        sorted Nil
    | Sorted_One:
        forall x: t. sorted (Cons x Nil)
    | Sorted_Two:
        forall x y: t, l: list t.
        le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))

  use Mem

  lemma sorted_mem:
    forall x: t, l: list t.
    (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l)
  meta "remove_unused:dependency" lemma sorted_mem, predicate sorted

  use Append

  lemma sorted_append:
    forall  l1 [@induction] l2: list t.
    (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y))
    <->
    sorted (l1 ++ l2)
  meta "remove_unused:dependency" lemma sorted_append, predicate sorted

end

(** {2 Sorted lists of integers} *)

module SortedInt

  use int.Int
  clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans

end

module RevSorted

  type t
  predicate le t t
  clone relations.Transitive with
    type t = t, predicate rel = le, axiom Trans
  predicate ge (x y: t) = le y x

  use List

  clone Sorted as Incr with type t = t, predicate le = le, goal .
  clone Sorted as Decr with type t = t, predicate le = ge, goal .

  predicate compat (s t: list t) =
    match s, t with
    | Cons x _, Cons y _ -> le x y
    | _, _ -> true
    end

  use RevAppend

  lemma rev_append_sorted_incr:
    forall s [@induction] t: list t.
      Incr.sorted (rev_append s t) <->
        Decr.sorted s /\ Incr.sorted t /\ compat s t

  lemma rev_append_sorted_decr:
    forall s [@induction] t: list t.
      Decr.sorted (rev_append s t) <->
        Incr.sorted s /\ Decr.sorted t /\ compat t s

end

(** {2 Number of occurrences in a list} *)

module NumOcc

  use int.Int
  use List

  function num_occ (x: 'a) (l: list 'a) : int =
    match l with
    | Nil      -> 0
    | Cons y r -> (if x = y then 1 else 0) + num_occ x r
    end
  (** number of occurrences of `x` in `l` *)

  lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0
  meta "remove_unused:dependency" lemma Num_Occ_NonNeg, function num_occ

  use Mem

  lemma Mem_Num_Occ :
    forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0
  meta "remove_unused:dependency" lemma Mem_Num_Occ, function num_occ

  use Append

  lemma Append_Num_Occ :
    forall x: 'a, l1 [@induction] l2: list 'a.
    num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2
  meta "remove_unused:dependency" lemma Append_Num_Occ, function num_occ

  use Reverse

  lemma reverse_num_occ :
    forall x: 'a, l: list 'a.
    num_occ x l = num_occ x (reverse l)
  meta "remove_unused:dependency" lemma reverse_num_occ, function num_occ

end

(** {2 Permutation of lists} *)

module Permut

  use NumOcc
  use List

  predicate permut (l1: list 'a) (l2: list 'a) =
    forall x: 'a. num_occ x l1 = num_occ x l2

  lemma Permut_refl: forall l: list 'a. permut l l
  meta "remove_unused:dependency" lemma Permut_refl, predicate permut

  lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1
  meta "remove_unused:dependency" lemma Permut_sym, predicate permut

  lemma Permut_trans:
    forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3
  meta "remove_unused:dependency" lemma Permut_trans, predicate permut

  lemma Permut_cons:
    forall x: 'a, l1 l2: list 'a.
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)
  meta "remove_unused:dependency" lemma Permut_cons, predicate permut

  lemma Permut_swap:
    forall x y: 'a, l: list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l))
  meta "remove_unused:dependency" lemma Permut_swap, predicate permut

  use Append

  lemma Permut_cons_append:
    forall x : 'a, l1 l2 : list 'a.
    permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
  meta "remove_unused:dependency" lemma Permut_cons_append, predicate permut

  lemma Permut_assoc:
    forall l1 l2 l3: list 'a.
    permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3))
  meta "remove_unused:dependency" lemma Permut_assoc, predicate permut

  lemma Permut_append:
    forall l1 l2 k1 k2 : list 'a.
    permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
  meta "remove_unused:dependency" lemma Permut_append, predicate permut

  lemma Permut_append_swap:
    forall l1 l2 : list 'a.
    permut (l1 ++ l2) (l2 ++ l1)
  meta "remove_unused:dependency" lemma Permut_append_swap, predicate permut

  use Mem

  lemma Permut_mem:
    forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2
  meta "remove_unused:dependency" lemma Permut_mem, predicate permut

  use Length

  lemma Permut_length:
    forall l1 [@induction] l2: list 'a. permut l1 l2 -> length l1 = length l2
  meta "remove_unused:dependency" lemma Permut_length, predicate permut

end

(** {2 List with pairwise distinct elements} *)

module Distinct

  use List
  use Mem

  predicate distinct (l: list 'a) =
    match l with
    | Nil | Cons _ Nil -> true
    | Cons x xs -> not (mem x xs) /\ distinct xs
    end

  use Append

  lemma distinct_append:
    forall l1 [@induction] l2: list 'a.
    distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
    distinct (l1 ++ l2)
  meta "remove_unused:dependency" lemma distinct_append, predicate distinct

end

module Prefix

  use List
  use int.Int

  let rec function prefix (n: int) (l: list 'a) : list 'a =
    if n <= 0 then Nil else
    match l with
    | Nil -> Nil
    | Cons x r -> Cons x (prefix (n-1) r)
    end

end

module Sum

  use List
  use int.Int

  let rec function sum (l: list int) : int =
    match l with
    | Nil -> 0
    | Cons x r -> x + sum r
    end

end

(*
(** {2 Induction on lists} *)

module Induction

  use List

  (* type elt *)

  (* predicate p (list elt) *)

  axiom Induction:
    forall p: list 'a -> bool.
    p (Nil: list 'a) ->
    (forall x:'a. forall l:list 'a. p l -> p (Cons x l)) ->
    forall l:list 'a. p l

end
*)

(** {2 Maps as lists of pairs} *)

module Map

  use List

  function map (f: 'a -> 'b) (l: list 'a) : list 'b =
    match l with
    | Nil      -> Nil
    | Cons x r -> Cons (f x) (map f r)
    end
end

(** {2 Generic recursors on lists} *)

module FoldLeft

  use List

  function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (l: list 'a) : 'b =
    match l with
    | Nil      -> acc
    | Cons x r -> fold_left f (f acc x) r
    end

  use Append

  lemma fold_left_append:
    forall l1 [@induction] l2: list 'a, f: 'b -> 'a -> 'b, acc : 'b.
    fold_left f acc (l1++l2) = fold_left f (fold_left f acc l1) l2
  meta "remove_unused:dependency" lemma fold_left_append, function fold_left

end

module FoldRight

  use List

  function fold_right (f: 'a -> 'b -> 'b) (l: list 'a) (acc: 'b) : 'b =
    match l with
    | Nil      -> acc
    | Cons x r -> f x (fold_right f r acc)
    end

  use Append

  lemma fold_right_append:
    forall l1 [@induction] l2: list 'a, f: 'a -> 'b -> 'b, acc : 'b.
    fold_right f (l1++l2) acc = fold_right f l1 (fold_right f l2 acc)
  meta "remove_unused:dependency" lemma fold_right_append, function fold_right

end

(** {2 Importation of all list theories in one} *)

module ListRich

  use export List
  use export Length
  use export Mem
  use export Nth
  use export HdTl
  use export NthHdTl
  use export Append
  use export Reverse
  use export RevAppend
  use export NumOcc
  use export Permut

end