phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/finite.v *)
Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Next Obligation.
  constructor; [ by rewrite list_elem_of_singleton | apply NoDup_singleton ].
Qed.
(* stdpp/finite.v *)
Lemma bool_card : card bool = 2.
Proof. done. Qed.
(* stdpp/finite.v *)
Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
  intros. apply NoDup_app; split_and?.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
  - intro. rewrite !list_elem_of_fmap. intros (?&?&?) (?&?&?); congruence.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
Qed.
(* stdpp/finite.v *)
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card, enum at 1, sum_finite. by rewrite length_app, !length_fmap. Qed.
(* stdpp/finite.v *)
Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
  {| enum := a ← enum A; (a,.) <$> enum B |}.
Next Obligation.
  intros A ?????. apply NoDup_bind.
  - intros a1 a2 [a b] ?? (?&?&_)%list_elem_of_fmap (?&?&_)%list_elem_of_fmap.
    naive_solver.
  - intros a ?. rewrite (NoDup_fmap _). apply NoDup_enum.
  - apply NoDup_enum.
Qed.
(* stdpp/finite.v *)
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
  unfold card, enum at 1, prod_finite. induction (enum A); csimpl; auto.
  rewrite length_app, length_fmap. auto.
Qed.
(* stdpp/finite.v *)
Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n)
:=
  match n with
  | 0 => [[#]]
  | S m => a ← l; vcons a <$> vec_enum l m
  end.
(* stdpp/finite.v *)
Instance vec_finite `{Finite A} n : Finite (vec A n) :=
  {| enum := vec_enum (enum A) n |}.
Next Obligation.
  intros A ?? n. induction n as [|n IH]; csimpl; [apply NoDup_singleton|].
  apply NoDup_bind.
  - intros x1 x2 y ?? (?&?&_)%list_elem_of_fmap (?&?&_)%list_elem_of_fmap.
    congruence.
  - intros x ?. rewrite NoDup_fmap by (intros ?; apply vcons_inj_2). done.
  - apply NoDup_enum.
Qed.
(* stdpp/finite.v *)
Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
Proof.
  unfold card, enum at 1, vec_finite. induction n as [|n IH]; simpl; [done|].
  rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
  induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
  by rewrite length_app, length_fmap, IH.
Qed.
(* stdpp/finite.v *)
Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
Proof.
  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ length_vec_to_list _)).
  - abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
  - abstract (intros [l <-]; exists (list_to_vec l);
      apply (sig_eq_pi _), vec_to_list_to_vec).
Defined.
(* stdpp/finite.v *)
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof.
  unfold card, enum at 1, list_finite, bijective_finite.
  rewrite length_fmap. apply vec_card.
Qed.
(* stdpp/finite.v *)
Fixpoint fin_enum (n : nat) : list (fin n)
:=
  match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
(* stdpp/finite.v *)
Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation.
  intros n. induction n; simpl; constructor.
  - rewrite list_elem_of_fmap. by intros (?&?&?).
  - by apply (NoDup_fmap _).
Qed.
(* stdpp/finite.v *)
Lemma fin_card n : card (fin n) = n.
Proof.
  unfold card, enum, fin_finite.
  induction n; simpl; rewrite ?length_fmap; auto.
Qed.
(* stdpp/finite.v *)
(* shouldn’t be an instance (cycle with [sig_finite]): *)
Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
  Decision (P x).
Proof.
  assert {xs : list A | ∀ x, P x ↔ x ∈ xs} as [xs ?].
  { clear x. exists (proj1_sig <$> enum _). intros x. split; intros Hx.
    - apply list_elem_of_fmap_2' with (x ↾ Hx); [apply elem_of_enum|]; done.
    - apply list_elem_of_fmap in Hx as [[x' Hx'] [-> _]]; done. }
  destruct (decide (x ∈ xs)); [left | right]; naive_solver.
Qed.
(* stdpp/finite.v *)
Fixpoint list_filter_sig (l : list A) : list (sig P)
:=
    match l with
    | [] => []
    | x :: l => match decide (P x) with
              | left H => x ↾ H :: list_filter_sig l
              | _ => list_filter_sig l
              end
    end.
(* stdpp/finite.v *)
Lemma list_filter_sig_filter (l : list A) :
    proj1_sig <$> list_filter_sig l = filter P l.
Proof.
    induction l as [| a l IH]; [done |].
    simpl; rewrite filter_cons.
    destruct (decide _); csimpl; by rewrite IH.
  Qed.
(* stdpp/finite.v *)
Instance sig_finite : Finite (sig P) :=
    {| enum := list_filter_sig (enum A) |}.
Next Obligation.
    eapply NoDup_fmap_1. rewrite list_filter_sig_filter.
    apply NoDup_filter, NoDup_enum.
  Qed.
(* stdpp/finite.v *)
Lemma sig_card : card (sig P) = length (filter P (enum A)).
Proof.
    unfold card, enum at 1, sig_finite.
    by rewrite <-list_filter_sig_filter, length_fmap.
  Qed.
(* stdpp/finite.v *)
Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) :
  card B < card A → ∃ x1 x2, x1 ≠ x2 ∧ f x1 = f x2.
Proof.
  intros. apply dec_stable; intros Heq.
  cut (Inj eq eq f); [intros ?%inj_card; lia|].
  intros x1 x2 ?. apply dec_stable. naive_solver.
Qed.
(* stdpp/finite.v *)
Lemma nat_pigeonhole (f : nat → nat) (n1 n2 : nat) :
  n2 < n1 →
  (∀ i, i < n1 → f i < n2) →
  ∃ i1 i2, i1 < i2 < n1 ∧ f i1 = f i2.
Proof.
  intros Hn Hf. pose (f' (i : fin n1) := nat_to_fin (Hf _ (fin_to_nat_lt i))).
  destruct (finite_pigeonhole f') as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
  apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
  unfold f' in Hf'. rewrite !fin_to_nat_to_fin in Hf'.
  pose proof (fin_to_nat_lt i1); pose proof (fin_to_nat_lt i2).
  destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; lia.
Qed.
(* stdpp/finite.v *)
Lemma list_pigeonhole {A} (l1 l2 : list A) :
  l1 ⊆ l2 →
  length l2 < length l1 →
  ∃ i1 i2 x, i1 < i2 ∧ l1 !! i1 = Some x ∧ l1 !! i2 = Some x.
Proof.
  intros Hl Hlen.
  assert (∀ i : fin (length l1), ∃ (j : fin (length l2)) x,
    l1 !! (fin_to_nat i) = Some x ∧
    l2 !! (fin_to_nat j) = Some x) as [f Hf]%fin_choice.
  { intros i. destruct (lookup_lt_is_Some_2 l1 i)
      as [x Hix]; [apply fin_to_nat_lt|].
    assert (x ∈ l2) as [j Hjx]%list_elem_of_lookup_1
      by (by eapply Hl, list_elem_of_lookup_2).
    exists (nat_to_fin (lookup_lt_Some _ _ _ Hjx)), x.
    by rewrite fin_to_nat_to_fin. }
  destruct (finite_pigeonhole f) as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
  destruct (Hf i1) as (x1&?&?), (Hf i2) as (x2&?&?).
  assert (x1 = x2) as -> by congruence.
  apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
  destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; eauto with lia.
Qed.
(* stdpp/fin_maps.v *)
(* Finiteness is axiomatized through a fold operation [map_fold f b m], which
folds a function [f] over each element of the map [m]. The order in which the
elements are passed to [f] is unspecified. *)
Class MapFold K A M
:= map_fold B : (K → A → B → B) → B → M → B.
(* stdpp/fin_maps.v *)
(* Finite map implementations are required to implement the [merge] function
which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with].

The function [diag_None f] is used in the specification and lemmas of [merge f].
It lifts a function [f : option A → option B → option C] by returning
[None] if both arguments are [None], to make sure that in [merge f m1 m2], the
function [f] can only operate on elements that are in the domain of either [m1]
or [m2]. *)
Definition diag_None {A B C} (f : option A → option B → option C)
    (mx : option A) (my : option B) : option C
:=
  match mx, my with None, None => None | _, _ => f mx my end.
(* stdpp/fin_maps.v *)
(* We need the [insert] operation as part of the [map_fold_ind] rule in the
[FinMap] interface. Hence we define it before the other derived operations. *)
Instance map_insert `{PartialAlter K A M} : Insert K A M
:=
  λ i x, partial_alter (λ _, Some x) i.
(* stdpp/fin_maps.v *)
Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
    PartialAlter K A (M A), OMap M, Merge M, ∀ A, MapFold K A (M A),
    EqDecision K}
:= {
  map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
  lookup_empty {A} i : (∅ : M A) !! i = None;
  lookup_partial_alter_eq {A} f (m : M A) i :
    partial_alter f i m !! i = f (m !! i);
  lookup_partial_alter_ne {A} f (m : M A) i j :
    i ≠ j → partial_alter f i m !! j = m !! j;
  lookup_fmap {A B} (f : A → B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
  lookup_omap {A B} (f : A → option B) (m : M A) i :
    omap f m !! i = m !! i ≫= f;
  lookup_merge {A B C} (f : option A → option B → option C) (m1 : M A) (m2 : M B) i :
    merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i);
  map_fold_empty {A B} (f : K → A → B → B) (b : B) :
    map_fold f b ∅ = b;
  (** The law [map_fold_fmap_ind] implies that all uses of [map_fold] and the
  induction principle traverse the map in the same way. This also means that
  [map_fold] enjoys parametricity, i.e., the order cannot depend on the choice
  of [A], [B], [f], and [b]. To make sure it cannot depend on [A], we quantify
  over a function [g : A → A')].
  This law can be used with [induction m as ... using map_fold_fmap_ind], but
  in practice [map_first_key_ind] is more convenient. *)
  map_fold_fmap_ind {A} (P : M A → Prop) :
    P ∅ →
    (∀ i x m,
      m !! i = None →
      (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
        map_fold f b (<[i:=x']> (g <$> m)) = f i x' (map_fold f b (g <$> m))) →
      P m →
      P (<[i:=x]> m)) →
    ∀ m, P m;
}.
(* stdpp/fin_maps.v *)
(* All of the following functions are defined in a generic way for arbitrary
finite map implementations. These generic implementations do not cause a
significant performance loss, which justifies including them in the finite map
interface as primitive operations. *)
Instance map_alter `{PartialAlter K A M} : Alter K A M
:=
  λ f, partial_alter (fmap f).
(* stdpp/fin_maps.v *)
Instance map_delete `{PartialAlter K A M} : Delete K M
:=
  partial_alter (λ _, None).
(* stdpp/fin_maps.v *)
Instance map_singleton `{PartialAlter K A M, Empty M} :
  SingletonM K A M
:= λ i x, <[i:=x]> ∅.
(* stdpp/fin_maps.v *)
Definition list_to_map `{Insert K A M, Empty M} : list (K * A) → M
:=
  fold_right (λ p, <[p.1:=p.2]>) ∅.
(* stdpp/fin_maps.v *)
Instance map_size `{MapFold K A M} : Size M
:=
  map_fold (λ _ _, S) 0.
(* stdpp/fin_maps.v *)
Definition map_to_list `{MapFold K A M} : M → list (K * A)
:=
  map_fold (λ i x, ((i,x) ::.)) [].
(* stdpp/fin_maps.v *)
(* The key [i] is the first to occur in the conversion to list/fold of [m].
This definition is useful in combination with [map_first_key_ind] and
[map_fold_insert_first_key]/[map_to_list_insert_first_key]. *)
Definition map_first_key `{MapFold K A M} (m : M) (i : K)
:=
  ∃ x, map_to_list m !! 0 = Some (i,x).
(* stdpp/fin_maps.v *)
Definition map_to_set `{MapFold K A M,
    Singleton B C, Empty C, Union C} (f : K → A → B) (m : M) : C
:=
  list_to_set (uncurry f <$> map_to_list m).
(* stdpp/fin_maps.v *)
Definition set_to_map `{Elements K C, Insert K A M, Empty M}
    (f : K → A) (X : C) : M
:=
  list_to_map ((λ i, (i, f i)) <$> elements X).
(* stdpp/fin_maps.v *)
Instance map_union_with `{Merge M} {A} : UnionWith A (M A)
:=
  λ f, merge (union_with f).
(* stdpp/fin_maps.v *)
Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A)
:=
  λ f, merge (intersection_with f).
(* stdpp/fin_maps.v *)
Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A)
:=
  λ f, merge (difference_with f).
(* stdpp/fin_maps.v *)
(* Higher precedence to make sure it's not used for other types with a [Lookup]
instance, such as lists. *)
Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20
:=
  λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
(* stdpp/fin_maps.v *)
Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop
:=
  λ m, ∀ i x, m !! i = Some x → P i x.
(* stdpp/fin_maps.v *)
Definition map_Exists `{Lookup K A M} (P : K → A → Prop) : M → Prop
:=
  λ m, ∃ i x, m !! i = Some x ∧ P i x.
(* stdpp/fin_maps.v *)
Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : K → A → B → Prop)
    (P : K → A → Prop) (Q : K → B → Prop) (m1 : M A) (m2 : M B) : Prop
:=
  ∀ i, option_relation (R i) (P i) (Q i) (m1 !! i) (m2 !! i).
(* stdpp/fin_maps.v *)
Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
    (R : K → A → B → Prop) (m1 : M A) (m2 : M B) : Prop
:=
  ∀ i, option_Forall2 (R i) (m1 !! i) (m2 !! i).
(* stdpp/fin_maps.v *)
Definition map_included `{∀ A, Lookup K A (M A)} {A B}
    (R : K → A → B → Prop) : M A → M B → Prop
:=
  map_relation R (λ _ _, False) (λ _ _, True).
(* stdpp/fin_maps.v *)
Definition map_agree `{∀ A, Lookup K A (M A)} {A} : relation (M A)
:=
  map_relation (λ _, (=)) (λ _ _, True) (λ _ _, True).
(* stdpp/fin_maps.v *)
Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A)
:=
  map_relation (λ _ _ _, False) (λ _ _, True) (λ _ _, True).
(* stdpp/fin_maps.v *)
Notation "( m ##ₘ.)"
:= (map_disjoint m) (only parsing) : stdpp_scope.
(* stdpp/fin_maps.v *)
Notation "(.##ₘ m )"
:= (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
(* stdpp/fin_maps.v *)
(* All maps in the list [ms] are pair-wise disjoint *)
Definition map_disjoint_list `{∀ A, Lookup K A (M A)} {A} (ms : list (M A)) : Prop
:=
  ∀ j1 j2 m1 m2,
    j1 ≠ j2 →
    ms !! j1 = Some m1 →
    ms !! j2 = Some m2 →
    m1 ##ₘ m2.
(* stdpp/fin_maps.v *)
Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A)
:=
  map_included (λ _, (=)).
(* stdpp/fin_maps.v *)
(* The union of two finite maps only has a meaningful definition for maps
that are disjoint. However, as working with partial functions is inconvenient
in Coq, we define the union as a total function. In case both finite maps
have a value at the same index, we take the value of the first map. *)
Instance map_union `{Merge M} {A} : Union (M A)
:= union_with (λ x _, Some x).
(* stdpp/fin_maps.v *)
Instance map_intersection `{Merge M} {A} : Intersection (M A)
:=
  intersection_with (λ x _, Some x).
(* stdpp/fin_maps.v *)
(* The difference operation removes all values from the first map whose
index contains a value in the second map as well. *)
Instance map_difference `{Merge M} {A} : Difference (M A)
:=
  difference_with (λ _ _, None).
(* stdpp/fin_maps.v *)
(* A stronger variant of [fmap] that allows the mapped function to use the
index of the elements. Implemented by folding over the map, and repeatedly
inserting the new elements, so not very efficient. (For [gmap] this function is
[O (n log n)], while [fmap] is [O (n)] in the size [n] of the map. *)
Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
    ∀ A, MapFold K A (M A)} {A B} (f : K → A → option B) : M A → M B
:=
  map_fold (λ i x m, match f i x with Some y => <[i:=y]> m | None => m end) ∅.
(* stdpp/fin_maps.v *)
(* Given a function [f : K1 → K2], the function [kmap f] turns a maps with
keys of type [K1] into a map with keys of type [K2]. The function [kmap f]
is only well-behaved if [f] is injective, as otherwise it could map multiple
entries into the same entry. All lemmas about [kmap f] thus have the premise
[Inj (=) (=) f]. *)
Definition kmap `{∀ A, Insert K2 A (M2 A), ∀ A, Empty (M2 A),
    ∀ A, MapFold K1 A (M1 A)} {A} (f : K1 → K2) (m : M1 A) : M2 A
:=
  list_to_map (fmap (prod_map f id) (map_to_list m)).
(* stdpp/fin_maps.v *)
(* The zip operation on maps combines two maps key-wise. The keys of resulting
map correspond to the keys that are in both maps. *)
Definition map_zip_with `{Merge M} {A B C} (f : A → B → C) : M A → M B → M C
:=
  merge (λ mx my,
    match mx, my with Some x, Some y => Some (f x y) | _, _ => None end).
(* stdpp/fin_maps.v *)
Notation map_zip
:= (map_zip_with pair).
(* stdpp/fin_maps.v *)
Instance map_filter
    `{MapFold K A M, Insert K A M, Empty M} : Filter (K * A) M
:=
  λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k:=v]> m else m) ∅.
