Commit 0144c537 authored by Robbert Krebbers's avatar Robbert Krebbers

Propers for monadic operations on option.

parent aad23129
Pipeline #3847 passed with stage
in 5 minutes and 14 seconds
......@@ -231,9 +231,15 @@ Proof. destruct mx; naive_solver. Qed.
Lemma bind_with_Some {A} (mx : option A) : mx = Some = mx.
Proof. by destruct mx. Qed.
Instance option_fmap_proper `{Equiv A, Equiv B} (f : A B) :
Proper (() ==> ()) f Proper (() ==> ()) (fmap (M:=option) f).
Instance option_fmap_proper `{Equiv A, Equiv B} :
Proper ((() ==> ()) ==> () ==> ()) (fmap (M:=option) (A:=A) (B:=B)).
Proof. destruct 2; constructor; auto. Qed.
Instance option_mbind_proper `{Equiv A, Equiv B} :
Proper ((() ==> ()) ==> () ==> ()) (mbind (M:=option) (A:=A) (B:=B)).
Proof. destruct 2; simpl; try constructor; auto. Qed.
Instance option_mjoin_proper `{Equiv A} :
Proper (() ==> ()) (mjoin (M:=option) (A:=A)).
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
(** ** Inverses of constructors *)
(** We can do this in a fancy way using dependent types, but rewrite does
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment