Some junk

From iris.algebra Require Import excl auth list gmap agree csum.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants proph_map.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".

Lemma replicate_map {A B} (f : A → B) (n : nat) (e : A) :
  map f (replicate n e) = replicate n (f e).
Proof. induction n as [|n IH]; simpl; [ done | by rewrite IH ]. Qed.

Lemma replicate_vec {A} n (e : A) :
  vec_to_list (vreplicate n e) = replicate n e.
Proof. induction n as [|n IH]; first done. by rewrite /= IH. Qed.

Lemma vreplicate_get {A} n (e : A) (i : fin n) :
  vreplicate n e !!! i = e.
Proof. induction i as [|n i IH]; [ done | by apply IH ]. Qed.

Lemma vreplicate_map {A B} (f : A → B) (n : nat) (e : A) :
  Vector.map f (vreplicate n e) = vreplicate n (f e).
Proof. induction n as [|n IH]; simpl; [ done | by rewrite IH ]. Qed.

Lemma vinsert_map {A B} (f : A → B) (n : nat) (i : fin n) e (v : vec A n) :
  vmap f (vinsert i e v) = vinsert i (f e) (vmap f v).
Proof.
  induction v as [|e' n v IH].
  - inversion i.
  - inv_fin i; first done. intros i. by rewrite /= (IH i).
Qed.

Lemma take_map {A B} (n : nat) (f : A → B) (l : list A) :
  take n (map f l) = map f (take n l).
Proof.
  revert n. induction l as [|e l IH]; intro n; first by destruct n.
  destruct n as [|n]; simpl; first done. by rewrite IH.
Qed.

Definition vtake {A} {s : nat} (n : fin s) (v : vec A s) : vec A n.
Proof.
  induction n as [|s' n IH]; first constructor. inv_vec v. intros e v.
  constructor. exact e. rewrite -/fin_to_nat. apply IH, v.
Defined.

Definition vdrop {A} {s : nat} (n : fin s) (v : vec A s) : vec A (s - n).
Proof.
  induction n as [|s' n IH]; first exact v. inv_vec v. intros e v.
  apply IH, v.
Defined.

Lemma vtake_vdrop {A} (s : nat) (n : fin s) (v : vec A s) :
  vtake n v ++ vdrop n v = v.
Proof.
  induction n as [|s' n IH]; first done. inv_vec v. intros e v.
  rewrite vec_to_list_cons.
  assert (vec_to_list (vtake (FS n) (e ::: v)) = e :: vtake n v) as -> by done.
  assert (vdrop (FS n) (e ::: v) = vdrop n v) as -> by done. simpl. by rewrite IH.
Qed.

Lemma drop_map {A B} (n : nat) (f : A → B) (l : list A) :
  drop n (map f l) = map f (drop n l).
Proof.
  revert n. induction l as [|e l IH]; intro n; first by destruct n.
  destruct n as [|n]; simpl; first done. by rewrite IH.
Qed.

Lemma lookup_map {A B} (f : A → B) (l : list A) (n : nat) (e : A) :
  l !! n = Some e → map f l !! n = Some (f e).
Proof.
  revert l. induction n as [|n IH]; intros l H.
  - destruct l; by inversion_clear H.
  - destruct l; first by inversion H. apply IH, H.
Qed.

Lemma drop_cons {A} (e : A) (l l' : list A) (n : nat) :
  e :: l' = drop n l → l' = drop (S n) l.
Proof.
  revert l.
  induction n as [|n IH]; intros l H; destruct l as [|e' l]; try done.
  - simpl in *. inversion_clear H. by rewrite drop_0.
  - simpl in *. apply IH, H.
Qed.

Lemma min_lt_left (m n : nat) : (m `min` n < n ↔ m < n)%nat.
Proof.
  split; intro H.
  - apply Nat.min_lt_iff in H.
    destruct H as [H|H]; [ done | by apply Nat.lt_irrefl in H ].
  - apply Nat.min_lt_iff. by left.
Qed.

Lemma drop_tail {A} (n : nat) (e : A) (l1 l2 : list A) :
  drop n l1 = e :: l2 → drop (S n) l1 = l2.
Proof.
  revert e l1 l2. induction n; intros e l1 l2 H.
  - rewrite drop_0 in H. by subst l1.
  - destruct l1 as [|f l1]; first by inversion H. by apply IHn in H.
Qed.

Lemma drop_absurd {A} (off : nat) (l : list A) :
  (off < length l)%nat → ¬ (drop off l = []).
Proof.
  revert off. induction l as [|e l IH]; intros off H1 H2.
  - inversion H1.
  - destruct off as [|off]; first by inversion H2.
    simpl in H2. refine (IH off _ H2). simpl in H1. omega.
Qed.

Lemma back_drop_insert {A} (off : nat) (l : list A) (v : A) :
  (off < length l)%nat → take off l ++ v :: drop (S off) l = <[off:=v]> l.
Proof.
  intro H. rewrite -[in X in _ = X](take_drop off l).
  assert (off = length (take off l) + 0)%nat as Hoff.
  { rewrite take_length. rewrite min_l; first done. omega. }
  rewrite [in X in <[X:=_]> _]Hoff insert_app_r. clear Hoff.
  assert (v :: drop (S off) l = <[0%nat:=v]> (drop off l)) as ->; last done.
  destruct (drop off l) eqn:HEq; simpl.
  - by apply drop_absurd in HEq.
  - apply drop_tail in HEq. by subst.
Qed.