-
Notifications
You must be signed in to change notification settings - Fork 0
/
core.v
159 lines (128 loc) · 4.58 KB
/
core.v
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
(* Function composition *)
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
fun x => g (f x).
Lemma funcomp_assoc {W X Y Z} (g: Y -> Z) (f: X -> Y) (h: W -> X) :
funcomp g (funcomp f h) = (funcomp (funcomp g f) h).
Proof.
reflexivity.
Qed.
(** ** Functor Instances
Exemplary functor instances needed to make Autosubst's generation possible for functors.
Two things are important:
1. The names are fixed.
2. For Coq to check termination, also the proofs have to be closed with Defined.
*)
(** *** List Instance *)
Require Import List.
Notation "'list_map'" := map.
Definition list_ext {A B} {f g : A -> B} :
(forall x, f x = g x) -> forall xs, list_map f xs = list_map g xs.
intros H. induction xs. reflexivity.
cbn. f_equal. apply H. apply IHxs.
Defined.
Definition list_id {A} { f : A -> A} :
(forall x, f x = x) -> forall xs, list_map f xs = xs.
Proof.
intros H. induction xs. reflexivity.
cbn. rewrite H. rewrite IHxs; eauto.
Defined.
Definition list_comp {A B C} {f: A -> B} {g: B -> C} {h} :
(forall x, (funcomp g f) x = h x) -> forall xs, map g (map f xs) = map h xs.
Proof.
induction xs. reflexivity.
cbn. rewrite <- H. f_equal. apply IHxs.
Defined.
(** *** Prod Instance *)
Definition prod_map {A B C D} (f : A -> C) (g : B -> D) (p : A * B) :
C * D.
Proof.
destruct p as [a b]. split.
exact (f a). exact (g b).
Defined.
Definition prod_id {A B} {f : A -> A} {g : B -> B} :
(forall x, f x = x) -> (forall x, g x = x) -> forall p, prod_map f g p = p.
Proof.
intros H0 H1. destruct p. cbn. f_equal; [ apply H0 | apply H1 ].
Defined.
Definition prod_ext {A B C D} {f f' : A -> C} {g g': B -> D} :
(forall x, f x = f' x) -> (forall x, g x = g' x) -> forall p, prod_map f g p = prod_map f' g' p.
Proof.
intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ].
Defined.
Definition prod_comp {A B C D E F} {f1 : A -> C} {g1 : C -> E} {h1 : A -> E} {f2: B -> D} {g2: D -> F} {h2 : B -> F}:
(forall x, (funcomp g1 f1) x = h1 x) -> (forall x, (funcomp g2 f2) x = h2 x) -> forall p, prod_map g1 g2 (prod_map f1 f2 p) = prod_map h1 h2 p.
Proof.
intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ].
Defined.
(** *** Option Instance *)
Definition option_map {A B} (f : A -> B) (p : option A) :
option B :=
match p with
| Some a => Some (f a)
| None => None
end.
Definition option_id {A} {f : A -> A} :
(forall x, f x = x) -> forall p, option_map f p = p.
Proof.
intros H. destruct p ; cbn.
- f_equal. apply H.
- reflexivity.
Defined.
Definition option_ext {A B} {f f' : A -> B} :
(forall x, f x = f' x) -> forall p, option_map f p = option_map f' p.
Proof.
intros H. destruct p as [a|] ; cbn.
- f_equal. apply H.
- reflexivity.
Defined.
Definition option_comp {A B C} {f : A -> B} {g : B -> C} {h : A -> C}:
(forall x, (funcomp g f) x = h x) ->
forall p, option_map g (option_map f p) = option_map h p.
Proof.
intros H. destruct p as [a|]; cbn.
- f_equal. apply H.
- reflexivity.
Defined.
#[export] Hint Rewrite in_map_iff : FunctorInstances.
(* Declaring the scopes that all our notations will live in *)
Declare Scope fscope.
Declare Scope subst_scope.
Ltac eta_reduce :=
repeat match goal with
| [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *)
end.
Ltac minimize :=
repeat match goal with
| [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *)
| [|- context[fun x => ?g (?f x)]] => change (fun x => g (f x)) with (funcomp g f) (* funcomp folding *)
end.
(* had to add this tactic abbreviation because I could not print a setoid_rewrite with the arrow *)
Ltac setoid_rewrite_left t := setoid_rewrite <- t.
Ltac check_no_evars :=
match goal with
| [|- ?x] => assert_fails (has_evar x)
end.
Require Import Setoid Morphisms.
Lemma pointwise_forall {X Y:Type} (f g: X -> Y) :
(pointwise_relation _ eq f g) -> forall x, f x = g x.
Proof.
trivial.
Qed.
#[export] Instance funcomp_morphism {X Y Z} :
Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp.
Proof.
cbv - [funcomp].
intros g0 g1 Hg f0 f1 Hf x.
unfold funcomp. rewrite Hf, Hg.
reflexivity.
Qed.
#[export] Instance funcomp_morphism2 {X Y Z} :
Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> eq ==> eq) funcomp.
Proof.
intros g0 g1 Hg f0 f1 Hf ? x ->.
unfold funcomp. rewrite Hf, Hg.
reflexivity.
Qed.
Ltac unfold_funcomp := match goal with
| |- context[(funcomp ?f ?g) ?s] => change ((funcomp f g) s) with (f (g s))
end.