(* stdpp/fin_maps.v *)
Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M
:=
  match xs with
  | [] => ∅
  | x :: xs => <[start:=x]> (map_seq (S start) xs)
  end.
(* stdpp/fin_maps.v *)
Fixpoint map_seqZ `{Insert Z A M, Empty M} (start : Z) (xs : list A) : M
:=
  match xs with
  | [] => ∅
  | x :: xs => <[start:=x]> (map_seqZ (Z.succ start) xs)
  end.
(* stdpp/fin_maps.v *)
Instance map_lookup_total `{!Lookup K A (M A), !Inhabited A} :
  LookupTotal K A (M A) | 20
:= λ i m, default inhabitant (m !! i).
(* stdpp/fin_maps.v *)
(* Given a finite map [m : M] with keys [K] and values [A], the image [map_img m]
gives a finite set containing with the values [A] of [m]. The type of [map_img]
is generic to support different map and set implementations. A possible instance
is [SA:=gset A]. *)
Definition map_img `{MapFold K A M,
  Singleton A SA, Empty SA, Union SA} : M → SA
:= map_to_set (λ _ x, x).
(* stdpp/fin_maps.v *)
(* Given a finite map [m] with keys [K] and values [A], the preimage
[map_preimg m] gives a finite map with keys [A] and values being sets of [K].
The type of [map_preimg] is very generic to support different map and set
implementations. A possible instance is [MKA:=gmap K A], [MASK:=gmap A (gset K)],
and [SK:=gset K]. *)
Definition map_preimg `{MapFold K A MKA, Empty MASK,
    PartialAlter A SK MASK, Empty SK, Singleton K SK, Union SK}
    (m : MKA) : MASK
