phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/mapset.v *)
Instance mapset_union: Union (mapset M)
:= λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
(* stdpp/mapset.v *)
Instance mapset_intersection: Intersection (mapset M)
:= λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
(* stdpp/mapset.v *)
Instance mapset_difference: Difference (mapset M)
:= λ X1 X2,
  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
(* stdpp/mapset.v *)
Instance mapset_elements: Elements K (mapset M)
:= λ X,
  let (m) := X in (map_to_list m).*1.
(* stdpp/mapset.v *)
Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
Proof.
  split; [by intros ->|].
  destruct X1 as [m1], X2 as [m2]. simpl. intros E.
  f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
Qed.
(* stdpp/mapset.v *)
Instance mapset_set: Set_ K (mapset M).
Proof.
  split; [split | | ].
  - unfold empty, elem_of, mapset_empty, mapset_elem_of.
    simpl. intros. by simpl_map.
  - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
    simpl. by split; intros; simplify_map_eq.
  - unfold union, elem_of, mapset_union, mapset_elem_of.
    intros [m1] [m2] x. simpl. rewrite lookup_union_Some_raw.
    destruct (m1 !! x) as [[]|]; tauto.
  - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
    intros [m1] [m2] x. simpl. rewrite lookup_intersection_Some.
    assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
    { split; eauto. by intros [[] ?]. }
    naive_solver.
  - unfold difference, elem_of, mapset_difference, mapset_elem_of.
    intros [m1] [m2] x. simpl. rewrite lookup_difference_Some.
    destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
(* stdpp/mapset.v *)
Instance mapset_leibniz : LeibnizEquiv (mapset M).
Proof. intros ??. apply mapset_eq. Qed.
(* stdpp/mapset.v *)
Instance mapset_fin_set : FinSet K (mapset M).
Proof.
  split.
  - apply _.
  - unfold elements, elem_of at 2, mapset_elements, mapset_elem_of.
    intros [m] x. simpl. rewrite list_elem_of_fmap. split.
    + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
    + intros. exists (x, ()). by rewrite elem_of_map_to_list.
  - unfold elements, mapset_elements. intros [m]. simpl.
    apply NoDup_fst_map_to_list.
Qed.
(* stdpp/mapset.v *)
Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Proof.
   refine (λ X1 X2,
    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
    abstract congruence.
  Defined.
(* stdpp/mapset.v *)
Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
    inj_countable mapset_car (Some ∘ Mapset) _.
Next Obligation. by intros ? ? []. Qed.
(* stdpp/mapset.v *)
Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.
Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
(* stdpp/mapset.v *)
Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1.
Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
(* stdpp/mapset.v *)
Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Proof.
   refine (λ X1 X2, cast_if (decide (X1 ∩ X2 = ∅)));
    abstract (by rewrite disjoint_intersection_L).
  Defined.
(* stdpp/mapset.v *)
Instance mapset_subseteq_dec : RelDecision (⊆@{mapset M}).
Proof.
   refine (λ X1 X2, cast_if (decide (X1 ∪ X2 = X2)));
    abstract (by rewrite subseteq_union_L).
  Defined.
(* stdpp/mapset.v *)
Definition mapset_map_with {A B} (f : bool → A → option B)
    (X : mapset M) : M A → M B
:=
  let (mX) := X in merge (λ x y,
    match x, y with
    | Some _, Some a => f true a | None, Some a => f false a | _, None => None
    end) mX.
(* stdpp/mapset.v *)
Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M
:=
  Mapset $ omap (λ a, if f a then Some () else None) m.
(* stdpp/mapset.v *)
Lemma lookup_mapset_map_with {A B} (f : bool → A → option B) X m i :
  mapset_map_with f X m !! i = m !! i ≫= f (bool_decide (i ∈ X)).
Proof.
  destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of.
  rewrite lookup_merge by done. simpl.
  by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i).
Qed.
(* stdpp/mapset.v *)
Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
  i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
Proof.
  unfold mapset_dom_with, elem_of, mapset_elem_of.
  simpl. rewrite lookup_omap. destruct (m !! i) as [a|]; simpl.
  - destruct (Is_true_reflect (f a)); naive_solver.
  - naive_solver.
