list.v

(* 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.
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.

(** * General definitions *)
(** Looking up elements and updating elements in a list. *)
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.

(** 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. *)
Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].

(** 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. *)
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.

(** * General theorems *)
Section general_properties.
Context {A : Type}.

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] ?;
    simplify_list_lookup; simplify_equality; constructor (solve [eauto]).
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.

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.

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 :
  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.

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,
  Decision (l = k) := list_eq_dec dec.
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.
End general_properties.

(** * Theorems on the prefix and suffix predicates *)
Section prefix_postfix.
Context {A : Type}.

Global Instance: PreOrder (@prefix_of A).
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 : list A) : prefix_of [] l.
Proof. now exists l. Qed.
Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
Proof. intros [k E]. discriminate. Qed.
Lemma prefix_of_cons x y (l1 l2 : list A) :
  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 : list A) :
  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 : list A) :
  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 : list A) :
  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 : list A) :
  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 A).
Proof.
  split.
  * intros ?. now eexists [].
  * intros ??? [k1 ?] [k2 ?].
    exists (k2 ++ k1). subst. now rewrite app_assoc.
Qed.

Lemma prefix_suffix_rev (l1 l2 : list A) :
  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 : list A) :
  suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.

Lemma suffix_of_nil (l : list A) : suffix_of [] l.
Proof. exists l. now rewrite app_nil_r. Qed.
Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) [].
Proof. intros [[] ?]; discriminate. Qed.
Lemma suffix_of_cons x y (l1 l2 : list A) :
  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 : list A) :
  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 : list A) :
  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 : list A) 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 : list A) :
  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 : list A) 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 : list A) :
  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 : list A) 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_equality. now apply suffix_of_app_r.
Qed.
Lemma suffix_of_cons_not x (l : list A) : ¬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_equality.
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 prefix_postfix.

(** The [simplify_suffix_of] removes [suffix_of] assumptions that are
tautologies, and simplifies [suffix_of] assumptions involving [(::)] and
[(++)]. *)
Ltac simplify_suffix_of := repeat
  match goal with
  | H : suffix_of (_ :: _) _ |- _ =>
    destruct (suffix_of_cons_not _ _ H)
  | H : suffix_of (_ :: _) [] |- _ =>
    destruct (suffix_of_nil_not _ _ 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_equality
  end.

(** 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 :=
  match goal with
  | _ => 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
  | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ =>
     match goal with
     | _ : suffix_of x z |- _ => fail 1
     | _ => assert (suffix_of x z) by (transitivity y; assumption);
            clear H1; clear H2; go (**i clear to avoid loops *)
     end
  end in go.
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
  unfold PropHolds; solve_suffix_of : typeclass_instances.

(** * Monadic operations *)
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).

Section list_fmap.
  Context {A B : Type} (f : A → B).

  Local Arguments fmap _ _ _ _ _ !_ /.

  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.
  Proof.
    split.
    * apply in_fmap_2.
    * intros [? [??]]. eauto using in_fmap_1_alt.
  Qed.
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.

(** * Indexed folds and maps *)
(** We define stronger variants of map and fold that also take the index of the
element into account. *)
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.

Definition ifold_right {A B} (f : nat → B → A → A)
    (a : nat → A) : nat → list B → A :=
  fix go (n : nat) (l : list B) : A :=
  match l with
  | nil => a n
  | b :: l => f n b (go (S n) l)
  end.

Lemma ifold_right_app {A B} (f : nat → B → A → A) (a : nat → A)
    (l1 l2 : list B) n :
  ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1.
Proof.
  revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.

(** * Lists of the same length *)
(** The [same_length] view allows convenient induction over two lists with the
same length. *)
Section same_length.
  Context {A B : Type}.

  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.
  Proof.
    split.
    * induction 1; simpl; auto.
    * revert k. induction l; intros [|??]; try discriminate;
      constructor; auto with arith.
  Qed.

  Lemma same_length_lookup l k i :
    same_length l k → is_Some (l !! i) → is_Some (k !! i).
  Proof.
    rewrite same_length_length.
    setoid_rewrite list_lookup_lt_length.
    intros E. now rewrite E.
  Qed.
End same_length.

(** * Zipping lists *)
(** Since we prefer Haskell style naming, we rename the standard library's
implementation [combine] into [zip] using a notation. *)
Notation zip := combine.

Section zip.
  Context {A B : Type}.

  Local Arguments fmap _ _ _ _ _ !_ /.

  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.