-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathCanonicalStructureSimplification.v
161 lines (128 loc) · 5.81 KB
/
CanonicalStructureSimplification.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
160
161
Require Export LtacReifiedSimplification.
Require Import SpecializedCategory Functor NaturalTransformation.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Section SimplifiedMorphism.
Section single_category.
Context `{C : SpecializedCategory objC}.
(* structure for packaging a morphism and its reification *)
Structure TaggedMorphism s d := Tag { untag :> Morphism C s d }.
Structure SimplifiedMorphism s d :=
ReifyMorphism
{
morphism_of : TaggedMorphism s d;
reified_morphism_of : ReifiedMorphism C s d;
reified_morphism_ok : untag morphism_of = ReifiedMorphismDenote reified_morphism_of
}.
Global Arguments ReifyMorphism [s d] morphism_of _ _.
(* main overloaded lemma for simplification *)
Lemma rsimplify_morphisms `(r : SimplifiedMorphism s d)
: untag (morphism_of r) = ReifiedMorphismDenote (ReifiedMorphismSimplify (reified_morphism_of r)).
rewrite <- ReifiedMorphismSimplifyOk.
destruct r; assumption.
Qed.
(* tags to control the order of application *)
Definition generic_tag {s d} := Tag s d.
Definition compose_tag {s d} := @generic_tag s d.
Definition functor_tag {s d} := @compose_tag s d.
Definition nt_tag {s d} := @functor_tag s d.
Canonical Structure identity_tag {s d} m := @nt_tag s d m.
End single_category.
(* canonical instances reifying each propositional constructor *)
(* into a respective value from reified *)
Local Ltac t := simpl;
repeat rewrite <- reified_morphism_ok;
reflexivity.
Section more_single_category.
Context `{C : SpecializedCategory objC}.
Lemma reifyIdentity x : Identity x = ReifiedMorphismDenote (ReifiedIdentityMorphism C x). reflexivity. Qed.
Canonical Structure reify_identity_morphism x := ReifyMorphism (identity_tag _) _ (reifyIdentity x).
Lemma reifyCompose s d d'
`(m1' : @SimplifiedMorphism objC C d d') `(m2' : @SimplifiedMorphism objC C s d)
: Compose (untag (morphism_of m1')) (untag (morphism_of m2'))
= ReifiedMorphismDenote (ReifiedComposedMorphism (reified_morphism_of m1') (reified_morphism_of m2')).
t.
Qed.
Canonical Structure reify_composition_morphism s d d' m1' m2' := ReifyMorphism (compose_tag _) _ (@reifyCompose s d d' m1' m2').
End more_single_category.
Section functor.
Context `{C : SpecializedCategory objC}.
Context `{D : SpecializedCategory objD}.
Variable F : SpecializedFunctor C D.
Lemma reifyFunctor `(m' : @SimplifiedMorphism objC C s d)
: MorphismOf F (untag (morphism_of m')) = ReifiedMorphismDenote (ReifiedFunctorMorphism F (reified_morphism_of m')).
t.
Qed.
Canonical Structure reify_functor_morphism s d m' := ReifyMorphism (functor_tag _) _ (@reifyFunctor s d m').
End functor.
Section natural_transformation.
Context `{C : SpecializedCategory objC}.
Context `{D : SpecializedCategory objD}.
Variables F G : SpecializedFunctor C D.
Variable T : SpecializedNaturalTransformation F G.
Lemma reifyNT (x : C) : T x = ReifiedMorphismDenote (ReifiedNaturalTransformationMorphism T x). reflexivity. Qed.
Canonical Structure reify_nt_morphism x := ReifyMorphism (nt_tag _) _ (@reifyNT x).
End natural_transformation.
Section generic.
Context `{C : SpecializedCategory objC}.
Lemma reifyGeneric s d (m : Morphism C s d) : m = ReifiedMorphismDenote (ReifiedGenericMorphism C s d m). reflexivity. Qed.
Canonical Structure reify_generic_morphism s d m := ReifyMorphism (generic_tag m) _ (@reifyGeneric s d m).
End generic.
End SimplifiedMorphism.
Ltac rsimplify_morphisms :=
simpl;
(* [refine] uses a unification algorithm compatible with
ssreflect-style canonical structures; [apply] is not (but
[apply:] in ssreflect is *)
etransitivity; [ refine (rsimplify_morphisms _) | ];
etransitivity; [ | symmetry; refine (rsimplify_morphisms _) ];
instantiate;
simpl.
(* Note: Using [lazy] in the above tactic makes ExponentialLaws die on
OOM after 1-2 GB of RAM and 40 minutes. *)
(*******************************************************************************)
(** Goals which are solved by [rsimplify_morphisms] **)
(*******************************************************************************)
Section good_examples.
Section id.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objC).
Variables F G : SpecializedFunctor C D.
Variable T : SpecializedNaturalTransformation F G.
Lemma good_example_00001 (x : C) :Compose (Identity x) (Identity x) = Identity (C := C) x.
rsimplify_morphisms.
reflexivity.
Qed.
Lemma good_example_00002 s d (m : Morphism C s d)
: MorphismOf F (Compose m (Identity s)) = MorphismOf F m.
rsimplify_morphisms.
reflexivity.
Qed.
Lemma good_example_00003 s d (m : Morphism C s d)
: MorphismOf F (Compose (Identity d) m) = MorphismOf F m.
rsimplify_morphisms.
reflexivity.
Qed.
End id.
End good_examples.
(***************************************************)
(* Confusing examples that don't quite work *)
Section bad_examples.
Require Import SumCategory.
Section bad_example_0001.
Context `(C0 : SpecializedCategory objC0).
Context `(C1 : SpecializedCategory objC1).
Context `(D : SpecializedCategory objD).
Variables s d d' : C0.
Variable m1 : Morphism C0 s d.
Variable m2 : Morphism C0 d d'.
Variable F : SpecializedFunctor (C0 + C1) D.
Goal MorphismOf F (s := inl _) (d := inl _) (Compose m2 m1) = Compose (MorphismOf F (s := inl _) (d := inl _) m2) (MorphismOf F (s := inl _) (d := inl _) m1).
simpl in *.
etransitivity; [ refine (rsimplify_morphisms _) | ].
Fail reflexivity.
Abort.
End bad_example_0001.
End bad_examples.