list.v 12.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 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 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
Require Import Permutation. 
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.

Section list_properties.
Context {A : Type}.

Definition option_list : option A  list A := option_rect _ (λ x, [x]) [].

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.
  induction 1; simpl. easy.
  constructor. rewrite in_app_iff. firstorder. firstorder.
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.

Global Instance list_eq_dec {dec :  x y : A, Decision (x = y)} :  l k : list A, Decision (l = k).
Proof. solve_decision. Qed.
Global Instance list_in_dec {dec :  x y : A, Decision (x = y)} :  x l,
  Decision (In x l) := in_dec dec.

Global Instance NoDup_dec {dec :  x y : A, Decision (x = y)} :  (l : list A), Decision (NoDup l) :=
  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.

Global Instance Forall_dec (P : A  Prop) {dec :  x, Decision (P x)} :  l, Decision (Forall P l) :=
  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.

Global Instance Exists_dec (P : A  Prop) {dec :  x, Decision (P x)} :  l, Decision (Exists P l) :=
  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.

Definition prefix_of (l1 l2 : list A) : Prop :=  k, l2 = l1 ++ k.
Definition suffix_of (l1 l2 : list A) : Prop :=  k, l2 = k ++ l1.

Global Instance: PreOrder prefix_of.
Proof.
  split.
   intros ?. eexists []. now rewrite app_nil_r.
  intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
Qed.

Lemma prefix_of_nil l : prefix_of [] l.
Proof. now exists l. Qed.
Lemma prefix_of_nil_not x l : ¬prefix_of (x :: l) [].
Proof. intros [k E]. discriminate. Qed.
Lemma prefix_of_cons x y l1 l2 : x = y  prefix_of l1 l2  prefix_of (x :: l1) (y :: l2).
Proof. intros ? [k E]. exists k. now subst. Qed.
Lemma prefix_of_cons_inv_1 x y l1 l2 : prefix_of (x :: l1) (y :: l2)  x = y.
Proof. intros [k E]. now injection E. Qed.
Lemma prefix_of_cons_inv_2 x y l1 l2 : prefix_of (x :: l1) (y :: l2)  prefix_of l1 l2.
Proof. intros [k E]. exists k. now injection E. Qed.

Lemma prefix_of_app_l l1 l2 l3 : prefix_of (l1 ++ l3) l2  prefix_of l1 l2.
Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
Lemma prefix_of_app_r l1 l2 l3 : prefix_of l1 l2  prefix_of l1 (l2 ++ l3).
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.

Global Instance prefix_of_dec `{ x y : A, Decision (x = y)} :  l1 l2, Decision (prefix_of l1 l2) :=
  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.

Global Instance: PreOrder suffix_of.
Proof.
  split.
   intros ?. now eexists [].
  intros ??? [k1 ?] [k2 ?]. exists (k2 ++ k1). subst. now rewrite app_assoc.
Qed.

Lemma prefix_suffix_rev l1 l2 : prefix_of l1 l2  suffix_of (rev l1) (rev l2).
Proof.
  split; intros [k E]; exists (rev k).
   now rewrite E, rev_app_distr.
  now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
Qed.
Lemma suffix_prefix_rev l1 l2 : suffix_of l1 l2  prefix_of (rev l1) (rev l2).
Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.

Lemma suffix_of_nil l : suffix_of [] l.
Proof. exists l. now rewrite app_nil_r. Qed.
Lemma suffix_of_nil_not x l : ¬suffix_of (x :: l) [].
Proof. intros [[] ?]; discriminate. Qed.
Lemma suffix_of_cons x y l1 l2 : x = y  suffix_of l1 l2  suffix_of (l1 ++ [x]) (l2 ++ [y]).
Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y])  x = y.
Proof. rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1. Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y])  suffix_of l1 l2.
Proof. rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2. Qed.

Lemma suffix_of_cons_l l1 l2 x : suffix_of (x :: l1) l2  suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
Lemma suffix_of_app_l l1 l2 l3 : suffix_of (l3 ++ l1) l2  suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
Lemma suffix_of_cons_r l1 l2 x : suffix_of l1 l2  suffix_of l1 (x :: l2).
Proof. intros [k ?]. exists (x :: k). now subst. Qed.
Lemma suffix_of_app_r l1 l2 l3 : suffix_of l1 l2  suffix_of l1 (l3 ++ l2).
Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.

Lemma suffix_of_cons_inv l1 l2 x y : 
  suffix_of (x :: l1) (y :: l2)  x :: l1 = y :: l2  suffix_of (x :: l1) l2.
Proof.
  intros [[|? k] E].
   now left.
  right. simplify_eqs. now apply suffix_of_app_r.
Qed.
Lemma suffix_of_cons_not x l : ¬suffix_of (x :: l) l.
Proof.
  intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
  rewrite app_assoc in E. apply app_inv_tail in E.
  destruct k; simplify_eqs.
Qed.

Global Program Instance suffix_of_dec `{ x y : A, Decision (x = y)} l1 l2 : Decision (suffix_of l1 l2) :=
  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.
