phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/tactics.v *)
(* Turn all leading ∀ and → of [p] into evars (∀-evars will be shelved), and
call [tac] with the term applied with those evars. This fill unfold definitions
to find leading ∀/→.
The type of [p] will be normalized by calling the [normalizer] function.

[_name_guard] is an unused argument where you can pass anything you want. If the
argument is an intro pattern, those will be taken into account by the [fresh]
that is inside this tactic, avoiding name collisions that can otherwise arise.
This is a work-around for https://github.com/coq/coq/issues/18109. *)
Ltac evar_foralls p _name_guard normalizer tac
:=
  let T := type of p in
  lazymatch normalizer T with
  | ?T1 → ?T2 =>
    (* This is the [fresh] where the presence of [_name_guard] matters.
    Note that the "opose_internal" is nice but not sufficient because
    it gets ignored when name mangling is enabled. *)
    let pT1 := fresh "__evar_foralls_internal" in
    assert T1 as pT1; [| evar_foralls (p pT1) _name_guard normalizer tac; clear pT1]
  | ∀ x : ?T1, _ =>
    let e := mk_evar T1 in
    evar_foralls (p e) _name_guard normalizer tac
  | ?T1 => tac p
  end.
(* stdpp/tactics.v *)
Ltac opose_specialize_foralls_core p _name_guard tac
:=
  opose_core p ltac:(fun p =>
    evar_foralls p _name_guard ltac:(fun t => eval hnf in t) tac).
(* stdpp/tactics.v *)
(* Helper for [ospecialize]: call [tac] with the name of the head term *if*
that term is a variable.

Written in CPS to get around weird thunking limitations. *)
Ltac ospecialize_ident_head_of t tac
:=
  let h := get_head t in
  tryif is_var h then tac h else
    fail "ospecialize can only specialize a local hypothesis;"
         "use opose proof instead".
(* stdpp/tactics.v *)
(* The block definitions are taken from [Coq.Program.Equality] and can be used
by tactics to separate their goal from hypotheses they generalize over. *)
Definition block {A : Type} (a : A)
:= a.
(* stdpp/tactics.v *)
Ltac block_goal
:= match goal with [ |- ?T ] => change (block T) end.
(* stdpp/tactics.v *)
Ltac unblock_goal
:= unfold block in *.
(* stdpp/tactics.v *)
(* The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
By closed we mean that [t] does not depend on any variable bound in the context.
axioms are considered closed terms by this tactic (but Section
variables are not). A function application is considered closed if the
function and the argument are closed, without considering the body of
the function (or whether it is opaque or not). This tactic is useful
for example to decide whether to call [vm_compute] on [t].

This trick was originally suggested by Jason Gross:
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Check.20that.20a.20term.20is.20closed.20in.20Ltac/near/240885618 *)
Ltac is_closed_term t
:=
  first [
      (** We use the [assert_succeeds] sandbox to be able to freely
      change the context. *)
      assert_succeeds (
          (** Make sure that the goal only contains [t]. (We use
          [const False t] instead of [let x := t in False] as the
          let-binding in the latter would be unfolded by the [unfold]
          later.) *)
          exfalso; change_no_check (const False t);
          (** Clear all hypotheses. *)
          repeat match goal with H : _ |- _ => try unfold H in *; clear H end;
          (** If there are still hypotheses left, [t] is not closed. *)
          lazymatch goal with H : _ |- _ => fail | _ => idtac end
        ) |
      fail 1 "The term" t "is not closed"
    ].
(* stdpp/tactics.v *)
(* Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on sets. The [naive_solver] tactic implements an
ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
mechanism. The tactic suffers from the following limitations:
- It might leave unresolved evars as Ltac provides no way to detect that.
- To avoid the tactic becoming too slow, we allow a universally quantified
  hypothesis to be instantiated only once during each search path.
- It does not perform backtracking on instantiation of universally quantified
  assumptions.

We use a counter to make the search breath first. Breath first search ensures
that a minimal number of hypotheses is instantiated, and thus reduced the
posibility that an evar remains unresolved.

Despite these limitations, it works much better than Coq's [firstorder] tactic
for the purposes of this development. This tactic either fails or proves the
goal. *)
Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
  (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
Proof. firstorder. Qed.
(* stdpp/telescopes.v *)
(* Telescopes *)
Inductive tele : Type
:=
  | TeleO : tele
  | TeleS {X} (binder : X → tele) : tele.
(* stdpp/telescopes.v *)
(* The telescope version of Coq's function type *)
Fixpoint tele_fun (TT : tele) (T : Type) : Type
:=
  match TT with
  | TeleO => T
  | TeleS b => ∀ x, tele_fun (b x) T
  end.
(* stdpp/telescopes.v *)
Notation "TT -t> A"
:=
  (tele_fun TT A) (at level 99, A at level 200, right associativity).
(* stdpp/telescopes.v *)
(* An eliminator for elements of [tele_fun].
    We use a [fix] because, for some reason, that makes stuff print nicer
    in the proofs in iris:bi/lib/telescopes.v *)
Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y)
  : (TT -t> X) → Y
:=
  (fix rec {TT} : (TT -t> X) → Y :=
     match TT as TT return (TT -t> X) → Y with
     | TeleO => λ x : X, base x
     | TeleS b => λ f, step (λ x, rec (f x))
     end) TT.
(* stdpp/telescopes.v *)
(* A duplication of the type [sigT] to avoid any connection to other universes *)
Record tele_arg_cons {X : Type} (f : X → Type) : Type
:= TeleArgCons
  { tele_arg_head : X;
    tele_arg_tail : f tele_arg_head }.
(* stdpp/telescopes.v *)
(* A sigma-like type for an "element" of a telescope, i.e. the data it
  takes to get a [T] from a [TT -t> T]. *)
Fixpoint tele_arg@{u} (t : tele@{u}) : Type@{u}
:=
  match t with
  | TeleO => unit
  | TeleS f => tele_arg_cons (λ x, tele_arg (f x))
  end.
(* stdpp/telescopes.v *)
(* The cast in the notation below is necessary to make Coq understand that
   [TargO] can be unified with [tele_arg TeleO]. *)
Notation TargO
:= (tt : tele_arg TeleO) (only parsing).
(* stdpp/telescopes.v *)
(* The casts and annotations are necessary for Coq to typecheck nested [TargS]
   as well as the final [TargO] in a chain of [TargS]. *)
Notation TargS a b
:=
  ((@TeleArgCons _ (λ x, tele_arg (_ x)) a b) : (tele_arg (TeleS _))) (only parsing).
(* stdpp/telescopes.v *)
Coercion tele_arg : tele >-> Sortclass.
(* stdpp/telescopes.v *)
Lemma tele_arg_ind (P : ∀ TT, tele_arg TT → Prop) :
  P TeleO TargO →
  (∀ T (b : T → tele) x xs, P (b x) xs → P (TeleS b) (TargS x xs)) →
  ∀ TT (xs : tele_arg TT), P TT xs.
Proof.
  intros H0 HS TT. induction TT as [|T b IH]; simpl.
  - by intros [].
  - intros [x xs]. by apply HS.
Qed.
(* stdpp/telescopes.v *)
Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> TT → U
:=
  match TT as TT return (TT -t> U) -> TT → U with
  | TeleO => λ F _, F
  | TeleS r => λ (F : TeleS r -t> U) '(TeleArgCons x b),
      tele_app (F x) b
  end.
(* stdpp/telescopes.v *)
(* This is a local coercion because otherwise, the "λ.." notation stops working. *)
Coercion tele_app : tele_fun >-> Funclass.
(* stdpp/telescopes.v *)
(* Inversion lemma for [tele_arg] *)
Lemma tele_arg_inv {TT : tele} (a : tele_arg TT) :
  match TT as TT return tele_arg TT → Prop with
  | TeleO => λ a, a = TargO
  | TeleS f => λ a, ∃ x a', a = TargS x a'
  end a.
Proof. destruct TT; destruct a; eauto. Qed.
(* stdpp/telescopes.v *)
Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
Proof. exact (tele_arg_inv a). Qed.
(* stdpp/telescopes.v *)
Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
  ∃ x a', a = TargS x a'.
Proof. exact (tele_arg_inv a). Qed.
(* stdpp/telescopes.v *)
(* Map below a tele_fun *)
Fixpoint tele_map {T U} {TT : tele} : (T → U) → (TT -t> T) → TT -t> U
:=
  match TT as TT return (T → U) → (TT -t> T) → TT -t> U with
  | TeleO => λ F : T → U, F
  | @TeleS X b => λ (F : T → U) (f : TeleS b -t> T) (x : X),
                  tele_map F (f x)
  end.
(* stdpp/telescopes.v *)
Lemma tele_map_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) :
  (tele_map F t) x = F (t x).
Proof.
  induction TT as [|X f IH]; simpl in *.
  - rewrite (tele_arg_O_inv x). done.
  - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl.
    rewrite <-IH. done.
Qed.
(* stdpp/telescopes.v *)
Instance tele_fmap {TT : tele} : FMap (tele_fun TT)
:= λ T U, tele_map.
(* stdpp/telescopes.v *)
Lemma tele_fmap_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) :
  (F <$> t) x = F (t x).
