phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_sets.v *)
Lemma set_bind_disj_union_L `{!LeibnizEquiv SB} f (X Y : C) :
    X ## Y → set_bind f (X ∪ Y) = set_bind f X ∪ set_bind f Y.
Proof. unfold_leibniz. apply set_bind_disj_union. Qed.
(* stdpp/fin_sets.v *)
Notation set_omap
:= (set_omap (C:=C) (D:=D)).
(* stdpp/fin_sets.v *)
Lemma elem_of_set_omap f X y : y ∈ set_omap f X ↔ ∃ x, x ∈ X ∧ f x = Some y.
Proof.
    unfold set_omap. rewrite elem_of_list_to_set, list_elem_of_omap.
    by setoid_rewrite elem_of_elements.
  Qed.
(* stdpp/fin_sets.v *)
Instance set_unfold_omap f X (P : A → Prop) y :
    (∀ x, SetUnfoldElemOf x X (P x)) →
    SetUnfoldElemOf y (set_omap f X) (∃ x, Some y = f x ∧ P x).
Proof. constructor. rewrite elem_of_set_omap; naive_solver. Qed.
(* stdpp/fin_sets.v *)
Instance set_omap_proper :
    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) set_omap.
Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
(* stdpp/fin_sets.v *)
Instance set_omap_mono :
    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) set_omap.
Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_set_omap_1 f X y : y ∈ set_omap f X → ∃ x, Some y = f x ∧ x ∈ X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma elem_of_set_omap_2 f X x y : x ∈ X → f x = Some y → y ∈ set_omap f X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_empty f : set_omap f ∅ = ∅.
Proof. unfold set_omap. by rewrite elements_empty. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_empty_iff f X : set_omap f X ≡ ∅ ↔ set_Forall (λ x, f x = None) X.
Proof.
    split; set_unfold; unfold set_Forall.
    - intros Hi x Hx. destruct (f x) as [y|] eqn:Hy; naive_solver.
    - intros Hi y (x & Hf & Hx). specialize (Hi x Hx). by rewrite Hi in Hf.
  Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_union f X Y : set_omap f (X ∪ Y) ≡ set_omap f X ∪ set_omap f Y.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton f x :
    set_omap f {[ x ]} ≡ match f x with Some y => {[ y ]} | None => ∅ end.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton_Some f x y : f x = Some y → set_omap f {[ x ]} ≡ {[ y ]}.
Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton_None f x : f x = None → set_omap f {[ x ]} ≡ ∅.
Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_alt f X : set_omap f X ≡ set_bind (λ x, option_to_set (f x)) X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_map_alt (f : A → B) X : set_map f X = set_omap (λ x, Some (f x)) X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_filter P `{∀ x, Decision (P x)} f X :
    (∀ x, x ∈ X → is_Some (f x) → P x) →
    set_omap f (filter P X) ≡ set_omap f X.
Proof. set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_union_L f X Y : set_omap f (X ∪ Y) = set_omap f X ∪ set_omap f Y.
Proof. unfold_leibniz. apply set_omap_union. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton_L f x :
      set_omap f {[ x ]} = match f x with Some y => {[ y ]} | None => ∅ end.
Proof. unfold_leibniz. apply set_omap_singleton. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton_Some_L f x y :
      f x = Some y → set_omap f {[ x ]} = {[ y ]}.
Proof. unfold_leibniz. apply set_omap_singleton_Some. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_singleton_None_L f x : f x = None → set_omap f {[ x ]} = ∅.
Proof. unfold_leibniz. apply set_omap_singleton_None. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_alt_L f X :
      set_omap f X = set_bind (λ x, option_to_set (f x)) X.
