list.mlw 11.9 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Apr 20, 2012 2 3 4 5 ``````(** {1 Polymorphic Lists} *) (** {2 Basic theory of polymorphic lists} *) `````` Andrei Paskevich committed Dec 22, 2017 6 ``````module List `````` Jean-Christophe Filliâtre committed Mar 23, 2010 7 `````` `````` Andrei Paskevich committed Jun 24, 2010 8 `````` type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 9 `````` `````` MARCHE Claude committed Mar 09, 2016 10 11 12 13 14 `````` let predicate is_nil (l:list 'a) ensures { result <-> l = Nil } = match l with Nil -> true | Cons _ _ -> false end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 15 16 ``````end `````` MARCHE Claude committed Apr 20, 2012 17 18 ``````(** {2 Length of a list} *) `````` Andrei Paskevich committed Dec 22, 2017 19 ``````module Length `````` 20 `````` `````` Andrei Paskevich committed Jun 15, 2018 21 22 `````` use int.Int use List `````` Jean-Christophe Filliâtre committed Mar 23, 2010 23 `````` `````` Andrei Paskevich committed Sep 19, 2015 24 `````` let rec function length (l: list 'a) : int = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 25 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 26 `````` | Nil -> 0 `````` Jean-Christophe Filliatre committed Nov 29, 2010 27 `````` | Cons _ r -> 1 + length r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 28 29 `````` end `````` Jean-Christophe Filliatre committed Aug 03, 2011 30 `````` lemma Length_nonnegative: forall l: list 'a. length l >= 0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 31 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 32 `````` lemma Length_nil: forall l: list 'a. length l = 0 <-> l = Nil `````` Jean-Christophe Filliatre committed Nov 10, 2010 33 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 34 35 ``````end `````` MARCHE Claude committed Mar 09, 2016 36 37 38 39 ``````(** {2 Quantifiers on lists} *) module Quant `````` Andrei Paskevich committed Jun 15, 2018 40 `````` use List `````` MARCHE Claude committed Mar 09, 2016 41 42 43 44 45 46 47 48 49 `````` let rec function for_all (p: 'a -> bool) (l:list 'a) : bool = 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 = match l with `````` MARCHE Claude committed Mar 24, 2016 50 `````` | Nil -> false `````` MARCHE Claude committed Mar 09, 2016 51 52 53 `````` | Cons x r -> p x || for_some p r end `````` MARCHE Claude committed Mar 24, 2016 54 55 56 `````` let function mem (eq:'a -> 'a -> bool) (x:'a) (l:list 'a) : bool = for_some (eq x) l `````` MARCHE Claude committed Mar 09, 2016 57 58 ``````end `````` MARCHE Claude committed Apr 20, 2012 59 60 ``````(** {2 Membership in a list} *) `````` Andrei Paskevich committed Dec 22, 2017 61 ``````module Mem `````` Andrei Paskevich committed Jun 15, 2018 62 `````` use List `````` MARCHE Claude committed Dec 15, 2010 63 `````` `````` Andrei Paskevich committed Jun 29, 2011 64 `````` predicate mem (x: 'a) (l: list 'a) = match l with `````` Andrei Paskevich committed Jun 17, 2010 65 `````` | Nil -> false `````` Andrei Paskevich committed Jun 29, 2011 66 `````` | Cons y r -> x = y \/ mem x r `````` Jean-Christophe Filliâtre committed Mar 23, 2010 67 68 69 70 `````` end end `````` Andrei Paskevich committed Dec 22, 2017 71 ``````module Elements `````` MARCHE Claude committed Aug 24, 2012 72 `````` `````` Jean-Christophe Filliatre committed Mar 07, 2019 73 `````` use set.Fset `````` Andrei Paskevich committed Jun 15, 2018 74 75 `````` use List use Mem `````` MARCHE Claude committed Aug 24, 2012 76 `````` `````` Jean-Christophe Filliatre committed Mar 07, 2019 77 `````` function elements (l: list 'a) : fset 'a = `````` Jean-Christophe Filliatre committed Mar 29, 2016 78 `````` match l with `````` Jean-Christophe Filliatre committed Mar 07, 2019 79 80 `````` | Nil -> empty | Cons x r -> add x (elements r) `````` Jean-Christophe Filliatre committed Mar 29, 2016 81 `````` end `````` MARCHE Claude committed Aug 24, 2012 82 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2016 83 `````` lemma elements_mem: `````` Jean-Christophe Filliatre committed Mar 07, 2019 84 `````` forall x: 'a, l: list 'a. mem x l <-> Fset.mem x (elements l) `````` MARCHE Claude committed Aug 24, 2012 85 `````` `````` MARCHE Claude committed Aug 24, 2012 86 87 ``````end `````` MARCHE Claude committed Apr 20, 2012 88 89 ``````(** {2 Nth element of a list} *) `````` Andrei Paskevich committed Dec 22, 2017 90 ``````module Nth `````` 91 `````` `````` Andrei Paskevich committed Jun 15, 2018 92 93 94 `````` use List use option.Option use int.Int `````` MARCHE Claude committed Dec 15, 2010 95 `````` `````` Andrei Paskevich committed Sep 19, 2015 96 `````` let rec function nth (n: int) (l: list 'a) : option 'a = `````` Andrei Paskevich committed Aug 20, 2015 97 `````` match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 98 `````` | Nil -> None `````` Jean-Christophe Filliatre committed Nov 10, 2010 99 `````` | Cons x r -> if n = 0 then Some x else nth (n - 1) r `````` Andrei Paskevich committed Aug 20, 2015 100 `````` end `````` 101 102 103 `````` end `````` Andrei Paskevich committed Dec 22, 2017 104 ``````module NthNoOpt `````` MARCHE Claude committed Jul 08, 2013 105 `````` `````` Andrei Paskevich committed Jun 15, 2018 106 107 `````` use List use int.Int `````` MARCHE Claude committed Jul 08, 2013 108 `````` `````` MARCHE Claude committed Dec 10, 2013 109 `````` function nth (n: int) (l: list 'a) : 'a `````` MARCHE Claude committed Jul 08, 2013 110 111 112 113 114 115 116 `````` 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 `````` Andrei Paskevich committed Dec 22, 2017 117 ``````module NthLength `````` Jean-Christophe committed Jul 21, 2012 118 `````` `````` Andrei Paskevich committed Jun 15, 2018 119 120 121 `````` use int.Int use option.Option use List `````` Jean-Christophe committed Jul 21, 2012 122 123 124 125 `````` use export Nth use export Length lemma nth_none_1: `````` Jean-Christophe Filliatre committed Dec 21, 2012 126 `````` forall l: list 'a, i: int. i < 0 -> nth i l = None `````` Jean-Christophe committed Jul 21, 2012 127 128 `````` lemma nth_none_2: `````` Jean-Christophe Filliatre committed Dec 21, 2012 129 `````` forall l: list 'a, i: int. i >= length l -> nth i l = None `````` Jean-Christophe committed Jul 21, 2012 130 131 132 133 134 135 `````` lemma nth_none_3: forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= length l end `````` MARCHE Claude committed Apr 20, 2012 136 137 ``````(** {2 Head and tail} *) `````` Andrei Paskevich committed Dec 22, 2017 138 ``````module HdTl `````` Jean-Christophe Filliatre committed Nov 15, 2010 139 `````` `````` Andrei Paskevich committed Jun 15, 2018 140 141 `````` use List use option.Option `````` Jean-Christophe Filliatre committed Nov 15, 2010 142 `````` `````` Andrei Paskevich committed Aug 20, 2015 143 `````` let function hd (l: list 'a) : option 'a = match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 144 `````` | Nil -> None `````` Jean-Christophe Filliatre committed Nov 15, 2010 145 146 147 `````` | Cons h _ -> Some h end `````` Andrei Paskevich committed Aug 20, 2015 148 `````` let function tl (l: list 'a) : option (list 'a) = match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 149 `````` | Nil -> None `````` Jean-Christophe Filliatre committed Nov 15, 2010 150 151 152 `````` | Cons _ t -> Some t end `````` Jean-Christophe Filliatre committed Feb 17, 2011 153 154 ``````end `````` Andrei Paskevich committed Dec 22, 2017 155 ``````module HdTlNoOpt `````` MARCHE Claude committed Dec 10, 2013 156 `````` `````` Andrei Paskevich committed Jun 15, 2018 157 `````` use List `````` MARCHE Claude committed Dec 10, 2013 158 159 160 161 162 163 164 165 166 167 168 `````` 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 `````` 169 ``````(** {2 Relation between head, tail, and nth} *) `````` MARCHE Claude committed Apr 20, 2012 170 `````` `````` Andrei Paskevich committed Dec 22, 2017 171 ``````module NthHdTl `````` Jean-Christophe Filliatre committed Feb 17, 2011 172 `````` `````` Andrei Paskevich committed Jun 15, 2018 173 174 175 176 177 `````` use int.Int use option.Option use List use Nth use HdTl `````` Jean-Christophe Filliatre committed Nov 15, 2010 178 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 179 180 `````` lemma Nth_tl: forall l1 l2: list 'a. tl l1 = Some l2 -> `````` 181 `````` forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1 `````` Jean-Christophe Filliatre committed Nov 15, 2010 182 183 `````` lemma Nth0_head: `````` Jean-Christophe Filliatre committed Jun 22, 2011 184 `````` forall l: list 'a. nth 0 l = hd l `````` Jean-Christophe Filliatre committed Nov 15, 2010 185 186 187 `````` end `````` MARCHE Claude committed Apr 20, 2012 188 ``````(** {2 Appending two lists} *) `````` Jean-Christophe Filliatre committed Nov 15, 2010 189 `````` `````` Andrei Paskevich committed Dec 22, 2017 190 ``````module Append `````` Guillaume Melquiond committed Aug 21, 2014 191 `````` `````` Andrei Paskevich committed Jun 15, 2018 192 `````` use List `````` Jean-Christophe Filliatre committed Nov 10, 2010 193 `````` `````` Andrei Paskevich committed Sep 19, 2015 194 `````` let rec function (++) (l1 l2: list 'a) : list 'a = `````` Andrei Paskevich committed Aug 20, 2015 195 `````` match l1 with `````` Jean-Christophe Filliatre committed Nov 10, 2010 196 `````` | Nil -> l2 `````` Jean-Christophe Filliatre committed Feb 18, 2011 197 `````` | Cons x1 r1 -> Cons x1 (r1 ++ l2) `````` Andrei Paskevich committed Aug 20, 2015 198 `````` end `````` Jean-Christophe Filliatre committed Nov 10, 2010 199 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 200 `````` lemma Append_assoc: `````` Guillaume Melquiond committed Jan 12, 2018 201 `````` forall l1 [@induction] l2 l3: list 'a. `````` Jean-Christophe Filliatre committed Feb 18, 2011 202 `````` l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 `````` Jean-Christophe Filliatre committed Nov 10, 2010 203 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 204 205 `````` lemma Append_l_nil: forall l: list 'a. l ++ Nil = l `````` Jean-Christophe Filliatre committed Nov 10, 2010 206 `````` `````` Andrei Paskevich committed Jun 15, 2018 207 208 `````` use Length use int.Int `````` Jean-Christophe Filliatre committed Nov 10, 2010 209 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 210 `````` lemma Append_length: `````` Guillaume Melquiond committed Jan 12, 2018 211 `````` forall l1 [@induction] l2: list 'a. length (l1 ++ l2) = length l1 + length l2 `````` Jean-Christophe Filliatre committed Nov 10, 2010 212 `````` `````` Andrei Paskevich committed Jun 15, 2018 213 `````` use Mem `````` 214 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 215 `````` lemma mem_append: `````` Guillaume Melquiond committed Jan 12, 2018 216 `````` forall x: 'a, l1 [@induction] l2: list 'a. `````` Andrei Paskevich committed Jun 29, 2011 217 `````` mem x (l1 ++ l2) <-> mem x l1 \/ mem x l2 `````` 218 `````` `````` Jean-Christophe Filliatre committed Aug 02, 2011 219 220 221 222 `````` lemma mem_decomp: forall x: 'a, l: list 'a. mem x l -> exists l1 l2: list 'a. l = l1 ++ Cons x l2 `````` Jean-Christophe Filliatre committed Nov 10, 2010 223 224 ``````end `````` Andrei Paskevich committed Dec 22, 2017 225 ``````module NthLengthAppend `````` Jean-Christophe committed Jul 21, 2012 226 `````` `````` Andrei Paskevich committed Jun 15, 2018 227 228 `````` use int.Int use List `````` Jean-Christophe committed Jul 21, 2012 229 230 231 232 233 234 235 236 `````` 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: `````` Guillaume Melquiond committed Jan 12, 2018 237 `````` forall l1 [@induction] l2: list 'a, i: int. `````` Jean-Christophe committed Jul 21, 2012 238 239 240 241 `````` length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end `````` Jean-Christophe Filliatre committed Apr 11, 2013 242 243 ``````(** {2 Reversing a list} *) `````` Andrei Paskevich committed Dec 22, 2017 244 ``````module Reverse `````` Jean-Christophe Filliatre committed Apr 11, 2013 245 `````` `````` Andrei Paskevich committed Jun 15, 2018 246 247 `````` use List use Append `````` Jean-Christophe Filliatre committed Apr 11, 2013 248 `````` `````` Andrei Paskevich committed Sep 19, 2015 249 `````` let rec function reverse (l: list 'a) : list 'a = `````` Andrei Paskevich committed Aug 20, 2015 250 `````` match l with `````` Jean-Christophe Filliatre committed Apr 11, 2013 251 252 `````` | Nil -> Nil | Cons x r -> reverse r ++ Cons x Nil `````` Andrei Paskevich committed Aug 20, 2015 253 `````` end `````` Jean-Christophe Filliatre committed Apr 11, 2013 254 255 256 257 258 `````` lemma reverse_append: forall l1 l2: list 'a, x: 'a. (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2) `````` Jean-Christophe Filliatre committed Mar 29, 2014 259 260 261 262 `````` lemma reverse_cons: forall l: list 'a, x: 'a. reverse (Cons x l) = reverse l ++ Cons x Nil `````` Léon Gondelman committed Sep 18, 2014 263 264 265 266 267 `````` lemma cons_reverse: forall l: list 'a, x: 'a. Cons x (reverse l) = reverse (l ++ Cons x Nil) `````` Jean-Christophe Filliatre committed Apr 11, 2013 268 269 270 `````` lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l `````` Andrei Paskevich committed Jun 15, 2018 271 `````` use Mem `````` Jean-Christophe Filliatre committed Mar 29, 2014 272 273 274 275 `````` lemma reverse_mem: forall l: list 'a, x: 'a. mem x l <-> mem x (reverse l) `````` Andrei Paskevich committed Jun 15, 2018 276 `````` use Length `````` Jean-Christophe Filliatre committed Apr 11, 2013 277 278 279 280 281 282 `````` lemma Reverse_length: forall l: list 'a. length (reverse l) = length l end `````` Jean-Christophe Filliatre committed Apr 11, 2013 283 284 ``````(** {2 Reverse append} *) `````` Andrei Paskevich committed Dec 22, 2017 285 ``````module RevAppend `````` Jean-Christophe Filliatre committed Apr 11, 2013 286 `````` `````` Andrei Paskevich committed Jun 15, 2018 287 `````` use List `````` Jean-Christophe Filliatre committed Apr 11, 2013 288 `````` `````` Andrei Paskevich committed Sep 19, 2015 289 `````` let rec function rev_append (s t: list 'a) : list 'a = `````` Jean-Christophe Filliatre committed Apr 11, 2013 290 291 292 293 294 `````` match s with | Cons x r -> rev_append r (Cons x t) | Nil -> t end `````` Andrei Paskevich committed Jun 15, 2018 295 `````` use Append `````` Jean-Christophe Filliatre committed Apr 11, 2013 296 297 `````` lemma rev_append_append_l: `````` Guillaume Melquiond committed Jan 12, 2018 298 `````` forall r [@induction] s t: list 'a. `````` Jean-Christophe Filliatre committed Apr 11, 2013 299 300 `````` rev_append (r ++ s) t = rev_append s (rev_append r t) `````` Andrei Paskevich committed Jun 15, 2018 301 302 `````` use int.Int use Length `````` Jean-Christophe Filliatre committed Apr 11, 2013 303 304 `````` lemma rev_append_length: `````` Guillaume Melquiond committed Jan 12, 2018 305 `````` forall s [@induction] t: list 'a. `````` Jean-Christophe Filliatre committed Apr 11, 2013 306 307 `````` length (rev_append s t) = length s + length t `````` Andrei Paskevich committed Jun 15, 2018 308 `````` use Reverse `````` Jean-Christophe Filliatre committed Mar 29, 2014 309 310 `````` lemma rev_append_def: `````` Guillaume Melquiond committed Jan 12, 2018 311 `````` forall r [@induction] s: list 'a. rev_append r s = reverse r ++ s `````` Léon Gondelman committed Sep 18, 2014 312 313 314 315 `````` lemma rev_append_append_r: forall r s t: list 'a. rev_append r (s ++ t) = rev_append (rev_append s r) t `````` Jean-Christophe Filliatre committed Mar 29, 2014 316 `````` `````` Jean-Christophe Filliatre committed Apr 11, 2013 317 318 ``````end `````` Jean-Christophe Filliatre committed Jun 12, 2013 319 320 ``````(** {2 Zip} *) `````` Andrei Paskevich committed Dec 22, 2017 321 ``````module Combine `````` Jean-Christophe Filliatre committed Jun 12, 2013 322 `````` `````` Andrei Paskevich committed Jun 15, 2018 323 `````` use List `````` Jean-Christophe Filliatre committed Jun 12, 2013 324 `````` `````` Andrei Paskevich committed Aug 20, 2015 325 326 `````` let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b) = match x, y with `````` Jean-Christophe Filliatre committed Jun 12, 2013 327 328 329 330 331 332 `````` | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y) | _ -> Nil end end `````` MARCHE Claude committed Apr 20, 2012 333 334 ``````(** {2 Sorted lists for some order as parameter} *) `````` Andrei Paskevich committed Dec 22, 2017 335 ``````module Sorted `````` Jean-Christophe Filliâtre committed Jul 07, 2010 336 `````` `````` Andrei Paskevich committed Jun 15, 2018 337 `````` use List `````` MARCHE Claude committed Dec 15, 2010 338 `````` `````` Jean-Christophe Filliatre committed Sep 15, 2011 339 340 `````` type t predicate le t t `````` Andrei Paskevich committed Jun 15, 2018 341 `````` clone relations.Transitive with `````` Andrei Paskevich committed Jun 15, 2018 342 `````` type t = t, predicate rel = le, axiom Trans `````` Jean-Christophe Filliatre committed Sep 15, 2011 343 344 `````` inductive sorted (l: list t) = `````` Jean-Christophe Filliatre committed Jun 22, 2011 345 `````` | Sorted_Nil: `````` Jean-Christophe Filliâtre committed Jul 07, 2010 346 `````` sorted Nil `````` Jean-Christophe Filliatre committed Jun 22, 2011 347 `````` | Sorted_One: `````` Jean-Christophe Filliatre committed Sep 15, 2011 348 `````` forall x: t. sorted (Cons x Nil) `````` Jean-Christophe Filliatre committed Jun 22, 2011 349 `````` | Sorted_Two: `````` Jean-Christophe Filliatre committed Sep 15, 2011 350 351 `````` forall x y: t, l: list t. le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) `````` MARCHE Claude committed Dec 15, 2010 352 `````` `````` Andrei Paskevich committed Jun 15, 2018 353 `````` use Mem `````` Jean-Christophe Filliâtre committed Jul 07, 2010 354 `````` `````` Jean-Christophe Filliatre committed Sep 15, 2011 355 356 357 358 `````` lemma sorted_mem: forall x: t, l: list t. (forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l) `````` Andrei Paskevich committed Jun 15, 2018 359 `````` use Append `````` Jean-Christophe Filliatre committed Mar 29, 2014 360 361 `````` lemma sorted_append: `````` Guillaume Melquiond committed Jan 12, 2018 362 `````` forall l1 [@induction] l2: list t. `````` Jean-Christophe Filliatre committed Apr 01, 2014 363 364 `````` (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y)) <-> `````` Jean-Christophe Filliatre committed Mar 29, 2014 365 366 `````` sorted (l1 ++ l2) `````` Jean-Christophe Filliatre committed Sep 15, 2011 367 368 ``````end `````` MARCHE Claude committed Apr 20, 2012 369 370 ``````(** {2 Sorted lists of integers} *) `````` Andrei Paskevich committed Dec 22, 2017 371 ``````module SortedInt `````` Jean-Christophe Filliatre committed Sep 15, 2011 372 `````` `````` Andrei Paskevich committed Jun 15, 2018 373 `````` use int.Int `````` Léon Gondelman committed Sep 18, 2014 374 `````` clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans `````` Jean-Christophe Filliâtre committed Jul 07, 2010 375 376 377 `````` end `````` Andrei Paskevich committed Dec 22, 2017 378 ``````module RevSorted `````` Jean-Christophe Filliatre committed Apr 11, 2013 379 380 381 `````` type t predicate le t t `````` Andrei Paskevich committed Jun 15, 2018 382 `````` clone relations.Transitive with `````` Andrei Paskevich committed Jun 14, 2018 383 `````` type t = t, predicate rel = le, axiom Trans `````` Jean-Christophe Filliatre committed Apr 11, 2013 384 385 `````` predicate ge (x y: t) = le y x `````` Andrei Paskevich committed Jun 15, 2018 386 `````` use List `````` Jean-Christophe Filliatre committed Apr 11, 2013 387 `````` `````` Andrei Paskevich committed Jun 15, 2018 388 389 `````` clone Sorted as Incr with type t = t, predicate le = le, goal . clone Sorted as Decr with type t = t, predicate le = ge, goal . `````` Jean-Christophe Filliatre committed Apr 11, 2013 390 391 392 393 394 395 396 `````` predicate compat (s t: list t) = match s, t with | Cons x _, Cons y _ -> le x y | _, _ -> true end `````` Andrei Paskevich committed Jun 15, 2018 397 `````` use RevAppend `````` Jean-Christophe Filliatre committed Apr 11, 2013 398 399 `````` lemma rev_append_sorted_incr: `````` Guillaume Melquiond committed Jan 12, 2018 400 `````` forall s [@induction] t: list t. `````` Jean-Christophe Filliatre committed Apr 11, 2013 401 402 403 404 `````` Incr.sorted (rev_append s t) <-> Decr.sorted s /\ Incr.sorted t /\ compat s t lemma rev_append_sorted_decr: `````` Guillaume Melquiond committed Jan 12, 2018 405 `````` forall s [@induction] t: list t. `````` Jean-Christophe Filliatre committed Apr 11, 2013 406 407 408 409 410 `````` Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s end `````` MARCHE Claude committed Apr 20, 2012 411 412 ``````(** {2 Number of occurrences in a list} *) `````` Andrei Paskevich committed Dec 22, 2017 413 ``````module NumOcc `````` MARCHE Claude committed Dec 15, 2010 414 `````` `````` Andrei Paskevich committed Jun 15, 2018 415 416 `````` use int.Int use List `````` Jean-Christophe Filliâtre committed Jul 07, 2010 417 `````` `````` Andrei Paskevich committed Jun 29, 2011 418 `````` function num_occ (x: 'a) (l: list 'a) : int = `````` Jean-Christophe Filliâtre committed Jul 07, 2010 419 `````` match l with `````` Jean-Christophe Filliatre committed Jun 22, 2011 420 `````` | Nil -> 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 421 `````` | Cons y r -> (if x = y then 1 else 0) + num_occ x r `````` Guillaume Melquiond committed Jan 28, 2014 422 `````` end `````` Guillaume Melquiond committed Jun 14, 2018 423 `````` (** number of occurrences of `x` in `l` *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 424 `````` `````` MARCHE Claude committed Nov 19, 2014 425 `````` lemma Num_Occ_NonNeg: forall x:'a, l: list 'a. num_occ x l >= 0 `````` Léon Gondelman committed Sep 18, 2014 426 `````` `````` Andrei Paskevich committed Jun 15, 2018 427 `````` use Mem `````` Jean-Christophe Filliâtre committed Jul 07, 2010 428 `````` `````` MARCHE Claude committed Dec 15, 2010 429 `````` lemma Mem_Num_Occ : `````` Jean-Christophe Filliatre committed Jun 22, 2011 430 `````` forall x: 'a, l: list 'a. mem x l <-> num_occ x l > 0 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 431 `````` `````` Andrei Paskevich committed Jun 15, 2018 432 `````` use Append `````` Jean-Christophe committed Jan 20, 2012 433 434 `````` lemma Append_Num_Occ : `````` Guillaume Melquiond committed Jan 12, 2018 435 `````` forall x: 'a, l1 [@induction] l2: list 'a. `````` Jean-Christophe committed Jan 20, 2012 436 437 `````` num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 `````` Andrei Paskevich committed Jun 15, 2018 438 `````` use Reverse `````` Jean-Christophe Filliatre committed Mar 29, 2014 439 440 441 442 443 `````` lemma reverse_num_occ : forall x: 'a, l: list 'a. num_occ x l = num_occ x (reverse l) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 444 445 ``````end `````` MARCHE Claude committed Apr 20, 2012 446 447 ``````(** {2 Permutation of lists} *) `````` Andrei Paskevich committed Dec 22, 2017 448 ``````module Permut `````` Jean-Christophe Filliâtre committed Jul 07, 2010 449 `````` `````` Andrei Paskevich committed Jun 15, 2018 450 451 `````` use NumOcc use List `````` Jean-Christophe Filliâtre committed Jul 07, 2010 452 `````` `````` Andrei Paskevich committed Jun 29, 2011 453 `````` predicate permut (l1: list 'a) (l2: list 'a) = `````` Jean-Christophe Filliatre committed Jun 22, 2011 454 `````` forall x: 'a. num_occ x l1 = num_occ x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 455 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 456 `````` lemma Permut_refl: forall l: list 'a. permut l l `````` Jean-Christophe Filliâtre committed Jul 07, 2010 457 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 458 `````` lemma Permut_sym: forall l1 l2: list 'a. permut l1 l2 -> permut l2 l1 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 459 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 460 461 `````` lemma Permut_trans: forall l1 l2 l3: list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 462 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 463 464 `````` lemma Permut_cons: forall x: 'a, l1 l2: list 'a. `````` Jean-Christophe Filliâtre committed Jul 07, 2010 465 466 `````` permut l1 l2 -> permut (Cons x l1) (Cons x l2) `````` Jean-Christophe Filliatre committed Jun 22, 2011 467 468 `````` lemma Permut_swap: forall x y: 'a, l: list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) `````` MARCHE Claude committed Dec 15, 2010 469 `````` `````` Andrei Paskevich committed Jun 15, 2018 470 `````` use Append `````` Jean-Christophe Filliatre committed Jan 20, 2012 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 `````` 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) `````` Andrei Paskevich committed Jun 15, 2018 488 `````` use Mem `````` Jean-Christophe Filliâtre committed Jul 07, 2010 489 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 490 491 `````` lemma Permut_mem: forall x: 'a, l1 l2: list 'a. permut l1 l2 -> mem x l1 -> mem x l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 492 `````` `````` Andrei Paskevich committed Jun 15, 2018 493 `````` use Length `````` Jean-Christophe Filliâtre committed Jul 07, 2010 494 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 495 `````` lemma Permut_length: `````` Jean-Christophe Filliatre committed May 24, 2018 496 `````` forall l1 [@induction] l2: list 'a. permut l1 l2 -> length l1 = length l2 `````` Jean-Christophe Filliâtre committed Jul 07, 2010 497 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 498 499 ``````end `````` MARCHE Claude committed Apr 20, 2012 500 501 ``````(** {2 List with pairwise distinct elements} *) `````` Andrei Paskevich committed Dec 22, 2017 502 ``````module Distinct `````` Jean-Christophe committed Mar 16, 2011 503 `````` `````` Andrei Paskevich committed Jun 15, 2018 504 505 `````` use List use Mem `````` Jean-Christophe committed Mar 16, 2011 506 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 507 508 509 510 511 `````` 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. `````` Jean-Christophe committed Mar 16, 2011 512 513 `````` not (mem x l) -> distinct l -> distinct (Cons x l) `````` Andrei Paskevich committed Jun 15, 2018 514 `````` use Append `````` Jean-Christophe committed Mar 16, 2011 515 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 516 `````` lemma distinct_append: `````` Guillaume Melquiond committed Jan 12, 2018 517 `````` forall l1 [@induction] l2: list 'a. `````` Jean-Christophe committed Mar 16, 2011 518 519 520 521 522 `````` distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end `````` Andrei Paskevich committed Dec 22, 2017 523 ``````module Prefix `````` Jean-Christophe Filliatre committed Jan 09, 2013 524 `````` `````` Andrei Paskevich committed Jun 15, 2018 525 526 `````` use List use int.Int `````` Jean-Christophe Filliatre committed Jan 09, 2013 527 `````` `````` Andrei Paskevich committed Sep 19, 2015 528 `````` let rec function prefix (n: int) (l: list 'a) : list 'a = `````` Jean-Christophe Filliatre committed Jan 09, 2013 529 530 531 532 533 534 535 536 `````` if n <= 0 then Nil else match l with | Nil -> Nil | Cons x r -> Cons x (prefix (n-1) r) end end `````` Andrei Paskevich committed Dec 22, 2017 537 ``````module Sum `````` Jean-Christophe Filliatre committed Jun 08, 2014 538 `````` `````` Andrei Paskevich committed Jun 15, 2018 539 540 `````` use List use int.Int `````` Jean-Christophe Filliatre committed Jun 08, 2014 541 `````` `````` Andrei Paskevich committed Sep 19, 2015 542 `````` let rec function sum (l: list int) : int = `````` Andrei Paskevich committed Aug 20, 2015 543 544 545 546 `````` match l with | Nil -> 0 | Cons x r -> x + sum r end `````` Jean-Christophe Filliatre committed Jun 08, 2014 547 548 549 `````` end `````` Mário Pereira committed Mar 23, 2017 550 ``````(* `````` MARCHE Claude committed Apr 20, 2012 551 552 ``````(** {2 Induction on lists} *) `````` Andrei Paskevich committed Dec 22, 2017 553 ``````module Induction `````` 554 `````` `````` Andrei Paskevich committed Jun 15, 2018 555 `````` use List `````` Jean-Christophe Filliâtre committed Mar 23, 2010 556 `````` `````` Mário Pereira committed Mar 23, 2017 557 `````` (* type elt *) `````` Jean-Christophe Filliâtre committed Jul 07, 2010 558 `````` `````` Mário Pereira committed Mar 23, 2017 559 `````` (* predicate p (list elt) *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 560 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2011 561 `````` axiom Induction: `````` Mário Pereira committed Mar 23, 2017 562 563 564 565 `````` 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 566 567 `````` end `````` Mário Pereira committed Mar 23, 2017 568 ``````*) `````` MARCHE Claude committed Aug 24, 2012 569 `````` `````` MARCHE Claude committed Apr 20, 2012 570 571 ``````(** {2 Maps as lists of pairs} *) `````` Andrei Paskevich committed Dec 22, 2017 572 ``````module Map `````` 573 `````` `````` Andrei Paskevich committed Jun 15, 2018 574 `````` use List `````` MARCHE Claude committed Dec 15, 2010 575 `````` `````` Mário Pereira committed Mar 23, 2017 576 `````` function map (f: 'a -> 'b) (l: list 'a) : list 'b = `````` Jean-Christophe Filliâtre committed Mar 23, 2010 577 `````` match l with `````` Andrei Paskevich committed Jun 17, 2010 578 `````` | Nil -> Nil `````` Mário Pereira committed Mar 23, 2017 579 `````` | Cons x r -> Cons (f x) (map f r) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 580 `````` end `````` Jean-Christophe Filliatre committed Aug 03, 2011 581 582 ``````end `````` MARCHE Claude committed Apr 20, 2012 583 584 ``````(** {2 Generic recursors on lists} *) `````` Andrei Paskevich committed Dec 22, 2017 585 ``````module FoldLeft `````` 586 `````` `````` Andrei Paskevich committed Jun 15, 2018 587 `````` use List `````` Jean-Christophe Filliatre committed Aug 03, 2011 588 `````` `````` Mário Pereira committed Mar 23, 2017 589 `````` function fold_left (f: 'b -> 'a -> 'b) (acc: 'b) (l: list 'a) : 'b = `````` Jean-Christophe Filliatre committed Aug 03, 2011 590 591 `````` match l with | Nil -> acc `````` Mário Pereira committed Mar 23, 2017 592 `````` | Cons x r -> fold_left f (f acc x) r `````` Jean-Christophe Filliatre committed Aug 03, 2011 593 `````` end `````` 594 `````` `````` Andrei Paskevich committed Jun 15, 2018 595 `````` use Append `````` Mário Pereira committed Mar 23, 2017 596 597 `````` lemma fold_left_append: `````` Guillaume Melquiond committed Jan 12, 2018 598 `````` forall l1 [@induction] l2: list 'a, f: 'b -> 'a -> 'b, acc : 'b. `````` Mário Pereira committed Mar 23, 2017 599 600 `````` fold_left f acc (l1++l2) = fold_left f (fold_left f acc l1) l2 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 601 602 ``````end `````` Andrei Paskevich committed Dec 22, 2017 603 ``````module FoldRight `````` 604 `````` `````` Andrei Paskevich committed Jun 15, 2018 605 `````` use List `````` Jean-Christophe Filliatre committed Aug 03, 2011 606 `````` `````` Mário Pereira committed Mar 23, 2017 607 `````` function fold_right (f: 'a -> 'b -> 'b) (l: list 'a) (acc: 'b) : 'b = `````` Jean-Christophe Filliatre committed Aug 03, 2011 608 609 `````` match l with | Nil -> acc `````` Mário Pereira committed Mar 23, 2017 610 `````` | Cons x r -> f x (fold_right f r acc) `````` Jean-Christophe Filliatre committed Aug 03, 2011 611 `````` end `````` 612 `````` `````` Andrei Paskevich committed Jun 15, 2018 613 `````` use Append `````` Jean-Christophe Filliatre committed Apr 04, 2017 614 615 `````` lemma fold_right_append: `````` Guillaume Melquiond committed Jan 12, 2018 616 `````` forall l1 [@induction] l2: list 'a, f: 'a -> 'b -> 'b, acc : 'b. `````` Jean-Christophe Filliatre committed Apr 04, 2017 617 618 `````` fold_right f (l1++l2) acc = fold_right f l1 (fold_right f l2 acc) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 619 ``````end `````` Jean-Christophe Filliatre committed Feb 17, 2011 620 `````` `````` MARCHE Claude committed Apr 20, 2012 621 622 ``````(** {2 Importation of all list theories in one} *) `````` Andrei Paskevich committed Dec 22, 2017 623 ``````module ListRich `````` 624 `````` `````` Jean-Christophe Filliatre committed Feb 17, 2011 625 626 627 628 629 630 631 632 `````` use export List use export Length use export Mem use export Nth use export HdTl use export NthHdTl use export Append use export Reverse `````` Jean-Christophe Filliatre committed Feb 18, 2014 633 `````` use export RevAppend `````` Jean-Christophe Filliatre committed Feb 17, 2011 634 635 `````` use export NumOcc use export Permut `````` 636 `````` `````` Jean-Christophe Filliatre committed Feb 17, 2011 637 ``end``