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