Qed.
(* stdpp/mapset.v *)
Instance mapset_dom {A} : Dom (M A) (mapset M)
:= λ m,
  Mapset $ fmap (λ _, ()) m.
(* stdpp/mapset.v *)
Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
  split; try apply _. intros A m i.
  unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
  rewrite lookup_fmap. destruct (m !! i); naive_solver.
Qed.
(* stdpp/namespaces.v *)
Record namespace
:= Namespace { namespace_car : list positive }.
(* stdpp/namespaces.v *)
Instance namespace_eq_dec : EqDecision namespace.
Proof. solve_decision. Defined.
(* stdpp/namespaces.v *)
Instance namespace_countable : Countable namespace.
Proof. apply (inj_countable' namespace_car Namespace). by intros []. Defined.
(* stdpp/namespaces.v *)
Definition nroot : namespace
:= Namespace [].
(* stdpp/namespaces.v *)
Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace
:=
  Namespace $ encode x :: namespace_car N.
(* stdpp/namespaces.v *)
Definition ndot_aux : seal (@ndot_def).
by eexists. Qed.
(* stdpp/namespaces.v *)
Definition ndot {A A_dec A_count}
:= unseal ndot_aux A A_dec A_count.
(* stdpp/namespaces.v *)
Definition ndot_unseal : @ndot = @ndot_def
:= seal_eq ndot_aux.
(* stdpp/namespaces.v *)
Definition nclose_def (N : namespace) : coPset
:=
  coPset_suffixes (positives_flatten (namespace_car N)).
(* stdpp/namespaces.v *)
Definition nclose_aux : seal (@nclose_def).
by eexists. Qed.
(* stdpp/namespaces.v *)
Instance nclose : UpClose namespace coPset
:= unseal nclose_aux.
(* stdpp/namespaces.v *)
Definition nclose_unseal : @nclose = @nclose_def
:= seal_eq nclose_aux.
(* stdpp/namespaces.v *)
Notation "N .@ x"
:= (ndot N x)
  (at level 19, left associativity, format "N .@ x") : stdpp_scope.
(* stdpp/namespaces.v *)
Notation "(.@)"
:= ndot (only parsing) : stdpp_scope.
(* stdpp/namespaces.v *)
Instance ndisjoint : Disjoint namespace
:= λ N1 N2, nclose N1 ## nclose N2.
(* stdpp/namespaces.v *)
Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. rewrite !ndot_unseal. intros [N1] x1 [N2] x2 [=]. naive_solver. Qed.
(* stdpp/namespaces.v *)
Lemma nclose_nroot : ↑nroot = (⊤:coPset).
Proof. rewrite nclose_unseal. by apply (sig_eq_pi _). Qed.
(* stdpp/namespaces.v *)
Lemma nclose_subseteq N x : ↑N.@x ⊆@{coPset} ↑N.
Proof.
    intros p. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
    unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
    destruct N as [N]. intros [q ->].
    destruct (positives_flatten_suffix N (encode x :: N)) as [q' ?].
    { by exists [encode x]. }
    by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
  Qed.
(* stdpp/namespaces.v *)
Lemma nclose_subseteq' E N x : ↑N ⊆ E → ↑N.@x ⊆ E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
(* stdpp/namespaces.v *)
Lemma nclose_infinite N : set_infinite (↑ N : coPset).
Proof. rewrite nclose_unseal. apply coPset_suffixes_infinite. Qed.
(* stdpp/namespaces.v *)
Lemma nclose_not_finite N : ¬set_finite (↑ N : coPset).
Proof. apply coPset_infinite_finite, nclose_infinite. Qed.
(* stdpp/namespaces.v *)
Lemma nclose_non_empty N : ↑ N ≠@{coPset} ∅.
Proof. apply set_infinite_non_empty, nclose_infinite. Qed.
(* stdpp/namespaces.v *)
Lemma ndot_ne_disjoint N x y : x ≠ y → N.@x ## N.@y.
Proof.
    intros Hxy a. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
    unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
    intros [qx ->] [qy Hqy].
    revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.
  Qed.
(* stdpp/namespaces.v *)
Lemma ndot_preserve_disjoint_l N E x : ↑N ## E → ↑N.@x ## E.
Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
(* stdpp/namespaces.v *)
Lemma ndot_preserve_disjoint_r N E x : E ## ↑N → E ## ↑N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
(* stdpp/namespaces.v *)
(* If-and-only-if rules. Well, not quite, but for the fragment we are
considering they are. *)
Definition coPset_subseteq_difference_r
:= subseteq_difference_r (C:=coPset).
(* stdpp/namespaces.v *)
Definition coPset_empty_subseteq
:= empty_subseteq (C:=coPset).
(* stdpp/namespaces.v *)
Definition coPset_union_least
:= union_least (C:=coPset).
(* stdpp/namespaces.v *)
(* For goals like [X ⊆ L ∪ R], backtrack for the two sides. *)
Definition coPset_union_subseteq_l'
:= union_subseteq_l' (C:=coPset).
(* stdpp/namespaces.v *)
Definition coPset_union_subseteq_r'
:= union_subseteq_r' (C:=coPset).
(* stdpp/namespaces.v *)
(* Fallback, loses lots of information but lets other rules make progress. *)
Definition coPset_subseteq_difference_l
:= subseteq_difference_l (C:=coPset).
(* stdpp/namespaces.v *)
(* Trivial cases. *)
Definition coPset_disjoint_empty_l
:= disjoint_empty_l (C:=coPset).
(* stdpp/namespaces.v *)
Definition coPset_disjoint_empty_r
:= disjoint_empty_r (C:=coPset).
(* stdpp/namespaces.v *)
(* If-and-only-if rules for ∪ on the left/right. *)
Definition coPset_disjoint_union_l X1 X2 Y
:=
  proj2 (disjoint_union_l (C:=coPset) X1 X2 Y).
(* stdpp/namespaces.v *)
Definition coPset_disjoint_union_r X Y1 Y2
:=
  proj2 (disjoint_union_r (C:=coPset) X Y1 Y2).
(* stdpp/namespaces.v *)
(* Before we apply disjoint_difference, let's make sure we normalize the goal
to [_ ∖ (_ ∪ _)]. *)
Lemma coPset_difference_difference (X1 X2 X3 Y : coPset) :
  X1 ∖ (X2 ∪ X3) ## Y →
  X1 ∖ X2 ∖ X3 ## Y.
Proof. set_solver. Qed.
(* stdpp/namespaces.v *)
(* Fallback, loses lots of information but lets other rules make progress.
Tests show trying [disjoint_difference_l1] first gives better performance. *)
Definition coPset_disjoint_difference_l1
:= disjoint_difference_l1 (C:=coPset).
(* stdpp/namespaces.v *)
Definition coPset_disjoint_difference_l2
:= disjoint_difference_l2 (C:=coPset).
(* stdpp/namespaces.v *)
Ltac solve_ndisj
:=
  repeat match goal with
  | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
  end;
  solve [eauto 12 with ndisj].
(* stdpp/natmap.v *)
Notation natmap_raw A
:= (list (option A)).
(* stdpp/natmap.v *)
Definition natmap_wf {A} (l : natmap_raw A)
:=
  match last l with None => True | Some x => is_Some x end.
(* stdpp/natmap.v *)
Instance natmap_wf_pi {A} (l : natmap_raw A) : ProofIrrel (natmap_wf l).
Proof. unfold natmap_wf. case_match; apply _. Qed.
(* stdpp/natmap.v *)
Lemma natmap_wf_inv {A} (o : option A) (l : natmap_raw A) :
  natmap_wf (o :: l) → natmap_wf l.
Proof. by destruct l. Qed.
(* stdpp/natmap.v *)
Lemma natmap_wf_lookup {A} (l : natmap_raw A) :
  natmap_wf l → l ≠ [] → ∃ i x, mjoin (l !! i) = Some x.
Proof.
  intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |].
  { exists 0. simpl. eauto. }
  destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i), x].
  intros ->. by destruct Hwf.
