phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_relations.v *)
Instance : ∀ n, Proper (Forall2 R ==> Forall2 R) (take n).
Proof. repeat intro. eauto using Forall2_take. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ n, Proper (Forall2 R ==> Forall2 R) (drop n).
Proof. repeat intro. eauto using Forall2_drop. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ i, Proper (Forall2 R ==> option_Forall2 R) (lookup i).
Proof. repeat intro. by apply Forall2_lookup. Qed.
(* stdpp/list_relations.v *)
Instance :
    Proper ((R ==> R) ==> (=) ==> Forall2 R ==> Forall2 R) (alter (M:=list A)).
Proof. repeat intro. subst. eauto using Forall2_alter. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ i, Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
Proof. repeat intro. eauto using Forall2_insert. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ i,
    Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (list_inserts i).
Proof. repeat intro. eauto using Forall2_inserts. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ i, Proper (Forall2 R ==> Forall2 R) (delete i).
Proof. repeat intro. eauto using Forall2_delete. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (option_Forall2 R ==> Forall2 R) option_list.
Proof. repeat intro. eauto using Forall2_option_list. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ P `{∀ x, Decision (P x)},
    Proper (R ==> iff) P → Proper (Forall2 R ==> Forall2 R) (filter P).
Proof. repeat intro; eauto using Forall2_filter. Qed.
(* stdpp/list_relations.v *)
Instance : ∀ n, Proper (R ==> Forall2 R) (replicate n).
Proof. repeat intro. eauto using Forall2_replicate. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (Forall2 R ==> Forall2 R) reverse.
Proof. repeat intro. eauto using Forall2_reverse. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (Forall2 R ==> option_Forall2 R) last.
Proof. repeat intro. eauto using Forall2_last. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
    Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
    Forall3 P (l1 ++ l2) (k1 ++ k2) (k1' ++ k2').
Proof. induction 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_cons_inv_l x l k k' :
    Forall3 P (x :: l) k k' → ∃ y k2 z k2',
      k = y :: k2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l k2 k2'.
Proof. inv 1; naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_app_inv_l l1 l2 k k' :
    Forall3 P (l1 ++ l2) k k' → ∃ k1 k2 k1' k2',
     k = k1 ++ k2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
    revert k k'. induction l1 as [|x l1 IH]; simpl; inv 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_cons_inv_m l y k k' :
    Forall3 P l (y :: k) k' → ∃ x l2 z k2',
      l = x :: l2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l2 k k2'.
Proof. inv 1; naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_app_inv_m l k1 k2 k' :
    Forall3 P l (k1 ++ k2) k' → ∃ l1 l2 k1' k2',
     l = l1 ++ l2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
    revert l k'. induction k1 as [|x k1 IH]; simpl; inv 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_cons_inv_r l k z k' :
    Forall3 P l k (z :: k') → ∃ x l2 y k2,
      l = x :: l2 ∧ k = y :: k2 ∧ P x y z ∧ Forall3 P l2 k2 k'.
Proof. inv 1; naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_app_inv_r l k k1' k2' :
    Forall3 P l k (k1' ++ k2') → ∃ l1 l2 k1 k2,
      l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
    revert l k. induction k1' as [|x k1' IH]; simpl; inv 1.
    - by repeat eexists; eauto.
    - by repeat eexists; eauto.
    - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_impl (Q : A → B → C → Prop) l k k' :
    Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
Proof. intros Hl ?; induction Hl; auto. Defined.
(* stdpp/list_relations.v *)
Lemma Forall3_length_lm l k k' : Forall3 P l k k' → length l = length k.
Proof. by induction 1; f_equal/=. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_length_lr l k k' : Forall3 P l k k' → length l = length k'.
Proof. by induction 1; f_equal/=. Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_lookup_lmr l k k' i x y z :
    Forall3 P l k k' →
    l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z.
Proof.
    intros H. revert i. induction H; intros [|?] ???; simplify_eq/=; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_lookup_l l k k' i x :
    Forall3 P l k k' → l !! i = Some x →
    ∃ y z, k !! i = Some y ∧ k' !! i = Some z ∧ P x y z.
Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_lookup_m l k k' i y :
    Forall3 P l k k' → k !! i = Some y →
    ∃ x z, l !! i = Some x ∧ k' !! i = Some z ∧ P x y z.
Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_lookup_r l k k' i z :
    Forall3 P l k k' → k' !! i = Some z →
    ∃ x y, l !! i = Some x ∧ k !! i = Some y ∧ P x y z.
Proof.
    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall3_alter_lm f g l k k' i :
    Forall3 P l k k' →
    (∀ x y z, l !! i = Some x → k !! i = Some y → k' !! i = Some z →
      P x y z → P (f x) (g y) z) →
    Forall3 P (alter f i l) (alter g i k) k'.
Proof. intros Hl. revert i. induction Hl; intros [|]; auto. Qed.
(* stdpp/list_relations.v *)
Instance list_subseteq_po : PreOrder (⊆@{list A}).
Proof. split; firstorder. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_nil l : [] ⊆ l.
Proof. intros x. by rewrite elem_of_nil. Qed.
(* stdpp/list_relations.v *)
Lemma list_nil_subseteq l : l ⊆ [] → l = [].
Proof.
  intro Hl. destruct l as [|x l1]; [done|]. exfalso.
  rewrite <-(elem_of_nil x).
  apply Hl, elem_of_cons. by left.
Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_skip x l1 l2 : l1 ⊆ l2 → x :: l1 ⊆ x :: l2.
Proof.
  intros Hin y Hy%elem_of_cons.
  destruct Hy as [-> | Hy]; [by left|]. right. by apply Hin.
Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_cons x l1 l2 : l1 ⊆ l2 → l1 ⊆ x :: l2.
Proof. intros Hin y Hy. right. by apply Hin. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_app_l l1 l2 l : l1 ⊆ l2 → l1 ⊆ l2 ++ l.
Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_app_r l1 l2 l : l1 ⊆ l2 → l1 ⊆ l ++ l2.
Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_app_iff_l l1 l2 l :
  l1 ++ l2 ⊆ l ↔ l1 ⊆ l ∧ l2 ⊆ l.
Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_cons_iff x l1 l2 :
  x :: l1 ⊆ l2 ↔ x ∈ l2 ∧ l1 ⊆ l2.
Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_cons. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_delete i l : delete i l ⊆ l.
Proof. apply sublist_subseteq, sublist_delete. Qed.
(* stdpp/list_relations.v *)
Lemma list_subseteq_filter P `{!∀ x : A, Decision (P x)} l : filter P l ⊆ l.
Proof. apply sublist_subseteq. apply sublist_filter. Qed.
(* stdpp/list_relations.v *)
Lemma subseteq_drop n l : drop n l ⊆ l.
Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_r. done. Qed.
(* stdpp/list_relations.v *)
Lemma subseteq_take n l : take n l ⊆ l.
Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_l. done. Qed.
(* stdpp/list_relations.v *)
Instance list_subseteq_Permutation:
  Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
