1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/relations.ma".
16 include "basics/types.ma".
17 include "arithmetics/nat.ma".
18 include "hints_declaration.ma".
19 include "basics/core_notation/invert_1.ma".
21 (******************* Quotienting in type theory **********************)
23 (* One fundamental operation in set theory is quotienting: given a set S
24 and an equivalence relation R over S, quotienting creates a new set S/R
25 whose elements are equivalence classes of elements of S. The idea behind
26 quotienting is to replace the structural equality over S with R, therefore
27 identifying elements up to R. The use of equivalence classes is just a
30 The type theory of Matita does not have quotient types. In the litterature
31 there are alternative proposals to introduce quotient types, but no consensus
32 have been reached yet. Nevertheless, quotient types can be dispensed and
33 replaced by setoids. A setoid is defined as a type S coupled with an
34 equivalence relation R, used to compare elements of S. In place of working
35 with equivalence classes of S up to R, one keeps working with elements of S,
36 but compares them using R in place of =. Setoids over types (elements of
37 Type[0]) can be declared in Matita as follows. *)
39 record equivalence_relation (A: Type[0]) : Type[0] ≝ {
41 ; equiv_refl: reflexive … eqrel
42 ; equiv_sym: symmetric … eqrel
43 ; equiv_trans: transitive … eqrel
46 record setoid : Type[1] ≝ {
48 ; eq_setoid: equivalence_relation carrier
51 (* Note that carrier has been defined as a coercion so that when S is a setoid
52 we can write x:S in place of x: carrier S. *)
54 (* We use the notation ≃ for the equality on setoid elements. *)
55 notation "hvbox(n break ≃ m)"
56 non associative with precedence 45
57 for @{ 'congruent $n $m }.
59 interpretation "eq_setoid" 'congruent n m = (eqrel ? (eq_setoid ?) n m).
61 (* Example: integers as pairs of naturals (n,m) quotiented by
62 (n1,m1) ≝ (n2,m2) iff n1 + m2 = m1 + n2. The integer +n is represented
63 by any pair (k,n+k), while the integer -n by any pair (n+k,n).
64 The three proof obligations are to prove reflexivity, symmetry and
65 transitivity. Only the latter is not closed by automation. *)
66 definition Z: setoid ≝
68 (mk_equivalence_relation …
69 (λc1,c2. \fst c1 + \snd c2 = \fst c2 + \snd c1) …).
70 whd // * #x1 #x2 * #y1 #y2 * #z1 #z3 #H1 #H2
71 cut (x1 + y2 + y1 + z3 = y1 + x2 + z1 + y2) // #H3
72 cut ((y2 + y1) + (x1 + z3) = (y2 + y1) + (z1 + x2)) // #H4
73 @(injective_plus_r … H4)
76 (* The two integers (0,1) and (1,2) are equal up to ≃, written
77 〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to
78 eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two
79 pairs are to be compare according to the equivalence relation
80 of an unknown setoid ? whose carrier is ℕ × ℕ. An hint can be
81 used to always pick Z as the setoid for ℕ × ℕ. *)
83 unification hint 0 ≔ ;
85 (* ---------------------------------------- *) ⊢
88 (* Thanks to the hint, Matita now accepts the statement. *)
89 example ex1: 〈0,1〉 ≃ 〈1,2〉.
93 (* Every type is a setoid when elements are compared up to Leibniz equality. *)
94 definition LEIBNIZ: Type[0] → setoid ≝
97 (mk_equivalence_relation … (eq …) …).
101 (* Note that we declare the hint with a lower precedence level (10 vs 0,
102 precedence levels are in decreasing order). In this way an ad-hoc setoid
103 hint will be always preferred to the Leibniz one. for example,
104 〈0,1〉 ≃ 〈1,2〉 is still interpreted in Z, while 1 ≃ 2 is interpreted as 1=2. *)
105 unification hint 10 ≔ A: Type[0];
107 (* ---------------------------------------- *) ⊢
110 (* Propositions up to coimplication form a setoid. *)
111 definition PROP: setoid ≝
113 (mk_equivalence_relation … (λx,y. x ↔ y) …).
114 whd [ @iff_trans | @iff_sym | /2/ ]
117 unification hint 0 ≔ ;
119 (* ---------------------------------------- *) ⊢
122 (* In set theory functions and relations over a quotient S/R can be defined
123 by lifting a function/relation over S that respects R. Respecting R means that
124 the relations holds for an element x of S iff it holds for every y of S such
125 that x R y. Similarly, a function f respects R iff f x = f y for every x,y
126 such that x R y. In type theory propositions are just special cases of
127 functions whose codomain is Prop.
129 Note that in the definition of respect for functions in set theory f x and
130 f y are compared using =. When working with setoids in type theory we need
131 to systematically abandon = in favour of ≃, unless we know in advance that
132 a certain type taken in input is never going to be quotiented. We say that
133 a function between two setoids is proper when it respects their equalities. *)
135 definition proper: ∀I,O:setoid. (I → O) → Prop ≝
136 λI,O,f. ∀x,y:I. x ≃ y → f x ≃ f y.
138 (* A proper function is called a morphism. *)
139 record morphism (I,O: setoid) : Type[0] ≝ {
141 ; mor_proper: proper … mor_carr
144 (* We introduce a notation for morphism using the symbols of an arrow followed by a dot. *)
145 notation "hvbox(I break ⤞ O)"
146 right associative with precedence 20
147 for @{ 'morphism $I $O }.
149 interpretation "morphism" 'morphism I O = (morphism I O).
151 (* By declaring mor_carr as a coercion it is possible to write f x for
152 mor_carr f x in order to apply a morphism f to an argument. *)
154 (* Example: opposite of an integer number. We first implement the function
155 over Z and then lift it to a morphism. The proof obligation is to prove
157 definition opp: Z → Z ≝ λc.〈\snd c,\fst c〉.
159 definition OPP: Z ⤞ Z ≝ mk_morphism … opp ….
163 (* When writing expressions over Z we will always use the function opp, that
164 does not carry additional information. The following hints will be automatically
165 used by the system to retrieve the morphism associated to opp when needed, i.e.
166 to retrieve the proof of properness of opp. This is a use of unification hints
167 to implement automatic proof search. The first hint is used when the function
168 is partially applied, the second one when it is applied to an argument. *)
170 unification hint 0 ≔ ;
172 (* ---------------------------------------- *) ⊢
175 unification hint 0 ≔ x:Z ;
177 (* ---------------------------------------- *) ⊢
178 opp x ≡ mor_carr … X x.
180 (* Example: we state that opp is proper and we will prove it without using
181 automation and without referring to OPP. When we apply the universal mor_proper
182 property of morphisms, Matita looks for the morphism associate to opp x and
183 finds it thanks to the second unification hint above, completing the proof. *)
184 example ex2: ∀x,y. x ≃ y → opp x ≃ opp y.
185 #x #y #EQ @mor_proper @EQ
188 (* The previous definition of proper only deals with unary functions. In type
189 theory n-ary functions are better handled in Curryfied form as unary functions
190 whose output is a function space type. When we restrict to morphisms, we do not
191 need a notion of properness for n-ary functions because the function space can
192 also be seen as a setoid quotienting functions using functional extensionality:
193 two morphisms are equal when they map equal elements to equal elements. *)
194 definition function_space: setoid → setoid → setoid ≝
197 (mk_equivalence_relation … (λf,g. ∀x,y:I. x ≃ y → f x ≃ g y) …).
199 [ #f1 #f2 #f3 #f1_f2 #f2_f3 #x #y #EQ @(equiv_trans … (f2 x)) /2/
200 | #f1 #f2 #f1_f2 #x #y #EQ @(equiv_sym … (f1_f2 …)) @equiv_sym //
201 | #f #x #y #EQ @mor_proper // ]
204 unification hint 0 ≔ I,O: setoid;
205 X ≟ function_space I O
206 (* ---------------------------------------- *) ⊢
209 (* We overload the notation so that I ⤞ O can mean both the type of morphisms
210 from I to O or the function space from I to O. *)
211 interpretation "function_space" 'morphism I O = (function_space I O).
213 (* A binary morphism is just obtained by Currification. In the following
214 we will use I1 ⤞ I2 ⤞ O directly in place of bin_morphism. *)
215 definition bin_morphism: setoid → setoid → setoid → Type[0] ≝
216 λI1,I2,O. I1 ⤞ I2 ⤞ O.
218 (* Directly inhabiting a binary morphism is annoying because one needs to
219 write a function that returns a morphism in place of a binary function.
220 Moreover, there are two proof obligations to prove. We can simplify the work
221 by introducing a new constructor for binary morphisms that takes in input a
222 binary function and opens a single proof obligation, called proper2. *)
223 definition proper2: ∀I1,I2,O: setoid. (I1 → I2 → O) → Prop ≝
225 ∀x1,x2,y1,y2. x1 ≃ x2 → y1 ≃ y2 → f x1 y1 ≃ f x2 y2.
227 definition mk_bin_morphism:
228 ∀I1,I2,O: setoid. ∀f: I1 → I2 → O. proper2 … f → I1 ⤞ I2 ⤞ O ≝
230 mk_morphism … (λx. mk_morphism … (λy. f x y) …) ….
234 (* We can also coerce a binary morphism to a binary function and prove that
235 proper2 holds for every binary morphism. *)
236 definition binary_function_of_binary_morphism:
237 ∀I1,I2,O: setoid. (I1 ⤞ I2 ⤞ O) → (I1 → I2 → O) ≝
238 λI1,I2,O,f,x,y. f x y.
240 coercion binary_function_of_binary_morphism:
241 ∀I1,I2,O: setoid. ∀f:I1 ⤞ I2 ⤞ O. (I1 → I2 → O) ≝
242 binary_function_of_binary_morphism
243 on _f: ? ⤞ ? ⤞ ? to ? → ? → ?.
245 theorem mor_proper2: ∀I1,I2,O: setoid. ∀f: I1 ⤞ I2 ⤞ O. proper2 … f.
246 #I2 #I2 #O #f #x1 #x2 #y1 #y2 #EQx #EQy @(mor_proper … f … EQx … EQy)
249 (* Example: addition of integer numbers. We define addition as a function
250 before lifting it to a morphism and declaring the hints to automatically
251 prove it proper when needed. *)
252 definition Zplus: Z → Z → Z ≝ λx,y. 〈\fst x + \fst y,\snd x + \snd y〉.
254 (* We overload + over integers. *)
255 interpretation "Zplus" 'plus x y = (Zplus x y).
257 definition ZPLUS: Z ⤞ Z ⤞ Z ≝ mk_bin_morphism … Zplus ….
258 normalize * #x1a #x1b * //
261 unification hint 0 ≔ x,y:Z ;
263 (* ---------------------------------------- *) ⊢
264 x + y ≡ mor_carr … X x y.
266 (* The identity function is a morphism and composition of morphisms is also
267 a morphism. This means that the identity function is always proper and
268 a compound context is proper if every constituent is. *)
269 definition id_morphism: ∀S: setoid. S ⤞ S ≝
270 λS. mk_morphism … (λx.x) ….
274 definition comp_morphism: ∀S1,S2,S3. (S2 ⤞ S3) → (S1 ⤞ S2) → (S1 ⤞ S3) ≝
275 λS1,S2,S3,f1,f2. mk_morphism … (λx. f1 (f2 x)) ….
276 normalize #x1 #x2 #EQ @mor_proper @mor_proper //
280 (* The following hint is an example of proof automation rule. It says that
281 f1 (f2 x) can be seen to be the application of the morphism
282 comp_morphism F1 F2 to x as long as two morphisms F1 and F2 can be
283 associated to f1 and f2. *)
285 S1,S2,S3: setoid, f1: S2 → S3, f2: S1 → S2, x:S1, F1: S2 ⤞ S3, F2: S1 ⤞ S2;
288 X ≟ comp_morphism … F1 F2
289 (* ---------------------------------------- *) ⊢
290 f1 (f2 x) ≡ mor_carr … X x. *)
292 (* By iterating applications of mor_proper, we can consume the context bit by
293 bit in order to perform a rewriting. Like in ex2, the script works on any
294 setoid because it does not reference OPP anywhere. The above theorem on
295 composition of morphisms justify the correctness of the scripts. *)
296 example ex3: ∀x,y. x ≃ y → opp (opp (opp x)) ≃ opp (opp (opp y)).
297 #x #y #EQ @mor_proper @mor_proper @mor_proper @EQ
300 (* We can improve the readability of the previous script by assigning
301 a notation to mor_proper and by packing together the various applications
302 of mor_proper and EQ. We pick the prefix symbol †. *)
303 notation "† c" with precedence 90 for @{'proper $c }.
305 interpretation "mor_proper" 'proper c = (mor_proper ????? c).
307 example ex3': ∀x,y. x ≃ y → opp (opp (opp x)) ≃ opp (opp (opp y)).
308 #x #y #EQ @(†(†(†EQ)))
311 (* While the term (†(†(†EQ))) can seem puzzling at first, note that it
312 closely matches the term (opp (opp (opp x))). Each occurrence of the
313 unary morphism opp is replaced by † and the occurrence x to be rewritten to y
314 is replaced by EQ: x ≃ y. Therefore the term (†(†(†EQ))) is a compact
315 notation to express at once where the rewriting should be performed and
316 what hypothesis should be used for the rewriting. We will explain now
317 the problem of rewriting setoid equalities in full generality, and a lightweight
320 (****** Rewriting setoid equalities *********)
322 (* In set theory, once a quotient S/R has been defined, its elements are
323 compared using the standard equality = whose main property is that of replacing
324 equals to equals in every context. If E1=E2 then f E1 can be replaced with f E2
325 for every context f. Note that f is applied to equivalence classes of elements
326 of S. Therefore every function and property in f must have been lifted to work
327 on equivalence classes, and this was possible only if f respected R.
329 When using setoids we keep working with elements of S instead of forming a new
330 type. Therefore, we must deal with contexts f that are not proper. When f is
331 not proper, f E1 cannot be replaced with f E2 even if E1 ≃ E2. For example,
332 〈0,1〉 ≃ 〈1,2〉 but \fst 〈0,1〉 ≠ \fst 〈1,2〉. Therefore every time we want to
333 rewrite E1 with E2 under the assumption that E1 ≃ E2 we need to prove the
334 context to be proper. Most of the time the context is just a composition of
335 morphisms and, like in ex3', the only information that the user needs to
336 give to the system is the position of the occurrences of E1 to be replaced
337 and the equations to be used for the rewriting. As for ex3', we can provide
338 a simple syntax to describe contexts and equations at the same time. The
339 syntax is just given by a few notations to hide applications of mor_proper,
340 reflexivity, symmetry and transitivity.
342 Here is a synopsis of the syntax:
343 - †_ to rewrite in the argument of a unary morphism
344 - _‡_ to rewrite in both arguments of a binary morphism
345 - # to avoid rewriting in this position
346 - t to rewrite from left to right in this position using the proof t.
347 Usually t is the name of an hypothesis in the context of type E1 ≃ E2
348 - t^-1 to rewrite from right to left in this position using the proof t.
349 Concretely, it applies symmetry to t, proving E2 ≃ E1 from E1 ≃ E2.
350 - ._ to start rewriting when the goal is not an equation ≃.
351 Concretely, it applies the proof of P E2 → P E1 obtained by splitting
352 the double implication P E2 ↔ P E1, which is equivalent to P E2 ≃ P E1
353 where ≃ is the equality of the PROP setoid. Thus the argument should
354 be a proof of P E2 ≃ P E1, obtained using the previous symbols according
356 - .=_ to prove an equation G1 ≃ G2 by first rewriting into E1 leaving a new
357 goal G1' ≃ G2. Concretely, it applies transitivity of ≃.
360 notation "l ‡ r" with precedence 90 for @{'proper2 $l $r }.
362 interpretation "mor_proper2" 'proper2 x y = (mor_proper ? (function_space ? ?) ?? ? x ?? y).
364 notation "#" with precedence 90 for @{'reflex}.
366 interpretation "reflexivity" 'reflex = (equiv_refl ???).
368 interpretation "symmetry" 'invert r = (equiv_sym ???? r).
370 notation ".= r" with precedence 55 for @{'trans $r}.
372 interpretation "transitivity" 'trans r = (equiv_trans ????? r ?).
374 notation ". r" with precedence 55 for @{'fi $r}.
376 definition fi: ∀A,B:Prop. A ≃ B → (B → A) ≝ λA,B,r. proj2 ?? r.
378 interpretation "fi" 'fi r = (fi ?? r).
380 (* The following example shows several of the features at once:
381 1. the first occurrence of x2 is turned into x1 by rewriting the hypothesis
383 2. the first occurrence of x1 is turned into x2 by rewriting the hypothesis
385 3. the two rewritings are performed at once.
386 4. the subterm z+y does not need to be rewritten. Therefore a single # is
387 used in place of #‡#, which is also correct but produces a larger proof.
388 5. we can directly start with an application of ‡ because the goal is a
390 example ex4: ∀x1,x2,y,z:Z. x1 ≃ x2 →
391 (y + x2) + (x1 + (z + y)) ≃ (y + x1) + (x2 + (z + y)).
392 #x1 #x2 #y #z #EQ @((#‡EQ^-1)‡(EQ‡#))
395 (* The following example is just to illustrate the use of .=. We prove the
396 same statement of ex4, but this time we perform one rewriting at a time.
397 Note that in an intermediate goal Matita replaces occurrences of Zplus with
398 occurrences of (the carrier of) ZPLUS. To recover the notation + it is
399 sufficient to expand the declaration of ZPLUS. *)
400 example ex5: ∀x1,x2,y,z:Z. x1 ≃ x2 →
401 (y + x2) + (x1 + (z + y)) ≃ (y + x1) + (x2 + (z + y)).
402 #x1 #x2 #y #z #EQ @(.=(#‡EQ^-1)‡#) whd in match ZPLUS; @(#‡(EQ‡#))
405 (* Our last example involves rewriting under a predicate different from ≃.
406 We first introduce such a predicate over integers. *)
407 definition is_zero: Z → Prop ≝ λc. \fst c = \snd c.
409 definition IS_ZERO: Z ⤞ PROP ≝ mk_morphism … is_zero ….
410 normalize /3 by conj,injective_plus_r/
413 unification hint 0 ≔ x:Z ;
415 (* ---------------------------------------- *) ⊢
416 is_zero x ≡ mor_carr … X x.
418 (* We can rewrite under any predicate starting with . *)
419 example ex6: ∀x,y:Z. x ≃ y → is_zero (x + y) → is_zero (x + x).
420 #x #y #EQ #H @(.†(#‡EQ)) @H
423 (****** Dependent setoids ********)
425 (* A setoid is essentially a type equipped with its own notion of equality.
426 In a dependent type theory, one expects to be able to both build types (and
427 setoids) dependent on other types (and setoids). Working with families of
428 setoids that depend over a plain type --- i.e. not another setoid --- pauses
429 no additional problem. For example, we can build a setoid out of vectors of
430 length n assigning to it the type ℕ → setoid. All the machinery for setoids
431 just introduced keeps working. On the other hand, types that depend over a
432 setoid require a much more complex machinery and, in practice, it is not
433 advised to try to work with them in an intentional type theory like the one
436 To understand the issue, imagine that we have defined a family of
437 types I dependent over integers: I: Z → Type. Because 〈0,1〉 and 〈1,2〉 both
438 represent the same integer +1, the two types I 〈0,1〉 and of I 〈1,2〉 should have
439 exactly the same inhabitants. However, being different types, their inhabitants
440 are disjoint. The solution is to equip the type I with a transport function
441 t: ∀n,m:Z. n ≃ m → I n → I m that maps an element of I n to the corresponding
442 element of I m. Starting from this idea, the picture quickly becomes complex
443 when one start considering all the additional equations that the transport
444 functions should satisfy. For example, if p: n ≃ m, then t … p (t … p^-1 x) = x,
445 i.e. the element in I n corresponding to the element in I m that corresponds to
446 x in I n should be exactly x. Moreover, for any function f: ∀n. I n → T n for
447 some other type T dependent over n the following equation should hold:
448 f … (t … p x) = t … p (f … x) (i.e. transporting and applying f should commute
449 because f should be insensitive too up to ≃ to the actual representation of the
452 Luckily enough, in practice types dependent overs setoids occur very rarely.
453 Most examples of dependent types are indexed over discrete objects, like
454 natural, integers and rationals, that admit an unique representation.
455 For continuity reasons, types dependent over real numbers can also be
456 represented as types dependent over a dense subset of the reals, like the
459 (****** Avoiding setoids *******)
461 (* Quotients are used pervasively in mathematics. In many practical situations,
462 for example when dealing with finite objects like pairs of naturals, an unique
463 representation can be imposed, for example by introducing a normalization
464 procedure to be called after every operation. For example, integer numbers can
465 be normalized to either 〈0,n〉 or 〈n,0〉. Or they can be represented as either 0
466 or a non zero number, with the latter being encoded by a boolean (the sign) and
467 a natural (the predecessor of the absolute value). For example, -3 would be
468 represented by NonZero 〈false,2〉, +3 by NonZero 〈true,2〉 and 0 by Zero.
469 Rational numbers n/m can be put in normal form by dividing both n and m by their
470 greatest common divisor, or by picking n=0, m=1 when n is 0. These normal form
471 is an unique representation.
473 Imposing an unique representation is not always possible. For example, picking
474 a canonical representative for a Cauchy sequence is not a computable operation.
475 Nevertheless, when possible, avoiding setoids is preferrable:
476 1) when the Leibniz equality is used, replacing n with m knowing n=m does not
477 require any proof of properness
478 2) at the moment automation in Matita is only available for Leibniz equalities.
479 By switching to setoids less proofs are automatically found
480 3) types dependent over plain types do not need ad-hoc transport functions
481 because the rewriting principle for Leibniz equality plays that role and
482 already satisfies for free all required equations
483 4) normal forms are usually smaller than other forms. By sticking to normal
484 forms both the memory consumption and the computational cost of operations