proposition: Lemma partial_alter_equiv_eq (f : option A → option A) (m1 m2 : M A) i : Proper ((≡) ==> (≡)) f → (∀ x1 mx2, Some x1 ≡ f mx2 → ∃ mx2', Some x1 = f mx2' ∧ mx2' ≡ mx2) → m1 ≡ partial_alter f i m2 ↔ ∃ m2', m1 = partial_alter f i m2' ∧ m2' ≡ m2.
proof: Proof. intros ? Hf. split; [|by intros (?&->&<-)]. intros Hm. assert (∃ mx2', m1 !! i = f mx2' ∧ mx2' ≡ m2 !! i) as (mx2'&?&?). { destruct (m1 !! i) as [x1|] eqn:Hix1. - apply (Hf x1 (m2 !! i)). by rewrite <-Hix1, Hm, lookup_partial_alter. - exists (m2 !! i). split; [|done]. apply symmetry, None_equiv_eq. by rewrite <-Hix1, Hm, lookup_partial_alter. } exists (partial_alter (λ _, mx2') i m1). split. - apply map_eq; intros j. destruct (decide (i = j)) as [->|?]. + by rewrite !lookup_partial_alter. + by rewrite !lookup_partial_alter_ne. - intros j. destruct (decide (i = j)) as [->|?]. + by rewrite lookup_partial_alter. + by rewrite Hm, !lookup_partial_alter_ne. Qed.
imports: Coq(Permutation) stdpp(options)