Proof.
  intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk.
Qed.
(* stdpp/list_relations.v *)
Instance list_subseteq_dec `{!EqDecision A} : RelDecision (⊆@{list A}) :=
  λ xs ys, cast_if (decide (Forall (λ x, x ∈ ys) xs)).
Next Obligation. intros ???. by rewrite Forall_forall. Qed.
(* stdpp/list_relations.v *)
Lemma list_equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
Proof. split; induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma list_equiv_lookup l k : l ≡ k ↔ ∀ i, l !! i ≡ k !! i.
Proof.
    rewrite list_equiv_Forall2, Forall2_lookup.
    by setoid_rewrite option_equiv_Forall2.
  Qed.
(* stdpp/list_relations.v *)
Instance list_equivalence :
    Equivalence (≡@{A}) → Equivalence (≡@{list A}).
Proof.
    split.
    - intros l. by apply list_equiv_Forall2.
    - intros l k; rewrite !list_equiv_Forall2; by intros.
    - intros l1 l2 l3; rewrite !list_equiv_Forall2; intros; by trans l2.
  Qed.
(* stdpp/list_relations.v *)
Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
(* stdpp/list_relations.v *)
Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) cons.
Proof. by constructor. Qed.
(* stdpp/list_relations.v *)
Instance app_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) app.
Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance length_proper : Proper ((≡@{list A}) ==> (=)) length.
Proof. induction 1; f_equal/=; auto. Qed.
(* stdpp/list_relations.v *)
Instance tail_proper : Proper ((≡@{list A}) ==> (≡)) tail.
Proof. destruct 1; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance take_proper n : Proper ((≡@{list A}) ==> (≡)) (take n).
Proof. induction n; destruct 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance drop_proper n : Proper ((≡@{list A}) ==> (≡)) (drop n).
Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance list_lookup_total_proper `{!Inhabited A} i :
    Proper (≡@{A}) inhabitant →
    Proper ((≡@{list A}) ==> (≡)) (lookup_total i).