:=
  map_fold (λ i, partial_alter (λ mX, Some $ {[ i ]} ∪ default ∅ mX)) ∅ m.
(* stdpp/fin_maps.v *)
Definition map_compose `{OMap MA, Lookup B C MB}
  (m : MB) (n : MA B) : MA C
:= omap (m !!.) n.
(* stdpp/fin_maps.v *)
Notation "(∘ₘ)"
:= map_compose (only parsing) : stdpp_scope.
(* stdpp/fin_maps.v *)
Notation "( m ∘ₘ.)"
:= (map_compose m) (only parsing) : stdpp_scope.
(* stdpp/fin_maps.v *)
Notation "(.∘ₘ m )"
:= (λ n, map_compose n m) (only parsing) : stdpp_scope.
(* stdpp/fin_maps.v *)
Definition map_uncurry {M1 M2 M12}
    `{!∀ A, MapFold K1 A (M1 A), !∀ A, MapFold K2 A (M2 A),
      !∀ A, Empty (M12 A), !∀ A, PartialAlter (K1 * K2) A (M12 A)} {A} :
    M1 (M2 A) → M12 A
:=
  map_fold (λ i1 m' macc,
    map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') ∅.
(* stdpp/fin_maps.v *)
Definition map_curry {M1 M2 M12}
    `{!∀ A, PartialAlter K1 A (M1 A), !∀ A, Empty (M1 A),
      !∀ A, PartialAlter K2 A (M2 A), !∀ A, Empty (M2 A),
      !∀ A, MapFold (K1 * K2) A (M12 A)} {A} :
    M12 A → M1 (M2 A)
:=
  map_fold (λ '(i1, i2) x,
    partial_alter (Some ∘ <[i2:=x]> ∘ default ∅) i1) ∅.
(* stdpp/fin_maps.v *)
(* ** General properties *)
Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i.
Proof. split; [by intros ->|]. apply map_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_spec {A} (m1 m2 : M A) :
  m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
Proof.
  unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
    specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Instance map_included_preorder {A} (R : K → relation A) :
  (∀ i, PreOrder (R i)) → PreOrder (map_included R : relation (M A)).
Proof.
  split; [intros m i; by destruct (m !! i); simpl|].
  intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
  destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
    done || etrans; eauto.
Qed.
(* stdpp/fin_maps.v *)
Instance map_subseteq_po {A} : PartialOrder (⊆@{M A}).
Proof.
  split; [apply _|].
  intros m1 m2; rewrite !map_subseteq_spec.
  intros; apply map_eq; intros i; apply option_eq; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_alt `{!Inhabited A} (m : M A) i :
  m !!! i = default inhabitant (m !! i).
Proof. reflexivity. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_correct `{!Inhabited A} (m : M A) i x :
  m !! i = Some x → m !!! i = x.
Proof. rewrite lookup_total_alt. by intros ->. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_lookup_total `{!Inhabited A} (m : M A) i :
  is_Some (m !! i) → m !! i = Some (m !!! i).
Proof. intros [x Hx]. by rewrite (lookup_total_correct m i x). Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_weaken {A} (m1 m2 : M A) i x :
  m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
Proof. rewrite !map_subseteq_spec. auto. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_weaken_is_Some {A} (m1 m2 : M A) i :
  is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i).
