1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads.
Inductive option_equiv A `{Equiv A} : Equiv (option A) :=
| option_equiv_Some : Proper ((=) ==> (=)) Some
| option_equiv_None : None = None.
#[global]
Existing Instance option_equiv.
#[global]
Hint Constructors option_equiv.
Section contents.
Context `{Setoid A}.
Lemma Some_ne_None x : Some x ≠ None.
Proof. intros E. inversion E. Qed.
Lemma None_ne_Some x : None ≠ Some x.
Proof. intros E. inversion E. Qed.
Global Instance: Setoid (option A).
Proof.
split.
intros [x|]. now apply option_equiv_Some. now apply option_equiv_None.
red. induction 1. now apply option_equiv_Some. now apply option_equiv_None.
intros x y z E. revert z. induction E.
intros z E2. inversion_clear E2.
apply option_equiv_Some. etransitivity; eassumption.
easy.
Qed.
Global Instance: Setoid_Morphism Some.
Proof. split; try apply _. now apply option_equiv_Some. Qed.
Global Instance: Injective Some.
Proof. split; try apply _. intros ? ? E. now inversion E. Qed.
Global Instance option_zero: MonUnit (option A) := None.
Global Instance option_op: SgOp (option A) := λ mx my,
match mx with
| Some x => Some x
| None => my
end.
Instance: Proper ((=) ==> (=) ==> (=)) option_op.
Proof. intros [?|] [?|] ? ???; simpl; try setoid_discriminate; auto. Qed.
Global Instance: Monoid (option A).
Proof. repeat (split; try apply _); now repeat intros [?|]. Qed.
Lemma option_equiv_alt x y :
x = y ↔ (∀ n, x = Some n ↔ y = Some n).
Proof.
split; intros E1.
intro. now rewrite E1.
destruct x, y.
now apply E1.
symmetry. now apply E1.
now apply E1.
easy.
Qed.
Global Program Instance option_dec `(A_dec : ∀ x y : A, Decision (x = y))
: ∀ x y : option A, Decision (x = y) := λ x y,
match x with
| Some r =>
match y with
| Some s => match A_dec r s with left _ => left _ | right _ => right _ end
| None => right _
end
| None =>
match y with
| Some s => right _
| None => left _
end
end.
Next Obligation. now apply (injective_ne Some). Qed.
Next Obligation. setoid_discriminate. Qed.
Next Obligation. setoid_discriminate. Qed.
End contents.
#[global]
Hint Extern 10 (Equiv (option _)) => apply @option_equiv : typeclass_instances.
Lemma option_equiv_eq {A} (x y : option A) :
@option_equiv A (≡) x y ↔ x ≡ y.
Proof.
split.
induction 1. now f_equal. reflexivity.
intros. subst.
now assert (@Setoid A (@eq A)) by (split; apply _).
Qed.
#[global]
Instance option_ret: MonadReturn option := λ A x, Some x.
#[global]
Instance option_bind: MonadBind option := λ A B f x,
match x with
| Some a => f a
| None => None
end.
#[global]
Instance option_ret_proper `{Equiv A} : Proper ((=) ==> (=)) (option_ret A).
Proof. intros x y E. now apply option_equiv_Some. Qed.
#[global]
Instance option_bind_proper `{Setoid A} `{Setoid (option B)}: Proper (=) (option_bind A B).
Proof.
intros f₁ f₂ E1 x₁ x₂ [?|].
unfold option_bind. simpl. now apply E1.
easy.
Qed.
#[global]
Instance: Monad option.
Proof.
repeat (split; try apply _); unfold bind, ret, option_bind, option_ret, compose.
intros. now apply setoids.ext_equiv_refl.
now intros ? ? ? [?|].
intros A ? B ? C ? ? f [???] g [???] [x|] [y|] E; try solve [inversion_clear E].
setoid_inject. cut (g x = g y); [|now rewrite E].
case (g x), (g y); intros E2; inversion_clear E2. now f_equiv. easy.
easy.
Qed.
#[global]
Instance option_map: SFmap option := option_map.
#[global]
Instance: FullMonad option.
Proof. apply @monad_default_full_monad. apply _. Qed.
Section map.
Context `{Setoid A} `{Setoid B} `{!Injective (f : A → B)}.
Global Instance: Injective (sfmap f).
Proof.
pose proof (injective_mor f).
repeat (split; try apply _).
intros [x|] [y|] E; try solve [inversion E | easy].
apply sm_proper. apply (injective f). now apply (injective Some).
Qed.
End map.
|