Qed.
(* stdpp/natmap.v *)
Record natmap (A : Type) : Type
:= NatMap {
  natmap_car : natmap_raw A;
  natmap_prf : natmap_wf natmap_car
}.
(* stdpp/natmap.v *)
Lemma natmap_eq {A} (m1 m2 : natmap A) :
  m1 = m2 ↔ natmap_car m1 = natmap_car m2.
Proof.
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
  simplify_eq/=; f_equal; apply proof_irrel.
Qed.
(* stdpp/natmap.v *)
Instance natmap_eq_dec `{EqDecision A} : EqDecision (natmap A)
:= λ m1 m2,
  match decide (natmap_car m1 = natmap_car m2) with
  | left H => left (proj2 (natmap_eq m1 m2) H)
  | right H => right (H ∘ proj1 (natmap_eq m1 m2))
  end.
(* stdpp/natmap.v *)
Instance natmap_empty {A} : Empty (natmap A)
:= NatMap [] I.
(* stdpp/natmap.v *)
Instance natmap_lookup {A} : Lookup nat A (natmap A)
:= λ i m,
  let (l,_) := m in mjoin (l !! i).
(* stdpp/natmap.v *)
Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A
:=
  match i with 0 => [Some x]| S i => None :: natmap_singleton_raw i x end.
(* stdpp/natmap.v *)
Lemma natmap_singleton_wf {A} (i : nat) (x : A) :
  natmap_wf (natmap_singleton_raw i x).
Proof. unfold natmap_wf. induction i as [|[]]; simplify_eq/=; eauto. Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_singleton_raw_eq {A} (i : nat) (x : A) :
  mjoin (natmap_singleton_raw i x !! i) = Some x.
Proof. induction i; simpl; auto. Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_singleton_raw_ne {A} (i j : nat) (x : A) :
  i ≠ j → mjoin (natmap_singleton_raw i x !! j) = None.
Proof. revert j; induction i; intros [|?]; simpl; auto with congruence. Qed.
(* stdpp/natmap.v *)
Definition natmap_cons_canon {A} (o : option A) (l : natmap_raw A)
:=
  match o, l with None, [] => [] | _, _ => o :: l end.
(* stdpp/natmap.v *)
Lemma natmap_cons_canon_wf {A} (o : option A) (l : natmap_raw A) :
  natmap_wf l → natmap_wf (natmap_cons_canon o l).
Proof. unfold natmap_wf, last. destruct o, l; simpl; eauto. Qed.
(* stdpp/natmap.v *)
Lemma natmap_cons_canon_O {A} (o : option A) (l : natmap_raw A) :
  mjoin (natmap_cons_canon o l !! 0) = o.
Proof. by destruct o, l. Qed.
(* stdpp/natmap.v *)
Lemma natmap_cons_canon_S {A} (o : option A) (l : natmap_raw A) i :
  natmap_cons_canon o l !! S i = l !! i.
Proof. by destruct o, l. Qed.
(* stdpp/natmap.v *)
Definition natmap_partial_alter_raw {A} (f : option A → option A) :
    nat → natmap_raw A → natmap_raw A
:=
  fix go i l {struct l} :=
  match l with
  | [] =>
     match f None with
     | Some x => natmap_singleton_raw i x | None => []
     end
  | o :: l =>
     match i with
     | 0 => natmap_cons_canon (f o) l | S i => natmap_cons_canon o (go i l)
     end
  end.
(* stdpp/natmap.v *)
Lemma natmap_partial_alter_wf {A} (f : option A → option A) i l :
  natmap_wf l → natmap_wf (natmap_partial_alter_raw f i l).
Proof.
  revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
    eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
Qed.
(* stdpp/natmap.v *)
Instance natmap_partial_alter {A} : PartialAlter nat A (natmap A)
:= λ f i m,
  let (l,Hl) := m in NatMap _ (natmap_partial_alter_wf f i l Hl).
(* stdpp/natmap.v *)
Lemma natmap_lookup_partial_alter_raw_eq {A} (f : option A → option A) i l :
  mjoin (natmap_partial_alter_raw f i l !! i) = f (mjoin (l !! i)).
Proof.
  revert i. induction l; intros [|?]; simpl; repeat case_match; simpl;
    autorewrite with natmap; auto.
Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_partial_alter_raw_ne {A} (f : option A → option A) i j l :
  i ≠ j → mjoin (natmap_partial_alter_raw f i l !! j) = mjoin (l !! j).
Proof.
  revert i j. induction l; intros [|?] [|?] ?; simpl;
    repeat case_match; simpl; autorewrite with natmap; auto with congruence.
  rewrite natmap_lookup_singleton_raw_ne; congruence.
Qed.
(* stdpp/natmap.v *)
Definition natmap_fmap_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B
:=
  fmap (fmap (M:=option) f).
(* stdpp/natmap.v *)
Lemma natmap_fmap_wf {A B} (f : A → B) l :
  natmap_wf l → natmap_wf (natmap_fmap_raw f l).
Proof.
  unfold natmap_fmap_raw, natmap_wf. rewrite fmap_last.
  destruct (last l); [|done]. by apply fmap_is_Some.
Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_fmap_raw {A B} (f : A → B) i l :
  mjoin (natmap_fmap_raw f l !! i) = f <$> mjoin (l !! i).
Proof.
  unfold natmap_fmap_raw. rewrite list_lookup_fmap. by destruct (l !! i).
Qed.
(* stdpp/natmap.v *)
Instance natmap_fmap : FMap natmap
:= λ A B f m,
  let (l,Hl) := m in NatMap (natmap_fmap_raw f l) (natmap_fmap_wf _ _ Hl).
(* stdpp/natmap.v *)
Definition natmap_omap_raw {A B} (f : A → option B) :
    natmap_raw A → natmap_raw B
:=
  fix go l :=
  match l with [] => [] | o :: l => natmap_cons_canon (o ≫= f) (go l) end.
(* stdpp/natmap.v *)
Lemma natmap_omap_raw_wf {A B} (f : A → option B) l :
  natmap_wf l → natmap_wf (natmap_omap_raw f l).
Proof. induction l; simpl; eauto using natmap_cons_canon_wf, natmap_wf_inv. Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_omap_raw {A B} (f : A → option B) l i :
  mjoin (natmap_omap_raw f l !! i) = mjoin (l !! i) ≫= f.
Proof.
  revert i. induction l; intros [|?]; simpl; autorewrite with natmap; auto.
Qed.
(* stdpp/natmap.v *)
Instance natmap_omap: OMap natmap
:= λ A B f m,
  let (l,Hl) := m in NatMap _ (natmap_omap_raw_wf f _ Hl).
(* stdpp/natmap.v *)
Definition natmap_merge_raw {A B C} (f : option A → option B → option C) :
    natmap_raw A → natmap_raw B → natmap_raw C
:=
  fix go l1 l2 :=
  match l1, l2 with
  | [], l2 => natmap_omap_raw (f None ∘ Some) l2
  | l1, [] => natmap_omap_raw (flip f None ∘ Some) l1
  | o1 :: l1, o2 :: l2 => natmap_cons_canon (diag_None f o1 o2) (go l1 l2)
  end.
(* stdpp/natmap.v *)
Lemma natmap_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
  natmap_wf l1 → natmap_wf l2 → natmap_wf (natmap_merge_raw f l1 l2).
Proof.
  revert l2. induction l1; intros [|??]; simpl;
    eauto using natmap_omap_raw_wf, natmap_cons_canon_wf, natmap_wf_inv.
Qed.
(* stdpp/natmap.v *)
Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C) l1 l2 i :
  mjoin (natmap_merge_raw f l1 l2 !! i) = diag_None f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
Proof.
  intros. revert i l2. induction l1; intros [|?] [|??]; simpl;
    autorewrite with natmap; auto;
    match goal with |- context [?o ≫= _] => by destruct o end.
Qed.
(* stdpp/natmap.v *)
Instance natmap_merge: Merge natmap
:= λ A B C f m1 m2,
  let (l1, Hl1) := m1 in let (l2, Hl2) := m2 in
  NatMap (natmap_merge_raw f l1 l2) (natmap_merge_wf _ _ _ Hl1 Hl2).
(* stdpp/natmap.v *)
Fixpoint natmap_fold_raw {A B} (f : nat → A → B → B)
    (j : nat) (b : B) (l : natmap_raw A) : B
:=
  match l with
  | [] => b
  | mx :: l => natmap_fold_raw f (S j)
                 match mx with Some x => f j x b | None => b end l
  end.
(* stdpp/natmap.v *)
Lemma natmap_fold_raw_cons_canon {A B} (f : nat → A → B → B) j b mx l :
  natmap_fold_raw f j b (natmap_cons_canon mx l)
  = natmap_fold_raw f (S j) match mx with Some x => f j x b | None => b end l.
Proof. by destruct mx, l. Qed.
(* stdpp/natmap.v *)
Lemma natmap_fold_raw_ind {A} (P : natmap_raw A → Prop) :
  P [] →
  (∀ i x l,
    natmap_wf l →
    mjoin (l !! i) = None →
    (∀ j A' B (f : nat → A' → B → B) (g : A → A') b x',
      natmap_fold_raw f j b
        (natmap_partial_alter_raw (λ _, Some x') i (natmap_fmap_raw g l))
      = f (i + j) x' (natmap_fold_raw f j b (natmap_fmap_raw g l))) →
    P l → P (natmap_partial_alter_raw (λ _, Some x) i l)) →
  ∀ l, natmap_wf l → P l.
Proof.
  intros Hemp Hinsert l Hl. revert P Hemp Hinsert Hl.
  induction l as [|mx l IH]; intros P Hemp Hinsert Hxl; simpl in *; [done|].
  assert (natmap_wf l) as Hl by (by destruct l).
  replace (mx :: l) with (natmap_cons_canon mx l)
    by (destruct mx, l; done || by destruct Hxl).
  apply (IH (λ l, P (natmap_cons_canon mx l))); [..|done].
  { destruct mx as [x|]; [|done].
    change (natmap_cons_canon (Some x) [])
      with (natmap_partial_alter_raw (λ _, Some x) 0 []).
    by apply (Hinsert 0). }
  intros i x l' Hl' ? Hfold.
  replace (natmap_cons_canon mx (natmap_partial_alter_raw (λ _, Some x) i l'))
    with (natmap_partial_alter_raw (λ _, Some x) (S i) (natmap_cons_canon mx l'))
    by (by destruct i, mx, l').
  apply Hinsert.
  - by apply natmap_cons_canon_wf.
  - by destruct mx, l'.
  - intros j A' B f g b x'.
    replace (natmap_partial_alter_raw (λ _, Some x') (S i)
        (natmap_fmap_raw g (natmap_cons_canon mx l')))
      with (natmap_cons_canon (g <$> mx)
        (natmap_partial_alter_raw (λ _, Some x') i (natmap_fmap_raw g l')))
      by (by destruct i, mx, l').
    replace (natmap_fmap_raw g (natmap_cons_canon mx l'))
      with (natmap_cons_canon (g <$> mx) (natmap_fmap_raw g l'))
      by (by destruct i, mx, l').
    rewrite !natmap_fold_raw_cons_canon, Nat.add_succ_comm. simpl; auto.
Qed.
(* stdpp/natmap.v *)
Instance natmap_fold {A} : MapFold nat A (natmap A)
:= λ B f d m,
  let (l,_) := m in natmap_fold_raw f 0 d l.
(* stdpp/natmap.v *)
Instance natmap_map : FinMap nat natmap.
Proof.
  split.
  - unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
    apply natmap_eq. revert l2 Hl1 Hl2 E. simpl.
    induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
    + done.
    + by specialize (E 0).
    + destruct (natmap_wf_lookup (None :: l2)) as (i&?&?); auto with congruence.
    + by specialize (E 0).
    + f_equal.
      * apply (E 0).
      * apply IH; eauto using natmap_wf_inv.
        intros i. apply (E (S i)).
    + by specialize (E 0).
    + destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
    + by specialize (E 0).
    + f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
  - done.
  - intros ?? [??] ?. apply natmap_lookup_partial_alter_raw_eq.
  - intros ?? [??] ??. apply natmap_lookup_partial_alter_raw_ne.
  - intros ??? [??] ?. apply natmap_lookup_fmap_raw.
  - intros ??? [??] ?. by apply natmap_lookup_omap_raw.
  - intros ???? [??] [??] ?. apply natmap_lookup_merge_raw.
  - done.
  - intros A P Hemp Hins [l Hl]. refine (natmap_fold_raw_ind
      (λ l, ∀ Hl, P (NatMap l Hl)) _ _ l Hl Hl); clear l Hl.
    { intros Hl.
      by replace (NatMap _ Hl) with (∅ : natmap A) by (by apply natmap_eq). }
    intros i x l Hl ? Hfold H Hxl.
    replace (NatMap _ Hxl) with (<[i:=x]> (NatMap _ Hl)) by (by apply natmap_eq).
    apply Hins; [done| |done].
    intros A' B f g b x'. rewrite <-(Nat.add_0_r i) at 2. apply (Hfold 0).
Qed.
(* stdpp/natmap.v *)
Fixpoint strip_Nones {A} (l : list (option A)) : list (option A)
:=
  match l with None :: l => strip_Nones l | _ => l end.
(* stdpp/natmap.v *)
Lemma list_to_natmap_wf {A} (l : list (option A)) :
  natmap_wf (reverse (strip_Nones (reverse l))).
Proof.
  unfold natmap_wf. rewrite last_reverse.
  induction (reverse l) as [|[]]; simpl; eauto.
Qed.
(* stdpp/natmap.v *)
Definition list_to_natmap {A} (l : list (option A)) : natmap A
:=
  NatMap (reverse (strip_Nones (reverse l))) (list_to_natmap_wf l).
(* stdpp/natmap.v *)
Lemma list_to_natmap_spec {A} (l : list (option A)) i :
  list_to_natmap l !! i = mjoin (l !! i).
Proof.
  unfold lookup at 1, natmap_lookup, list_to_natmap; simpl.
  rewrite <-(reverse_involutive l) at 2. revert i.
  induction (reverse l) as [|[x|] l' IH]; intros i; simpl; auto.
  rewrite reverse_cons, IH. clear IH. revert i.
  induction (reverse l'); intros [|?]; simpl; auto.
Qed.
(* stdpp/natmap.v *)
(* Finally, we can construct sets of [nat]s satisfying extensional equality. *)
Notation natset
:= (mapset natmap).
(* stdpp/natmap.v *)
Instance natmap_dom {A} : Dom (natmap A) natset
:= mapset_dom.
(* stdpp/natmap.v *)
Instance : FinMapDom nat natmap natset
:= mapset_dom_spec.
(* stdpp/natmap.v *)
(* Fixpoint avoids this definition from being unfolded *)
Definition bools_to_natset (βs : list bool) : natset
:=
  let f (β : bool) := if β then Some () else None in
  Mapset $ list_to_natmap $ f <$> βs.
(* stdpp/natmap.v *)
Definition natset_to_bools (sz : nat) (X : natset) : list bool
:=
  let f (mu : option ()) := match mu with Some _ => true | None => false end in
  resize sz false $ f <$> natmap_car (mapset_car X).
(* stdpp/natmap.v *)
Lemma bools_to_natset_unfold βs :
  let f (β : bool) := if β then Some () else None in
  bools_to_natset βs = Mapset $ list_to_natmap $ f <$> βs.
Proof. by destruct βs. Qed.
(* stdpp/natmap.v *)
Lemma elem_of_bools_to_natset βs i : i ∈ bools_to_natset βs ↔ βs !! i = Some true.
Proof.
  rewrite bools_to_natset_unfold; unfold elem_of, mapset_elem_of; simpl.
  rewrite list_to_natmap_spec, list_lookup_fmap.
  destruct (βs !! i) as [[]|]; compute; intuition congruence.
Qed.
(* stdpp/natmap.v *)
Lemma bools_to_natset_union βs1 βs2 :
  length βs1 = length βs2 →
  bools_to_natset (βs1 ||* βs2) = bools_to_natset βs1 ∪ bools_to_natset βs2.
Proof.
  rewrite <-Forall2_same_length; intros Hβs.
  apply set_eq. intros i. rewrite elem_of_union, !elem_of_bools_to_natset.
  revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
Qed.
(* stdpp/natmap.v *)
Lemma length_natset_to_bools (X : natset) sz : length (natset_to_bools sz X) = sz.
Proof. apply length_resize. Qed.
(* stdpp/natmap.v *)
Lemma lookup_natset_to_bools_ge sz X i : sz ≤ i → natset_to_bools sz X !! i = None.
Proof. by apply lookup_resize_old. Qed.