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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Reducible.
Require Import ExtLib.Structures.Traversable.
Require Import ExtLib.Structures.Applicative.
Require Import ExtLib.Structures.Functor.
Require Import ExtLib.Structures.FunctorLaws.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Tactics.Injection.
Require Import ExtLib.Tactics.Consider.
Set Implicit Arguments.
Set Strict Implicit.
(** For backwards compatibility with hint locality attributes. *)
Set Warnings "-unsupported-attributes".
Global Instance Foldable_option {T} : Foldable (option T) T :=
fun _ f d v =>
match v with
| None => d
| Some x => f x d
end.
Global Instance Traversable_option : Traversable option :=
{| mapT := fun F _ _ _ f o =>
match o with
| None => pure None
| Some o => ap (pure (@Some _)) (f o)
end
|}.
Global Instance Applicative_option : Applicative option :=
{| pure := @Some
; ap := fun _ _ f x =>
match f , x with
| Some f , Some x => Some (f x)
| _ , _ => None
end
|}.
Global Instance Functor_option : Functor option :=
{| fmap := fun _ _ f x => match x with
| None => None
| Some x => Some (f x)
end |}.
Section relation.
Context {T : Type}.
Variable (R : relation T).
Inductive Roption : Relation_Definitions.relation (option T) :=
| Roption_None : Roption None None
| Roption_Some : forall x y, R x y -> Roption (Some x) (Some y).
Lemma Reflexive_Roption : Reflexive R -> Reflexive Roption.
Proof. clear. compute. destruct x; try constructor; auto. Qed.
Lemma Symmetric_Roption : Symmetric R -> Symmetric Roption.
Proof. clear. compute. intros.
destruct H0; constructor. auto.
Qed.
Lemma Transitive_Roption : Transitive R -> Transitive Roption.
Proof.
clear. compute. intros.
destruct H0; auto.
inversion H1. constructor; auto. subst. eapply H; eassumption.
Qed.
Global Instance Injective_Roption_None
: Injective (Roption None None).
refine {| result := True |}.
auto.
Defined.
Global Instance Injective_Roption_None_Some a
: Injective (Roption None (Some a)).
refine {| result := False |}.
inversion 1.
Defined.
Global Instance Injective_Roption_Some_None a
: Injective (Roption (Some a) None).
refine {| result := False |}.
inversion 1.
Defined.
Global Instance Injective_Roption_Some_Some a b
: Injective (Roption (Some a) (Some b)).
refine {| result := R a b |}.
inversion 1. auto.
Defined.
Global Instance Injective_Proper_Roption_Some x
: Injective (Proper Roption (Some x)).
refine {| result := R x x |}.
abstract (inversion 1; assumption).
Defined.
End relation.
(*
Global Instance FunctorLaws_option : FunctorLaws Functor_option type_option.
Proof.
constructor.
{ simpl. red. destruct x; destruct y; simpl; auto.
inversion 1; simpl. red in H0.
unfold id. constructor. etransitivity. eapply H0. 2: eauto.
eapply proper_left; eauto.
inversion 1. }
{ intros. simpl in *.
red. intros.
destruct H4; simpl.
- unfold compose. constructor.
- unfold compose. constructor.
eapply H3. eapply H2. assumption. }
{ intros; simpl in *.
red. red. inversion 2. constructor.
constructor. apply H1. assumption. }
Qed.
*)
Global Instance Injective_Some (T : Type) (a b : T) : Injective (Some a = Some b) :=
{ result := a = b
; injection :=
fun P : Some a = Some b =>
match P with
| eq_refl => eq_refl
end
}.
Require ExtLib.Core.EquivDec.
Global Instance EqDec_option (T : Type) (EDT : EquivDec.EqDec T (@eq T)) : EquivDec.EqDec (option T) (@eq _).
Proof.
red. unfold Equivalence.equiv, RelationClasses.complement. intros.
change (x = y -> False) with (x <> y).
decide equality. apply EDT.
Qed.
Section OptionEq.
Variable T : Type.
Variable EDT : RelDec (@eq T).
(** Specialization for equality **)
Global Instance RelDec_eq_option : RelDec (@eq (option T)) :=
{ rel_dec := fun x y =>
match x , y with
| None , None => true
| Some x , Some y => eq_dec x y
| _ , _ => false
end }.
Variable EDCT : RelDec_Correct EDT.
Global Instance RelDec_Correct_eq_option : RelDec_Correct RelDec_eq_option.
Proof.
constructor; destruct x; destruct y; split; simpl in *; intros; try congruence;
f_equal; try match goal with
| [ H : context [ eq_dec ?X ?Y ] |- _ ] =>
consider (eq_dec X Y)
| [ |- context [ eq_dec ?X ?Y ] ] =>
consider (eq_dec X Y)
end; auto; congruence.
Qed.
End OptionEq.
Lemma eq_option_eq
: forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
match pf in _ = x return option (F x) with
| eq_refl => val
end = match val with
| None => None
| Some val => Some match pf in _ = x return F x with
| eq_refl => val
end
end.
Proof.
destruct pf. destruct val; reflexivity.
Defined.
#[global]
Hint Rewrite eq_option_eq : eq_rw.
|
