phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_union_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
    (f : A → A → option A) (m1 m2a m2b : M A) :
  Proper ((≡) ==> (≡) ==> (≡)) f →
  (∀ y x1 x2,
    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
  m1 ≡ union_with f m2a m2b ↔
    ∃ m2a' m2b', m1 = union_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
  intros ? [x1|] [x2|]; simpl;
    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
    by repeat econstructor.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_intersection_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
    (f : A → A → option A) (m1 m2a m2b : M A) :
  Proper ((≡) ==> (≡) ==> (≡)) f →
  (∀ y x1 x2,
    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
  m1 ≡ intersection_with f m2a m2b ↔
    ∃ m2a' m2b', m1 = intersection_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
  intros ? [x1|] [x2|]; simpl;
    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
    by repeat econstructor.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
    (f : A → A → option A) (m1 m2a m2b : M A) :
  Proper ((≡) ==> (≡) ==> (≡)) f →
  (∀ y x1 x2,
    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
  m1 ≡ difference_with f m2a m2b ↔
    ∃ m2a' m2b', m1 = difference_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
  intros ? [x1|] [x2|]; simpl;
    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
    by repeat econstructor.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
  m1 ≡ m2a ∪ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∪ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  apply map_union_with_equiv_eq; [solve_proper|]. intros ??? ?%(inj _); eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_intersection_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
  m1 ≡ m2a ∩ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∩ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  apply map_intersection_with_equiv_eq; [solve_proper|]. intros ??? ?%(inj _); eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
  m1 ≡ m2a ∖ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∖ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  apply map_difference_with_equiv_eq; [constructor|]. intros ??? [=]%None_equiv_eq.
Qed.
(* stdpp/fin_maps.v *)
Instance map_seq_proper `{Equiv A} start :
    Proper ((≡@{list A}) ==> (≡@{M A})) (map_seq start).
Proof.
    intros l1 l2 Hl. revert start.
    induction Hl as [|x1 x2 l1 l2 ?? IH]; intros start; simpl.
    - intros ?. rewrite lookup_empty; constructor.
    - repeat (done || f_equiv).
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq start xs i :
    map_seq (M:=M A) start xs !! i = (guard (start ≤ i);; xs !! (i - start)).
Proof.
    revert start. induction xs as [|x' xs IH]; intros start; simpl.
    { rewrite lookup_empty; simplify_option_eq; by rewrite ?lookup_nil. }
    destruct (decide (start = i)) as [->|?].
    - by rewrite lookup_insert_eq, option_guard_True, Nat.sub_diag by lia.
    - rewrite lookup_insert_ne, IH by done.
      simplify_option_eq; try done || lia.
      by replace (i - start) with (S (i - S start)) by lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq_0 xs i : map_seq (M:=M A) 0 xs !! i = xs !! i.
Proof. by rewrite lookup_map_seq, option_guard_True, Nat.sub_0_r by lia. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq_Some_inv start xs i x :
    xs !! i = Some x ↔ map_seq (M:=M A) start xs !! (start + i) = Some x.
Proof.
    rewrite lookup_map_seq, option_guard_True by lia.
    by rewrite Nat.add_sub_swap, Nat.sub_diag.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq_Some start xs i x :
    map_seq (M:=M A) start xs !! i = Some x ↔ start ≤ i ∧ xs !! (i - start) = Some x.
Proof. rewrite lookup_map_seq. case_guard; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq_None start xs i :
    map_seq (M:=M A) start xs !! i = None ↔ i < start ∨ start + length xs ≤ i.
Proof.
    rewrite lookup_map_seq.
    case_guard; simplify_option_eq; rewrite ?lookup_ge_None; naive_solver lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seq_is_Some start xs i x :
    is_Some (map_seq (M:=M A) start xs !! i) ↔ start ≤ i < start + length xs.
Proof. rewrite <-not_eq_None_Some, lookup_map_seq_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_singleton start x :
    map_seq (M:=M A) start [x] = {[start:=x]}.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
(* [map_seq_disjoint] uses [length xs = 0] instead of [xs = []] as
  [lia] can handle the former but not the latter. *)
Lemma map_seq_disjoint start1 start2 xs1 xs2 :
    map_seq (M:=M A) start1 xs1 ##ₘ map_seq start2 xs2 ↔
      start1 + length xs1 ≤ start2 ∨ start2 + length xs2 ≤ start1
      ∨ length xs1 = 0 ∨ length xs2 = 0.
Proof.
    rewrite map_disjoint_alt. setoid_rewrite lookup_map_seq_None.
    split; intros Hi; [|lia]. pose proof (Hi start1). pose proof (Hi start2). lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_app_disjoint start xs1 xs2 :
    map_seq (M:=M A) start xs1 ##ₘ map_seq (start + length xs1) xs2.
Proof. apply map_seq_disjoint. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_app start xs1 xs2 :
    map_seq start (xs1 ++ xs2)
    =@{M A} map_seq start xs1 ∪ map_seq (start + length xs1) xs2.
Proof.
    revert start. induction xs1 as [|x1 xs1 IH]; intros start; simpl.
    - by rewrite (left_id_L _ _), Nat.add_0_r.
    - by rewrite IH, Nat.add_succ_r, !insert_union_singleton_l, (assoc_L _).
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_cons_disjoint start xs :
    map_seq (M:=M A) (S start) xs !! start = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_cons start xs x :
    map_seq start (x :: xs) =@{M A} <[start:=x]> (map_seq (S start) xs).
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_snoc_disjoint start xs :
    map_seq (M:=M A) start xs !! (start+length xs) = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_snoc start xs x :
    map_seq start (xs ++ [x]) =@{M A} <[start+length xs:=x]> (map_seq start xs).
Proof.
    rewrite map_seq_app, map_seq_singleton.
    by rewrite insert_union_singleton_r by (by rewrite map_seq_snoc_disjoint).
  Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_map_seq {B} (f : A → B) start xs :
    f <$> map_seq start xs =@{M B} map_seq start (f <$> xs).
Proof.
    revert start. induction xs as [|x xs IH]; intros start; csimpl.
    { by rewrite fmap_empty. }
    by rewrite fmap_insert, IH.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_map_seq start xs i x:
    start ≤ i < start + length xs →
    <[i:=x]> (map_seq start xs) =@{M A} map_seq start (<[i - start:=x]> xs).
Proof.
    intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
    - rewrite lookup_insert_eq, lookup_map_seq, option_guard_True by lia.
      by rewrite list_lookup_insert_eq by lia.
    - rewrite lookup_insert_ne, !lookup_map_seq by done.
      case_guard; [|done]. by rewrite list_lookup_insert_ne by lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seq_insert start xs i x:
    i < length xs →
    map_seq start (<[i:=x]> xs) =@{M A} <[start + i:=x]> (map_seq start xs).
Proof. intros. rewrite insert_map_seq by lia. auto with f_equal lia. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_map_seq_0 xs i x:
    i < length xs →
    <[i:=x]> (map_seq 0 xs) =@{M A} map_seq 0 (<[i:=x]> xs).
Proof. intros. rewrite insert_map_seq by lia. auto with f_equal lia. Qed.
(* stdpp/fin_maps.v *)
Instance map_seq_inj start : Inj (=) (=) (map_seq (M:=M A) start).
Proof.
    intros xs1 xs2. rewrite map_eq_iff. intros Hmap. apply list_eq. intros i.
    specialize Hmap with (i + start).
    rewrite !lookup_map_seq in Hmap.
    rewrite !option_guard_True in Hmap by lia.
    by rewrite Nat.add_sub in Hmap.
  Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_zip_seq start xs :
    list_to_map (zip (seq start (length xs)) xs) = map_seq (M:=M A) start xs.
Proof.
    apply map_eq; intros i. apply option_eq; intros x.
    assert (NoDup (zip (seq start (length xs)) xs).*1).
    { rewrite fst_zip by (rewrite length_seq; lia). apply NoDup_seq. }
    rewrite lookup_map_seq_Some, <-elem_of_list_to_map by done.
    rewrite list_elem_of_lookup.
    setoid_rewrite lookup_zip_Some. setoid_rewrite lookup_seq. split.
    - intros (i' & [-> ?] & <-). auto with f_equal lia.
    - intros [??]. assert (i - start < length xs) by eauto using lookup_lt_Some.
      exists (i - start). auto with lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_seq start xs :
    map_to_list (map_seq (M:=M A) start xs) ≡ₚ zip (seq start (length xs)) xs.
Proof.
    apply list_to_map_inj.
    - apply NoDup_fst_map_to_list.
    - rewrite fst_zip by (rewrite length_seq; lia). apply NoDup_seq.
    - by rewrite list_to_map_to_list, list_to_map_zip_seq.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_seqZ_proper `{Equiv A} start :
    Proper ((≡@{list A}) ==> (≡@{M A})) (map_seqZ start).
Proof.
    intros l1 l2 Hl. revert start.
    induction Hl as [|x1 x2 l1 l2 ?? IH]; intros start; simpl.
    - intros ?. rewrite lookup_empty; constructor.
    - repeat (done || f_equiv).
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ start xs i :
    map_seqZ (M:=M A) start xs !! i = (guard (start ≤ i);; xs !! Z.to_nat (i - start)).
Proof.
    revert start. induction xs as [|x' xs IH]; intros start; simpl.
    { rewrite lookup_empty; simplify_option_eq; by rewrite ?lookup_nil. }
    destruct (decide (start = i)) as [->|?].
    - by rewrite lookup_insert_eq, option_guard_True, Z.sub_diag by lia.
    - rewrite lookup_insert_ne, IH by done.
      simplify_option_eq; try done || lia.
      replace (i - start) with (Z.succ (i - Z.succ start)) by lia.
      by rewrite Z2Nat.inj_succ; [|lia].
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ_0 xs i :
    0 ≤ i →
    map_seqZ (M:=M A) 0 xs !! i = xs !! Z.to_nat i.
Proof. intros ?. by rewrite lookup_map_seqZ, option_guard_True, Z.sub_0_r. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ_Some_inv start xs i x :
    xs !! i = Some x ↔ map_seqZ (M:=M A) start xs !! (start + Z.of_nat i) = Some x.
Proof.
    rewrite ->lookup_map_seqZ, option_guard_True by lia.
    assert (Z.to_nat (start + Z.of_nat i - start) = i) as -> by lia.
    done.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ_Some start xs i x :
    map_seqZ (M:=M A) start xs !! i = Some x ↔
      start ≤ i ∧ xs !! Z.to_nat (i - start) = Some x.
Proof. rewrite lookup_map_seqZ. case_guard; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ_None start xs i :
    map_seqZ (M:=M A) start xs !! i = None ↔
      i < start ∨ start + Z.of_nat (length xs) ≤ i.
Proof.
    rewrite lookup_map_seqZ.
    case_guard; simplify_option_eq; rewrite ?lookup_ge_None; naive_solver lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_seqZ_is_Some start xs i :
    is_Some (map_seqZ (M:=M A) start xs !! i) ↔
      start ≤ i < start + Z.of_nat (length xs).
Proof. rewrite <-not_eq_None_Some, lookup_map_seqZ_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_singleton start x :
    map_seqZ (M:=M A) start [x] = {[start:=x]}.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
(* [map_seqZ_disjoint] uses [length xs = 0] instead of [xs = []] as
  [lia] can handle the former but not the latter. *)
Lemma map_seqZ_disjoint start1 start2 xs1 xs2 :
    map_seqZ (M:=M A) start1 xs1 ##ₘ map_seqZ (M:=M A) start2 xs2 ↔
     start1 + Z.of_nat (length xs1) ≤ start2 ∨ start2 + Z.of_nat (length xs2) ≤ start1
     ∨ length xs1 = 0%nat ∨ length xs2 = 0%nat.
Proof.
    rewrite map_disjoint_alt. setoid_rewrite lookup_map_seqZ_None.
    split; intros Hi; [|lia]. pose proof (Hi start1). pose proof (Hi start2). lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_app_disjoint start xs1 xs2 :
    map_seqZ (M:=M A) start xs1 ##ₘ map_seqZ (start + Z.of_nat (length xs1)) xs2.
Proof. apply map_seqZ_disjoint. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_app start xs1 xs2 :
    map_seqZ start (xs1 ++ xs2)
    =@{M A} map_seqZ start xs1 ∪ map_seqZ (start + Z.of_nat (length xs1)) xs2.
Proof.
    revert start. induction xs1 as [|x1 xs1 IH]; intros start; simpl.
    - by rewrite ->(left_id_L _ _), Z.add_0_r.
    - by rewrite IH, Nat2Z.inj_succ, Z.add_succ_r, Z.add_succ_l,
        !insert_union_singleton_l, (assoc_L _).
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_cons_disjoint start xs :
    map_seqZ (M:=M A) (Z.succ start) xs !! start = None.
Proof. rewrite lookup_map_seqZ_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_cons start xs x :
    map_seqZ start (x :: xs) =@{M A} <[start:=x]> (map_seqZ (Z.succ start) xs).
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_snoc_disjoint start xs :
    map_seqZ (M:=M A) start xs !! (start + Z.of_nat (length xs)) = None.
Proof. rewrite lookup_map_seqZ_None. lia. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_snoc start xs x :
    map_seqZ start (xs ++ [x])
    =@{M A} <[(start + Z.of_nat (length xs)):=x]> (map_seqZ start xs).
Proof.
    rewrite map_seqZ_app, map_seqZ_singleton.
    by rewrite insert_union_singleton_r by (by rewrite map_seqZ_snoc_disjoint).
  Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_map_seqZ {B} (f : A → B) start xs :
    f <$> map_seqZ start xs =@{M B} map_seqZ start (f <$> xs).
Proof.
    revert start. induction xs as [|x xs IH]; intros start; csimpl.
    { by rewrite fmap_empty. }
    by rewrite fmap_insert, IH.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_map_seqZ start xs i x:
    start ≤ i < start + Z.of_nat (length xs) →
    <[i:=x]> (map_seqZ start xs)
    =@{M A} map_seqZ start (<[Z.to_nat (i - start):=x]> xs).
Proof.
    intros. apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
    - rewrite lookup_insert_eq, lookup_map_seqZ, option_guard_True by lia.
      by rewrite list_lookup_insert_eq by lia.
    - rewrite lookup_insert_ne, !lookup_map_seqZ by done.
      case_guard; [|done]. by rewrite list_lookup_insert_ne by lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_insert start xs i x:
    (i < length xs)%nat →
    map_seqZ start (<[i:=x]> xs) =@{M A}
    <[start + Z.of_nat i:=x]> (map_seqZ start xs).
Proof. intros. rewrite insert_map_seqZ by lia. auto with lia f_equal. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_map_seqZ_0 xs i x:
    0 ≤ i < Z.of_nat (length xs) →
    <[i:=x]> (map_seqZ 0 xs) =@{M A} map_seqZ 0 (<[Z.to_nat i:=x]> xs).
Proof. intros. rewrite insert_map_seqZ by lia. auto with lia f_equal. Qed.
(* stdpp/fin_maps.v *)
Lemma map_seqZ_insert_0 xs i x:
    (i < length xs)%nat →
    map_seqZ 0 (<[i:=x]> xs) =@{M A} <[Z.of_nat i:=x]> (map_seqZ 0 xs).
Proof. intros. by rewrite map_seqZ_insert. Qed.
(* stdpp/fin_maps.v *)
Instance map_seqZ_inj start : Inj (=) (=) (map_seqZ (M:=M A) start).
Proof.
    intros xs1 xs2. rewrite map_eq_iff. intros Hmap. apply list_eq. intros i.
    specialize Hmap with (Z.of_nat i + start).
    rewrite !lookup_map_seqZ in Hmap.
    rewrite !option_guard_True in Hmap by lia.
    by rewrite !Z.add_simpl_r, !Nat2Z.id in Hmap.
  Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_zip_seqZ start xs :
    list_to_map (zip (seqZ start (Z.of_nat (length xs))) xs)
    = map_seqZ (M:=M A) start xs.
Proof.
    apply map_eq; intros i. apply option_eq; intros x.
    assert (NoDup (zip (seqZ start (Z.of_nat (length xs))) xs).*1).
    { rewrite fst_zip by (rewrite length_seqZ; lia). apply NoDup_seqZ. }
    rewrite lookup_map_seqZ_Some, <-elem_of_list_to_map by done.
    rewrite list_elem_of_lookup.
    setoid_rewrite lookup_zip_Some. setoid_rewrite lookup_seqZ. split.
    - intros (i' & [-> ?] & <-). auto with f_equal lia.
    - intros [??]. assert (Z.to_nat (i - start) < length xs)%nat
        by eauto using lookup_lt_Some.
      exists (Z.to_nat (i - start)). auto with lia.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_seqZ start xs :
    map_to_list (map_seqZ (M:=M A) start xs)
    ≡ₚ zip (seqZ start (Z.of_nat (length xs))) xs.
Proof.
    apply list_to_map_inj.
    - apply NoDup_fst_map_to_list.
    - rewrite fst_zip; first apply NoDup_seqZ.
      by rewrite length_seqZ, Nat2Z.id.
    - by rewrite list_to_map_to_list, list_to_map_zip_seqZ.
  Qed.
(* stdpp/fin_maps.v *)
Notation kmap
:= (kmap (M1:=M1) (M2:=M2)).
(* stdpp/fin_maps.v *)
Lemma lookup_kmap_Some {A} (m : M1 A) (j : K2) x :
    kmap f m !! j = Some x ↔ ∃ i, j = f i ∧ m !! i = Some x.
Proof.
    assert (∀ x',
      (j, x) ∈ prod_map f id <$> map_to_list m →
      (j, x') ∈ prod_map f id <$> map_to_list m → x = x').
    { intros x'. rewrite !list_elem_of_fmap.
      intros [[j' y1] [??]] [[? y2] [??]]; simplify_eq/=.
      by apply (map_to_list_unique m j'). }
    unfold kmap. rewrite <-elem_of_list_to_map', list_elem_of_fmap by done.
    setoid_rewrite elem_of_map_to_list'. split.
    - intros [[??] [??]]; naive_solver.
    - intros [? [??]]. eexists (_, _); naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_kmap_is_Some {A} (m : M1 A) (j : K2) :
    is_Some (kmap f m !! j) ↔ ∃ i, j = f i ∧ is_Some (m !! i).
Proof. unfold is_Some. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_kmap_None {A} (m : M1 A) (j : K2) :
    kmap f m !! j = None ↔ ∀ i, j = f i → m !! i = None.
Proof.
    setoid_rewrite eq_None_not_Some.
    rewrite lookup_kmap_is_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
(* Note that to state a lemma [map_kmap f m !! j = ...] we need to have a
  partial inverse [f_inv] of [f] (which one cannot define constructively). Then
  we could write [map_kmap f m !! j = (i ← f_inv j; m !! i)] *)
Lemma lookup_kmap {A} (m : M1 A) (i : K1) :
    kmap f m !! (f i) = m !! i.
Proof. apply option_eq. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_kmap `{Inhabited A} (m : M1 A) (i : K1) :
    kmap f m !!! (f i) = m !!! i.
Proof. by rewrite !lookup_total_alt, lookup_kmap. Qed.
(* stdpp/fin_maps.v *)
Instance kmap_inj {A} : Inj (=@{M1 A}) (=) (kmap f).
Proof.
    intros m1 m2 Hm. apply map_eq. intros i. by rewrite <-!lookup_kmap, Hm.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_empty {A} : kmap f ∅ =@{M2 A} ∅.
Proof. unfold kmap. by rewrite map_to_list_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_empty_iff {A} (m : M1 A) : kmap f m = ∅ ↔ m = ∅.
Proof. rewrite !map_empty. setoid_rewrite lookup_kmap_None. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_singleton {A} i (x : A) : kmap f {[i:=x]} = {[f i:=x]}.
Proof. unfold kmap. by rewrite map_to_list_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_partial_alter {A} (g : option A → option A) (m : M1 A) i :
    kmap f (partial_alter g i m) = partial_alter g (f i) (kmap f m).
Proof.
    apply map_eq; intros j. apply option_eq; intros y.
    destruct (decide (j = f i)) as [->|?].
    { by rewrite lookup_partial_alter_eq, !lookup_kmap, lookup_partial_alter_eq. }
    rewrite lookup_partial_alter_ne, !lookup_kmap_Some by done. split.
    - intros [i' [? Hm]]; simplify_eq/=.
      rewrite lookup_partial_alter_ne in Hm by naive_solver. naive_solver.
    - intros [i' [? Hm]]; simplify_eq/=. exists i'.
      rewrite lookup_partial_alter_ne by naive_solver. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_insert {A} (m : M1 A) i x :
    kmap f (<[i:=x]> m) = <[f i:=x]> (kmap f m).
Proof. apply kmap_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_delete {A} (m : M1 A) i :
    kmap f (delete i m) = delete (f i) (kmap f m).
Proof. apply kmap_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_alter {A} (g : A → A) (m : M1 A) i :
    kmap f (alter g i m) = alter g (f i) (kmap f m).
Proof. apply kmap_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_merge {A B C} (g : option A → option B → option C)
      (m1 : M1 A) (m2 : M1 B) :
    kmap f (merge g m1 m2) = merge g (kmap f m1) (kmap f m2).
Proof.
    apply map_eq; intros j. apply option_eq; intros y.
    rewrite lookup_merge, lookup_kmap_Some.
    setoid_rewrite lookup_merge. split.
    { intros [i [-> ?]]. by rewrite !lookup_kmap. }
    intros Hg. destruct (kmap f m1 !! j) as [x1|] eqn:Hm1.
    { apply lookup_kmap_Some in Hm1 as (i&->&Hm1i).
      exists i. split; [done|]. by rewrite Hm1i, <-lookup_kmap. }
    destruct (kmap f m2 !! j) as [x2|] eqn:Hm2; [|naive_solver].
    apply lookup_kmap_Some in Hm2 as (i&->&Hm2i).
    exists i. split; [done|]. by rewrite Hm2i, <-lookup_kmap, Hm1.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_union_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
    kmap f (union_with g m1 m2)
    = union_with g (kmap f m1) (kmap f m2).
Proof. apply kmap_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_intersection_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
    kmap f (intersection_with g m1 m2)
    = intersection_with g (kmap f m1) (kmap f m2).
Proof. apply kmap_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_difference_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
    kmap f (difference_with g m1 m2)
    = difference_with g (kmap f m1) (kmap f m2).
Proof. apply kmap_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_union {A} (m1 m2 : M1 A) :
    kmap f (m1 ∪ m2) = kmap f m1 ∪ kmap f m2.
Proof. apply kmap_union_with. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_intersection {A} (m1 m2 : M1 A) :
    kmap f (m1 ∩ m2) = kmap f m1 ∩ kmap f m2.
Proof. apply kmap_intersection_with. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_difference {A} (m1 m2 : M1 A) :
    kmap f (m1 ∖ m2) = kmap f m1 ∖ kmap f m2.
Proof. apply kmap_difference_with. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_zip_with {A B C} (g : A → B → C) (m1 : M1 A) (m2 : M1 B) :
    kmap f (map_zip_with g m1 m2) = map_zip_with g (kmap f m1) (kmap f m2).
Proof. by apply kmap_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_imap {A B} (g : K2 → A → option B) (m : M1 A) :
    kmap f (map_imap (g ∘ f) m) = map_imap g (kmap f m).
Proof.
    apply map_eq; intros j. apply option_eq; intros y.
    rewrite map_lookup_imap, bind_Some. setoid_rewrite lookup_kmap_Some.
    setoid_rewrite map_lookup_imap. setoid_rewrite bind_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_omap {A B} (g : A → option B) (m : M1 A) :
    kmap f (omap g m) = omap g (kmap f m).
Proof.
    apply map_eq; intros j. apply option_eq; intros y.
    rewrite lookup_omap, bind_Some. setoid_rewrite lookup_kmap_Some.
    setoid_rewrite lookup_omap. setoid_rewrite bind_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_fmap {A B} (g : A → B) (m : M1 A) :
    kmap f (g <$> m) = g <$> (kmap f m).
Proof. by rewrite !map_fmap_alt, kmap_omap. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_kmap {A} (m1 m2 : M1 A) :
    kmap f m1 ##ₘ kmap f m2 ↔ m1 ##ₘ m2.
Proof.
    rewrite !map_disjoint_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_kmap {A} (m1 m2 : M1 A) :
    map_agree (kmap f m1) (kmap f m2) ↔ map_agree m1 m2.
Proof.
    rewrite !map_agree_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_subseteq {A} (m1 m2 : M1 A) :
    kmap f m1 ⊆ kmap f m2 ↔ m1 ⊆ m2.
Proof.
    rewrite !map_subseteq_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_subset {A} (m1 m2 : M1 A) :
    kmap f m1 ⊂ kmap f m2 ↔ m1 ⊂ m2.
Proof. unfold strict. by rewrite !kmap_subseteq. Qed.
(* stdpp/fin_maps.v *)
(* This lemma is not an equality [=] but a permutation [≡ₚ] because it not
  guaranteed that when we perform the list conversion on [m : M1] and
  [kmap f m : M2] it happens in the same order. After all, [M1] and [M2] could
  use two entirely different implementations of a finite map. *)
Lemma map_to_list_kmap {A} (m : M1 A) :
    map_to_list (kmap f m) ≡ₚ prod_map f id <$> map_to_list m.
Proof.
    induction m as [|i x m ?? IH] using map_first_key_ind.
    { by rewrite kmap_empty, !map_to_list_empty. }
    rewrite map_to_list_insert_first_key by done.
    rewrite kmap_insert, map_to_list_insert by (by rewrite lookup_kmap).
    by rewrite IH.
  Qed.
(* stdpp/fin_maps.v *)
Lemma kmap_list_to_map {A} (l : list (K1 * A)) :
    kmap f (list_to_map l) = list_to_map (prod_map f id <$> l).
Proof.
    induction l as [|[i x] l IH]; simpl; first by rewrite kmap_empty.
    by rewrite kmap_insert, IH.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_kmap {A} (m : M1 A) : size (kmap f m) = size m.
Proof. by rewrite <-!length_map_to_list, map_to_list_kmap, length_fmap. Qed.