Proof. apply tele_map_app. Qed.
(* stdpp/telescopes.v *)
(* Operate below [tele_fun]s with argument telescope [TT]. *)
Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U
:=
  match TT as TT return (TT → U) → TT -t> U with
  | TeleO => λ F, F tt
  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
      tele_bind (λ a, F (TargS x a))
  end.
(* stdpp/telescopes.v *)
(* Show that tele_app ∘ tele_bind is the identity. *)
Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
  (tele_bind f) x = f x.
Proof.
  induction TT as [|X b IH]; simpl in *.
  - rewrite (tele_arg_O_inv x). done.
  - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl.
    rewrite IH. done.
Qed.
(* stdpp/telescopes.v *)
(* We can define the identity function and composition of the [-t>] function
space. *)
Definition tele_fun_id {TT : tele} : TT -t> TT
:= tele_bind id.
(* stdpp/telescopes.v *)
Lemma tele_fun_id_eq {TT : tele} (x : TT) :
  tele_fun_id x = x.
Proof. unfold tele_fun_id. rewrite tele_app_bind. done. Qed.
(* stdpp/telescopes.v *)
Definition tele_fun_compose {TT1 TT2 TT3 : tele} :
  (TT2 -t> TT3) → (TT1 -t> TT2) → (TT1 -t> TT3)
