proposition: Lemma merge_equiv_eq `{Equiv A, !Equivalence (≡@{A}), Equiv B, !Equivalence (≡@{B}), Equiv C, !Equivalence (≡@{C})} (f : option A → option B → option C) (m1 : M C) (m2a : M A) (m2b : M B) : Proper ((≡) ==> (≡) ==> (≡)) f → (∀ y mx1 mx2, Some y ≡ f mx1 mx2 → ∃ mx1' mx2', Some y = f mx1' mx2' ∧ mx1' ≡ mx1 ∧ mx2' ≡ mx2) → m1 ≡ merge f m2a m2b ↔ ∃ m2a' m2b', m1 = merge f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
proof: Proof. intros ? Hf. split; [|by intros (?&?&->&->&->)]. revert m1. induction m2a as [|i x m2a ? IH] using map_ind; intros m1. { assert (∀ y x, Some y ≡ f None (Some x) → ∃ x', Some y = f None (Some x') ∧ x' ≡ x). { intros ?? (?&?&?&->%None_equiv_eq&(?&->&?)%Some_equiv_eq)%Hf; eauto. } rewrite merge_empty_l, map_omap_equiv_eq by (done || solve_proper). intros (m2'&->&?). exists ∅, m2'. by rewrite merge_empty_l. } unfold insert at 1, map_insert at 1. rewrite <-(partial_alter_merge_l _ (λ _, f (Some x) (m2b !! i))) by done. destruct (f (Some x) (m2b !! i)) as [y|] eqn:Hfi. - intros (y'&m'&->&Hy&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%insert_equiv_eq. destruct (Hf y' (Some x) (m2b !! i)) as (mx1&mx2&?&(x'&->&?)%Some_equiv_eq&?). { by rewrite Hy, Hfi. } exists (<[i:=x']> m2a'), (partial_alter (λ _, mx2) i m2b'). split_and!; [by apply partial_alter_merge|by f_equiv|]. intros j. destruct (decide (i = j)) as [->|?]. + by rewrite lookup_partial_alter. + by rewrite Hm2b, lookup_partial_alter_ne. - intros (m'&->&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%delete_equiv_eq. exists (<[i:=x]> m2a'), m2b'. split_and!; [|by f_equiv|done]. apply partial_alter_merge_l, symmetry, None_equiv_eq; simpl. by rewrite Hm2b, Hfi. Qed.
imports: Coq(Permutation) stdpp(options)