diff --git a/theories/list.v b/theories/list.v index c0506bba6768dfe6e3bb1d2adacb97db5059d145..b8a79c79f813600db9d5a49f148c2f6bfc6a0a2b 100644 --- a/theories/list.v +++ b/theories/list.v @@ -3181,15 +3181,20 @@ Section mapM. Qed. Lemma mapM_is_Some l : is_Some (mapM f l) ↔ Forall (is_Some ∘ f) l. Proof. split; auto using mapM_is_Some_1, mapM_is_Some_2. Qed. + + Lemma mapM_fmap_Forall_Some (g : B → A) (l : list B) : + Forall (λ x, f (g x) = Some x) l → mapM f (g <\$> l) = Some l. + Proof. by induction 1; simpl; simplify_option_eq. Qed. Lemma mapM_fmap_Some (g : B → A) (l : list B) : (∀ x, f (g x) = Some x) → mapM f (g <\$> l) = Some l. - Proof. intros. by induction l; simpl; simplify_option_eq. Qed. - Lemma mapM_fmap_Some_inv (g : B → A) (l : list B) (k : list A) : - (∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <\$> l. - Proof. - intros Hgf. revert l; induction k as [|??]; intros [|??] ?; - simplify_option_eq; try f_equiv; eauto. - Qed. + Proof. intros. by apply mapM_fmap_Forall_Some, Forall_true. Qed. + + Lemma mapM_fmap_Forall2_Some_inv (g : B → A) (l : list A) (k : list B) : + mapM f l = Some k → Forall2 (λ x y, f x = Some y → g y = x) l k → g <\$> k = l. + Proof. induction 2; simplify_option_eq; naive_solver. Qed. + Lemma mapM_fmap_Some_inv (g : B → A) (l : list A) (k : list B) : + mapM f l = Some k → (∀ x y, f x = Some y → g y = x) → g <\$> k = l. + Proof. eauto using mapM_fmap_Forall2_Some_inv, Forall2_true, mapM_length. Qed. End mapM. (** ** Properties of the [permutations] function *)