Proof. intros ?. induction i; destruct 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Instance list_alter_proper :
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{list A})) alter.
Proof.
    intros f1 f2 Hf i ? <-. induction i; destruct 1; constructor; eauto.
  Qed.
(* stdpp/list_relations.v *)
Instance list_insert_proper i :
    Proper ((≡) ==> (≡) ==> (≡@{list A})) (insert i).
Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
(* stdpp/list_relations.v *)
Instance list_inserts_proper i :
    Proper ((≡) ==> (≡) ==> (≡@{list A})) (list_inserts i).
Proof.
    intros k1 k2 Hk; revert i.
    induction Hk; intros ????; simpl; try f_equiv; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Instance list_delete_proper i :
    Proper ((≡) ==> (≡@{list A})) (delete i).
Proof. induction i; destruct 1; try constructor; eauto. Qed.
(* stdpp/list_relations.v *)
Instance option_list_proper : Proper ((≡) ==> (≡@{list A})) option_list.
Proof. destruct 1; repeat constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance list_filter_proper P `{∀ x, Decision (P x)} :
    Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡@{list A})) (filter P).
Proof. intros ???. rewrite !list_equiv_Forall2. by apply Forall2_filter. Qed.
(* stdpp/list_relations.v *)
Instance replicate_proper n : Proper ((≡@{A}) ==> (≡)) (replicate n).
Proof. induction n; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance reverse_proper : Proper ((≡) ==> (≡@{list A})) reverse.
Proof.
    induction 1; rewrite ?reverse_cons; simpl; [constructor|].
    apply app_proper; repeat constructor; auto.
  Qed.
(* stdpp/list_relations.v *)
Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance cons_equiv_inj : Inj2 (≡) (≡) (≡) (@cons A).
Proof. inv 1; auto. Qed.
(* stdpp/list_relations.v *)
Lemma nil_equiv_eq l : l ≡ [] ↔ l = [].
Proof. split; [by inv 1|intros ->; constructor]. Qed.
(* stdpp/list_relations.v *)
Lemma cons_equiv_eq l x k : l ≡ x :: k ↔ ∃ x' k', l = x' :: k' ∧ x' ≡ x ∧ k' ≡ k.
Proof. split; [inv 1; naive_solver|naive_solver (by constructor)]. Qed.
(* stdpp/list_relations.v *)
Lemma list_singleton_equiv_eq l x : l ≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡ x.
Proof. rewrite cons_equiv_eq. setoid_rewrite nil_equiv_eq. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma app_equiv_eq l k1 k2 :
    l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
Proof.
    split; [|intros (?&?&->&?&?); by f_equiv].
    setoid_rewrite list_equiv_Forall2. rewrite Forall2_app_inv_r. naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma equiv_Permutation l1 l2 l3 :
    l1 ≡ l2 → l2 ≡ₚ l3 → ∃ l2', l1 ≡ₚ l2' ∧ l2' ≡ l3.
Proof.
    intros Hequiv Hperm. revert l1 Hequiv.
    induction Hperm as [|x l2 l3 _ IH|x y l2|l2 l3 l4 _ IH1 _ IH2]; intros l1.
    - intros ?. by exists l1.
    - intros (x'&l2'&->&?&(l2''&?&?)%IH)%cons_equiv_eq.
      exists (x' :: l2''). by repeat constructor.
    - intros (y'&?&->&?&(x'&l2'&->&?&?)%cons_equiv_eq)%cons_equiv_eq.
      exists (x' :: y' :: l2'). by repeat constructor.
    - intros (l2'&?&(l3'&?&?)%IH2)%IH1. exists l3'. split; [by etrans|done].
  Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_equiv `{!Equivalence (≡@{A})} l1 l2 l3 :
    l1 ≡ₚ l2 → l2 ≡ l3 → ∃ l2', l1 ≡ l2' ∧ l2' ≡ₚ l3.
