list.v 18.7 KB
 Robbert Krebbers committed Aug 29, 2012 1 2 3 4 5 ``````(* Copyright (c) 2012, Robbert Krebbers. *) (* 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. *) Require Import Permutation. `````` Robbert Krebbers committed Jun 11, 2012 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````Require Export base decidable option. Arguments cons {_} _ _. Arguments app {_} _ _. Arguments In {_} _ _. Arguments NoDup_nil {_}. Arguments Permutation {_} _ _. 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 Aug 29, 2012 22 23 ``````(** * General definitions *) (** Looking up elements and updating elements in a list. *) `````` Robbert Krebbers committed Aug 21, 2012 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 ``````Global Instance list_lookup: Lookup nat list := fix list_lookup A (i : nat) (l : list A) {struct l} : option A := match l with | [] => None | x :: l => match i with | 0 => Some x | S i => @lookup _ _ list_lookup _ i l end end. Global Instance list_alter: Alter nat list := fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} := match l with | [] => [] | x :: l => match i with | 0 => f x :: l | S i => x :: @alter _ _ list_alter _ f i l end end. `````` Robbert Krebbers committed Aug 29, 2012 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 ``````(** The [simpl] tactic does not simplify [list_lookup] as it is wrapped into an operational type class and we cannot let it unfold on a per instance basis. Therefore we use the [simplify_list_lookup] tactic to perform these simplifications. Bug: it does not unfold under binders. *) Ltac simplify_list_lookup := repeat match goal with | |- context C [@nil ?A !! _] => let X := (context C [@None A]) in change X | |- context C [(?x :: _) !! 0] => let X := (context C [Some x]) in change X | |- context C [(_ :: ?l) !! S ?i] => let X := (context C [l !! i]) in change X | H : context C [@nil ?A !! _] |- _ => let X := (context C [@None A]) in change X in H | H : context C [(?x :: _) !! 0] |- _ => let X := (context C [Some x]) in change X in H | H : context C [(_ :: ?l) !! S ?i] |- _ => let X := (context C [l !! i]) in change X in H end. (** The function [option_list] converts an element of the option type into a list. *) `````` Robbert Krebbers committed Aug 21, 2012 68 ``````Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) []. `````` Robbert Krebbers committed Aug 29, 2012 69 70 71 `````` (** The predicate [prefix_of] holds if the first list is a prefix of the second. The predicate [suffix_of] holds if the first list is a suffix of the second. *) `````` Robbert Krebbers committed Aug 21, 2012 72 73 74 ``````Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k. Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1. `````` Robbert Krebbers committed Aug 29, 2012 75 76 ``````(** * General theorems *) Section general_properties. `````` Robbert Krebbers committed Jun 11, 2012 77 78 ``````Context {A : Type}. `````` Robbert Krebbers committed Aug 21, 2012 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 ``````Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2. Proof. revert l2. induction l1; intros [|??] H. * easy. * discriminate (H 0). * discriminate (H 0). * f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)). Qed. Lemma list_lookup_nil i : @nil A !! i = None. Proof. now destruct i. Qed. Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i. Proof. now destruct l. Qed. Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x → In x l. Proof. revert i. induction l; intros [|i] ?; `````` Robbert Krebbers committed Aug 29, 2012 96 `````` simplify_list_lookup; simplify_equality; constructor (solve [eauto]). `````` Robbert Krebbers committed Aug 21, 2012 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 ``````Qed. Lemma list_lookup_In_Some (l : list A) x : In x l → ∃ i, l !! i = Some x. Proof. induction l; destruct 1; subst. * now exists 0. * destruct IHl as [i ?]; auto. now exists (S i). Qed. Lemma list_lookup_In (l : list A) x : In x l ↔ ∃ i, l !! i = Some x. Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed. Lemma list_lookup_app_length (l1 l2 : list A) (x : A) : (l1 ++ x :: l2) !! length l1 = Some x. Proof. induction l1; simpl; now simplify_list_lookup. Qed. Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i) ↔ i < length l. Proof. revert i. induction l. * split; now inversion 1. * intros [|?]; simplify_list_lookup; simpl. + split; auto with arith. + now rewrite <-NPeano.Nat.succ_lt_mono. Qed. Lemma list_lookup_weaken (l l' : list A) i x : l !! i = Some x → (l ++ l') !! i = Some x. Proof. revert i. induction l. discriminate. now intros []. Qed. `````` Robbert Krebbers committed Aug 29, 2012 124 125 126 127 128 ``````Lemma fold_right_permutation {B} (f : A → B → B) (b : B) : (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) → Proper (Permutation ==> (=)) (fold_right f b). Proof. intro. induction 1; simpl; congruence. Qed. `````` Robbert Krebbers committed Aug 21, 2012 129 130 131 132 133 134 135 136 137 138 139 140 141 ``````Lemma Forall_impl (P Q : A → Prop) l : Forall P l → (∀ x, P x → Q x) → Forall Q l. Proof. induction 1; auto. Qed. Lemma Forall2_length {B} (P : A → B → Prop) l1 l2 : Forall2 P l1 l2 → length l1 = length l2. Proof. induction 1; simpl; auto. Qed. Lemma Forall2_impl {B} (P Q : A → B → Prop) l1 l2 : Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2. Proof. induction 1; auto. Qed. Lemma Forall2_unique {B} (P : A → B → Prop) l k1 k2 : `````` Robbert Krebbers committed Aug 29, 2012 142 143 144 145 146 147 148 `````` Forall2 P l k1 → Forall2 P l k2 → (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2. Proof. intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 149 150 151 152 153 154 `````` Lemma NoDup_singleton (x : A) : NoDup [x]. Proof. constructor. easy. constructor. Qed. Lemma NoDup_app (l k : list A) : NoDup l → NoDup k → (∀ x, In x l → ¬In x k) → NoDup (l ++ k). Proof. `````` Robbert Krebbers committed Aug 21, 2012 155 156 157 `````` induction 1; simpl. * easy. * constructor. rewrite in_app_iff. firstorder. firstorder. `````` Robbert Krebbers committed Jun 11, 2012 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 ``````Qed. Global Instance: ∀ k : list A, Injective (=) (=) (k ++). Proof. intros ???. apply app_inv_head. Qed. Global Instance: ∀ k : list A, Injective (=) (=) (++ k). Proof. intros ???. apply app_inv_tail. Qed. Lemma in_nil_inv (l : list A) : (∀ x, ¬In x l) → l = []. Proof. destruct l. easy. now edestruct 1; constructor. Qed. Lemma nil_length (l : list A) : length l = 0 → l = []. Proof. destruct l. easy. discriminate. Qed. Lemma NoDup_inv_1 (x : A) (l : list A) : NoDup (x :: l) → ¬In x l. Proof. now inversion_clear 1. Qed. Lemma NoDup_inv_2 (x : A) (l : list A) : NoDup (x :: l) → NoDup l. Proof. now inversion_clear 1. Qed. Lemma Forall_inv_2 (P : A → Prop) x l : Forall P (x :: l) → Forall P l. Proof. now inversion 1. Qed. Lemma Exists_inv (P : A → Prop) x l : Exists P (x :: l) → P x ∨ Exists P l. Proof. inversion 1; intuition. Qed. `````` Robbert Krebbers committed Aug 21, 2012 178 179 ``````Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k, Decision (l = k) := list_eq_dec dec. `````` Robbert Krebbers committed Jun 11, 2012 180 181 182 ``````Global Instance list_in_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l, Decision (In x l) := in_dec dec. `````` Robbert Krebbers committed Aug 21, 2012 183 184 ``````Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ (l : list A), Decision (NoDup l) := `````` Robbert Krebbers committed Jun 11, 2012 185 186 187 188 189 190 191 192 193 194 195 196 197 198 `````` fix NoDup_dec l := match l return Decision (NoDup l) with | [] => left NoDup_nil | x :: l => match In_dec dec x l with | left Hin => right (λ H, NoDup_inv_1 _ _ H Hin) | right Hin => match NoDup_dec l with | left H => left (NoDup_cons _ Hin H) | right H => right (H ∘ NoDup_inv_2 _ _) end end end. `````` Robbert Krebbers committed Aug 21, 2012 199 200 ``````Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Forall P l) := `````` Robbert Krebbers committed Jun 11, 2012 201 202 203 204 205 206 207 208 209 210 211 212 213 214 `````` fix go (l : list A) := match l return {Forall P l} + {¬Forall P l} with | [] => left (Forall_nil _) | x :: l => match dec x with | left Hx => match go l with | left Hl => left (Forall_cons _ Hx Hl) | right Hl => right (Hl ∘ Forall_inv_2 _ _ _) end | right Hx => right (Hx ∘ @Forall_inv _ _ _ _) end end. `````` Robbert Krebbers committed Aug 21, 2012 215 216 ``````Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Exists P l) := `````` Robbert Krebbers committed Jun 11, 2012 217 218 219 220 221 222 223 224 225 226 227 228 229 `````` fix go (l : list A) := match l return {Exists P l} + {¬Exists P l} with | [] => right (proj1 (Exists_nil _)) | x :: l => match dec x with | left Hx => left (Exists_cons_hd _ _ _ Hx) | right Hx => match go l with | left Hl => left (Exists_cons_tl _ Hl) | right Hl => right (or_ind Hx Hl ∘ Exists_inv _ _ _) end end end. `````` Robbert Krebbers committed Aug 29, 2012 230 231 232 233 234 ``````End general_properties. (** * Theorems on the prefix and suffix predicates *) Section prefix_postfix. Context {A : Type}. `````` Robbert Krebbers committed Jun 11, 2012 235 `````` `````` Robbert Krebbers committed Aug 21, 2012 236 ``````Global Instance: PreOrder (@prefix_of A). `````` Robbert Krebbers committed Jun 11, 2012 237 238 239 240 241 242 ``````Proof. split. intros ?. eexists []. now rewrite app_nil_r. intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 243 ``````Lemma prefix_of_nil (l : list A) : prefix_of [] l. `````` Robbert Krebbers committed Jun 11, 2012 244 ``````Proof. now exists l. Qed. `````` Robbert Krebbers committed Aug 21, 2012 245 ``````Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) []. `````` Robbert Krebbers committed Jun 11, 2012 246 ``````Proof. intros [k E]. discriminate. Qed. `````` Robbert Krebbers committed Aug 21, 2012 247 248 ``````Lemma prefix_of_cons x y (l1 l2 : list A) : x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2). `````` Robbert Krebbers committed Jun 11, 2012 249 ``````Proof. intros ? [k E]. exists k. now subst. Qed. `````` Robbert Krebbers committed Aug 21, 2012 250 251 ``````Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) : prefix_of (x :: l1) (y :: l2) → x = y. `````` Robbert Krebbers committed Jun 11, 2012 252 ``````Proof. intros [k E]. now injection E. Qed. `````` Robbert Krebbers committed Aug 21, 2012 253 254 ``````Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) : prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2. `````` Robbert Krebbers committed Jun 11, 2012 255 256 ``````Proof. intros [k E]. exists k. now injection E. Qed. `````` Robbert Krebbers committed Aug 21, 2012 257 258 ``````Lemma prefix_of_app_l (l1 l2 l3 : list A) : prefix_of (l1 ++ l3) l2 → prefix_of l1 l2. `````` Robbert Krebbers committed Jun 11, 2012 259 ``````Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 260 261 ``````Lemma prefix_of_app_r (l1 l2 l3 : list A) : prefix_of l1 l2 → prefix_of l1 (l2 ++ l3). `````` Robbert Krebbers committed Jun 11, 2012 262 263 ``````Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 264 265 ``````Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} : ∀ l1 l2, Decision (prefix_of l1 l2) := `````` Robbert Krebbers committed Jun 11, 2012 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 `````` fix prefix_of_dec l1 l2 := match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with | [], _ => left (prefix_of_nil _) | _, [] => right (prefix_of_nil_not _ _) | x :: l1, y :: l2 => match decide_rel (=) x y with | left Exy => match prefix_of_dec l1 l2 with | left Hl1l2 => left (prefix_of_cons _ _ _ _ Exy Hl1l2) | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _) end | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _) end end. `````` Robbert Krebbers committed Aug 21, 2012 281 ``````Global Instance: PreOrder (@suffix_of A). `````` Robbert Krebbers committed Jun 11, 2012 282 283 ``````Proof. split. `````` Robbert Krebbers committed Aug 21, 2012 284 285 286 `````` * intros ?. now eexists []. * intros ??? [k1 ?] [k2 ?]. exists (k2 ++ k1). subst. now rewrite app_assoc. `````` Robbert Krebbers committed Jun 11, 2012 287 288 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2012 289 290 ``````Lemma prefix_suffix_rev (l1 l2 : list A) : prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2). `````` Robbert Krebbers committed Jun 11, 2012 291 292 ``````Proof. split; intros [k E]; exists (rev k). `````` Robbert Krebbers committed Aug 21, 2012 293 294 `````` * now rewrite E, rev_app_distr. * now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive. `````` Robbert Krebbers committed Jun 11, 2012 295 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2012 296 297 ``````Lemma suffix_prefix_rev (l1 l2 : list A) : suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2). `````` Robbert Krebbers committed Jun 11, 2012 298 299 ``````Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed. `````` Robbert Krebbers committed Aug 21, 2012 300 ``````Lemma suffix_of_nil (l : list A) : suffix_of [] l. `````` Robbert Krebbers committed Jun 11, 2012 301 ``````Proof. exists l. now rewrite app_nil_r. Qed. `````` Robbert Krebbers committed Aug 21, 2012 302 ``````Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) []. `````` Robbert Krebbers committed Jun 11, 2012 303 ``````Proof. intros [[] ?]; discriminate. Qed. `````` Robbert Krebbers committed Aug 21, 2012 304 305 ``````Lemma suffix_of_cons x y (l1 l2 : list A) : x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]). `````` Robbert Krebbers committed Jun 11, 2012 306 ``````Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 307 308 ``````Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) : suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y. `````` Robbert Krebbers committed Aug 29, 2012 309 310 311 ``````Proof. rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1. Qed. `````` Robbert Krebbers committed Aug 21, 2012 312 313 ``````Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) : suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2. `````` Robbert Krebbers committed Aug 29, 2012 314 315 316 ``````Proof. rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2. Qed. `````` Robbert Krebbers committed Jun 11, 2012 317 `````` `````` Robbert Krebbers committed Aug 21, 2012 318 319 ``````Lemma suffix_of_cons_l (l1 l2 : list A) x : suffix_of (x :: l1) l2 → suffix_of l1 l2. `````` Robbert Krebbers committed Jun 11, 2012 320 ``````Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 321 322 ``````Lemma suffix_of_app_l (l1 l2 l3 : list A) : suffix_of (l3 ++ l1) l2 → suffix_of l1 l2. `````` Robbert Krebbers committed Jun 11, 2012 323 ``````Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed. `````` Robbert Krebbers committed Aug 21, 2012 324 325 ``````Lemma suffix_of_cons_r (l1 l2 : list A) x : suffix_of l1 l2 → suffix_of l1 (x :: l2). `````` Robbert Krebbers committed Jun 11, 2012 326 ``````Proof. intros [k ?]. exists (x :: k). now subst. Qed. `````` Robbert Krebbers committed Aug 21, 2012 327 328 ``````Lemma suffix_of_app_r (l1 l2 l3 : list A) : suffix_of l1 l2 → suffix_of l1 (l3 ++ l2). `````` Robbert Krebbers committed Jun 11, 2012 329 330 ``````Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed. `````` Robbert Krebbers committed Aug 29, 2012 331 ``````Lemma suffix_of_cons_inv (l1 l2 : list A) x y : `````` Robbert Krebbers committed Jun 11, 2012 332 333 334 335 `````` suffix_of (x :: l1) (y :: l2) → x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2. Proof. intros [[|? k] E]. now left. `````` Robbert Krebbers committed Aug 29, 2012 336 `````` right. simplify_equality. now apply suffix_of_app_r. `````` Robbert Krebbers committed Jun 11, 2012 337 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2012 338 ``````Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l. `````` Robbert Krebbers committed Jun 11, 2012 339 340 341 ``````Proof. intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E. rewrite app_assoc in E. apply app_inv_tail in E. `````` Robbert Krebbers committed Aug 29, 2012 342 `````` destruct k; simplify_equality. `````` Robbert Krebbers committed Jun 11, 2012 343 344 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2012 345 346 ``````Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 : Decision (suffix_of l1 l2) := `````` Robbert Krebbers committed Jun 11, 2012 347 348 349 350 351 `````` match decide_rel prefix_of (rev_append l1 []) (rev_append l2 []) with | left Hpre => left _ | right Hpre => right _ end. Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed. `````` Robbert Krebbers committed Aug 29, 2012 352 353 ``````Next Obligation. intro. destruct Hpre. rewrite <-!rev_alt. `````` Robbert Krebbers committed Aug 21, 2012 354 355 `````` now apply suffix_prefix_rev. Qed. `````` Robbert Krebbers committed Aug 29, 2012 356 ``````End prefix_postfix. `````` Robbert Krebbers committed Jun 11, 2012 357 `````` `````` Robbert Krebbers committed Aug 29, 2012 358 359 360 ``````(** The [simplify_suffix_of] removes [suffix_of] assumptions that are tautologies, and simplifies [suffix_of] assumptions involving [(::)] and [(++)]. *) `````` Robbert Krebbers committed Jun 11, 2012 361 362 ``````Ltac simplify_suffix_of := repeat match goal with `````` Robbert Krebbers committed Aug 29, 2012 363 364 365 366 `````` | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H) | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H) `````` Robbert Krebbers committed Aug 21, 2012 367 368 `````` | H : suffix_of (_ :: _) (_ :: _) |- _ => destruct (suffix_of_cons_inv _ _ _ _ H); clear H `````` Robbert Krebbers committed Jun 11, 2012 369 370 371 `````` | H : suffix_of ?x ?x |- _ => clear H | H : suffix_of ?x (_ :: ?x) |- _ => clear H | H : suffix_of ?x (_ ++ ?x) |- _ => clear H `````` Robbert Krebbers committed Aug 29, 2012 372 `````` | _ => progress simplify_equality `````` Robbert Krebbers committed Jun 11, 2012 373 374 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 375 376 377 378 379 380 ``````(** The [solve_suffix_of] tries to solve goals involving [suffix_of]. It uses [simplify_suffix_of] to simplify assumptions, tries to solve [suffix_of] conclusions, and adds transitive consequences of assumptions to the context. This tactic either fails or proves the goal. *) Ltac solve_suffix_of := let rec go := `````` Robbert Krebbers committed Aug 21, 2012 381 `````` match goal with `````` Robbert Krebbers committed Aug 29, 2012 382 383 384 385 386 387 388 `````` | _ => progress simplify_suffix_of; go | |- suffix_of [] _ => apply suffix_of_nil | |- suffix_of _ _ => reflexivity | |- suffix_of _ _ => solve [auto] | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r; go | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r; go | H : ¬suffix_of _ _ |- _ => destruct H; go `````` Robbert Krebbers committed Aug 21, 2012 389 390 `````` | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ => match goal with `````` Robbert Krebbers committed Aug 29, 2012 391 `````` | _ : suffix_of x z |- _ => fail 1 `````` Robbert Krebbers committed Aug 21, 2012 392 `````` | _ => assert (suffix_of x z) by (transitivity y; assumption); `````` Robbert Krebbers committed Aug 29, 2012 393 `````` clear H1; clear H2; go (**i clear to avoid loops *) `````` Robbert Krebbers committed Aug 21, 2012 394 `````` end `````` Robbert Krebbers committed Aug 29, 2012 395 396 397 `````` end in go. Hint Extern 0 (PropHolds (suffix_of _ _)) => unfold PropHolds; solve_suffix_of : typeclass_instances. `````` Robbert Krebbers committed Jun 11, 2012 398 `````` `````` Robbert Krebbers committed Aug 29, 2012 399 ``````(** * Monadic operations *) `````` Robbert Krebbers committed Jun 11, 2012 400 401 402 403 404 405 406 ``````Global Instance list_ret: MRet list := λ A a, [a]. Global Instance list_fmap: FMap list := fix go A B (f : A → B) (l : list A) := match l with | [] => [] | x :: l => f x :: @fmap _ go _ _ f l end. `````` Robbert Krebbers committed Aug 29, 2012 407 ``````Global Instance list_join: MJoin list := `````` Robbert Krebbers committed Jun 11, 2012 408 409 410 411 412 413 414 `````` fix go A (l : list (list A)) : list A := match l with | [] => [] | x :: l => x ++ @mjoin _ go _ l end. Global Instance list_bind: MBind list := λ A B f l, mjoin (f <\$> l). `````` Robbert Krebbers committed Aug 21, 2012 415 416 ``````Section list_fmap. Context {A B : Type} (f : A → B). `````` Robbert Krebbers committed Jun 11, 2012 417 `````` `````` Robbert Krebbers committed Aug 29, 2012 418 419 `````` Local Arguments fmap _ _ _ _ _ !_ /. `````` Robbert Krebbers committed Aug 21, 2012 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 `````` Lemma fmap_length l : length (f <\$> l) = length l. Proof. induction l; simpl; auto. Qed. Lemma list_lookup_fmap l i : (f <\$> l) !! i = f <\$> (l !! i). Proof. revert i. induction l; now intros [|]. Qed. Lemma in_fmap_1 l x : In x l → In (f x) (f <\$> l). Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed. Lemma in_fmap_1_alt l x y : In x l → y = f x → In y (f <\$> l). Proof. intros. subst. now apply in_fmap_1. Qed. Lemma in_fmap_2 l x : In x (f <\$> l) → ∃ y, x = f y ∧ In y l. Proof. induction l as [|y l]; destruct 1; subst. * exists y; now intuition. * destruct IHl as [y' [??]]. easy. exists y'; now intuition. Qed. Lemma in_fmap l x : In x (f <\$> l) ↔ ∃ y, x = f y ∧ In y l. `````` Robbert Krebbers committed Jun 11, 2012 437 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 438 439 440 `````` split. * apply in_fmap_2. * intros [? [??]]. eauto using in_fmap_1_alt. `````` Robbert Krebbers committed Jun 11, 2012 441 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 442 443 444 445 446 447 448 449 450 ``````End list_fmap. Lemma Forall_fst {A B} (l : list (A * B)) (P : A → Prop) : Forall (P ∘ fst) l ↔ Forall P (fst <\$> l). Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed. Lemma Forall_snd {A B} (l : list (A * B)) (P : B → Prop) : Forall (P ∘ snd) l ↔ Forall P (snd <\$> l). Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 451 452 453 ``````(** * Indexed folds and maps *) (** We define stronger variants of map and fold that also take the index of the element into account. *) `````` Robbert Krebbers committed Aug 21, 2012 454 455 456 457 458 459 460 ``````Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B := fix go (n : nat) (l : list A) := match l with | [] => [] | x :: l => f n x :: go (S n) l end. Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0. `````` Robbert Krebbers committed Jun 11, 2012 461 `````` `````` Robbert Krebbers committed Aug 29, 2012 462 463 ``````Definition ifold_right {A B} (f : nat → B → A → A) (a : nat → A) : nat → list B → A := `````` Robbert Krebbers committed Aug 21, 2012 464 465 466 467 468 `````` fix go (n : nat) (l : list B) : A := match l with | nil => a n | b :: l => f n b (go (S n) l) end. `````` Robbert Krebbers committed Jun 11, 2012 469 `````` `````` Robbert Krebbers committed Aug 29, 2012 470 471 ``````Lemma ifold_right_app {A B} (f : nat → B → A → A) (a : nat → A) (l1 l2 : list B) n : `````` Robbert Krebbers committed Aug 21, 2012 472 `````` ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1. `````` Robbert Krebbers committed Aug 29, 2012 473 474 475 ``````Proof. revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 476 `````` `````` Robbert Krebbers committed Aug 29, 2012 477 478 479 ``````(** * Lists of the same length *) (** The [same_length] view allows convenient induction over two lists with the same length. *) `````` Robbert Krebbers committed Aug 21, 2012 480 481 ``````Section same_length. Context {A B : Type}. `````` Robbert Krebbers committed Jun 11, 2012 482 `````` `````` Robbert Krebbers committed Aug 21, 2012 483 484 485 486 487 488 489 `````` Inductive same_length : list A → list B → Prop := | same_length_nil : same_length [] [] | same_length_cons x y l k : same_length l k → same_length (x :: l) (y :: k). Lemma same_length_length l k : same_length l k ↔ length l = length k. `````` Robbert Krebbers committed Jun 11, 2012 490 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 491 492 493 494 `````` split. * induction 1; simpl; auto. * revert k. induction l; intros [|??]; try discriminate; constructor; auto with arith. `````` Robbert Krebbers committed Jun 11, 2012 495 496 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 497 498 `````` Lemma same_length_lookup l k i : same_length l k → is_Some (l !! i) → is_Some (k !! i). `````` Robbert Krebbers committed Jun 11, 2012 499 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 500 501 502 `````` rewrite same_length_length. setoid_rewrite list_lookup_lt_length. intros E. now rewrite E. `````` Robbert Krebbers committed Jun 11, 2012 503 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 504 ``````End same_length. `````` Robbert Krebbers committed Jun 11, 2012 505 `````` `````` Robbert Krebbers committed Aug 29, 2012 506 507 508 ``````(** * Zipping lists *) (** Since we prefer Haskell style naming, we rename the standard library's implementation [combine] into [zip] using a notation. *) `````` Robbert Krebbers committed Aug 21, 2012 509 ``````Notation zip := combine. `````` Robbert Krebbers committed Jun 11, 2012 510 `````` `````` Robbert Krebbers committed Aug 21, 2012 511 512 513 ``````Section zip. Context {A B : Type}. `````` Robbert Krebbers committed Aug 29, 2012 514 515 `````` Local Arguments fmap _ _ _ _ _ !_ /. `````` Robbert Krebbers committed Aug 21, 2012 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 `````` Lemma zip_fst_le (l1 : list A) (l2 : list B) : length l1 ≤ length l2 → fst <\$> zip l1 l2 = l1. Proof. revert l2. induction l1; intros [|??] ?; simpl; f_equal; auto with arith. edestruct Le.le_Sn_0; eauto. Qed. Lemma zip_fst (l1 : list A) (l2 : list B) : same_length l1 l2 → fst <\$> zip l1 l2 = l1. Proof. rewrite same_length_length. intros H. apply zip_fst_le. now rewrite H. Qed. Lemma zip_snd_le (l1 : list A) (l2 : list B) : length l2 ≤ length l1 → snd <\$> zip l1 l2 = l2. Proof. revert l2. induction l1; intros [|??] ?; simpl; f_equal; auto with arith. edestruct Le.le_Sn_0; eauto. Qed. Lemma zip_snd (l1 : list A) (l2 : list B) : same_length l1 l2 → snd <\$> zip l1 l2 = l2. Proof. rewrite same_length_length. intros H. apply zip_snd_le. now rewrite H. Qed. End zip.``````