:=
  λ t1 t2, tele_bind (compose (tele_app t1) (tele_app t2)).
(* stdpp/telescopes.v *)
Lemma tele_fun_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x :
  tele_fun_compose f g $ x = (f ∘ g) x.
Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
(* stdpp/telescopes.v *)
(* Notation *)
Notation "'[tele' x .. z ]"
:=
  (TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))
  (x binder, z binder, format "[tele  '[hv' x  ..  z ']' ]").
(* stdpp/telescopes.v *)
Notation "'[tele' ]"
:= (TeleO)
  (format "[tele ]").
(* stdpp/telescopes.v *)
Notation "'[tele_arg' x ; .. ; z ]"
:=
  (TargS x ( .. (TargS z TargO) ..))
  (format "[tele_arg  '[hv' x ;  .. ;  z ']' ]").
(* stdpp/telescopes.v *)
Notation "'[tele_arg' ]"
:= (TargO)
  (format "[tele_arg ]").
(* stdpp/telescopes.v *)
(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
   binder so that, after simplifying, this matches the way we typically write
   notations involving telescopes. *)
Notation "'λ..' x .. y , e"
:=
  (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
  (at level 200, x binder, y binder, right associativity,
   format "'[  ' 'λ..'  x  ..  y ']' ,  e") : stdpp_scope.
(* stdpp/telescopes.v *)
(* Telescopic quantifiers *)
Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop
:=
  tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ).