Next Obligation. intro. destruct Hpre. rewrite <-!rev_alt. now apply suffix_prefix_rev. Qed.
End list_properties.

Hint Resolve suffix_of_nil suffix_of_cons_r suffix_of_app_r : list.
Hint Extern 0 (prefix_of _ _) => reflexivity : list.
Hint Extern 0 (suffix_of _ _) => reflexivity: list.
Hint Extern 0 (PropHolds (suffix_of _ _)) => red; auto with list : typeclass_instances.

Ltac simplify_suffix_of := repeat
  match goal with
  | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H); clear H
  | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H); clear H
  | H : suffix_of (_ :: _) (_ :: _) |- _ => destruct (suffix_of_cons_inv _ _ _ _ H); clear H
  | H : suffix_of ?x ?x |- _ => clear H
  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
  | _ => progress simplify_eqs
  end.

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.
Local Arguments lookup _ _ _ _ _ !_ /.

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.

Lemma list_eq {A} (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_tail {A} (l : list A) i : tail l !! i = l !! S i.
Proof. now destruct l. Qed.

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.
Global Instance list_join: MJoin list := 
  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).

Lemma list_lookup_weaken {A} (l l' : list A) i x :
  l !! i = Some x  (l ++ l') !! i = Some x.
Proof. revert i. induction l. discriminate. now intros []. Qed.

Lemma list_lookup_fmap {A B} (f : A  B) l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; now intros [|]. Qed.

Lemma fold_right_permutation `(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. intros Hflip. induction 1; simpl; try congruence. Qed.

(*
Section NoDupA.
  Fixpoint removeDups (l : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      let k := removeDups l in
      if InA_dec dec x k then k else x :: k
    end.

  Lemma removeDups_NoDupA l : NoDupA R (removeDups l).
  Proof. induction l; simpl; try case InA_dec; intuition. Qed.

  Definition elem_removeDups x l : x ∈ removeDups l → x ∈ l.
  Proof.
    induction l; simpl; auto.
    case InA_dec; eauto.
    intros ? Hin. destruct (list_elem_inv _ _ _ Hin); subst; eauto.
  Qed.

  Lemma elem_InA x y l : x ∈ l → R y x → InA R y l.
  Proof. induction 1; subst; intuition. Qed.

  Lemma InA_elem x l : InA R x l → ∃ y, y ∈ l ∧ R x y.
  Proof. induction 1. eauto. destruct IHInA as [? [??]]; eauto. Qed.

  Context `{!Equivalence R}.

  Lemma in_removeDups_inv x l : x ∈ l → ∃ y, y ∈ l ∧ R x y ∧ y ∈ removeDups l.
  Proof.
    induction l as [|y l]; simpl.
     inversion 1.
    case InA_dec.
     inversion 2; subst.
      destruct (InA_elem y (removeDups l)) as [z [??]]; auto.
      exists z. intuition. right. now apply elem_removeDups.
     destruct IHl as [z [?[??]]]. auto. exists z. intuition.
    intros ? Hin. destruct (list_elem_inv _ _ _ Hin).
     subst. exists y. intuition.
    destruct IHl as [z [?[??]]]. easy. exists z. intuition.
  Qed.

  Lemma in_removeDups x l : InA R x l ↔ InA R x (removeDups l).
  Proof.
    split.
     induction 1 as [?? E|]; simpl; [rewrite E|]; case InA_dec; intuition.
    induction l; simpl; auto.
    case InA_dec. auto. inversion_clear 2; auto.
  Qed.
End NoDupA.

Lemma InA_lift_rel {A B} (R : relation A) (f : B → A) x l : InA R (f x) (f <$> l) ↔ InA (lift_rel R f) x l.
Proof. split; induction l; unfold fmap; simpl; inversion_clear 1; auto. Qed.

Lemma NoDupA_lift_rel {A B} (R : relation A) (f : B → A) l : NoDupA R (f <$> l) ↔ NoDupA (lift_rel R f) l.
Proof.
  split.
   induction l; [easy |].
   intros HnoDup. constructor.
    intro. destruct (NoDupA_inv_1 R _ _ HnoDup). now apply InA_lift_rel.
   eapply IHl, NoDupA_inv_2; eauto.
  induction 1; constructor. now rewrite InA_lift_rel. easy.
Qed.
*)