Proof. unfold_leibniz. apply set_omap_alt. Qed.
(* stdpp/fin_sets.v *)
Lemma set_omap_filter_L P `{∀ x, Decision (P x)} f X :
      (∀ x, x ∈ X → is_Some (f x) → P x) →
      set_omap f (filter P X) = set_omap f X.
Proof. unfold_leibniz. apply set_omap_filter. Qed.
(* stdpp/fin_sets.v *)
(* * Decision procedures *)
Lemma set_Forall_elements P X : set_Forall P X ↔ Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
(* stdpp/fin_sets.v *)
Lemma set_Exists_elements P X : set_Exists P X ↔ Exists P (elements X).
Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed.
(* stdpp/fin_sets.v *)
Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X :
  {set_Forall P X} + {set_Exists Q X}.
Proof.
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
   [by apply set_Forall_elements|by apply set_Exists_elements].
Defined.
(* stdpp/fin_sets.v *)
Lemma not_set_Forall_Exists P `{dec : ∀ x, Decision (P x)} X :
  ¬set_Forall P X → set_Exists (not ∘ P) X.
Proof. intro. by destruct (set_Forall_Exists_dec P (not ∘ P) dec X). Qed.
(* stdpp/fin_sets.v *)
Lemma not_set_Exists_Forall P `{dec : ∀ x, Decision (P x)} X :
  ¬set_Exists P X → set_Forall (not ∘ P) X.
Proof.
  by destruct (set_Forall_Exists_dec
    (not ∘ P) P (λ x, swap_if (decide (P x))) X).
Qed.
(* stdpp/fin_sets.v *)
Instance set_Forall_dec (P : A → Prop) `{∀ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
Proof.
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
Defined.
(* stdpp/fin_sets.v *)
Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
Proof.
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
Defined.
(* stdpp/fin_sets.v *)
(* Alternative versions of finite and infinite predicates *)
Lemma pred_finite_set (P : A → Prop) :
  pred_finite P ↔ (∃ X : C, ∀ x, P x → x ∈ X).
Proof.
  split.
  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
  - intros [X Hfin]. exists (elements X). set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma dec_pred_finite_set_alt (P : A → Prop) `{!∀ x : A, Decision (P x)} :
  pred_finite P ↔ (∃ X : C, ∀ x, P x ↔ x ∈ X).
Proof.
  rewrite dec_pred_finite_alt; [|done]. split.
  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
  - intros [X Hfin]. exists (elements X). set_solver.
Qed.
(* stdpp/fin_sets.v *)
Lemma pred_infinite_set (P : A → Prop) :
  pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X).
Proof.
  split.
  - intros Hinf X. destruct (Hinf (elements X)). set_solver.
  - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver.
Qed.
(* stdpp/fin_sets.v *)
(* Properties about the [fresh] operation on finite sets *)
Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
(* stdpp/fin_sets.v *)
Lemma is_fresh X : fresh X ∉ X.
Proof.
    unfold fresh, set_fresh. rewrite <-elem_of_elements. apply infinite_is_fresh.
  Qed.
(* stdpp/fin_sets.v *)
Lemma exist_fresh X : ∃ x, x ∉ X.
Proof. exists (fresh X). apply is_fresh. Qed.
(* stdpp/fin_sets.v *)
(* Properties about the [fresh_list] operation on finite sets *)
Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
(* stdpp/fin_sets.v *)
Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs.
Proof. induction 1; by constructor. Qed.
(* stdpp/fin_sets.v *)
Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X.
Proof.
    intros HX; revert x; rewrite <-Forall_forall. by induction HX; constructor.
  Qed.
(* stdpp/fin_sets.v *)
Lemma Forall_fresh_alt X xs :
    Forall_fresh X xs ↔ NoDup xs ∧ ∀ x, x ∈ xs → x ∉ X.
Proof.
    split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of.
    rewrite <-Forall_forall.
    intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
  Qed.
(* stdpp/fin_sets.v *)
Lemma Forall_fresh_subseteq X Y xs :
    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
(* stdpp/fin_sets.v *)
Lemma length_fresh_list n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed.
(* stdpp/fin_sets.v *)
Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
Proof.
    revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
    apply IH in Hin; set_solver.
  Qed.
(* stdpp/fin_sets.v *)
Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
Proof.
    revert X. induction n; simpl; constructor; auto.
    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
  Qed.
(* stdpp/fin_sets.v *)
Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
Proof.
    rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh.
  Qed.
(* stdpp/fin_sets.v *)
Lemma size_set_seq `{FinSet nat C} start len :
  size (set_seq (C:=C) start len) = len.
Proof.
  rewrite <-list_to_set_seq, size_list_to_set.
  2:{ apply NoDup_seq. }
  rewrite length_seq. done.
Qed.
(* stdpp/fin_sets.v *)
(* This is placed outside of the section because [set_ind] could not work with
[C:=D] if it was inside. *)
Lemma size_set_map `{FinSet A C, FinSet B D} (f : A → B) (X : C) :
  size (C:=D) (set_map f X) ≤ size X.
Proof.
  pattern X. apply set_ind; clear X.
  - by intros ?? ->.
  - by rewrite set_map_empty, !size_empty.
  - intros x X ? IH. rewrite set_map_union, set_map_singleton.
    rewrite size_union_alt, size_difference_alt.
    rewrite (size_union _ X), !size_singleton by set_solver. lia.
Qed.
(* stdpp/functions.v *)
Instance fn_insert : Insert A T (A → T)
:=
    λ a t f b, if decide (a = b) then t else f b.
(* stdpp/functions.v *)
Instance fn_alter : Alter A T (A → T)
:=
    λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
(* stdpp/functions.v *)
Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
(* stdpp/functions.v *)
Lemma fn_lookup_insert_rev  (f : A → T) a t1 t2 :
    <[a:=t1]>f a = t2 → t1 = t2.
Proof. rewrite fn_lookup_insert. congruence. Qed.
(* stdpp/functions.v *)
Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b.
Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
(* stdpp/functions.v *)
Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
(* stdpp/functions.v *)
Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
    a ≠ b → alter g a f b = f b.
Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
(* stdpp/gmap.v *)
Notation "P ~ 0"
:= (λ p, P p~0) : function_scope.
(* stdpp/gmap.v *)
Notation "P ~ 1"
:= (λ p, P p~1) : function_scope.
(* stdpp/gmap.v *)
(* * The tree data structure *)
Inductive gmap_dep_ne (A : Type) (P : positive → Prop)
:=
  | GNode001 : gmap_dep_ne A P~1  → gmap_dep_ne A P 
  | GNode010 : P 1 → A → gmap_dep_ne A P
  | GNode011 : P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode100 : gmap_dep_ne A P~0 → gmap_dep_ne A P
  | GNode101 : gmap_dep_ne A P~0 → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode110 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P
  | GNode111 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P.
(* stdpp/gmap.v *)
(* Using [Variant] we suppress the generation of the induction scheme. We use
the induction scheme [gmap_ind] in terms of the smart constructors to reduce the
number of cases, similar to Appel and Leroy. *)
Variant gmap_dep (A : Type) (P : positive → Prop)
:=
  | GEmpty : gmap_dep A P
  | GNodes : gmap_dep_ne A P → gmap_dep A P.
(* stdpp/gmap.v *)
Record gmap_key K `{Countable K} (q : positive)
:=
  GMapKey { _ : encode (A:=K) <$> decode q = Some q }.
(* stdpp/gmap.v *)
Lemma gmap_key_encode `{Countable K} (k : K) : gmap_key K (encode k).
Proof. constructor. by rewrite decode_encode. Qed.
(* stdpp/gmap.v *)
Instance gmap_key_pi `{Countable K} q : ProofIrrel (gmap_key K q).
Proof. intros [?] [?]. f_equal. apply (proof_irrel _). Qed.
(* stdpp/gmap.v *)
Record gmap K `{Countable K} A
:= GMap { gmap_car : gmap_dep A (gmap_key K) }.
(* stdpp/gmap.v *)
Instance gmap_dep_ne_eq_dec {A P} :
  EqDecision A → (∀ i, ProofIrrel (P i)) → EqDecision (gmap_dep_ne A P).
Proof.
  intros ? Hirr t1 t2. revert P t1 t2 Hirr.
  refine (fix go {P} (t1 t2 : gmap_dep_ne A P) {Hirr : _} : Decision (t1 = t2) :=
    match t1, t2 with
    | GNode001 r1, GNode001 r2 => cast_if (go r1 r2)
    | GNode010 _ x1, GNode010 _ x2 => cast_if (decide (x1 = x2))
    | GNode011 _ x1 r1, GNode011 _ x2 r2 =>
       cast_if_and (decide (x1 = x2)) (go r1 r2)
    | GNode100 l1, GNode100 l2 => cast_if (go l1 l2)
    | GNode101 l1 r1, GNode101 l2 r2 => cast_if_and (go l1 l2) (go r1 r2)
    | GNode110 l1 _ x1, GNode110 l2 _ x2 =>
       cast_if_and (go l1 l2) (decide (x1 = x2))
    | GNode111 l1 _ x1 r1, GNode111 l2 _ x2 r2 =>
       cast_if_and3 (go l1 l2) (decide (x1 = x2)) (go r1 r2)
    | _, _ => right _
    end);
    clear go; abstract first [congruence|f_equal; done || apply Hirr|idtac].
Defined.
(* stdpp/gmap.v *)
Instance gmap_dep_eq_dec {A P} :
  (∀ i, ProofIrrel (P i)) → EqDecision A → EqDecision (gmap_dep A P).
Proof. intros. solve_decision. Defined.
(* stdpp/gmap.v *)
Instance gmap_eq_dec `{Countable K} {A} :
  EqDecision A → EqDecision (gmap K A).
Proof. intros. solve_decision. Defined.
(* stdpp/gmap.v *)
(* The smart constructor [GNode] and eliminator [gmap_dep_ne_case] are used to
reduce the number of cases, similar to Appel and Leroy. *)
Definition GNode {A P}
    (ml : gmap_dep A P~0)
    (mx : option (P 1 * A)) (mr : gmap_dep A P~1) : gmap_dep A P
:=
  match ml, mx, mr with
  | GEmpty, None, GEmpty => GEmpty
  | GEmpty, None, GNodes r => GNodes (GNode001 r)
  | GEmpty, Some (p,x), GEmpty => GNodes (GNode010 p x)
  | GEmpty, Some (p,x), GNodes r => GNodes (GNode011 p x r)
  | GNodes l, None, GEmpty => GNodes (GNode100 l)
  | GNodes l, None, GNodes r => GNodes (GNode101 l r)
  | GNodes l, Some (p,x), GEmpty => GNodes (GNode110 l p x)
  | GNodes l, Some (p,x), GNodes r => GNodes (GNode111 l p x r)
  end.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_case {A P B} (t : gmap_dep_ne A P)
    (f : gmap_dep A P~0 → option (P 1 * A) → gmap_dep A P~1 → B) : B
:=
  match t with
  | GNode001 r => f GEmpty None (GNodes r)
  | GNode010 p x => f GEmpty (Some (p,x)) GEmpty
  | GNode011 p x r => f GEmpty (Some (p,x)) (GNodes r)
  | GNode100 l => f (GNodes l) None GEmpty
  | GNode101 l r => f (GNodes l) None (GNodes r)
  | GNode110 l p x => f (GNodes l) (Some (p,x)) GEmpty
  | GNode111 l p x r => f (GNodes l) (Some (p,x)) (GNodes r)
  end.
(* stdpp/gmap.v *)
(* Operations *)
Definition gmap_dep_ne_lookup {A} : ∀ {P}, positive → gmap_dep_ne A P → option A
:=
  fix go {P} i t {struct t} :=
  match t, i with
  | (GNode010 _ x | GNode011 _ x _ | GNode110 _ _ x | GNode111 _ _ x _), 1 => Some x
  | (GNode100 l | GNode110 l _ _ | GNode101 l _ | GNode111 l _ _ _), i~0 => go i l
  | (GNode001 r | GNode011 _ _ r | GNode101 _ r | GNode111 _ _ _ r), i~1 => go i r
  | _, _ => None
  end.
(* stdpp/gmap.v *)
Definition gmap_dep_lookup {A P}
    (i : positive) (mt : gmap_dep A P) : option A
:=
  match mt with GEmpty => None | GNodes t => gmap_dep_ne_lookup i t end.
(* stdpp/gmap.v *)
Instance gmap_lookup `{Countable K} {A} :
    Lookup K A (gmap K A)
:= λ k mt,
  gmap_dep_lookup (encode k) (gmap_car mt).
(* stdpp/gmap.v *)
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A)
:= GMap GEmpty.
(* stdpp/gmap.v *)
Fixpoint gmap_dep_ne_singleton {A P} (i : positive) :
    P i → A → gmap_dep_ne A P
:=
  match i with
  | 1 => GNode010
  | i~0 => λ p x, GNode100 (gmap_dep_ne_singleton i p x)
  | i~1 => λ p x, GNode001 (gmap_dep_ne_singleton i p x)
  end.
(* stdpp/gmap.v *)
Definition gmap_partial_alter_aux {A P}
    (go : ∀ i, P i → gmap_dep_ne A P → gmap_dep A P)
    (f : option A → option A) (i : positive) (p : P i)
    (mt : gmap_dep A P) : gmap_dep A P
:=
  match mt with
  | GEmpty =>
     match f None with
     | None => GEmpty | Some x => GNodes (gmap_dep_ne_singleton i p x)
     end
  | GNodes t => go i p t
  end.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_partial_alter {A} (f : option A → option A) :
    ∀ {P} (i : positive), P i → gmap_dep_ne A P → gmap_dep A P
:=
  Eval lazy -[gmap_dep_ne_singleton] in
  fix go {P} i p t {struct t} :=
    gmap_dep_ne_case t $ λ ml mx mr,
      match i with
      | 1 => λ p, GNode ml ((p,.) <$> f (snd <$> mx)) mr
      | i~0 => λ p, GNode (gmap_partial_alter_aux go f i p ml) mx mr
      | i~1 => λ p, GNode ml mx (gmap_partial_alter_aux go f i p mr)
      end p.
(* stdpp/gmap.v *)
Definition gmap_dep_partial_alter {A P}
    (f : option A → option A) : ∀ i : positive, P i → gmap_dep A P → gmap_dep A P
:=
  gmap_partial_alter_aux (gmap_dep_ne_partial_alter f) f.
(* stdpp/gmap.v *)
Instance gmap_partial_alter `{Countable K} {A} :
    PartialAlter K A (gmap K A)
:= λ f k '(GMap mt),
  GMap $ gmap_dep_partial_alter f (encode k) (gmap_key_encode k) mt.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_fmap {A B} (f : A → B) :
    ∀ {P}, gmap_dep_ne A P → gmap_dep_ne B P
:=
  fix go {P} t :=
    match t with
    | GNode001 r => GNode001 (go r)
    | GNode010 p x => GNode010 p (f x)
    | GNode011 p x r => GNode011 p (f x) (go r)
    | GNode100 l => GNode100 (go l)
    | GNode101 l r => GNode101 (go l) (go r)
    | GNode110 l p x => GNode110 (go l) p (f x)
    | GNode111 l p x r => GNode111 (go l) p (f x) (go r)
    end.
(* stdpp/gmap.v *)
Definition gmap_dep_fmap {A B P} (f : A → B)
    (mt : gmap_dep A P) : gmap_dep B P
:=
  match mt with GEmpty => GEmpty | GNodes t => GNodes (gmap_dep_ne_fmap f t) end.
(* stdpp/gmap.v *)
Instance gmap_fmap `{Countable K} : FMap (gmap K)
:= λ {A B} f '(GMap mt),
  GMap $ gmap_dep_fmap f mt.
(* stdpp/gmap.v *)
Definition gmap_dep_omap_aux {A B P}
    (go : gmap_dep_ne A P → gmap_dep B P) (tm : gmap_dep A P) : gmap_dep B P
:=
  match tm with GEmpty => GEmpty | GNodes t' => go t' end.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_omap {A B} (f : A → option B) :
    ∀ {P}, gmap_dep_ne A P → gmap_dep B P
:=
  fix go {P} t :=
    gmap_dep_ne_case t $ λ ml mx mr,
      GNode (gmap_dep_omap_aux go ml) ('(p,x) ← mx; (p,.) <$> f x)
            (gmap_dep_omap_aux go mr).
(* stdpp/gmap.v *)
Definition gmap_dep_omap {A B P} (f : A → option B) :
  gmap_dep A P → gmap_dep B P
:= gmap_dep_omap_aux (gmap_dep_ne_omap f).
(* stdpp/gmap.v *)
Instance gmap_omap `{Countable K} : OMap (gmap K)
:= λ {A B} f '(GMap mt),
  GMap $ gmap_dep_omap f mt.
(* stdpp/gmap.v *)
Definition gmap_merge_aux {A B C P}
    (go : gmap_dep_ne A P → gmap_dep_ne B P → gmap_dep C P)
    (f : option A → option B → option C)
    (mt1 : gmap_dep A P) (mt2 : gmap_dep B P) : gmap_dep C P
:=
  match mt1, mt2 with
  | GEmpty, GEmpty => GEmpty
  | GNodes t1', GEmpty => gmap_dep_ne_omap (λ x, f (Some x) None) t1'
  | GEmpty, GNodes t2' => gmap_dep_ne_omap (λ x, f None (Some x)) t2'
  | GNodes t1', GNodes t2' => go t1' t2'
  end.
(* stdpp/gmap.v *)
Definition diag_None' {A B C} {P : Prop}
    (f : option A → option B → option C)
    (mx : option (P * A)) (my : option (P * B)) : option (P * C)
:=
  match mx, my with
  | None, None => None
  | Some (p,x), None => (p,.) <$> f (Some x) None
  | None, Some (p,y) => (p,.) <$> f None (Some y)
  | Some (p,x), Some (_,y) => (p,.) <$> f (Some x) (Some y)
  end.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_merge {A B C} (f : option A → option B → option C) :
    ∀ {P}, gmap_dep_ne A P → gmap_dep_ne B P → gmap_dep C P
:=
  fix go {P} t1 t2 {struct t1} :=
    gmap_dep_ne_case t1 $ λ ml1 mx1 mr1,
      gmap_dep_ne_case t2 $ λ ml2 mx2 mr2,
        GNode (gmap_merge_aux go f ml1 ml2) (diag_None' f mx1 mx2)
              (gmap_merge_aux go f mr1 mr2).
(* stdpp/gmap.v *)
Definition gmap_dep_merge {A B C P} (f : option A → option B → option C) :
    gmap_dep A P → gmap_dep B P → gmap_dep C P
:=
  gmap_merge_aux (gmap_dep_ne_merge f) f.
(* stdpp/gmap.v *)
Instance gmap_merge `{Countable K} : Merge (gmap K)
:=
  λ {A B C} f '(GMap mt1) '(GMap mt2), GMap $ gmap_dep_merge f mt1 mt2.
(* stdpp/gmap.v *)
Definition gmap_fold_aux {A B P}
    (go : positive → B → gmap_dep_ne A P → B)
    (i : positive) (y : B) (mt : gmap_dep A P) : B
:=
  match mt with GEmpty => y | GNodes t => go i y t end.
(* stdpp/gmap.v *)
Definition gmap_dep_ne_fold {A B} (f : positive → A → B → B) :
    ∀ {P}, positive → B → gmap_dep_ne A P → B
:=
  fix go {P} i y t :=
    gmap_dep_ne_case t $ λ ml mx mr,
      gmap_fold_aux go i~1
        (gmap_fold_aux go i~0
          match mx with None => y | Some (p,x) => f (Pos.reverse i) x y end ml) mr.
(* stdpp/gmap.v *)
Definition gmap_dep_fold {A B P} (f : positive → A → B → B) :
    positive → B → gmap_dep A P → B
:=
  gmap_fold_aux (gmap_dep_ne_fold f).
(* stdpp/gmap.v *)
Instance gmap_fold `{Countable K} {A} :
    MapFold K A (gmap K A)
:= λ {B} f y '(GMap mt),
  gmap_dep_fold (λ i x, match decode i with Some k => f k x | None => id end) 1 y mt.
(* stdpp/gmap.v *)
(* Proofs *)
Definition GNode_valid {A P}
    (ml : gmap_dep A P~0) (mx : option (P 1 * A)) (mr : gmap_dep A P~1)
:=
  match ml, mx, mr with GEmpty, None, GEmpty => False | _, _, _ => True end.
(* stdpp/gmap.v *)
Lemma gmap_dep_ind A (Q : ∀ P, gmap_dep A P → Prop) :
  (∀ P, Q P GEmpty) →
  (∀ P ml mx mr, GNode_valid ml mx mr → Q _ ml → Q _ mr → Q P (GNode ml mx mr)) →
  ∀ P mt, Q P mt.
Proof.
  intros Hemp Hnode P [|t]; [done|]. induction t.
  - by apply (Hnode _ GEmpty None (GNodes _)).
  - by apply (Hnode _ GEmpty (Some (_,_)) GEmpty).
  - by apply (Hnode _ GEmpty (Some (_,_)) (GNodes _)).
  - by apply (Hnode _ (GNodes _) None GEmpty).
  - by apply (Hnode _ (GNodes _) None (GNodes _)).
  - by apply (Hnode _ (GNodes _) (Some (_,_)) GEmpty).
  - by apply (Hnode _ (GNodes _) (Some (_,_)) (GNodes _)).
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_lookup_GNode {A P} (ml : gmap_dep A P~0) mr mx i :
  gmap_dep_lookup i (GNode ml mx mr) =
    match i with
    | 1 => snd <$> mx | i~0 => gmap_dep_lookup i ml | i~1 => gmap_dep_lookup i mr
    end.
Proof. by destruct ml, mx as [[]|], mr, i. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_ne_lookup_not_None {A P} (t : gmap_dep_ne A P) :
  ∃ i, P i ∧ gmap_dep_ne_lookup i t ≠ None.
Proof.
  induction t; repeat select (∃ _, _) (fun H => destruct H);
    try first [by eexists 1|by eexists _~0|by eexists _~1].
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_eq_empty {A P} (mt : gmap_dep A P) :
  (∀ i, P i → gmap_dep_lookup i mt = None) → mt = GEmpty.
Proof.
  intros Hlookup. destruct mt as [|t]; [done|].
  destruct (gmap_dep_ne_lookup_not_None t); naive_solver.
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_eq {A P} (mt1 mt2 : gmap_dep A P) :
  (∀ i, ProofIrrel (P i)) →
  (∀ i, P i → gmap_dep_lookup i mt1 = gmap_dep_lookup i mt2) → mt1 = mt2.
Proof.
  revert mt2. induction mt1 as [|P ml1 mx1 mr1 _ IHl IHr] using gmap_dep_ind;
    intros mt2 ? Hlookup;
    destruct mt2 as [|? ml2 mx2 mr2 _ _ _] using gmap_dep_ind.
  - done.
  - symmetry. apply gmap_dep_eq_empty. naive_solver.
  - apply gmap_dep_eq_empty. naive_solver.
  - f_equal.
    + apply (IHl _ _). intros i. generalize (Hlookup (i~0)).
      by rewrite !gmap_dep_lookup_GNode.
    + generalize (Hlookup 1). rewrite !gmap_dep_lookup_GNode.
      destruct mx1 as [[]|], mx2 as [[]|]; intros; simplify_eq/=;
        repeat f_equal; try  apply proof_irrel; naive_solver.
    + apply (IHr _ _). intros i. generalize (Hlookup (i~1)).
      by rewrite !gmap_dep_lookup_GNode.
Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_ne_lookup_singleton_eq {A P} i (p : P i) (x : A) :
  gmap_dep_ne_lookup i (gmap_dep_ne_singleton i p x) = Some x.
Proof. revert P p. induction i; by simpl. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_ne_lookup_singleton_ne {A P} i j (p : P i) (x : A) :
  i ≠ j → gmap_dep_ne_lookup j (gmap_dep_ne_singleton i p x) = None.
Proof. revert P j p. induction i; intros ? [?|?|]; naive_solver. Qed.
(* stdpp/gmap.v *)
Lemma gmap_dep_partial_alter_GNode {A P} (f : option A → option A)
    i (p : P i) (ml : gmap_dep A P~0) mx mr :
  GNode_valid ml mx mr →
  gmap_dep_partial_alter f i p (GNode ml mx mr) =
    match i with
    | 1 => λ p, GNode ml ((p,.) <$> f (snd <$> mx)) mr
    | i~0 => λ p, GNode (gmap_dep_partial_alter f i p ml) mx mr
    | i~1 => λ p, GNode ml mx (gmap_dep_partial_alter f i p mr)
    end p.
Proof. by destruct ml, mx as [[]|], mr. Qed.