(* stdpp/telescopes.v *)
Definition texist {TT : tele} (Ψ : TT → Prop) : Prop
:=
  tele_fold ex (λ x, x) (tele_bind Ψ).
(* stdpp/telescopes.v *)
Notation "'∀..' x .. y , P"
:= (tforall (λ x, .. (tforall (λ y, P)) .. ))
  (at level 200, x binder, y binder, right associativity,
  format "∀..  x  ..  y ,  P") : stdpp_scope.
(* stdpp/telescopes.v *)
Notation "'∃..' x .. y , P"
:= (texist (λ x, .. (texist (λ y, P)) .. ))
  (at level 200, x binder, y binder, right associativity,
  format "∃..  x  ..  y ,  P") : stdpp_scope.
(* stdpp/telescopes.v *)
Lemma tforall_forall {TT : tele} (Ψ : TT → Prop) :
  tforall Ψ ↔ (∀ x, Ψ x).
Proof.
  symmetry. unfold tforall. induction TT as [|X ft IH].
  - simpl. split.
    + done.
    + intros ? p. rewrite (tele_arg_O_inv p). done.
  - simpl. split; intros Hx a.
    + rewrite <-IH. done.
    + destruct (tele_arg_S_inv a) as [x [pf ->]].
      revert pf. setoid_rewrite IH. done.
Qed.
(* stdpp/telescopes.v *)
Lemma texist_exist {TT : tele} (Ψ : TT → Prop) :
  texist Ψ ↔ ex Ψ.
Proof.
  symmetry. induction TT as [|X ft IH].
  - simpl. split.
    + intros [p Hp]. rewrite (tele_arg_O_inv p) in Hp. done.
    + intros. by exists TargO.
  - simpl. split; intros [p Hp]; revert Hp.
    + destruct (tele_arg_S_inv p) as [x [pf ->]]. intros ?.
      exists x. rewrite <-(IH x (λ a, Ψ (TargS x a))). eauto.
    + rewrite <-(IH p (λ a, Ψ (TargS p a))).
      intros [??]. eauto.
Qed.
(* stdpp/topGset.v *)
Inductive topGset `{Countable A}
:=
  | FinGSet (X : gset A)
  | TopGSet.
(* stdpp/topGset.v *)
Instance topGset_eq_dec `{Countable A} : EqDecision (topGset A).
Proof. solve_decision. Defined.
(* stdpp/topGset.v *)
Instance topGset_countable `{Countable A} : Countable (topGset A).
Proof.
  apply (inj_countable'
    (λ X, match X with FinGSet X => Some X | TopGSet => None end)
    (λ s, match s with Some X => FinGSet X | None => TopGSet end)).
  by intros [].
Qed.
(* stdpp/topGset.v *)
Instance topGset_elem_of : ElemOf A (topGset A)
:= λ x X,
    match X with FinGSet X => x ∈ X | TopGSet => True end.
(* stdpp/topGset.v *)
Instance topGset_empty : Empty (topGset A)
:= FinGSet ∅.
(* stdpp/topGset.v *)
Instance topGset_top : Top (topGset A)
:= TopGSet.
(* stdpp/topGset.v *)
Instance topGset_singleton : Singleton A (topGset A)
:= λ x,
    FinGSet {[x]}.
(* stdpp/topGset.v *)
Instance topGset_union : Union (topGset A)
:= λ X Y,
    match X, Y with
    | FinGSet X, FinGSet Y => FinGSet (X ∪ Y)
    | _, _ => TopGSet
    end.
(* stdpp/topGset.v *)
Instance topGset_set : SemiSet A (topGset A).
Proof.
    split.
    - by intros ??.
    - intros x y. unfold elem_of, topGset_elem_of; simpl.
      by rewrite elem_of_singleton.
    - intros [X|] [Y|] x; unfold elem_of, topGset_elem_of, topGset_union;
        naive_solver set_solver.
  Qed.
(* stdpp/topGset.v *)
Instance topGset_top_set : TopSet A (topGset A).
Proof. by split. Qed.
(* stdpp/topGset.v *)
Instance topGset_elem_of_dec `{Countable A} : RelDecision (∈@{topGset A})
:=
  λ x X,
  match X with
  | FinGSet X => decide_rel elem_of x X
  | TopGSet => left I
  end.