Proof.
    intros Hperm%symmetry Hequiv%symmetry.
    destruct (equiv_Permutation _ _  _ Hequiv Hperm) as (l2'&?&?).
    by exists l2'.
  Qed.
(* stdpp/list_relations.v *)
Lemma TCForall_Forall {A} (P : A → Prop) xs : TCForall P xs ↔ Forall P xs.
Proof. split; induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance TCForall_app {A} (P : A → Prop) xs ys :
  TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
(* stdpp/list_relations.v *)
Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys :
  TCForall2 P xs ys ↔ Forall2 P xs ys.
Proof. split; induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma TCExists_Exists {A} (P : A → Prop) l : TCExists P l ↔ Exists P l.
Proof. split; induction 1; constructor; solve [auto]. Qed.
(* stdpp/list_tactics.v *)
(* We define a simple data structure [rlist] to capture a syntactic
representation of lists consisting of constants, applications and the nil list.
Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *)
Inductive rlist (A : Type)
:=
  rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
(* stdpp/list_tactics.v *)
Fixpoint to_list {A} (t : rlist A) : list A
:=
  match t with
  | rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
  end.
(* stdpp/list_tactics.v *)
Notation env A
:= (list (list A)) (only parsing).
(* stdpp/list_tactics.v *)
Definition eval {A} (E : env A) : rlist nat → list A
:=
  fix go t :=
  match t with
  | rnil => []
  | rnode i => default [] (E !! i)
  | rapp t1 t2 => go t1 ++ go t2
  end.
(* stdpp/list_tactics.v *)
Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat)
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_lookup_end x : QuoteLookup [] [x] x 0
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_lookup_further E1 E2 x i y :
    QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000
:= {}.
(* stdpp/list_tactics.v *)
Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat)
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_nil E1 : Quote E1 E1 [] rnil
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_node E1 E2 l i:
    QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_cons E1 E2 E3 x l i t :
    QuoteLookup E1 E2 [x] i →
    Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t)
:= {}.
(* stdpp/list_tactics.v *)
Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
    Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2)
:= {}.
(* stdpp/list_tactics.v *)
Lemma eval_alt t : eval E t = to_list t ≫= default [] ∘ (E !!.).
Proof.
    induction t; csimpl.
    - done.
    - by rewrite (right_id_L [] (++)).
    - rewrite bind_app. by f_equal.
  Qed.
(* stdpp/list_tactics.v *)
Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
(* stdpp/list_tactics.v *)
Lemma eval_Permutation t1 t2 :
    to_list t1 ≡ₚ to_list t2 → eval E t1 ≡ₚ eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
(* stdpp/list_tactics.v *)
Lemma eval_submseteq t1 t2 :
    to_list t1 ⊆+ to_list t2 → eval E t1 ⊆+ eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
(* stdpp/list_tactics.v *)
(* * Tactics *)
Ltac quote_Permutation
:=
  match goal with
  | |- ?l1 ≡ₚ ?l2 =>
    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
      change (rlist.eval E3 t1 ≡ₚ rlist.eval E3 t2)
    end end
  end.
