Why3 Standard Library index



Polymorphic Lists


Basic theory of polymorphic lists

theory List

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

end

Length of a list

theory Length

  use import int.Int
  use import List

  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

  lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil

end

Membership in a list

theory Mem
  use import List

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

end

theory Elements

  use import List
  use Mem
  use set.Fset as FSet

  function elements (list 'a) : FSet.set 'a

  axiom elements_mem:
    forall l:list 'a, x:'a.
      Mem.mem x l <-> FSet.mem x (elements l)

  lemma elements_Nil:
    elements (Nil : list 'a) = FSet.empty

end

Nth element of a list

theory Nth

  use import List
  use import option.Option
  use import int.Int

  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

theory NthNoOpt

  use import List
  use import 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
  axiom nth_cons_n: forall x:'a, r:list 'a, n:int.
    n > 0 -> nth n (Cons x r) = nth (n-1) r

end

theory NthLength

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

  lemma nth_none_1:
     forall l: list 'a, i: int. i < 0 -> nth i l = None

  lemma nth_none_2:
     forall l: list 'a, i: int. i >= length l -> nth i l = None

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

end

Head and tail

theory HdTl

  use import List
  use import option.Option

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

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

end

theory HdTlNoOpt

  use import List

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

  axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x

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

  axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r

end

Relation between head, tail, and nth

theory NthHdTl

  use import int.Int
  use import option.Option
  use import List
  use import Nth
  use import 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

  lemma Nth0_head:
    forall l: list 'a. nth 0 l = hd l

end

Appending two lists

theory Append

  use import List

  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

  lemma Append_l_nil:
    forall l: list 'a. l ++ Nil = l

  use import Length
  use import int.Int

  lemma Append_length:
    forall l1 "induction" l2: list 'a. length (l1 ++ l2) = length l1 + length l2

  use import Mem

  lemma mem_append:
    forall x: 'a, l1 "induction" l2: list 'a.
    mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2

  lemma mem_decomp:
    forall x: 'a, l: list 'a.
    mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2

end

theory NthLengthAppend

  use import int.Int
  use import 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

  lemma nth_append_2:
    forall l1 "induction" l2: list 'a, i: int.
    length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2

end

Reversing a list

theory Reverse

  use import List
  use import Append

  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)

  lemma reverse_cons:
    forall l: list 'a, x: 'a.
    reverse (Cons x l) = reverse l ++ Cons x Nil

  lemma cons_reverse:
    forall l: list 'a, x: 'a.
    Cons x (reverse l) = reverse (l ++ Cons x Nil)

  lemma reverse_reverse:
    forall l: list 'a. reverse (reverse l) = l

  use import Mem

  lemma reverse_mem:
    forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)

  use import Length

  lemma Reverse_length:
    forall l: list 'a. length (reverse l) = length l

end

Reverse append

theory RevAppend

  use import List

  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 import 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)

  use import int.Int
  use import Length

  lemma rev_append_length:
    forall s "induction" t: list 'a.
      length (rev_append s t) = length s + length t

  use import Reverse

  lemma rev_append_def:
    forall r "induction" s: list 'a. rev_append r s = reverse r ++ s

  lemma rev_append_append_r:
    forall r s t: list 'a.
      rev_append r (s ++ t) = rev_append (rev_append s r) t

end

Zip

theory Combine

  use import List

  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

Sorted lists for some order as parameter

theory Sorted

  use import List

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

  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 import 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)

  use import 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)

end

Sorted lists of integers

theory SortedInt

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

end

theory RevSorted

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

  use import List

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

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

  use import 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

Number of occurrences in a list

theory NumOcc

  use import int.Int
  use import 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

  use import Mem

  lemma Mem_Num_Occ :
    forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0

  use import 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

  use import Reverse

  lemma reverse_num_occ :
    forall x: 'a, l: list 'a.
    num_occ x l = num_occ x (reverse l)

end

Permutation of lists

theory Permut

  use import NumOcc
  use import 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

  lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1

  lemma Permut_trans:
    forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3

  lemma Permut_cons:
    forall x: 'a, l1 l2: list 'a.
    permut l1 l2 -> permut (Cons x l1) (Cons x l2)

  lemma Permut_swap:
    forall x y: 'a, l: list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l))

  use import Append

  lemma Permut_cons_append:
    forall x : 'a, l1 l2 : list 'a.
    permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)

  lemma Permut_assoc:
    forall l1 l2 l3: list 'a.
    permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3))

  lemma Permut_append:
    forall l1 l2 k1 k2 : list 'a.
    permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)

  lemma Permut_append_swap:
    forall l1 l2 : list 'a.
    permut (l1 ++ l2) (l2 ++ l1)

  use import Mem

  lemma Permut_mem:
    forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2

  use import Length

  lemma Permut_length:
    forall l1 l2: list 'a. permut l1 l2 -> length l1 = length l2

end

List with pairwise distinct elements

theory Distinct

  use import List
  use import Mem

  inductive distinct (l: list 'a) =
    | distinct_zero: distinct (Nil: list 'a)
    | distinct_one : forall x:'a. distinct (Cons x Nil)
    | distinct_many:
        forall x:'a, l: list 'a.
        not (mem x l) -> distinct l -> distinct (Cons x l)

  use import 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)

end

theory Prefix

  use import List
  use import int.Int

  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

theory Sum

  use import List
  use import int.Int

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

end

Induction on lists

theory Induction

  use import List

  type elt

  predicate p (list elt)

  axiom Induction:
    p (Nil: list elt) ->
    (forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
    forall l:list elt. p l

end

Maps as lists of pairs

theory Map

  use import List

  type a
  type b
  function f a : b

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

Generic recursors on lists

theory FoldLeft

  use import List

  type a
  type b
  function f b a : b

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

end

theory FoldRight

  use import List

  type a
  type b
  function f a b : b

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

end

Importation of all list theories in one

theory 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

Generated by why3doc 0.87.2