(* stdpp/topGset.v *)
(* [topGset A] is only [LeibnizEquiv] for infinite [A], as, for example for
  [unit], [FinGSet {[ tt ]}] and [TopGSet] are equivalent ([≡]), but not equal
  ([=]). *)
Instance topGset_leibniz : LeibnizEquiv (topGset A).
Proof.
    intros [X|] [Y|]; rewrite set_equiv;
    unfold elem_of, topGset_elem_of; simpl; intros HXY.
    - f_equal. by apply leibniz_equiv.
    - destruct (exist_fresh X) as [? ?]; naive_solver.
    - destruct (exist_fresh Y) as [? ?]; naive_solver.
    - done.
  Qed.
(* stdpp/topGset.v *)
Instance topGset_equiv_dec : RelDecision (≡@{topGset A}).
Proof.
    refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
  Defined.
(* stdpp/topGset.v *)
(* We need [Inhabited A] to conclude that [TopGSet] is not disjoint from
  itself. *)
Instance topGset_disjoint_dec `{Inhabited A} :
      RelDecision (##@{topGset A}) := λ X Y,
    match X, Y return _ with
    | FinGSet X, FinGSet Y => cast_if (decide (X ## Y))
    | FinGSet X, TopGSet => cast_if (decide (X = ∅))
    | TopGSet, FinGSet Y => cast_if (decide (Y = ∅))
    | TopGSet, TopGSet => right _
    end.
Next Obligation. done. Qed.
(* stdpp/topGset.v *)
Instance topGset_subseteq_dec : RelDecision (⊆@{topGset A}).
Proof.
    refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
      abstract (by rewrite subseteq_union_L).
  Defined.
(* stdpp/topGset.v *)
Definition topGset_finite (X : topGset A) : bool
:=
    match X with FinGSet _ => true | TopGSet => false end.
(* stdpp/topGset.v *)
Lemma topGset_finite_spec X : set_finite X ↔ topGset_finite X.
Proof.
    destruct X as [X|];
    unfold set_finite, elem_of at 1, topGset_elem_of; simpl.
    - split; [done|intros _]. exists (elements X). set_solver.
    - split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
      destruct (exist_fresh Y) as [? ?]. naive_solver.
  Qed.
(* stdpp/topGset.v *)
Instance topGset_finite_dec (X : topGset A) :
    Decision (set_finite X).
Proof.
    refine (cast_if (decide (topGset_finite X)));
      abstract (by rewrite topGset_finite_spec).
  Defined.
(* stdpp/topGset.v *)
(* * Conversion from gset *)
Definition gset_to_topGset `{Countable A} : gset A → topGset A
:= FinGSet.
(* stdpp/topGset.v *)
Lemma elem_of_gset_to_topGset (X : gset A) x : x ∈ gset_to_topGset X ↔ x ∈ X.
Proof. done. Qed.
(* stdpp/topGset.v *)
Lemma gset_to_topGset_finite (X : gset A) : set_finite (gset_to_topGset X).
Proof. exists (elements X). set_solver. Qed.
(* stdpp/topGset.v *)
(* * Conversion to coPset *)
Definition topGset_to_coPset (X : topGset positive) : coPset
:=
  match X with
  | FinGSet X => gset_to_coPset X
  | TopGSet => ⊤
  end.
(* stdpp/topGset.v *)
Lemma elem_of_topGset_to_coPset X x : x ∈ topGset_to_coPset X ↔ x ∈ X.
Proof.
  destruct X as [X|]; simpl.
  - by rewrite elem_of_gset_to_coPset.
  - done.