(* stdpp/list_tactics.v *)
Ltac solve_Permutation
:=
  quote_Permutation; apply rlist.eval_Permutation;
  compute_done.
(* stdpp/list_tactics.v *)
Ltac quote_submseteq
:=
  match goal with
  | |- ?l1 ⊆+ ?l2 =>
    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
      change (rlist.eval E3 t1 ⊆+ rlist.eval E3 t2)
    end end
  end.
(* stdpp/list_tactics.v *)
Ltac solve_submseteq
:=
  quote_submseteq; apply rlist.eval_submseteq;
  compute_done.
(* stdpp/list_tactics.v *)
Ltac decompose_list_elem_of
:= repeat
  match goal with
  | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
  | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
  | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
  end.
(* stdpp/list_tactics.v *)
Ltac solve_length
:=
  simplify_eq/=;
  repeat (rewrite length_fmap || rewrite length_app);
  repeat match goal with
  | H : _ =@{list _} _ |- _ => apply (f_equal length) in H
  | H : Forall2 _ _ _ |- _ => apply Forall2_length in H
  | H : context[length (_ <$> _)] |- _ => rewrite length_fmap in H
  end; done || congruence.
(* stdpp/list_tactics.v *)
Ltac simplify_list_eq :
:= repeat
  match goal with
  | _ => progress simplify_eq/=
  | H : [?x] !! ?i = Some ?y |- _ =>
    destruct i; [change (Some x = Some y) in H | discriminate]
  | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
  | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
  | H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
  | H : [] = zip_with _ _ _ |- _ => symmetry in H
  | |- context [(_ ++ _) ++ _] => rewrite <-(assoc_L (++))
  | H : context [(_ ++ _) ++ _] |- _ => rewrite <-(assoc_L (++)) in H
  | H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
  | |- context [_ <$> (_ ++ _)]  => rewrite fmap_app
  | |- context [_ ++ []] => rewrite (right_id_L [] (++))
  | H : context [_ ++ []] |- _ => rewrite (right_id_L [] (++)) in H
  | |- context [take _ (_ <$> _)] => rewrite <-fmap_take
  | H : context [take _ (_ <$> _)] |- _ => rewrite <-fmap_take in H
  | |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
  | H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
  | H : _ ++ _ = _ ++ _ |- _ =>
    repeat (rewrite <-app_comm_cons in H || rewrite <-(assoc_L (++)) in H);
    apply app_inj_1 in H; [destruct H|solve_length]
  | H : _ ++ _ = _ ++ _ |- _ =>
    repeat (rewrite app_comm_cons in H || rewrite (assoc_L (++)) in H);
    apply app_inj_2 in H; [destruct H|solve_length]
  | |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
    rewrite zip_with_app by solve_length
  | |- context [take _ (_ ++ _)] => rewrite take_app_length' by solve_length
  | |- context [drop _ (_ ++ _)] => rewrite drop_app_length' by solve_length
  | H : context [zip_with _ (_ ++ _) (_ ++ _)] |- _ =>
    rewrite zip_with_app in H by solve_length
  | H : context [take _ (_ ++ _)] |- _ =>
    rewrite take_app_length' in H by solve_length
  | H : context [drop _ (_ ++ _)] |- _ =>
    rewrite drop_app_length' in H by solve_length
  | H : ?l !! ?i = _, H2 : context [(_ <$> ?l) !! ?i] |- _ =>
     rewrite list_lookup_fmap, H in H2
  end.
(* stdpp/list_tactics.v *)
Ltac list_simplifier
:=
  simplify_eq/=;
  repeat match goal with
  | _ => progress decompose_Forall_hyps
  | _ => progress simplify_list_eq
  | H : _ <$> _ = _ :: _ |- _ =>
    apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
  | H : _ <$> _ = _ ++ _ |- _ =>
    apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
  | H : zip_with _ _ _ = _ :: _ |- _ =>
    apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
  | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
  | H : zip_with _ _ _ = _ ++ _ |- _ =>
    apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?&?)
  | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
  end.
