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

Arguments length {_} _.
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _.

Notation Forall_nil_2 := Forall_nil.
Notation Forall_cons_2 := Forall_cons.

Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
Notation take_drop := firstn_skipn.
Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

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, updating, and deleting elements of a list. *)
Instance list_lookup {A} : Lookup nat A (list A) :=
  fix go (i : nat) (l : list A) {struct l} : option A :=
  match l with
  | [] => None
  | x :: l =>
    match i with
    | 0 => Some x
    | S i => @lookup _ _ _ go i l
    end
  end.
Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
  fix go (i : nat) (l : list A) {struct l} :=
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => f x :: l
    | S i => x :: @alter _ _ _ f go i l
    end
  end.
Instance list_delete {A} : Delete nat (list A) :=
  fix go (i : nat) (l : list A) {struct l} : list A :=
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => l
    | S i => x :: @delete _ _ go i l
    end
  end.
Instance list_insert {A} : Insert nat A (list A) := λ i x,
  alter (λ _, x) i.

(** 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 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) :=
  fix go P _ l :=
  match l with
  | [] => []
  | x :: l =>
     if decide (P x)
     then x :: @filter _ _ (@go) _ _ l
     else @filter _ _ (@go) _ _ l
  end.

(** 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 :=
  match n with
  | 0 => []
  | S n => x :: replicate n x
  end.

(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].

(** 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
  | x :: l =>
    match n with
    | 0 => []
    | S n => x :: resize n y l
    end
  end.
Arguments resize {_} !_ _ !_.

(** 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. *)
Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.
Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
Definition max_prefix_of `{∀ x y : A, Decision (x = y)} :
    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 =>
     if decide_rel (=) x1 x2
     then snd_map (x1 ::) (go l1 l2)
     else (x1 :: l1, x2 :: l2, [])
  end.
Definition max_suffix_of `{∀ x y : A, Decision (x = y)} (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.

(** * Tactics on lists *)
Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
  x1 :: l1 = x2 :: l2 → x1 = x2 ∧ l1 = l2.
Proof. by injection 1. Qed.

(** The tactic [discriminate_list_equality] discharges goals containing
invalid list equalities as an assumption. *)
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
  repeat (simpl in H || rewrite app_length in H);
  exfalso; lia.
Tactic Notation "discriminate_list_equality" :=
  solve [repeat_on_hyps (fun H => discriminate_list_equality H)].

(** The tactic [simplify_list_equality] simplifies assumptions involving
equalities on lists. *)
Ltac simplify_list_equality := repeat
  match goal with
  | H : _ :: _ = _ :: _ |- _ =>
     apply cons_inv in H; destruct H
     (* to circumvent bug #2939 in some situations *)
  | H : _ ++ _ = _ ++ _ |- _ => first
     [ apply app_inj_tail in H; destruct H
     | apply app_inv_head in H
     | apply app_inv_tail in H ]
  | H : [?x] !! ?i = Some ?y |- _ =>
     destruct i; [change (Some x = Some y) in H|discriminate]
  | _ => progress simplify_equality
  | H : _ |- _ => discriminate_list_equality H
  end.

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

Global Instance: ∀ x : A, Injective (=) (=) (x ::).
Proof. by injection 1. Qed.
Global Instance: ∀ l : list A, Injective (=) (=) (:: l).
Proof. by injection 1. 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.
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.

Lemma app_inj (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 list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
  * done.
  * discriminate (H 0).
  * discriminate (H 0).
  * f_equal; [by injection (H 0) |].
    apply IHl1. intro. apply (H (S _)).
Qed.
Lemma list_eq_nil (l : list A) : (∀ i, l !! i = None) → l = nil.
Proof. intros. by apply list_eq. Qed.

Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
  Decision (l = k) := list_eq_dec dec.
Definition list_singleton_dec (l : list A) : { x | l = [x] } + { length l ≠ 1 }.
Proof.
 by refine (
  match l with
  | [x] => inleft (x ↾ _)
  | _ => inright _
  end).
Defined.

Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠ 0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length (l : list A) : length l = 0 → l = [].
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
Lemma lookup_tail (l : list A) i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.

Lemma lookup_lt_length (l : list A) i :
  is_Some (l !! i) ↔ i < length l.
Proof.
  revert i. induction l.
  * split; by inversion 1.
  * intros [|?]; simpl.
    + split; eauto with arith.
    + by rewrite <-NPeano.Nat.succ_lt_mono.
Qed.
Lemma lookup_lt_length_1 (l : list A) i :
  is_Some (l !! i) → i < length l.
Proof. apply lookup_lt_length. Qed.
Lemma lookup_lt_length_alt (l : list A) i x :
  l !! i = Some x → i < length l.
Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
Lemma lookup_lt_length_2 (l : list A) i :
  i < length l → is_Some (l !! i).
Proof. apply lookup_lt_length. Qed.

Lemma lookup_ge_length (l : list A) i :
  l !! i = None ↔ length l ≤ i.
Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
Lemma lookup_ge_length_1 (l : list A) i :
  l !! i = None → length l ≤ i.
Proof. by rewrite lookup_ge_length. Qed.
Lemma lookup_ge_length_2 (l : list A) i :
  length l ≤ i → l !! i = None.
Proof. by rewrite lookup_ge_length. Qed.

Lemma list_eq_length_eq (l1 l2 : list A) :
  length l2 = length l1 →
  (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) →
  l1 = l2.
Proof.
  intros Hlength Hlookup. apply list_eq. intros i.
  destruct (l2 !! i) as [x|] eqn:E.
  * feed inversion (lookup_lt_length_2 l1 i) as [y].
    { pose proof (lookup_lt_length_alt l2 i x E). lia. }
    f_equal. eauto.
  * rewrite lookup_ge_length in E |- *. lia.
Qed.

Lemma lookup_app_l (l1 l2 : list A) i :
  i < length l1 →
  (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_app_l_Some (l1 l2 : list A) i x :
  l1 !! i = Some x →
  (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.

Lemma lookup_app_r (l1 l2 : list A) i :
  (l1 ++ l2) !! (length l1 + i) = l2 !! i.
Proof.
  revert i.
  induction l1; intros [|i]; simpl in *; simplify_equality; auto.
Qed.
Lemma lookup_app_r_alt (l1 l2 : list A) i :
  length l1 ≤ i →
  (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply lookup_app_r.
Qed.
Lemma lookup_app_r_Some (l1 l2 : list A) i x :
  l2 !! i = Some x →
  (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
Lemma lookup_app_r_Some_alt (l1 l2 : list A) i x :
  length l1 ≤ i →
  l2 !! (i - length l1) = Some x →
  (l1 ++ l2) !! i = Some x.
Proof. intro. by rewrite lookup_app_r_alt. Qed.

Lemma lookup_app_inv (l1 l2 : list A) i x :
  (l1 ++ l2) !! i = Some x →
  l1 !! i = Some x ∨ l2 !! (i - length l1) = Some x.
Proof.
  revert i.
  induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
Qed.

Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
  (l1 ++ x :: l2) !! length l1 = Some x.
Proof. by induction l1; simpl. Qed.

Lemma alter_length (f : A → A) l i :
  length (alter f i l) = length l.
Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
Lemma insert_length (l : list A) i x :
  length (<[i:=x]>l) = length l.
Proof. apply alter_length. Qed.

Lemma list_lookup_alter (f : A → A) l i :
  alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne (f : A → A) l i j :
  i ≠ j → alter f i l !! j = l !! j.
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
Lemma list_lookup_insert (l : list A) i x :
  i < length l →
  <[i:=x]>l !! i = Some x.
Proof.
  intros Hi. unfold insert, list_insert.
  rewrite list_lookup_alter.
  by feed inversion (lookup_lt_length_2 l i).
Qed.
Lemma list_lookup_insert_ne (l : list A) i j x :
  i ≠ j → <[i:=x]>l !! j = l !! j.
Proof. apply list_lookup_alter_ne. Qed.

Lemma list_lookup_other (l : list A) i x :
  length l ≠ 1 →
  l !! i = Some x →
  ∃ j y, j ≠ i ∧ l !! j = Some y.
Proof.
  intros Hl Hi.
  destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

Lemma alter_app_l (f : A → A) (l1 l2 : list A) i :
  i < length l1 →
  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof.
  revert i.
  induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma alter_app_r (f : A → A) (l1 l2 : list A) i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
Proof.
  revert i.
  induction l1; intros [|?]; simpl in *; f_equal; auto.
Qed.
Lemma alter_app_r_alt (f : A → A) (l1 l2 : list A) i :
  length l1 ≤ i →
  alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.

Lemma insert_app_l (l1 l2 : list A) i x :
  i < length l1 →
  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. apply alter_app_l. Qed.
Lemma insert_app_r (l1 l2 : list A) i x :
  <[length l1 + i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. apply alter_app_r. Qed.
Lemma insert_app_r_alt (l1 l2 : list A) i x :
  length l1 ≤ i →
  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.

Lemma insert_consecutive_length (l : list A) i k :
  length (insert_consecutive i k l) = length l.
Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.

Lemma not_elem_of_nil (x : A) : x ∉ [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil (x : A) : x ∈ [] ↔ False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv (l : list A) : (∀ x, x ∉ l) → l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_cons (l : list A) x y :
  x ∈ y :: l ↔ x = y ∨ x ∈ l.
Proof.
  split.
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
Qed.
Lemma not_elem_of_cons (l : list A) x y :
  x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app (l1 l2 : list A) x :
  x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
Proof.
  induction l1.
  * split; [by right|]. intros [Hx|]; [|done].
    by destruct (elem_of_nil x).
  * simpl. rewrite !elem_of_cons, IHl1. tauto.
Qed.
Lemma not_elem_of_app (l1 l2 : list A) x :
  x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.

Lemma elem_of_list_singleton (x y : A) : x ∈ [y] ↔ x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.

Global Instance elem_of_list_permutation_proper (x : A) :
  Proper (Permutation ==> iff) (x ∈).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.

Lemma elem_of_list_split (l : list A) x :
  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.

Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} :
  ∀ (x : A) l, Decision (x ∈ l).
Proof.
 intros x. refine (
  fix go l :=
  match l return Decision (x ∈ l) with
  | [] => right (not_elem_of_nil _)
  | y :: l => cast_if_or (decide_rel (=) x y) (go l)
  end); clear go dec; subst; try (by constructor); by inversion 1.
Defined.

Lemma elem_of_list_lookup_1 (l : list A) x :
  x ∈ l → ∃ i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH].
  * by exists 0.
  * destruct IH as [i ?]; auto. by exists (S i).
Qed.
Lemma elem_of_list_lookup_2 (l : list A) i x :
  l !! i = Some x → x ∈ l.
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.
Lemma elem_of_list_lookup (l : list A) x :
  x ∈ l ↔ ∃ i, l !! i = Some x.
Proof.
  firstorder eauto using
    elem_of_list_lookup_1, elem_of_list_lookup_2.
Qed.

Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
Lemma NoDup_cons (x : A) l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 (x : A) l : NoDup (x :: l) → x ∉ l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 (x : A) l : NoDup (x :: l) → NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton (x : A) : NoDup [x].
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

Lemma NoDup_app (l k : list A) :
  NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
Proof.
  induction l; simpl.
  * rewrite NoDup_nil.
    setoid_rewrite elem_of_nil. naive_solver.
  * rewrite !NoDup_cons.
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
    naive_solver.
Qed.

Global Instance NoDup_proper:
  Proper (Permutation ==> iff) (@NoDup A).
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.

Lemma NoDup_Permutation (l k : list A) :
  NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → Permutation l k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
  * intros k _ Hk.
    rewrite (elem_of_nil_inv k); [done |].
    intros x. rewrite <-Hk, elem_of_nil. intros [].
  * intros k Hk Hlk.
    destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
    { rewrite <-Hlk. by constructor. }
    rewrite <-Permutation_middle, NoDup_cons in Hk.
    destruct Hk as [??].
    apply Permutation_cons_app, IH; [done |].
    intros y. specialize (Hlk y).
    rewrite <-Permutation_middle, !elem_of_cons in Hlk.
    naive_solver.
Qed.

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_2
  | x :: l =>
    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
  end.

Section remove_dups.
  Context `{!∀ x y : A, Decision (x = y)}.

  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.

  Lemma elem_of_remove_dups l x :
    x ∈ remove_dups l ↔ x ∈ l.
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_cons; intuition (simplify_equality; auto).
  Qed.

  Lemma remove_dups_nodup l : NoDup (remove_dups l).
  Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
End remove_dups.

Lemma elem_of_list_filter `{∀ x : A, Decision (P x)} l x :
  x ∈ filter P l ↔ P x ∧ x ∈ l.
Proof.
  unfold filter. induction l; simpl; repeat case_decide;
     rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
Qed.
Lemma filter_nodup P `{∀ x : A, Decision (P x)} l :
  NoDup l → NoDup (filter P l).
Proof.
  unfold filter. induction 1; simpl; repeat case_decide;
    rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.

Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_singleton (x : A) : reverse [x] = [x].
Proof. done. Qed.
Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app (l1 l2 : list A) :
  reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length (l : list A) : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 

Lemma take_nil n :
  take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app (l k : list A) :
  take (length l) (l ++ k) = l.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt (l k : list A) n :
  n = length l →
  take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le (l k : list A) n :
  n ≤ length l →
  take n (l ++ k) = take n l.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_app_ge (l k : list A) n :
  length l ≤ n →
  take n (l ++ k) = l ++ take (n - length l) k.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_ge (l : list A) n :
  length l ≤ n →
  take n l = l.
Proof.
  revert n.
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.

Lemma take_take (l : list A) n m :
  take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
Lemma take_idempotent (l : list A) n :
  take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.

Lemma take_length (l : list A) n :
  length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_alt (l : list A) n :
  n ≤ length l →
  length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.

Lemma lookup_take (l : list A) n i :
  i < n → take n l !! i = l !! i.
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
Lemma lookup_take_ge (l : list A) n i :
  n ≤ i → take n l !! i = None.
Proof.
  revert n i.
  induction l; intros [|?] [|?] ?; simpl; auto with lia.
Qed.
Lemma take_alter (f : A → A) l n i :
  n ≤ i → take n (alter f i l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  * by rewrite !lookup_take_ge.
  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert (l : list A) n i x :
  n ≤ i → take n (<[i:=x]>l) = take n l.
Proof take_alter _ _ _ _.

Lemma drop_nil n :
  drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_app (l k : list A) :
  drop (length l) (l ++ k) = k.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt (l k : list A) n :
  n = length l →
  drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length (l : list A) n :
  length (drop n l) = length l - n.
Proof.
  revert n. by induction l; intros [|i]; simpl; f_equal.
Qed.
Lemma drop_all (l : list A) :
  drop (length l) l = [].
Proof. induction l; simpl; auto. Qed.
Lemma drop_all_alt (l : list A) n :
  n = length l →
  drop n l = [].
Proof. intros. subst. by rewrite drop_all. Qed.

Lemma lookup_drop (l : list A) n i :
  drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter (f : A → A) l n i  :
  i < n → drop n (alter f i l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert (l : list A) n i x :
  i < n → drop n (<[i:=x]>l) = drop n l.
Proof drop_alter _ _ _ _.

Lemma replicate_length n (x : A) : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n (x : A) i :
  i < n →
  replicate n x !! i = Some x.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_inv n (x y : A) i :
  replicate n x !! i = Some y → y = x ∧ i < n.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma replicate_plus n m (x : A) :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

Lemma take_replicate n m (x : A) :
  take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma take_replicate_plus n m (x : A) :
  take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m (x : A) :
  drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m (x : A) :
  drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.

Lemma resize_spec (l : list A) n x :
  resize n x l = take n l ++ replicate (n - length l) x.
Proof.
  revert n.
  induction l; intros [|?]; simpl; f_equal; auto.
Qed.
Lemma resize_0 (l : list A) x :
  resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n (x : A) :
  resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge (l : list A) n x :
  length l ≤ n →
  resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le (l : list A) n x :
  n ≤ length l →
  resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
  simpl. by rewrite (right_id [] (++)).
Qed.

Lemma resize_all (l : list A) x :
  resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt (l : list A) n x :
  n = length l →
  resize n x l = l.
Proof. intros. subst. by rewrite resize_all. Qed.

Lemma resize_plus (l : list A) n m x :
  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto.
  * by rewrite plus_0_r, (right_id [] (++)).
  * by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq (l : list A) n m x :
  length l = n →
  resize (n + m) x l = l ++ replicate m x.
Proof.
  intros. subst.
  by rewrite resize_plus, resize_all, drop_all, resize_nil.
Qed.

Lemma resize_app_le (l1 l2 : list A) n x :
  n ≤ length l1 →
  resize n x (l1 ++ l2) = resize n x l1.
Proof.
  intros.
  by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
Qed.
Lemma resize_app_ge (l1 l2 : list A) n x :
  length l1 ≤ n →
  resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
  intros.
  rewrite !resize_spec, take_app_ge, (associative (++)) by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.

Lemma resize_length (l : list A) n x : length (resize n x l) = n.
Proof.
  rewrite resize_spec, app_length, replicate_length, take_length. lia.
Qed.
Lemma resize_replicate (x : A) n m :
  resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.

Lemma resize_resize (l : list A) n m x :
  n ≤ m →
  resize n x (resize m x l) = resize n x l.
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite !resize_nil, resize_replicate.
  * intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_idempotent (l : list A) n x :
  resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.

Lemma resize_take_le (l : list A) n m x :
  n ≤ m →
  resize n x (take m l) = resize n x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_take_eq (l : list A) n x :
  resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.

Lemma take_resize (l : list A) n m x :
  take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
Qed.
Lemma take_resize_le (l : list A) n m x :
  n ≤ m →
  take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_eq (l : list A) n x :
  take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_length_resize (l : list A) n x :
  length l ≤ n →
  take (length l) (resize n x l) = l.
Proof. intros. by rewrite take_resize_le, resize_all. Qed.
Lemma take_length_resize_alt (l : list A) n m x :
  m = length l →
  m ≤ n →
  take m (resize n x l) = l.
Proof. intros. subst. by apply take_length_resize. Qed.
Lemma take_resize_plus (l : list A) n m x :
  take n (resize (n + m) x l) = resize n x l.
Proof. by rewrite take_resize, min_l by lia. Qed.

Lemma drop_resize_le (l : list A) n m x :
  n ≤ m →
  drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus (l : list A) n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.

Section Forall_Exists.
  Context (P : A → Prop).

  Lemma Forall_forall l :
    Forall P l ↔ ∀ x, x ∈ l → P x.
  Proof.
    split.
    * induction 1; inversion 1; subst; auto.
    * intros Hin. induction l; constructor.
      + apply Hin. constructor.
      + apply IHl. intros ??. apply Hin. by constructor.
  Qed.

  Lemma Forall_nil : Forall P [] ↔ True.
  Proof. done. Qed.
  Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
  Lemma Forall_singleton x : Forall P [x] ↔ P x.
  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H ?]. induction H; simpl; intuition.
  Qed.
  Lemma Forall_true l : (∀ x, P x) → Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl l (Q : A → Prop) :
    Forall P l → (∀ x, P x → Q x) → Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.

  Lemma Forall_delete l i : Forall P l → Forall P (delete i l).
  Proof.
    intros H. revert i.
    by induction H; intros [|i]; try constructor.
  Qed.
  Lemma Forall_lookup l :
    Forall P l ↔ ∀ i x, l !! i = Some x → P x.
  Proof.
    rewrite Forall_forall.
    setoid_rewrite elem_of_list_lookup.
    naive_solver.
  Qed.
  Lemma Forall_lookup_1 l i x :
    Forall P l → l !! i = Some x → P x.
  Proof. rewrite Forall_lookup. eauto. Qed.
  Lemma Forall_alter f l i :
    Forall P l →
    (∀ x, l !! i = Some x → P x → P (f x)) →
    Forall P (alter f i l).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.

  Lemma Forall_replicate n x :
    P x → Forall P (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall_replicate_eq n (x : A) :
    Forall (=x) (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Exists_exists l :
    Exists P l ↔ ∃ x, x ∈ l ∧ P x.
  Proof.
    split.
    * induction 1 as [x|y ?? IH].
      + exists x. split. constructor. done.
      + destruct IH as [x [??]]. exists x. split. by constructor. done. 
    * intros [x [Hin ?]]. induction l.
      + by destruct (not_elem_of_nil x).
      + inversion Hin; subst. by left. right; auto.
  Qed.
  Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
  Proof. inversion 1; intuition trivial. Qed.
  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H|H].
      + induction H; simpl; intuition.
      + induction l1; simpl; intuition. 
  Qed.

  Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.
  Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.

  Context {dec : ∀ x, Decision (P x)}.

  Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not ∘ P) l}.
  Proof.
   refine (
    match l with
    | [] => left _
    | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
    end); clear Forall_Exists_dec; abstract intuition.
  Defined.

  Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
  Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.

  Global Instance Forall_dec l : Decision (Forall P l) :=
    match Forall_Exists_dec l with
    | left H => left H
    | right H => right (Exists_not_Forall _ H)
    end.

  Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not ∘ P) l}.
  Proof.
   refine (
    match l with
    | [] => right _
    | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
    end); clear Exists_Forall_dec; abstract intuition.
  Defined.

  Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
  Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.

  Global Instance Exists_dec l : Decision (Exists P l) :=
    match Exists_Forall_dec l with
    | left H => left H
    | right H => right (Forall_not_Exists _ H)
    end.
End Forall_Exists.
End general_properties.

Section Forall2.
  Context {A B} (P : A → B → Prop).

  Lemma Forall2_nil_inv_l k :
    Forall2 P [] k → k = [].
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_inv_r k :
    Forall2 P k [] → k = [].
  Proof. by inversion 1. Qed.

  Lemma Forall2_cons_inv l1 l2 x1 x2 :
    Forall2 P (x1 :: l1) (x2 :: l2) → P x1 x2 ∧ Forall2 P l1 l2.
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv_l l1 k x1 :
    Forall2 P (x1 :: l1) k → ∃ x2 l2,
      P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x2 :: l2.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_inv_r k l2 x2 :
    Forall2 P k (x2 :: l2) → ∃ x1 l1,
      P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x1 :: l1.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_nil_inv l1 x1 :
    Forall2 P (x1 :: l1) [] → False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_cons_inv l2 x2 :
    Forall2 P [] (x2 :: l2) → False.
  Proof. by inversion 1. Qed.