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
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
Require Import
MathClasses.interfaces.abstract_algebra
MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms
MathClasses.theory.categories MathClasses.categories.varieties.
Require MathClasses.theory.setoids.
Section algebras.
Context
(sig: Signature) (I: Type) (carriers: I → sorts sig → Type)
`(∀ i s, Equiv (carriers i s))
`{∀ i, AlgebraOps sig (carriers i)}
`{∀ i, Algebra sig (carriers i)}.
Definition carrier: sorts sig → Type := λ sort, ∀ i: I, carriers i sort.
Fixpoint rec_impl o: (∀ i, op_type (carriers i) o) → op_type carrier o :=
match o return (∀ i, op_type (carriers i) o) → op_type carrier o with
| ne_list.one _ => id
| ne_list.cons _ g => λ X X0, rec_impl g (λ i, X i (X0 i))
end.
Instance u (s: sorts sig): Equiv (∀ i : I, carriers i s) := products.dep_prod_equiv _ _.
Instance rec_impl_proper: ∀ o,
Proper (@products.dep_prod_equiv I _ (fun _ => op_type_equiv _ _ _) ==> (=)) (rec_impl o).
Proof with auto.
induction o; simpl. repeat intro...
intros ? ? Y x0 y0 ?. apply IHo.
intros. intro. apply Y. change (x0 i = y0 i)...
Qed.
Global Instance product_ops: AlgebraOps sig carrier := λ o, rec_impl (sig o) (λ i, algebra_op o).
Instance: ∀ o: sig, Proper (=) (algebra_op o: op_type carrier (sig o)).
Proof. intro. apply rec_impl_proper. intro. apply (algebra_propers _). Qed.
Instance product_e sort: Equiv (carrier sort) := (=). (* hint; shouldn't be needed *)
Global Instance product_algebra: Algebra sig carrier := {}.
Lemma preservation i o: Preservation sig carrier (carriers i) (λ _ v, v i) (algebra_op o) (algebra_op o).
unfold product_ops, algebra_op.
set (select_op := λ i0 : I, H0 i0 o).
replace (H0 i o) with (select_op i) by reflexivity.
clearbody select_op.
revert select_op.
induction (operation_type sig o). simpl. reflexivity.
intros. intro. apply IHo0.
Qed.
Lemma algebra_projection_morphisms i: @HomoMorphism sig carrier (carriers i) _ _ _ _ (λ a v, v i).
Proof.
constructor; try apply _.
intro. rapply (@products.dep_prod_morphism I (λ i, carriers i a) (λ i, _: Equiv (carriers i a))).
intro. apply _.
apply preservation.
Qed.
End algebras.
Section varieties.
Context
(et: EquationalTheory)
(I: Type) (carriers: I → sorts et → Type)
`(∀ i s, Equiv (carriers i s))
`(∀ i, AlgebraOps et (carriers i))
`(∀ i, InVariety et (carriers i)).
Notation carrier := (carrier et I carriers).
Instance carrier_e : forall s, Equiv _ := product_e et I carriers _.
Fixpoint nqe {t}: op_type carrier t → (∀ i, op_type (carriers i) t) → Prop :=
match t with
| ne_list.one _ => λ f g, ∀ i, f i = g i
| ne_list.cons _ _ => λ f g, ∀ tuple, nqe (f tuple) (λ i, g i (tuple i))
end. (* todo: rename *)
Instance nqe_proper t: Proper ((=) ==> (λ x y, ∀ i, x i = y i) ==> iff) (@nqe t).
Proof with auto; try reflexivity.
induction t; simpl; intros ? ? P ? ? E.
intuition. rewrite <- (P i), <- E... rewrite (P i), E...
split; intros U tuple;
apply (IHt (x tuple) (y tuple) (P tuple tuple (reflexivity _))
(λ u, x0 u (tuple u)) (λ u, y0 u (tuple u)))...
intro. apply E...
intro. apply E...
Qed.
Lemma nqe_always {t} (term: Term _ nat t) vars:
nqe (eval et vars term) (λ i, eval et (λ sort n, vars sort n i) term).
Proof.
induction term; simpl in *.
reflexivity.
set (k := (λ i : I,
eval et (λ (sort: sorts et) (n : nat), vars sort n i) term1
(eval et vars term2 i))).
cut (nqe (eval et vars term1 (eval et vars term2)) k).
set (p := λ i : I, eval et (λ (sort : sorts et) (n : nat), vars sort n i) term1
(eval et (λ (sort : sorts et) (n : nat), vars sort n i) term2)).
assert (op_type_equiv (sorts et) carrier t
(eval et vars term1 (eval et vars term2))
(eval et vars term1 (eval et vars term2))).
apply sig_type_refl.
intro. apply _.
apply eval_proper; try apply _.
reflexivity.
reflexivity.
apply (nqe_proper t (eval et vars term1 (eval et vars term2)) (eval et vars term1 (eval et vars term2)) H2 k p).
subst p k.
simpl.
intro.
pose proof (eval_proper et _ (λ (sort : sorts et) (n : nat), vars sort n i) (λ (sort : sorts et) (n : nat), vars sort n i) (reflexivity _) term1 term1 eq_refl).
apply H3.
apply IHterm2.
apply IHterm1.
change (nqe (rec_impl et _ _ (et o) (λ i : I, @algebra_op _ (carriers i) _ o)) (λ i : I, @algebra_op _ (carriers i) _ o)).
generalize (λ i: I, @algebra_op et (carriers i) _ o).
induction (et o); simpl. reflexivity.
intros. apply IHo0.
Qed.
Lemma component_equality_to_product t
(A A': op_type carrier t)
(B B': ∀ i, op_type (carriers i) t):
(∀ i, B i = B' i) → nqe A B → nqe A' B' → A = A'.
Proof with auto.
induction t; simpl in *; intros BE ABE ABE'.
intro. rewrite ABE, ABE'...
intros x y U.
apply (IHt (A x) (A' y) (λ i, B i (x i)) (λ i, B' i (y i)))...
intros. apply BE, U.
Qed.
Lemma laws_hold s: et_laws et s → ∀ vars, eval_stmt et vars s.
Proof.
intros.
pose proof (λ i, variety_laws s H2 (λ sort n, vars sort n i)). clear H2.
assert (∀ i : I, eval_stmt (et_sig et)
(λ (sort : sorts (et_sig et)) (n : nat), vars sort n i)
(entailment_as_conjunctive_statement (et_sig et) s)).
intros.
rewrite <- boring_eval_entailment.
apply (H3 i).
clear H3.
rewrite boring_eval_entailment.
destruct s.
simpl in *.
destruct entailment_conclusion.
simpl in *.
destruct i.
simpl in *.
intro.
apply component_equality_to_product with
(λ i, eval et (λ sort n, vars sort n i) t) (λ i, eval et (λ sort n, vars sort n i) t0).
intro.
apply H2. clear H2. simpl.
induction entailment_premises. simpl in *.
intuition.
simpl.
rewrite <- (nqe_always (fst (projT2 a)) vars i).
rewrite <- (nqe_always (snd (projT2 a)) vars i).
intuition.
apply H3.
apply IHentailment_premises.
apply H3.
apply nqe_always.
apply nqe_always.
Qed. (* todo: clean up! also, we shouldn't have to go through boring.. *)
Global Instance product_variety: InVariety et carrier (e:=carrier_e).
Proof.
constructor. apply product_algebra. intro i. apply _.
apply laws_hold.
Qed.
End varieties.
Require MathClasses.categories.varieties.
Section categorical.
Context
(et: EquationalTheory).
Global Instance: Producer (varieties.Object et) := λ I carriers,
{| varieties.variety_carriers := λ s, ∀ i, carriers i s
; varieties.variety_proof := product_variety et I _ _ _ (fun H => varieties.variety_proof et (carriers H)) |}.
(* todo: clean up *)
Section for_a_given_c.
Context (I: Type) (c: I → varieties.Object et).
Global Program Instance: ElimProduct c (product c) := λ i _ c, c i.
Next Obligation.
apply (@algebra_projection_morphisms et I c
(λ x, @varieties.variety_equiv et (c x)) (λ x, varieties.variety_ops et (c x)) ).
intro. apply _.
Qed.
Global Program Instance: IntroProduct c (product c) := λ H h a X i, h i a X.
Next Obligation. Proof with intuition.
repeat constructor; try apply _.
intros ?? E ?. destruct h. simpl. rewrite E...
intro o.
pose proof (λ i, @preserves _ _ _ _ _ _ _ _ (proj2_sig (h i)) o) as H0.
unfold product_ops, algebra_op.
set (o0 := λ i, varieties.variety_ops et (c i) o).
set (o1 := varieties.variety_ops et H o) in *.
change (∀i : I, Preservation et H (c i) (` (h i)) o1 (o0 i)) in H0.
clearbody o0 o1. revert o0 o1 H0.
induction (et o); simpl...
apply (@product_algebra et I c)...
Qed.
Global Instance: Product c (product c).
Proof.
split; repeat intro. reflexivity.
symmetry. simpl. apply H.
Qed.
End for_a_given_c.
Global Instance: HasProducts (varieties.Object et) := {}.
End categorical.
(* Todo: Lots of cleanup. *)
|