(* stdpp/list_tactics.v *)
Ltac decompose_Forall
:= repeat
  match goal with
  | |- Forall _ _ => by apply Forall_true
  | |- Forall _ [] => constructor
  | |- Forall _ (_ :: _) => constructor
  | |- Forall _ (_ ++ _) => apply Forall_app_2
  | |- Forall _ (_ <$> _) => apply Forall_fmap
  | |- Forall _ (_ ≫= _) => apply Forall_bind
  | |- Forall2 _ _ _ => apply Forall_Forall2_diag
  | |- Forall2 _ [] [] => constructor
  | |- Forall2 _ (_ :: _) (_ :: _) => constructor
  | |- Forall2 _ (_ ++ _) (_ ++ _) => first
    [ apply Forall2_app; [by decompose_Forall |]
    | apply Forall2_app; [| by decompose_Forall]]
  | |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
  | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
  | _ => progress decompose_Forall_hyps
  | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
  | H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
  | |- Forall _ _ =>
    apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
  | |- Forall2 _ _ _ =>
    apply Forall2_same_length_lookup_2; [solve_length|];
    intros ?????; progress decompose_Forall_hyps
  end.
(* stdpp/list_tactics.v *)
(* The [simplify_suffix] tactic removes [suffix] hypotheses that are
tautologies, and simplifies [suffix] hypotheses involving [(::)] and
[(++)]. *)
Ltac simplify_suffix
:= repeat
  match goal with
  | H : suffix (_ :: _) _ |- _ => destruct (suffix_cons_not _ _ H)
  | H : suffix (_ :: _) [] |- _ => apply suffix_nil_inv in H
  | H : suffix (_ ++ _) (_ ++ _) |- _ => apply suffix_app_inv in H
  | H : suffix (_ :: _) (_ :: _) |- _ =>
    destruct (suffix_cons_inv _ _ _ _ H); clear H
  | H : suffix ?x ?x |- _ => clear H
  | H : suffix ?x (_ :: ?x) |- _ => clear H
  | H : suffix ?x (_ ++ ?x) |- _ => clear H
  | _ => progress simplify_eq/=
  end.
(* stdpp/list_tactics.v *)
(* The [solve_suffix] tactic tries to solve goals involving [suffix]. It
uses [simplify_suffix] to simplify hypotheses and tries to solve [suffix]
conclusions. This tactic either fails or proves the goal. *)
Ltac solve_suffix
:= by intuition (repeat
  match goal with
  | _ => done
  | _ => progress simplify_suffix
  | |- suffix [] _ => apply suffix_nil
  | |- suffix _ _ => reflexivity
  | |- suffix _ (_ :: _) => apply suffix_cons_r
  | |- suffix _ (_ ++ _) => apply suffix_app_r
  | H : suffix _ _ → False |- _ => destruct H
  end).
(* stdpp/mapset.v *)
(* Given a type of maps [M : Type → Type], we construct sets as [M ()], i.e.,
maps with unit values. To avoid unnecessary universe constraints, we first
define [mapset' Munit] with [Munit : Type] as a record, and then [mapset M] with
[M : Type → Type] as a notation. See [tests/universes.v] for a test case that
fails otherwise. *)
Record mapset' (Munit : Type) : Type
:=
  Mapset { mapset_car: Munit }.
(* stdpp/mapset.v *)
Notation mapset M
:= (mapset' (M unit)).
(* stdpp/mapset.v *)
Instance mapset_elem_of: ElemOf K (mapset M)
:= λ x X,
  mapset_car X !! x = Some ().
(* stdpp/mapset.v *)
Instance mapset_empty: Empty (mapset M)
:= Mapset ∅.
(* stdpp/mapset.v *)
Instance mapset_singleton: Singleton K (mapset M)
:= λ x,
  Mapset {[ x := () ]}.