list.v 151 KB
Newer Older
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 3 4 ``````(* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose definitions and theorems on lists that are not in the Coq standard library. *) `````` Robbert Krebbers committed May 07, 2013 5 ``````Require Export Permutation. `````` Robbert Krebbers committed Nov 16, 2015 6 ``````Require Export prelude.numbers prelude.base prelude.decidable prelude.option. `````` Robbert Krebbers committed Jun 11, 2012 7 `````` `````` Robbert Krebbers committed Oct 19, 2012 8 ``````Arguments length {_} _. `````` Robbert Krebbers committed Jun 11, 2012 9 10 11 ``````Arguments cons {_} _ _. Arguments app {_} _ _. Arguments Permutation {_} _ _. `````` Robbert Krebbers committed Nov 12, 2012 12 ``````Arguments Forall_cons {_} _ _ _ _ _. `````` Robbert Krebbers committed Jun 11, 2012 13 `````` `````` Robbert Krebbers committed Oct 19, 2012 14 15 16 ``````Notation tail := tl. Notation take := firstn. Notation drop := skipn. `````` Robbert Krebbers committed May 07, 2013 17 `````` `````` Robbert Krebbers committed Oct 19, 2012 18 19 20 ``````Arguments take {_} !_ !_ /. Arguments drop {_} !_ !_ /. `````` Robbert Krebbers committed Jun 11, 2012 21 22 23 24 25 26 27 ``````Notation "(::)" := cons (only parsing) : C_scope. Notation "( x ::)" := (cons x) (only parsing) : C_scope. Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope. Notation "(++)" := app (only parsing) : C_scope. Notation "( l ++)" := (app l) (only parsing) : C_scope. Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope. `````` Robbert Krebbers committed May 07, 2013 28 29 30 31 32 33 34 35 36 ``````Infix "≡ₚ" := Permutation (at level 70, no associativity) : C_scope. Notation "(≡ₚ)" := Permutation (only parsing) : C_scope. Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : C_scope. Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : C_scope. Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : C_scope. Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : C_scope. Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope. Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope. `````` Robbert Krebbers committed Feb 22, 2013 37 38 39 ``````(** * Definitions *) (** The operation [l !! i] gives the [i]th element of the list [l], or [None] in case [i] is out of bounds. *) `````` Robbert Krebbers committed Jan 05, 2013 40 ``````Instance list_lookup {A} : Lookup nat A (list A) := `````` Robbert Krebbers committed May 02, 2014 41 `````` fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in `````` Robbert Krebbers committed Aug 21, 2012 42 `````` match l with `````` Robbert Krebbers committed May 02, 2014 43 `````` | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end `````` Robbert Krebbers committed Aug 21, 2012 44 `````` end. `````` Robbert Krebbers committed Feb 22, 2013 45 46 47 `````` (** The operation [alter f i l] applies the function [f] to the [i]th element of [l]. In case [i] is out of bounds, the list is returned unchanged. *) `````` Robbert Krebbers committed Jun 16, 2014 48 49 ``````Instance list_alter {A} : Alter nat A (list A) := λ f, fix go i l {struct l} := `````` Robbert Krebbers committed Aug 21, 2012 50 51 `````` match l with | [] => [] `````` Robbert Krebbers committed Jun 16, 2014 52 `````` | x :: l => match i with 0 => f x :: l | S i => x :: go i l end `````` Robbert Krebbers committed Aug 21, 2012 53 `````` end. `````` Robbert Krebbers committed Feb 22, 2013 54 `````` `````` Robbert Krebbers committed Jun 17, 2013 55 56 ``````(** The operation [<[i:=x]> l] overwrites the element at position [i] with the value [x]. In case [i] is out of bounds, the list is returned unchanged. *) `````` Robbert Krebbers committed May 02, 2014 57 58 59 60 61 62 ``````Instance list_insert {A} : Insert nat A (list A) := fix go i y l {struct l} := let _ : Insert _ _ _ := @go in match l with | [] => [] | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end end. `````` Robbert Krebbers committed Feb 16, 2015 63 64 65 66 67 ``````Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A := match k with | [] => l | y :: k => <[i:=y]>(list_inserts (S i) k l) end. `````` Robbert Krebbers committed Jun 17, 2013 68 `````` `````` Robbert Krebbers committed Feb 22, 2013 69 70 71 ``````(** The operation [delete i l] removes the [i]th element of [l] and moves all consecutive elements one position ahead. In case [i] is out of bounds, the list is returned unchanged. *) `````` Robbert Krebbers committed Nov 12, 2012 72 73 ``````Instance list_delete {A} : Delete nat (list A) := fix go (i : nat) (l : list A) {struct l} : list A := `````` Robbert Krebbers committed Oct 19, 2012 74 75 `````` match l with | [] => [] `````` Robbert Krebbers committed May 07, 2013 76 `````` | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end `````` Robbert Krebbers committed Aug 29, 2012 77 `````` end. `````` Robbert Krebbers committed Feb 22, 2013 78 79 80 `````` (** The function [option_list o] converts an element [Some x] into the singleton list [[x]], and [None] into the empty list [[]]. *) `````` Robbert Krebbers committed Jan 05, 2013 81 ``````Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) []. `````` Robbert Krebbers committed May 02, 2014 82 83 ``````Definition list_singleton {A} (l : list A) : option A := match l with [x] => Some x | _ => None end. `````` Robbert Krebbers committed Jan 05, 2013 84 85 86 87 `````` (** The function [filter P l] returns the list of elements of [l] that satisfies [P]. The order remains unchanged. *) Instance list_filter {A} : Filter A (list A) := `````` Robbert Krebbers committed May 02, 2014 88 `````` fix go P _ l := let _ : Filter _ _ := @go in `````` Robbert Krebbers committed Jan 05, 2013 89 90 `````` match l with | [] => [] `````` Robbert Krebbers committed May 02, 2014 91 `````` | x :: l => if decide (P x) then x :: filter P l else filter P l `````` Robbert Krebbers committed Jun 17, 2013 92 93 94 95 `````` end. (** The function [list_find P l] returns the first index [i] whose element satisfies the predicate [P]. *) `````` Robbert Krebbers committed Feb 08, 2015 96 ``````Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A) := `````` Robbert Krebbers committed Jun 17, 2013 97 98 `````` fix go l := match l with `````` Robbert Krebbers committed Feb 08, 2015 99 100 `````` | [] => None | x :: l => if decide (P x) then Some (0,x) else prod_map S id <\$> go l `````` Robbert Krebbers committed Jun 17, 2013 101 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 102 103 104 105 `````` (** The function [replicate n x] generates a list with length [n] of elements with value [x]. *) Fixpoint replicate {A} (n : nat) (x : A) : list A := `````` Robbert Krebbers committed May 07, 2013 106 `````` match n with 0 => [] | S n => x :: replicate n x end. `````` Robbert Krebbers committed Jan 05, 2013 107 108 109 110 `````` (** The function [reverse l] returns the elements of [l] in reverse order. *) Definition reverse {A} (l : list A) : list A := rev_append l []. `````` Robbert Krebbers committed May 02, 2014 111 112 113 114 ``````(** The function [last l] returns the last element of the list [l], or [None] if the list [l] is empty. *) Fixpoint last {A} (l : list A) : option A := match l with [] => None | [x] => Some x | _ :: l => last l end. `````` Robbert Krebbers committed Mar 25, 2013 115 `````` `````` Robbert Krebbers committed Jan 05, 2013 116 117 118 119 120 121 ``````(** The function [resize n y l] takes the first [n] elements of [l] in case [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain a list of length [n]. *) Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A := match l with | [] => replicate n y `````` Robbert Krebbers committed May 07, 2013 122 `````` | x :: l => match n with 0 => [] | S n => x :: resize n y l end `````` Robbert Krebbers committed Jan 05, 2013 123 124 125 `````` end. Arguments resize {_} !_ _ !_. `````` Robbert Krebbers committed May 02, 2014 126 127 128 ``````(** The function [reshape k l] transforms [l] into a list of lists whose sizes are specified by [k]. In case [l] is too short, the resulting list will be padded with empty lists. In case [l] is too long, it will be truncated. *) `````` Robbert Krebbers committed Jun 24, 2013 129 130 ``````Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) := match szs with `````` Robbert Krebbers committed May 02, 2014 131 `````` | [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l) `````` Robbert Krebbers committed Jun 24, 2013 132 133 `````` end. `````` Robbert Krebbers committed Jun 17, 2013 134 ``````Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) := `````` Robbert Krebbers committed May 02, 2014 135 136 137 138 `````` guard (i + n ≤ length l); Some (take n (drop i l)). Definition sublist_alter {A} (f : list A → list A) (i n : nat) (l : list A) : list A := take i l ++ f (take n (drop i l)) ++ drop (i + n) l. `````` Robbert Krebbers committed Jun 17, 2013 139 `````` `````` Robbert Krebbers committed Feb 22, 2013 140 141 142 143 ``````(** Functions to fold over a list. We redefine [foldl] with the arguments in the same order as in Haskell. *) Notation foldr := fold_right. Definition foldl {A B} (f : A → B → A) : A → list B → A := `````` Robbert Krebbers committed May 02, 2014 144 `````` fix go a l := match l with [] => a | x :: l => go (f a x) l end. `````` Robbert Krebbers committed Feb 22, 2013 145 146 147 `````` (** The monadic operations. *) Instance list_ret: MRet list := λ A x, x :: @nil A. `````` Robbert Krebbers committed Jun 16, 2014 148 149 ``````Instance list_fmap : FMap list := λ A B f, fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end. `````` Robbert Krebbers committed Jul 10, 2014 150 151 152 153 154 155 ``````Instance list_omap : OMap list := λ A B f, fix go (l : list A) := match l with | [] => [] | x :: l => match f x with Some y => y :: go l | None => go l end end. `````` Robbert Krebbers committed Jun 16, 2014 156 157 ``````Instance list_bind : MBind list := λ A B f, fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end. `````` Robbert Krebbers committed Feb 22, 2013 158 159 ``````Instance list_join: MJoin list := fix go A (ls : list (list A)) : list A := `````` Robbert Krebbers committed May 07, 2013 160 `````` match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end. `````` Robbert Krebbers committed May 02, 2014 161 ``````Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) := `````` Robbert Krebbers committed Jun 17, 2013 162 `````` fix go l := `````` Robbert Krebbers committed May 02, 2014 163 `````` match l with [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end. `````` Robbert Krebbers committed Feb 22, 2013 164 165 166 167 168 `````` (** We define stronger variants of map and fold that allow the mapped function to use the index of the elements. *) Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B := fix go (n : nat) (l : list A) := `````` Robbert Krebbers committed May 07, 2013 169 `````` match l with [] => [] | x :: l => f n x :: go (S n) l end. `````` Robbert Krebbers committed Feb 22, 2013 170 ``````Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0. `````` Robbert Krebbers committed May 07, 2013 171 172 173 174 ``````Definition zipped_map {A B} (f : list A → list A → A → B) : list A → list A → list B := fix go l k := match k with [] => [] | x :: k => f l k x :: go (x :: l) k end. `````` Robbert Krebbers committed Jun 05, 2015 175 176 177 178 179 180 181 182 183 ``````Definition imap2_go {A B C} (f : nat → A → B → C) : nat → list A → list B → list C:= fix go (n : nat) (l : list A) (k : list B) := match l, k with | [], _ |_, [] => [] | x :: l, y :: k => f n x y :: go (S n) l k end. Definition imap2 {A B C} (f : nat → A → B → C) : list A → list B → list C := imap2_go f 0. `````` Robbert Krebbers committed May 07, 2013 184 185 186 187 188 189 190 ``````Inductive zipped_Forall {A} (P : list A → list A → A → Prop) : list A → list A → Prop := | zipped_Forall_nil l : zipped_Forall P l [] | zipped_Forall_cons l k x : P l k x → zipped_Forall P (x :: l) k → zipped_Forall P l (x :: k). Arguments zipped_Forall_nil {_ _} _. Arguments zipped_Forall_cons {_ _} _ _ _ _ _. `````` Robbert Krebbers committed Feb 22, 2013 191 `````` `````` Robbert Krebbers committed May 02, 2014 192 193 194 195 196 197 198 ``````(** The function [mask f βs l] applies the function [f] to elements in [l] at positions that are [true] in [βs]. *) Fixpoint mask {A} (f : A → A) (βs : list bool) (l : list A) : list A := match βs, l with | β :: βs, x :: l => (if β then f x else x) :: mask f βs l | _, _ => l end. `````` Robbert Krebbers committed Feb 22, 2013 199 200 201 202 `````` (** The function [permutations l] yields all permutations of [l]. *) Fixpoint interleave {A} (x : A) (l : list A) : list (list A) := match l with `````` Robbert Krebbers committed May 02, 2014 203 `````` | [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::) <\$> interleave x l) `````` Robbert Krebbers committed Feb 22, 2013 204 205 `````` end. Fixpoint permutations {A} (l : list A) : list (list A) := `````` Robbert Krebbers committed May 02, 2014 206 `````` match l with [] => [[]] | x :: l => permutations l ≫= interleave x end. `````` Robbert Krebbers committed Feb 22, 2013 207 `````` `````` Robbert Krebbers committed Feb 01, 2013 208 209 ``````(** The predicate [suffix_of] holds if the first list is a suffix of the second. The predicate [prefix_of] holds if the first list is a prefix of the second. *) `````` Robbert Krebbers committed Feb 19, 2013 210 211 ``````Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1. Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k. `````` Robbert Krebbers committed May 07, 2013 212 213 ``````Infix "`suffix_of`" := suffix_of (at level 70) : C_scope. Infix "`prefix_of`" := prefix_of (at level 70) : C_scope. `````` Robbert Krebbers committed Jun 16, 2014 214 215 ``````Hint Extern 0 (?x `prefix_of` ?y) => reflexivity. Hint Extern 0 (?x `suffix_of` ?y) => reflexivity. `````` Robbert Krebbers committed Jan 05, 2013 216 `````` `````` Robbert Krebbers committed Feb 19, 2013 217 218 219 220 221 222 223 224 ``````Section prefix_suffix_ops. Context `{∀ x y : A, Decision (x = y)}. Definition max_prefix_of : list A → list A → list A * list A * list A := fix go l1 l2 := match l1, l2 with | [], l2 => ([], l2, []) | l1, [] => (l1, [], []) | x1 :: l1, x2 :: l2 => `````` Robbert Krebbers committed May 07, 2013 225 `````` if decide_rel (=) x1 x2 `````` Robbert Krebbers committed May 02, 2014 226 `````` then prod_map id (x1 ::) (go l1 l2) else (x1 :: l1, x2 :: l2, []) `````` Robbert Krebbers committed Feb 19, 2013 227 228 229 230 231 `````` end. Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A := match max_prefix_of (reverse l1) (reverse l2) with | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3) end. `````` Robbert Krebbers committed May 02, 2014 232 233 `````` Definition strip_prefix (l1 l2 : list A) := (max_prefix_of l1 l2).1.2. Definition strip_suffix (l1 l2 : list A) := (max_suffix_of l1 l2).1.2. `````` Robbert Krebbers committed Feb 19, 2013 234 ``````End prefix_suffix_ops. `````` Robbert Krebbers committed Jan 05, 2013 235 `````` `````` Robbert Krebbers committed Jun 17, 2013 236 ``````(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements `````` Robbert Krebbers committed Feb 19, 2013 237 238 239 ``````from [l1] without changing the order. *) Inductive sublist {A} : relation (list A) := | sublist_nil : sublist [] [] `````` Robbert Krebbers committed May 07, 2013 240 `````` | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2) `````` Robbert Krebbers committed Jun 17, 2013 241 `````` | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2). `````` Robbert Krebbers committed May 07, 2013 242 ``````Infix "`sublist`" := sublist (at level 70) : C_scope. `````` Robbert Krebbers committed Jun 16, 2014 243 ``````Hint Extern 0 (?x `sublist` ?y) => reflexivity. `````` Robbert Krebbers committed May 07, 2013 244 245 `````` (** A list [l2] contains a list [l1] if [l2] is obtained by removing elements `````` Robbert Krebbers committed May 02, 2014 246 ``````from [l1] while possiblity changing the order. *) `````` Robbert Krebbers committed May 07, 2013 247 248 249 250 ``````Inductive contains {A} : relation (list A) := | contains_nil : contains [] [] | contains_skip x l1 l2 : contains l1 l2 → contains (x :: l1) (x :: l2) | contains_swap x y l : contains (y :: x :: l) (x :: y :: l) `````` Robbert Krebbers committed Jun 17, 2013 251 `````` | contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2) `````` Robbert Krebbers committed May 07, 2013 252 253 `````` | contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3. Infix "`contains`" := contains (at level 70) : C_scope. `````` Robbert Krebbers committed Jun 16, 2014 254 ``````Hint Extern 0 (?x `contains` ?y) => reflexivity. `````` Robbert Krebbers committed May 07, 2013 255 256 257 258 259 260 261 262 263 264 `````` Section contains_dec_help. Context {A} {dec : ∀ x y : A, Decision (x = y)}. Fixpoint list_remove (x : A) (l : list A) : option (list A) := match l with | [] => None | y :: l => if decide (x = y) then Some l else (y ::) <\$> list_remove x l end. Fixpoint list_remove_list (k : list A) (l : list A) : option (list A) := match k with `````` Robbert Krebbers committed May 02, 2014 265 `````` | [] => Some l | x :: k => list_remove x l ≫= list_remove_list k `````` Robbert Krebbers committed May 07, 2013 266 267 `````` end. End contains_dec_help. `````` Robbert Krebbers committed Feb 19, 2013 268 `````` `````` Robbert Krebbers committed May 02, 2014 269 270 271 272 273 ``````Inductive Forall3 {A B C} (P : A → B → C → Prop) : list A → list B → list C → Prop := | Forall3_nil : Forall3 P [] [] [] | Forall3_cons x y z l k k' : P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). `````` Robbert Krebbers committed May 07, 2013 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 `````` (** Set operations on lists *) Section list_set. Context {A} {dec : ∀ x y : A, Decision (x = y)}. Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} (x : A) : ∀ l, Decision (x ∈ l). Proof. refine ( fix go l := match l return Decision (x ∈ l) with | [] => right _ | y :: l => cast_if_or (decide (x = y)) (go l) end); clear go dec; subst; try (by constructor); abstract by inversion 1. Defined. Fixpoint remove_dups (l : list A) : list A := match l with | [] => [] | x :: l => if decide_rel (∈) x l then remove_dups l else x :: remove_dups l end. Fixpoint list_difference (l k : list A) : list A := match l with | [] => [] | x :: l => if decide_rel (∈) x k `````` Robbert Krebbers committed May 02, 2014 299 `````` then list_difference l k else x :: list_difference l k `````` Robbert Krebbers committed May 07, 2013 300 `````` end. `````` Robbert Krebbers committed Jun 05, 2014 301 `````` Definition list_union (l k : list A) : list A := list_difference l k ++ k. `````` Robbert Krebbers committed May 07, 2013 302 303 304 305 306 `````` Fixpoint list_intersection (l k : list A) : list A := match l with | [] => [] | x :: l => if decide_rel (∈) x k `````` Robbert Krebbers committed May 02, 2014 307 `````` then x :: list_intersection l k else list_intersection l k `````` Robbert Krebbers committed May 07, 2013 308 309 310 311 312 313 314 315 316 `````` end. Definition list_intersection_with (f : A → A → option A) : list A → list A → list A := fix go l k := match l with | [] => [] | x :: l => foldr (λ y, match f x y with None => id | Some z => (z ::) end) (go l k) k end. End list_set. `````` Robbert Krebbers committed Feb 22, 2013 317 318 `````` (** * Basic tactics on lists *) `````` Robbert Krebbers committed Feb 19, 2013 319 320 321 ``````(** The tactic [discriminate_list_equality] discharges a goal if it contains a list equality involving [(::)] and [(++)] of two lists that have a different length as one of its hypotheses. *) `````` Robbert Krebbers committed Oct 19, 2012 322 323 ``````Tactic Notation "discriminate_list_equality" hyp(H) := apply (f_equal length) in H; `````` Robbert Krebbers committed Sep 06, 2014 324 `````` repeat (csimpl in H || rewrite app_length in H); exfalso; lia. `````` Robbert Krebbers committed Oct 19, 2012 325 ``````Tactic Notation "discriminate_list_equality" := `````` Robbert Krebbers committed May 07, 2013 326 327 328 `````` match goal with | H : @eq (list _) _ _ |- _ => discriminate_list_equality H end. `````` Robbert Krebbers committed Oct 19, 2012 329 `````` `````` Robbert Krebbers committed Feb 19, 2013 330 331 332 ``````(** The tactic [simplify_list_equality] simplifies hypotheses involving equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies lookups in singleton lists. *) `````` Robbert Krebbers committed May 02, 2014 333 334 335 336 337 338 339 340 341 ``````Lemma app_injective_1 {A} (l1 k1 l2 k2 : list A) : length l1 = length k1 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2. Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed. Lemma app_injective_2 {A} (l1 k1 l2 k2 : list A) : length l2 = length k2 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2. Proof. intros ? Hl. apply app_injective_1; auto. apply (f_equal length) in Hl. rewrite !app_length in Hl. lia. Qed. `````` Robbert Krebbers committed Dec 16, 2014 342 ``````Ltac simplify_list_equality := `````` Robbert Krebbers committed May 07, 2013 343 `````` repeat match goal with `````` Robbert Krebbers committed Sep 06, 2014 344 `````` | _ => progress simplify_equality' `````` Robbert Krebbers committed Oct 19, 2012 345 `````` | H : _ ++ _ = _ ++ _ |- _ => first `````` Robbert Krebbers committed May 02, 2014 346 347 348 `````` [ apply app_inv_head in H | apply app_inv_tail in H | apply app_injective_1 in H; [destruct H|done] | apply app_injective_2 in H; [destruct H|done] ] `````` Robbert Krebbers committed Jan 05, 2013 349 `````` | H : [?x] !! ?i = Some ?y |- _ => `````` Robbert Krebbers committed May 07, 2013 350 `````` destruct i; [change (Some x = Some y) in H | discriminate] `````` Robbert Krebbers committed Sep 06, 2014 351 `````` end. `````` Robbert Krebbers committed Nov 12, 2012 352 `````` `````` Robbert Krebbers committed Aug 29, 2012 353 354 ``````(** * General theorems *) Section general_properties. `````` Robbert Krebbers committed Jun 11, 2012 355 ``````Context {A : Type}. `````` Robbert Krebbers committed May 07, 2013 356 357 ``````Implicit Types x y z : A. Implicit Types l k : list A. `````` Robbert Krebbers committed Jun 11, 2012 358 `````` `````` Robbert Krebbers committed May 07, 2013 359 360 361 ``````Global Instance: Injective2 (=) (=) (=) (@cons A). Proof. by injection 1. Qed. Global Instance: ∀ k, Injective (=) (=) (k ++). `````` Robbert Krebbers committed Nov 12, 2012 362 ``````Proof. intros ???. apply app_inv_head. Qed. `````` Robbert Krebbers committed May 07, 2013 363 ``````Global Instance: ∀ k, Injective (=) (=) (++ k). `````` Robbert Krebbers committed Nov 12, 2012 364 ``````Proof. intros ???. apply app_inv_tail. Qed. `````` Robbert Krebbers committed Feb 01, 2013 365 366 367 368 369 370 ``````Global Instance: Associative (=) (@app A). Proof. intros ???. apply app_assoc. Qed. Global Instance: LeftId (=) [] (@app A). Proof. done. Qed. Global Instance: RightId (=) [] (@app A). Proof. intro. apply app_nil_r. Qed. `````` Robbert Krebbers committed Nov 12, 2012 371 `````` `````` Robbert Krebbers committed May 07, 2013 372 ``````Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = []. `````` Robbert Krebbers committed May 02, 2014 373 ``````Proof. split. apply app_eq_nil. by intros [-> ->]. Qed. `````` Robbert Krebbers committed May 07, 2013 374 375 ``````Lemma app_singleton l1 l2 x : l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = []. `````` Robbert Krebbers committed May 02, 2014 376 ``````Proof. split. apply app_eq_unit. by intros [[-> ->]|[-> ->]]. Qed. `````` Robbert Krebbers committed May 07, 2013 377 378 379 ``````Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2. Proof. done. Qed. Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2. `````` Robbert Krebbers committed Aug 21, 2012 380 381 ``````Proof. revert l2. induction l1; intros [|??] H. `````` Robbert Krebbers committed Oct 19, 2012 382 `````` * done. `````` Robbert Krebbers committed Aug 21, 2012 383 384 `````` * discriminate (H 0). * discriminate (H 0). `````` Robbert Krebbers committed May 02, 2014 385 `````` * f_equal; [by injection (H 0)|]. apply (IHl1 _ \$ λ i, H (S i)). `````` Robbert Krebbers committed Aug 21, 2012 386 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 387 ``````Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k, `````` Robbert Krebbers committed Nov 12, 2012 388 `````` Decision (l = k) := list_eq_dec dec. `````` Robbert Krebbers committed May 02, 2014 389 390 391 392 393 394 395 396 ``````Global Instance list_eq_nil_dec l : Decision (l = []). Proof. by refine match l with [] => left _ | _ => right _ end. Defined. Lemma list_singleton_reflect l : option_reflect (λ x, l = [x]) (length l ≠ 1) (list_singleton l). Proof. by destruct l as [|? []]; constructor. Defined. Definition nil_length : length (@nil A) = 0 := eq_refl. Definition cons_length x l : length (x :: l) = S (length l) := eq_refl. `````` Robbert Krebbers committed May 07, 2013 397 ``````Lemma nil_or_length_pos l : l = [] ∨ length l ≠ 0. `````` Robbert Krebbers committed Nov 12, 2012 398 ``````Proof. destruct l; simpl; auto with lia. Qed. `````` Robbert Krebbers committed May 02, 2014 399 ``````Lemma nil_length_inv l : length l = 0 → l = []. `````` Robbert Krebbers committed Nov 12, 2012 400 401 ``````Proof. by destruct l. Qed. Lemma lookup_nil i : @nil A !! i = None. `````` Robbert Krebbers committed Oct 19, 2012 402 ``````Proof. by destruct i. Qed. `````` Robbert Krebbers committed May 07, 2013 403 ``````Lemma lookup_tail l i : tail l !! i = l !! S i. `````` Robbert Krebbers committed Oct 19, 2012 404 ``````Proof. by destruct l. Qed. `````` Robbert Krebbers committed May 15, 2013 405 406 ``````Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l. Proof. `````` Robbert Krebbers committed Jun 17, 2013 407 `````` revert i. induction l; intros [|?] ?; simplify_equality'; auto with arith. `````` Robbert Krebbers committed May 15, 2013 408 409 410 411 412 ``````Qed. Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l. Proof. intros [??]; eauto using lookup_lt_Some. Qed. Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i). Proof. `````` Robbert Krebbers committed Jun 17, 2013 413 `````` revert i. induction l; intros [|?] ?; simplify_equality'; eauto with lia. `````` Robbert Krebbers committed May 15, 2013 414 415 416 417 418 419 420 421 422 ``````Qed. Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l. Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed. Lemma lookup_ge_None l i : l !! i = None ↔ length l ≤ i. Proof. rewrite eq_None_not_Some, lookup_lt_is_Some. lia. Qed. Lemma lookup_ge_None_1 l i : l !! i = None → length l ≤ i. Proof. by rewrite lookup_ge_None. Qed. Lemma lookup_ge_None_2 l i : length l ≤ i → l !! i = None. Proof. by rewrite lookup_ge_None. Qed. `````` Robbert Krebbers committed Jun 23, 2014 423 424 425 ``````Lemma list_eq_same_length l1 l2 n : length l2 = n → length l1 = n → (∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2. `````` Robbert Krebbers committed Jan 05, 2013 426 ``````Proof. `````` Robbert Krebbers committed Jun 23, 2014 427 428 429 430 431 `````` intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx. * destruct (lookup_lt_is_Some_2 l1 i) as [y Hy]. { rewrite Hlen; eauto using lookup_lt_Some. } rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some. * by rewrite lookup_ge_None, Hlen, <-lookup_ge_None. `````` Robbert Krebbers committed Jan 05, 2013 432 ``````Qed. `````` Robbert Krebbers committed May 15, 2013 433 ``````Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i. `````` Robbert Krebbers committed Nov 12, 2012 434 ``````Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed. `````` Robbert Krebbers committed May 15, 2013 435 436 ``````Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x → (l1 ++ l2) !! i = Some x. Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed. `````` Robbert Krebbers committed Jan 25, 2015 437 ``````Lemma lookup_app_r l1 l2 i : `````` Robbert Krebbers committed Jun 17, 2013 438 `````` length l1 ≤ i → (l1 ++ l2) !! i = l2 !! (i - length l1). `````` Robbert Krebbers committed Jan 25, 2015 439 440 441 442 443 444 445 446 447 448 449 ``````Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed. Lemma lookup_app_Some l1 l2 i x : (l1 ++ l2) !! i = Some x ↔ l1 !! i = Some x ∨ length l1 ≤ i ∧ l2 !! (i - length l1) = Some x. Proof. split. * revert i. induction l1 as [|y l1 IH]; intros [|i] ?; simplify_equality'; auto with lia. destruct (IH i) as [?|[??]]; auto with lia. * intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r. Qed. `````` Robbert Krebbers committed May 02, 2014 450 451 452 ``````Lemma list_lookup_middle l1 l2 x n : n = length l1 → (l1 ++ x :: l2) !! n = Some x. Proof. intros ->. by induction l1. Qed. `````` Robbert Krebbers committed Aug 21, 2012 453 `````` `````` Robbert Krebbers committed Jan 25, 2015 454 455 ``````Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l. Proof. by revert i; induction l; intros []; intros; f_equal'. Qed. `````` Robbert Krebbers committed May 07, 2013 456 ``````Lemma alter_length f l i : length (alter f i l) = length l. `````` Robbert Krebbers committed May 02, 2014 457 ``````Proof. revert i. by induction l; intros [|?]; f_equal'. Qed. `````` Robbert Krebbers committed May 07, 2013 458 ``````Lemma insert_length l i x : length (<[i:=x]>l) = length l. `````` Robbert Krebbers committed May 02, 2014 459 ``````Proof. revert i. by induction l; intros [|?]; f_equal'. Qed. `````` Robbert Krebbers committed May 07, 2013 460 ``````Lemma list_lookup_alter f l i : alter f i l !! i = f <\$> l !! i. `````` Robbert Krebbers committed Oct 19, 2012 461 ``````Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed. `````` Robbert Krebbers committed May 12, 2013 462 ``````Lemma list_lookup_alter_ne f l i j : i ≠ j → alter f i l !! j = l !! j. `````` Robbert Krebbers committed Oct 19, 2012 463 ``````Proof. `````` Robbert Krebbers committed Jun 16, 2014 464 `````` revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence. `````` Robbert Krebbers committed Oct 19, 2012 465 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 466 ``````Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x. `````` Robbert Krebbers committed May 02, 2014 467 468 ``````Proof. revert i. induction l; intros [|?] ?; f_equal'; auto with lia. Qed. Lemma list_lookup_insert_ne l i j x : i ≠ j → <[i:=x]>l !! j = l !! j. `````` Robbert Krebbers committed Nov 12, 2012 469 ``````Proof. `````` Robbert Krebbers committed May 02, 2014 470 `````` revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence. `````` Robbert Krebbers committed Nov 12, 2012 471 ``````Qed. `````` Robbert Krebbers committed Feb 16, 2015 472 473 474 475 476 477 478 479 480 481 482 483 484 485 ``````Lemma list_lookup_insert_Some l i x j y : <[i:=x]>l !! j = Some y ↔ i = j ∧ x = y ∧ j < length l ∨ i ≠ j ∧ l !! j = Some y. Proof. destruct (decide (i = j)) as [->|]; [split|rewrite list_lookup_insert_ne by done; tauto]. * intros Hy. assert (j < length l). { rewrite <-(insert_length l j x); eauto using lookup_lt_Some. } rewrite list_lookup_insert in Hy by done; naive_solver. * intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver. Qed. Lemma list_insert_commute l i j x y : i ≠ j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l). Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal'; auto. Qed. `````` Robbert Krebbers committed May 07, 2013 486 487 ``````Lemma list_lookup_other l i x : length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y. `````` Robbert Krebbers committed Jan 05, 2013 488 ``````Proof. `````` Robbert Krebbers committed Jun 17, 2013 489 `````` intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'. `````` Robbert Krebbers committed Nov 11, 2015 490 491 `````` * by exists 1, x1. * by exists 0, x0. `````` Robbert Krebbers committed Jan 05, 2013 492 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 493 494 ``````Lemma alter_app_l f l1 l2 i : i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2. `````` Robbert Krebbers committed May 02, 2014 495 ``````Proof. revert i. induction l1; intros [|?] ?; f_equal'; auto with lia. Qed. `````` Robbert Krebbers committed May 07, 2013 496 ``````Lemma alter_app_r f l1 l2 i : `````` Robbert Krebbers committed Nov 12, 2012 497 `````` alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2. `````` Robbert Krebbers committed May 02, 2014 498 ``````Proof. revert i. induction l1; intros [|?]; f_equal'; auto. Qed. `````` Robbert Krebbers committed May 07, 2013 499 500 ``````Lemma alter_app_r_alt f l1 l2 i : length l1 ≤ i → alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2. `````` Robbert Krebbers committed Nov 12, 2012 501 502 503 504 ``````Proof. intros. assert (i = length l1 + (i - length l1)) as Hi by lia. rewrite Hi at 1. by apply alter_app_r. Qed. `````` Robbert Krebbers committed Jan 29, 2015 505 506 ``````Lemma list_alter_id f l i : (∀ x, f x = x) → alter f i l = l. Proof. intros ?. revert i. induction l; intros [|?]; f_equal'; auto. Qed. `````` Robbert Krebbers committed May 02, 2014 507 508 509 ``````Lemma list_alter_ext f g l k i : (∀ x, l !! i = Some x → f x = g x) → l = k → alter f i l = alter g i k. Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal'; auto. Qed. `````` Robbert Krebbers committed Jun 17, 2013 510 511 ``````Lemma list_alter_compose f g l i : alter (f ∘ g) i l = alter f i (alter g i l). `````` Robbert Krebbers committed May 02, 2014 512 ``````Proof. revert i. induction l; intros [|?]; f_equal'; auto. Qed. `````` Robbert Krebbers committed Jun 17, 2013 513 514 ``````Lemma list_alter_commute f g l i j : i ≠ j → alter f i (alter g j l) = alter g j (alter f i l). `````` Robbert Krebbers committed May 02, 2014 515 ``````Proof. revert i j. induction l; intros [|?][|?] ?; f_equal'; auto with lia. Qed. `````` Robbert Krebbers committed May 07, 2013 516 517 ``````Lemma insert_app_l l1 l2 i x : i < length l1 → <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2. `````` Robbert Krebbers committed May 02, 2014 518 ``````Proof. revert i. induction l1; intros [|?] ?; f_equal'; auto with lia. Qed. `````` Robbert Krebbers committed May 07, 2013 519 ``````Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2. `````` Robbert Krebbers committed May 02, 2014 520 ``````Proof. revert i. induction l1; intros [|?]; f_equal'; auto. Qed. `````` Robbert Krebbers committed May 07, 2013 521 522 ``````Lemma insert_app_r_alt l1 l2 i x : length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2. `````` Robbert Krebbers committed May 02, 2014 523 524 525 526 ``````Proof. intros. assert (i = length l1 + (i - length l1)) as Hi by lia. rewrite Hi at 1. by apply insert_app_r. Qed. `````` Robbert Krebbers committed May 07, 2013 527 ``````Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2. `````` Robbert Krebbers committed May 02, 2014 528 ``````Proof. induction l1; f_equal'; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 529 `````` `````` Robbert Krebbers committed Feb 16, 2015 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 ``````Lemma inserts_length l i k : length (list_inserts i k l) = length l. Proof. revert i. induction k; intros ?; csimpl; rewrite ?insert_length; auto. Qed. Lemma list_lookup_inserts l i k j : i ≤ j < i + length k → j < length l → list_inserts i k l !! j = k !! (j - i). Proof. revert i j. induction k as [|y k IH]; csimpl; intros i j ??; [lia|]. destruct (decide (i = j)) as [->|]. { by rewrite list_lookup_insert, Nat.sub_diag by (rewrite inserts_length; lia). } rewrite list_lookup_insert_ne, IH by lia. by replace (j - i) with (S (j - S i)) by lia. Qed. Lemma list_lookup_inserts_lt l i k j : j < i → list_inserts i k l !! j = l !! j. Proof. revert i j. induction k; intros i j ?; csimpl; rewrite ?list_lookup_insert_ne by lia; auto with lia. Qed. Lemma list_lookup_inserts_ge l i k j : i + length k ≤ j → list_inserts i k l !! j = l !! j. Proof. revert i j. induction k; csimpl; intros i j ?; rewrite ?list_lookup_insert_ne by lia; auto with lia. Qed. Lemma list_lookup_inserts_Some l i k j y : list_inserts i k l !! j = Some y ↔ (j < i ∨ i + length k ≤ j) ∧ l !! j = Some y ∨ i ≤ j < i + length k ∧ j < length l ∧ k !! (j - i) = Some y. Proof. destruct (decide (j < i)). { rewrite list_lookup_inserts_lt by done; intuition lia. } destruct (decide (i + length k ≤ j)). { rewrite list_lookup_inserts_ge by done; intuition lia. } split. * intros Hy. assert (j < length l). { rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. } rewrite list_lookup_inserts in Hy by lia. intuition lia. * intuition. by rewrite list_lookup_inserts by lia. Qed. Lemma list_insert_inserts_lt l i j x k : i < j → <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l). Proof. revert i j. induction k; intros i j ?; simpl; rewrite 1?list_insert_commute by lia; auto with f_equal. Qed. `````` Robbert Krebbers committed Feb 22, 2013 579 ``````(** ** Properties of the [elem_of] predicate *) `````` Robbert Krebbers committed May 07, 2013 580 ``````Lemma not_elem_of_nil x : x ∉ []. `````` Robbert Krebbers committed Nov 12, 2012 581 ``````Proof. by inversion 1. Qed. `````` Robbert Krebbers committed May 07, 2013 582 ``````Lemma elem_of_nil x : x ∈ [] ↔ False. `````` Robbert Krebbers committed Nov 12, 2012 583 ``````Proof. intuition. by destruct (not_elem_of_nil x). Qed. `````` Robbert Krebbers committed May 07, 2013 584 ``````Lemma elem_of_nil_inv l : (∀ x, x ∉ l) → l = []. `````` Robbert Krebbers committed Nov 12, 2012 585 ``````Proof. destruct l. done. by edestruct 1; constructor. Qed. `````` Robbert Krebbers committed Jun 05, 2014 586 587 ``````Lemma elem_of_not_nil x l : x ∈ l → l ≠ []. Proof. intros ? ->. by apply (elem_of_nil x). Qed. `````` Robbert Krebbers committed May 07, 2013 588 ``````Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l. `````` Robbert Krebbers committed Feb 01, 2017 589 ``````Proof. by split; [inversion 1; subst|intros [->|?]]; constructor. Qed. `````` Robbert Krebbers committed May 07, 2013 590 ``````Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l. `````` Robbert Krebbers committed Jan 05, 2013 591 ``````Proof. rewrite elem_of_cons. tauto. Qed. `````` Robbert Krebbers committed May 07, 2013 592 ``````Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2. `````` Robbert Krebbers committed Oct 19, 2012 593 ``````Proof. `````` Robbert Krebbers committed Nov 12, 2012 594 `````` induction l1. `````` Robbert Krebbers committed May 07, 2013 595 `````` * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x). `````` Robbert Krebbers committed Nov 12, 2012 596 `````` * simpl. rewrite !elem_of_cons, IHl1. tauto. `````` Robbert Krebbers committed Oct 19, 2012 597 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 598 ``````Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2. `````` Robbert Krebbers committed Jan 05, 2013 599 ``````Proof. rewrite elem_of_app. tauto. Qed. `````` Robbert Krebbers committed May 07, 2013 600 ``````Lemma elem_of_list_singleton x y : x ∈ [y] ↔ x = y. `````` Robbert Krebbers committed Nov 12, 2012 601 ``````Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed. `````` Robbert Krebbers committed May 12, 2013 602 ``````Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈). `````` Robbert Krebbers committed Nov 12, 2012 603 ``````Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed. `````` Robbert Krebbers committed May 07, 2013 604 ``````Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2. `````` Robbert Krebbers committed Nov 12, 2012 605 ``````Proof. `````` Robbert Krebbers committed May 02, 2014 606 `````` induction 1 as [x l|x y l ? [l1 [l2 ->]]]; [by eexists [], l|]. `````` Robbert Krebbers committed Nov 11, 2015 607 `````` by exists (y :: l1), l2. `````` Robbert Krebbers committed Nov 12, 2012 608 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 609 ``````Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x. `````` Robbert Krebbers committed Nov 12, 2012 610 ``````Proof. `````` Robbert Krebbers committed May 07, 2013 611 612 `````` induction 1 as [|???? IH]; [by exists 0 |]. destruct IH as [i ?]; auto. by exists (S i). `````` Robbert Krebbers committed Nov 12, 2012 613 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 614 ``````Lemma elem_of_list_lookup_2 l i x : l !! i = Some x → x ∈ l. `````` Robbert Krebbers committed Nov 12, 2012 615 ``````Proof. `````` Robbert Krebbers committed Jun 17, 2013 616 `````` revert i. induction l; intros [|i] ?; simplify_equality'; constructor; eauto. `````` Robbert Krebbers committed Nov 12, 2012 617 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 618 619 ``````Lemma elem_of_list_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x. Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed. `````` Robbert Krebbers committed Jul 10, 2014 620 621 622 623 624 625 ``````Lemma elem_of_list_omap {B} (f : A → option B) l (y : B) : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y. Proof. split. * induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst; setoid_rewrite elem_of_cons; naive_solver. `````` Robbert Krebbers committed Feb 01, 2017 626 627 `````` * intros (x&Hx&?). by induction Hx; csimpl; repeat case_match; simplify_equality; try constructor; auto. `````` Robbert Krebbers committed Jul 10, 2014 628 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 629 `````` `````` Robbert Krebbers committed Feb 22, 2013 630 ``````(** ** Properties of the [NoDup] predicate *) `````` Robbert Krebbers committed Nov 12, 2012 631 632 ``````Lemma NoDup_nil : NoDup (@nil A) ↔ True. Proof. split; constructor. Qed. `````` Robbert Krebbers committed May 07, 2013 633 ``````Lemma NoDup_cons x l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l. `````` Robbert Krebbers committed Nov 12, 2012 634 ``````Proof. split. by inversion 1. intros [??]. by constructor. Qed. `````` Robbert Krebbers committed May 07, 2013 635 ``````Lemma NoDup_cons_11 x l : NoDup (x :: l) → x ∉ l. `````` Robbert Krebbers committed Nov 12, 2012 636 ``````Proof. rewrite NoDup_cons. by intros [??]. Qed. `````` Robbert Krebbers committed May 07, 2013 637 ``````Lemma NoDup_cons_12 x l : NoDup (x :: l) → NoDup l. `````` Robbert Krebbers committed Nov 12, 2012 638 ``````Proof. rewrite NoDup_cons. by intros [??]. Qed. `````` Robbert Krebbers committed May 07, 2013 639 ``````Lemma NoDup_singleton x : NoDup [x]. `````` Robbert Krebbers committed Nov 12, 2012 640 ``````Proof. constructor. apply not_elem_of_nil. constructor. Qed. `````` Robbert Krebbers committed May 07, 2013 641 ``````Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k. `````` Robbert Krebbers committed Jun 11, 2012 642 ``````Proof. `````` Robbert Krebbers committed Nov 12, 2012 643 `````` induction l; simpl. `````` Robbert Krebbers committed May 07, 2013 644 `````` * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver. `````` Robbert Krebbers committed Nov 12, 2012 645 `````` * rewrite !NoDup_cons. `````` Robbert Krebbers committed Feb 24, 2013 646 `````` setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver. `````` Robbert Krebbers committed Jun 11, 2012 647 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 648 ``````Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A). `````` Robbert Krebbers committed Nov 12, 2012 649 650 651 652 653 654 655 ``````Proof. induction 1 as [|x l k Hlk IH | |]. * by rewrite !NoDup_nil. * by rewrite !NoDup_cons, IH, Hlk. * rewrite !NoDup_cons, !elem_of_cons. intuition. * intuition. Qed. `````` Robbert Krebbers committed Jun 24, 2013 656 657 ``````Lemma NoDup_lookup l i j x : NoDup l → l !! i = Some x → l !! j = Some x → i = j. `````` Robbert Krebbers committed Jun 17, 2013 658 659 660 661 662 663 ``````Proof. intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH]. { intros; simplify_equality. } intros [|i] [|j] ??; simplify_equality'; eauto with f_equal; exfalso; eauto using elem_of_list_lookup_2. Qed. `````` Robbert Krebbers committed Jun 24, 2013 664 665 ``````Lemma NoDup_alt l : NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j. `````` Robbert Krebbers committed Nov 12, 2012 666 ``````Proof. `````` Robbert Krebbers committed Jun 17, 2013 667 668 669 670 671 `````` split; eauto using NoDup_lookup. induction l as [|x l IH]; intros Hl; constructor. * rewrite elem_of_list_lookup. intros [i ?]. by feed pose proof (Hl (S i) 0 x); auto. * apply IH. intros i j x' ??. by apply (injective S), (Hl (S i) (S j) x'). `````` Robbert Krebbers committed Nov 12, 2012 672 ``````Qed. `````` Robbert Krebbers committed Jun 11, 2012 673 `````` `````` Robbert Krebbers committed May 07, 2013 674 675 676 677 678 679 ``````Section no_dup_dec. Context `{!∀ x y, Decision (x = y)}. Global Instance NoDup_dec: ∀ l, Decision (NoDup l) := fix NoDup_dec l := match l return Decision (NoDup l) with | [] => left NoDup_nil_2 `````` Robbert Krebbers committed Nov 12, 2012 680 `````` | x :: l => `````` Robbert Krebbers committed May 07, 2013 681 682 683 684 685 686 687 688 `````` match decide_rel (∈) x l with | left Hin => right (λ H, NoDup_cons_11 _ _ H Hin) | right Hin => match NoDup_dec l with | left H => left (NoDup_cons_2 _ _ Hin H) | right H => right (H ∘ NoDup_cons_12 _ _) end end `````` Robbert Krebbers committed Nov 12, 2012 689 `````` end. `````` Robbert Krebbers committed May 07, 2013 690 `````` Lemma elem_of_remove_dups l x : x ∈ remove_dups l ↔ x ∈ l. `````` Robbert Krebbers committed Nov 12, 2012 691 692 693 694 `````` Proof. split; induction l; simpl; repeat case_decide; rewrite ?elem_of_cons; intuition (simplify_equality; auto). Qed. `````` Robbert Krebbers committed Jun 05, 2014 695 `````` Lemma NoDup_remove_dups l : NoDup (remove_dups l). `````` Robbert Krebbers committed Nov 12, 2012 696 697 698 699 `````` Proof. induction l; simpl; repeat case_decide; try constructor; auto. by rewrite elem_of_remove_dups. Qed. `````` Robbert Krebbers committed May 07, 2013 700 ``````End no_dup_dec. `````` Robbert Krebbers committed Oct 19, 2012 701 `````` `````` Robbert Krebbers committed Jun 05, 2014 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 ``````(** ** Set operations on lists *) Section list_set. Context {dec : ∀ x y, Decision (x = y)}. Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k. Proof. split; induction l; simpl; try case_decide; rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence. Qed. Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k). Proof. induction 1; simpl; try case_decide. * constructor. * done. * constructor. rewrite elem_of_list_difference; intuition. done. Qed. Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k. Proof. unfold list_union. rewrite elem_of_app, elem_of_list_difference. intuition. case (decide (x ∈ k)); intuition. Qed. Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k). Proof. intros. apply NoDup_app. repeat split. * by apply NoDup_list_difference. * intro. rewrite ``````