Proof. inv 1. eauto using lookup_weaken. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_weaken_None {A} (m1 m2 : M A) i :
  m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
Proof.
  rewrite map_subseteq_spec, !eq_None_not_Some.
  intros Hm2 Hm [??]; destruct Hm2; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y :
  m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some y → x = y.
Proof. intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. congruence. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_ne {A} (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
Proof. congruence. Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty {A} (m : M A) : m = ∅ ↔ ∀ i, m !! i = None.
Proof.
  split.
  - intros -> i. by rewrite lookup_empty.
  - intros Hm. apply map_eq. intros i. by rewrite Hm, lookup_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_empty_is_Some {A} i : ¬is_Some ((∅ : M A) !! i).
Proof. rewrite lookup_empty. by inv 1. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_empty_Some {A} i (x : A) : ¬(∅ : M A) !! i = Some x.
Proof. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_empty `{!Inhabited A} i : (∅ : M A) !!! i = inhabitant.
Proof. by rewrite lookup_total_alt, lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
Proof.
  intros [_ []]. rewrite map_subseteq_spec. intros ??. by rewrite lookup_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_subseteq {A} (m : M A) : ∅ ⊆ m.
Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
(* stdpp/fin_maps.v *)
(* Use [map_first_key_ind] instead. *)
Lemma map_fold_ind {A} (P : M A → Prop) :
  P ∅ →
  (∀ i x m,
    m !! i = None →
    (∀ B (f : K → A → B → B) b x',
      map_fold f b (<[i:=x']> m) = f i x' (map_fold f b m)) →
    P m →
    P (<[i:=x]> m)) →
  ∀ m, P m.
Proof.
  intros Hemp Hins m.
  induction m as [|i x m ? Hfold IH] using map_fold_fmap_ind; [done|].
  apply Hins; [done| |done]. intros B f b x'.
  assert (m = id <$> m) as ->.
  { apply map_eq; intros j; by rewrite lookup_fmap, option_fmap_id. }
  apply Hfold.
Qed.
(* stdpp/fin_maps.v *)
(* Use as [induction m as ... using map_first_key_ind]. In the inductive case
[map_first_key (<[i:=x]> m) i] can be used in combination with the lemmas
[map_fold_insert_first_key] and [map_to_list_first_key]. *)
Lemma map_first_key_ind {A} (P : M A → Prop) :
  P ∅ →
  (∀ i x m,
    m !! i = None → map_first_key (<[i:=x]> m) i →
    P m →
    P (<[i:=x]> m)) →
  ∀ m, P m.
Proof.
  intros Hemp Hins m.
  induction m as [|i x m ? Hfold IH] using map_fold_ind; first done.
  apply Hins; [done| |done]. unfold map_first_key, map_to_list.
  rewrite Hfold. eauto.
Qed.
(* stdpp/fin_maps.v *)
(* The lemma [map_fold_weak_ind] exists for backwards compatibility; use
[map_first_key_ind] instead, which is much more convenient to use. *)
Lemma map_fold_weak_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
  P b ∅ →
  (∀ i x m r, m !! i = None → P r m → P (f i x r) (<[i:=x]> m)) →
  ∀ m, P (map_fold f b m) m.
Proof.
  intros Hemp Hins m. induction m as [|i x m ? Hfold IH] using map_fold_ind.
  - by rewrite map_fold_empty.
  - rewrite Hfold. by apply Hins.
Qed.
(* stdpp/fin_maps.v *)
(* [NoDup_map_to_list] and [NoDup_map_to_list] need to be proved mutually,
hence a [Local] helper lemma. *)
Lemma map_to_list_spec {A} (m : M A) :
  NoDup (map_to_list m) ∧ (∀ i x, (i,x) ∈ map_to_list m ↔ m !! i = Some x).
Proof.
  apply (map_fold_weak_ind (λ l m,
    NoDup l ∧ ∀ i x, (i,x) ∈ l ↔ m !! i = Some x)); clear m.
  { split; [constructor|]. intros i x. by rewrite elem_of_nil, lookup_empty. }
  intros i x m l ? [IH1 IH2]. split; [constructor; naive_solver|].
  intros j y. rewrite elem_of_cons, IH2.
  unfold insert, map_insert. destruct (decide (i = j)) as [->|].
  - rewrite lookup_partial_alter_eq. naive_solver.
  - rewrite lookup_partial_alter_ne by done. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m).
Proof. apply map_to_list_spec. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_to_list {A} (m : M A) i x :
  (i,x) ∈ map_to_list m ↔ m !! i = Some x.
Proof. apply map_to_list_spec. Qed.