From 49e3e00f0a92527211b62b9e44d6e715589375b6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 22 Nov 2016 11:18:53 +0100 Subject: [PATCH] prove fmap_Some_setoid --- prelude/option.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/prelude/option.v b/prelude/option.v index 5557f2ac..24544dab 100644 --- a/prelude/option.v +++ b/prelude/option.v @@ -180,6 +180,16 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed. Lemma fmap_Some {A B} (f : A → B) mx y : f <\$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x. Proof. destruct mx; naive_solver. Qed. +Lemma fmap_Some_setoid {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)} + (f : A → B) mx y : + f <\$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x. +Proof. + destruct mx; simpl; split. + - intros ?%Some_equiv_inj. eauto. + - intros (? & ->%Some_inj & ?). constructor. done. + - intros ?%symmetry%equiv_None. done. + - intros (? & ? & ?). done. +Qed. Lemma fmap_None {A B} (f : A → B) mx : f <\$> mx = None ↔ mx = None. Proof. by destruct mx. Qed. Lemma option_fmap_id {A} (mx : option A) : id <\$> mx = mx. -- GitLab