list.why 4.07 KB
Newer Older
1
2
3

theory List

4
  type list 'a = Nil | Cons 'a (list 'a)
5
6
7
8
9
10
11

end

theory Length
  use import int.Int
  use import List

12
  logic length (l : list 'a) : int = 
13
    match l with
14
15
    | Nil      -> 0
    | Cons _ r -> 1 + length(r)
16
17
    end

18
  lemma Length_nonnegative : forall l:list 'a. length(l) >= 0
19

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

22
23
24
25
26
end

theory Mem
  use export List
 
27
  logic mem (x: 'a) (l : list 'a) = match l with
28
    | Nil      -> false
29
    | Cons y r -> x = y or mem x r
30
31
32
33
    end

end

34
35
theory Nth
  use export List
36
  use export option.Option
37
38
  use import int.Int
  
39
  logic nth (n : int) (l : list 'a) : option 'a = match l with
40
41
    | Nil -> None
    | Cons x r -> if n = 0 then Some x else nth (n - 1) r
42
43
44
45
  end

end

46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
theory HdTl "head and tail"

  use export List
  use export option.Option

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

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

  (* TODO: move these lemmas into another theory? *)
  use import Nth
  use import int.Int

  lemma Nth_tl :
    forall l1 l2 : list 'a. tl l1 = Some l2 -> 
    forall i : int. nth i l2 = nth (i+1) l1

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

end


75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
theory Append
  use export List

  logic append (l1 l2 : list 'a) : list 'a = match l1 with
    | Nil -> l2
    | Cons x1 r1 -> Cons x1 (append r1 l2)
  end

  lemma Append_assoc : 
    forall l1 l2 l3 : list 'a. 
    append l1 (append l2 l3) = append (append l1 l2) l3

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

  use import Length
  use import int.Int

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

end

theory Reverse

  use export List
  use import Append

  logic reverse (l : list 'a) : list 'a = match l with
    | Nil -> Nil
    | Cons x r -> append (reverse r) (Cons x Nil)
  end

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

end

115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
theory Sorted

  use export List
  use import int.Int
 
  inductive sorted (l : list int) =
    | Sorted_Nil : 
        sorted Nil
    | Sorted_One : 
        forall x:int. sorted (Cons x Nil)
    | Sorted_Two : 
        forall x y : int, l : list int. 
        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
 
  use import Mem

  lemma Sorted_mem :
    forall x : int, l : list int.
    (forall y : int. mem y l -> x <= y) and sorted l <-> sorted (Cons x l)

end

theory NumOcc
  
  use import int.Int
  use import List

  (* number of occurence of x in l *)
  logic 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

  use import Mem

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

end

156
theory Permut
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187

  use import NumOcc
  use import List

  logic 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 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

188
189
190
191
192
end

theory Induction
  use import List

193
194
195
  type elt

  logic p (list elt)
196
197

  axiom Induction : 
198
199
200
    p (Nil : list elt) ->
    (forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
    forall l:list elt. p l
201
202
203
204
205
206
207
208

end

theory Map
  use import List
 
  type a
  type b 
209
  logic f a : b
210

211
  logic map(l : list a) : list b = 
212
    match l with
213
    | Nil      -> Nil
214
    | Cons x r -> Cons (f x) (map r)
215
216
217
218
219
220
221
    end

end

theory Fold
  (* TODO (a la Map) *)
end