mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
645 lines
12 KiB
Plaintext
645 lines
12 KiB
Plaintext
|
|
(** {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
|
|
|
|
lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil
|
|
|
|
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
|
|
axiom nth_cons_n: forall x:'a, r:list 'a, n:int.
|
|
n > 0 -> nth n (Cons x r) = nth (n-1) r
|
|
|
|
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
|
|
|
|
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
|
|
|
|
(** {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
|
|
|
|
function tl (l: list 'a) : list 'a
|
|
|
|
axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r
|
|
|
|
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
|
|
|
|
lemma Nth0_head:
|
|
forall l: list 'a. nth 0 l = hd l
|
|
|
|
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
|
|
|
|
lemma Append_l_nil:
|
|
forall l: list 'a. l ++ Nil = l
|
|
|
|
use Length
|
|
use int.Int
|
|
|
|
lemma Append_length:
|
|
forall l1 [@induction] l2: list 'a. length (l1 ++ l2) = length l1 + length l2
|
|
|
|
use 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
|
|
|
|
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
|
|
|
|
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
|
|
|
|
(** {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)
|
|
|
|
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 Mem
|
|
|
|
lemma reverse_mem:
|
|
forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l)
|
|
|
|
use Length
|
|
|
|
lemma Reverse_length:
|
|
forall l: list 'a. length (reverse l) = length l
|
|
|
|
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)
|
|
|
|
use int.Int
|
|
use Length
|
|
|
|
lemma rev_append_length:
|
|
forall s [@induction] t: list 'a.
|
|
length (rev_append s t) = length s + length t
|
|
|
|
use 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
|
|
|
|
(** {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)
|
|
|
|
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)
|
|
|
|
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
|
|
|
|
use Mem
|
|
|
|
lemma Mem_Num_Occ :
|
|
forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0
|
|
|
|
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
|
|
|
|
use Reverse
|
|
|
|
lemma reverse_num_occ :
|
|
forall x: 'a, l: list 'a.
|
|
num_occ x l = num_occ x (reverse l)
|
|
|
|
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
|
|
|
|
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 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 Mem
|
|
|
|
lemma Permut_mem:
|
|
forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2
|
|
|
|
use Length
|
|
|
|
lemma Permut_length:
|
|
forall l1 [@induction] l2: list 'a. permut l1 l2 -> length l1 = length l2
|
|
|
|
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)
|
|
|
|
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
|
|
|
|
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)
|
|
|
|
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
|