Qed.
(* stdpp/topGset.v *)
(* * If the union of two [topGset]s is [⊤], then one of them is also [⊤]. *)
Lemma topGset_union_top `{Countable A} (X Y : topGset A) :
  X ∪ Y = ⊤ → X = ⊤ ∨ Y = ⊤.
Proof. destruct X, Y; naive_solver. Qed.
(* stdpp/vector.v *)
(* The type [vec n] represents lists of consisting of exactly [n] elements.
Whereas the standard library declares exactly the same notations for vectors as
used for lists, we use slightly different notations so it becomes easier to use
lists and vectors together. *)
Notation vec
:= Vector.t.
(* stdpp/vector.v *)
Notation vnil
:= Vector.nil.
(* stdpp/vector.v *)
Notation vcons
:= Vector.cons.
(* stdpp/vector.v *)
Notation vapp
:= Vector.append.
(* stdpp/vector.v *)
Notation "(:::)"
:= vcons (only parsing) : vector_scope.
(* stdpp/vector.v *)
Notation "( x :::.)"
:= (vcons x) (only parsing) : vector_scope.
(* stdpp/vector.v *)
Notation "(.::: v )"
:= (λ x, vcons x v) (only parsing) : vector_scope.
(* stdpp/vector.v *)
Notation "[# ] "
:= vnil : vector_scope.
(* stdpp/vector.v *)
Notation "[# x ] "
:= (vcons x vnil) : vector_scope.
(* stdpp/vector.v *)
Notation "[# x ; .. ; y ] "
:= (vcons x .. (vcons y vnil) ..) : vector_scope.
(* stdpp/vector.v *)
Notation "(+++)"
:= vapp (only parsing) : vector_scope.
(* stdpp/vector.v *)
Notation "( v +++.)"
:= (vapp v) (only parsing) : vector_scope.
(* stdpp/vector.v *)
Notation "(.+++ w )"
:= (λ v, vapp v w) (only parsing) : vector_scope.
(* stdpp/vector.v *)
(* Similar to [fin], we provide an inversion principle that keeps the length
fixed. We define a tactic [inv_vec v] to perform case analysis on [v], using
this inversion principle. *)
Notation vec_0_inv
:= Vector.case0.
(* stdpp/vector.v *)
Definition vec_S_inv {A n} (P : vec A (S n) → Type)
  (Hcons : ∀ x v, P (x ::: v)) v : P v.
Proof.
  revert P Hcons.
  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
Defined.
(* stdpp/vector.v *)
Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m)
:=
  fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
  match i in fin m return vec A m → A with
  | 0%fin => vec_S_inv (λ _, A) (λ x _, x)
  | FS j => vec_S_inv (λ _, A) (λ _ v, v !!! j)
  end.
(* stdpp/vector.v *)
(* The tactic [vec_double_ind v1 v2] performs double induction on [v1] and [v2]
provided that they have the same length. *)
Notation vec_rect2
:= Vector.rect2.
(* stdpp/vector.v *)
Ltac vec_double_ind v1 v2
:=
  match type of v1 with
  | vec _ ?n =>
    repeat match goal with
    | H' : context [ n ] |- _ => var_neq v1 H'; var_neq v2 H'; revert H'
    end;
    revert n v1 v2;
    match goal with |- ∀ n v1 v2, @?P n v1 v2 => apply (vec_rect2 P) end
  end.
(* stdpp/vector.v *)
Notation vcons_inj
:= VectorSpec.cons_inj.
(* stdpp/vector.v *)
Lemma vcons_inj_1 {A n} x y (v w : vec A n) : x ::: v = y ::: w → x = y.
Proof. apply vcons_inj. Qed.
(* stdpp/vector.v *)
Lemma vcons_inj_2 {A n} x y (v w : vec A n) : x ::: v = y ::: w → v = w.
Proof. apply vcons_inj. Qed.
(* stdpp/vector.v *)
Lemma vec_eq {A n} (v w : vec A n) : (∀ i, v !!! i = w !!! i) → v = w.
Proof.
  vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal.
  - apply (Hi 0%fin).
  - apply IH. intros i. apply (Hi (FS i)).
Qed.
(* stdpp/vector.v *)
Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
Proof.
 refine (vec_rect2
  (λ n (v w : vec A n), { v = w } + { v ≠ w })
  (left _)
  (λ _ _ _ H x y, cast_if_and (dec x y) H));
  f_equal; eauto using vcons_inj_1, vcons_inj_2.
Defined.
(* stdpp/vector.v *)
Ltac inv_vec v
:=
  let T := type of v in
  match eval hnf in T with
  | vec _ ?n =>
    match eval hnf in n with
    | 0 =>
      generalize dependent v;
      match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
    | S ?n =>
      generalize dependent v;
      match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
      (* Try going on recursively. *)
      try (let x := fresh "x" in intros x v; inv_vec v; revert x)
    end
  end.
(* stdpp/vector.v *)
(* The following tactic performs case analysis on all hypotheses of the shape
[fin 0], [fin (S n)], [vec A 0] and [vec A (S n)] until no further case
analyses are possible. *)
Ltac inv_all_vec_fin
:= block_goal;
  repeat match goal with
  | v : vec _ _ |- _ => inv_vec v; intros
  | i : fin _ |- _ => inv_fin i; intros
  end; unblock_goal.
(* stdpp/vector.v *)
(* We define a coercion from [vec] to [list] and show that it preserves the
operations on vectors. We also define a function to go in the other way, but
do not define it as a coercion, as it would otherwise introduce ambiguity. *)
Fixpoint vec_to_list {A n} (v : vec A n) : list A
:=
  match v with [#] => [] | x ::: v => x :: vec_to_list v end.
(* stdpp/vector.v *)
Coercion vec_to_list : vec >-> list.
(* stdpp/vector.v *)
Notation list_to_vec
:= Vector.of_list.
(* stdpp/vector.v *)
Lemma vec_to_list_cons {A n} x (v : vec A n) :
  vec_to_list (x ::: v) = x :: vec_to_list v.
Proof. done. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
  vec_to_list (v +++ w) = vec_to_list v ++ vec_to_list w.
Proof. by induction v; f_equal/=. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_to_vec {A} (l : list A): vec_to_list (list_to_vec l) = l.
Proof. by induction l; f_equal/=. Qed.
(* stdpp/vector.v *)
Lemma length_vec_to_list {A n} (v : vec A n) : length (vec_to_list v) = n.
Proof. induction v; simpl; by f_equal. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
  length v = length w.
Proof. by rewrite !length_vec_to_list. Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
  vec_to_list v = vec_to_list w → n = m.
Proof.
  revert m w. induction v; intros ? [|???] ?;
    simplify_eq/=; f_equal; eauto.
Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) :
  vec_to_list v = vec_to_list w → v = w.
Proof.
  revert w. induction v; intros w; inv_vec w; intros;
    simplify_eq/=; f_equal; eauto.
Qed.
(* stdpp/vector.v *)
Lemma list_to_vec_to_list {A n} (v : vec A n) :
  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (length_vec_to_list v)).
Proof.
  apply vec_to_list_inj2. rewrite vec_to_list_to_vec.
  by destruct (eq_sym (length_vec_to_list v)).
Qed.
(* stdpp/vector.v *)
Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
  ∃ i : fin (n + S m), x = (v +++ x ::: w) !!! i.
Proof.
  induction v as [|??? IHv]; simpl; [by eexists 0%fin|].
  destruct IHv as [i ?]. by exists (FS i).
Qed.
(* stdpp/vector.v *)
Lemma vec_to_list_lookup_middle {A n} (v : vec A n) (l k : list A) x :
  vec_to_list v = l ++ x :: k →
    ∃ i : fin n, l = take i v ∧ x = v !!! i ∧ k = drop (S i) v.
Proof.
  intros H.
  rewrite <-(vec_to_list_to_vec l), <-(vec_to_list_to_vec k) in H.
  rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
  pose proof (vec_to_list_inj1 _ _ H); subst.
  apply vec_to_list_inj2 in H; subst. induction l as [|?? IHl]; simpl.
  - eexists 0%fin. simpl. by rewrite vec_to_list_to_vec.
  - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
Qed.