3 Matita Tutorial: inductively generated formal topologies
4 ========================================================
6 This is a not so short introduction to Matita, based on
7 the formalization of the paper
9 > Between formal topology and game theory: an
10 > explicit solution for the conditions for an
11 > inductive generation of formal topologies
13 by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
15 The tutorial spends a considerable amount of effort in defining
16 notations that resemble the ones used in the original paper. We believe
17 this a important part of every formalization, not only for the aesthetic
18 point of view, but also from the practical point of view. Being
19 consistent allows to follow the paper in a pedantic way, and hopefully
20 to make the formalization (at least the definitions and proved
21 statements) readable to the author of the paper.
26 The graphical interface of Matita is composed of three windows:
27 the script window, on the left, is where you type; the sequent
28 window on the top right is where the system shows you the ongoing proof;
29 the error window, on the bottom right, is where the system complains.
30 On the top of the script window five buttons drive the processing of
31 the proof script. From left to right the requesting the system to:
33 - go back to the beginning of the script
35 - go to the current cursor position
37 - advance to the end of the script
39 When the system processes a command, it locks the part of the script
40 corresponding to the command, such that you cannot edit it anymore
41 (without to go back). Locked parts are coloured in blue.
43 The sequent window is hyper textual, i.e. you can click on symbols
44 to jump to their definition, or switch between different notation
45 for the same expression (for example, equality has two notations,
46 one of them makes the type of the arguments explicit).
48 Everywhere in the script you can use the `ncheck (term).` command to
49 ask for the type a given term. If you that in the middle of a proof,
50 the term is assumed to live in the current proof context (i.e. can use
51 variables introduced so far).
53 To ease the typing of mathematical symbols, the script window
54 implements two unusual input facilities:
56 - some TeX symbols can be typed using their TeX names, and are
57 automatically converted to UTF-8 characters. For a list of
58 the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
59 Moreover some ASCII-art is understood as well, like `=>` and `->`
60 to mean double or single arrows.
61 Here we recall some of these "shortcuts":
63 - ∀ can be typed with `\Forall`
64 - λ can be typed with `\lambda`
65 - ≝ can be typed with `\def` or `:=`
66 - → can be typed with `to` or `->`
68 - some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
69 The user can cycle between variants typing one of them and then
70 pressing ALT-L. Note that also letters do have variants, for
71 example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
72 Variants are listed in the aforementioned TeX/UTF-8 table.
74 CIC (as implemented in Matita) in a nutshell
75 --------------------------------------------
79 Type is a set equipped with the Id equality (i.e. an intensional,
80 not quotiented set). We will avoid using Leibnitz equality Id,
81 thus we will explicitly equip a set with an equality when needed.
82 We will call this structure `setoid`. Note that we will
83 attach the infix = symbols only to the equality of a setoid,
88 We write Type[i] to mention a Type in the predicative hierarchy
89 of types. To ease the comprehension we will use Type[0] for sets,
90 and Type[1] for classes.
92 For every Type[i] there is a corresponding level of predicative
93 propositions CProp[i].
95 CIC is also equipped with an impredicative sort Prop that we will not
98 The standard library and the `include` command
99 ----------------------------------------------
101 Some basic notions, like subset, membership, intersection and union
102 are part of the standard library of Matita.
104 These notions come with some standard notation attached to them:
108 - A ≬ B `A \between B`
110 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
112 The `include` command tells Matita to load a part of the library,
113 in particular the part that we will use can be loaded as follows:
117 include "sets/sets.ma".
121 Some basic results that we will use are also part of the sets library:
123 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
124 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
129 A set of axioms is made of a set S, a family of sets I and a
130 family C of subsets of S indexed by elements a of S and I(a).
132 It is desirable to state theorems like "for every set of axioms, …"
133 without explicitly mentioning S, I and C. To do that, the three
134 components have to be grouped into a record (essentially a dependently
135 typed tuple). The system is able to generate the projections
136 of the record for free, and they are named as the fields of
137 the record. So, given a axiom set `A` we can obtain the set
138 with `S A`, the family of sets with `I A` and the family of subsets
143 nrecord Ax : Type[1] ≝ {
146 C : ∀a:S. I a → Ω ^ S
151 Forget for a moment the `:>` that will be detailed later, and focus on
152 the record definition. It is made of a list of pairs: a name, followed
153 by `:` and the its type. It is a dependently typed tuple, thus
154 already defined names (fields) can be used in the types that follow.
156 Note that `S` is declared to be a `setoid` and not a Type. The original
157 paper probably also considers I to generate setoids, and both I and C
158 to be morphisms. For the sake of simplicity, we will "cheat" and use
159 setoids only when strictly needed (i.e. where we want to talk about
160 equality). Setoids will play a role only when we will define
161 the alternative version of the axiom set.
163 Note that the field `S` was declared with `:>` instead of a simple `:`.
164 This declares the `S` projection to be a coercion. A coercion is
165 a function case the system automatically inserts when it is needed.
166 In that case, the projection `S` has type `Ax → setoid`, and whenever
167 the expected type of a term is `setoid` while its type is `Ax`, the
168 system inserts the coercion around it, to make the whole term well types.
170 When formalizing an algebraic structure, declaring the carrier as a
171 coercion is a common practice, since it allows to write statements like
173 ∀G:Group.∀x:G.x * x^-1 = 1
175 The quantification over `x` of type `G` is ill-typed, since `G` is a term
176 (of type `Group`) and thus not a type. Since the carrier projection
177 `carr` of `G` is a coercion, that maps a `Group` into the type of
178 its elements, the system automatically inserts `carr` around `G`,
179 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
180 when it displays a term.
182 In this particular case, the coercion `S` allows to write
186 Since `A` is not a type, but it can be turned into a `setoid` by `S`
187 and a `setoid` can be turned into a type by its `carr` projection, the
188 composed coercion `carr ∘ S` is silently inserted.
193 Something that is not still satisfactory, is that the dependent type
194 of `I` and `C` are abstracted over the Axiom set. To obtain the
195 precise type of a term, you can use the `ncheck` command as follows.
204 One would like to write `I a` and not `I A a` under a context where
205 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
206 mechanism simply `A`). In Matita, a question mark represents an implicit
207 argument, i.e. a missing piece of information the system is asked to
208 infer. Matita performs some sort of type inference, thus writing
209 `I ? a` is enough: since the second argument of `I` is typed by the
210 first one, the first one can be inferred just computing the type of `a`.
214 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
218 This is still not completely satisfactory, since you have always type
219 `?`; to fix this minor issue we have to introduce the notational
220 support built in Matita.
225 Matita is quipped with a quite complex notational support,
226 allowing the user to define and use mathematical notations
227 ([From Notation to Semantics: There and Back Again][1]).
229 Since notations are usually ambiguous (e.g. the frequent overloading of
230 symbols) Matita distinguishes between the term level, the
231 content level, and the presentation level, allowing multiple
232 mappings between the content and the term level.
234 The mapping between the presentation level (i.e. what is typed on the
235 keyboard and what is displayed in the sequent window) and the content
236 level is defined with the `notation` command. When followed by
237 `>`, it defines an input (only) notation.
241 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
242 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
246 The first notation defines the writing `𝐈 a` where `a` is a generic
247 term of precedence 90, the maximum one. This high precedence forces
248 parentheses around any term of a lower precedence. For example `𝐈 x`
249 would be accepted, since identifiers have precedence 90, but
250 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
251 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
253 To obtain the `𝐈` is enough to type `I` and then cycle between its
254 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
255 regular letters or the round parentheses, thus their variants (like the
256 bold ones) have to be used.
258 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
259 new content element to which a term `$a` is passed.
261 Content elements have to be interpreted, and possibly multiple,
262 incompatible, interpretations can be defined.
266 interpretation "I" 'I a = (I ? a).
267 interpretation "C" 'C a i = (C ? a i).
271 The `interpretation` command allows to define the mapping between
272 the content level and the terms level. Here we associate the `I` and
273 `C` projections of the Axiom set record, where the Axiom set is an implicit
274 argument `?` to be inferred by the system.
276 Interpretation are bi-directional, thus when displaying a term like
277 `C _ a i`, the system looks for a presentation for the content element
282 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
283 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
287 For output purposes we can define more complex notations, for example
288 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
289 the size of the arguments and lowering their baseline (i.e. putting them
290 as subscript), separating them with a comma followed by a little space.
292 The first (technical) definition
293 --------------------------------
295 Before defining the cover relation as an inductive predicate, one
296 has to notice that the infinity rule uses, in its hypotheses, the
297 cover relation between two subsets, while the inductive predicate
298 we are going to define relates an element and a subset.
300 An option would be to unfold the definition of cover between subsets,
301 but we prefer to define the abstract notion of cover between subsets
302 (so that we can attach a (ambiguous) notation to it).
304 Anyway, to ease the understanding of the definition of the cover relation
305 between subsets, we first define the inductive predicate unfolding the
306 definition, and we later refine it with.
310 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
311 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
312 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
316 We defined the xcover (x will be removed in the final version of the
317 definition) as an inductive predicate. The arity of the inductive
318 predicate has to be carefully analyzed:
320 > (A : Ax) (U : Ω^A) : A → CProp[0]
322 The syntax separates with `:` abstractions that are fixed for every
323 constructor (introduction rule) and abstractions that can change. In that
324 case the parameter `U` is abstracted once and forall in front of every
325 constructor, and every occurrence of the inductive predicate is applied to
326 `U` in a consistent way. Arguments abstracted on the right of `:` are not
327 constant, for example the xcinfinity constructor introduces `a ◃ U`,
328 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
329 had side of the predicate changes, thus it has to be abstracted (in the arity
330 of the inductive predicate) on the right of `:`.
334 (* ncheck xcreflexivity. *)
338 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
339 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
341 This notion has to be abstracted over the cover relation (whose
342 type is the arity of the inductive `xcover` predicate just defined).
344 Then it has to be abstracted over the arguments of that cover relation,
345 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
346 sitting on the left hand side of `◃`.
350 ndefinition cover_set :
351 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
353 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
357 The `ndefinition` command takes a name, a type and body (of that type).
358 The type can be omitted, and in that case it is inferred by the system.
359 If the type is given, the system uses it to infer implicit arguments
360 of the body. In that case all types are left implicit in the body.
362 We now define the notation `a ◃ b`. Here the keywork `hvbox`
363 and `break` tell the system how to wrap text when it does not
364 fit the screen (they can be safely ignore for the scope of
365 this tutorial). We also add an interpretation for that notation,
366 where the (abstracted) cover relation is implicit. The system
367 will not be able to infer it from the other arguments `C` and `U`
368 and will thus prompt the user for it. This is also why we named this
369 interpretation `covers set temp`: we will later define another
370 interpretation in which the cover relation is the one we are going to
375 notation "hvbox(a break ◃ b)" non associative with precedence 45
376 for @{ 'covers $a $b }.
378 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
385 We can now define the cover relation using the `◃` notation for
386 the premise of infinity.
390 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
391 | creflexivity : ∀a. a ∈ U → cover ? U a
392 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
393 (** screenshot "cover". *)
399 Note that the system accepts the definition
400 but prompts the user for the relation the `cover_set` notion is
405 The horizontal line separates the hypotheses from the conclusion.
406 The `napply cover` command tells the system that the relation
407 it is looking for is exactly our first context entry (i.e. the inductive
408 predicate we are defining, up to α-conversion); while the `nqed` command
409 ends a definition or proof.
411 We can now define the interpretation for the cover relation between an
412 element and a subset fist, then between two subsets (but this time
413 we fixed the relation `cover_set` is abstracted on).
417 interpretation "covers" 'covers a U = (cover ? U a).
418 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
422 We will proceed similarly for the fish relation, but before going
423 on it is better to give a short introduction to the proof mode of Matita.
424 We define again the `cover_set` term, but this time we will build
425 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
426 and terms share the same syntax, and it is thus possible to use the
427 commands devoted to build proof term to build regular definitions.
428 A tentative semantics for the proof mode commands (called tactics)
429 in terms of sequent calculus rules are given in the
430 <a href="#appendix">appendix</a>.
434 ndefinition xcover_set :
435 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
436 (** screenshot "xcover-set-1". *)
437 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
438 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
439 napply cover; (** screenshot "xcover-set-4". *)
447 The system asks for a proof of the full statement, in an empty context.
449 The `#` command is the ∀-introduction rule, it gives a name to an
450 assumption putting it in the context, and generates a λ-abstraction
454 We have now to provide a proposition, and we exhibit it. We left
455 a part of it implicit; since the system cannot infer it it will
456 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
460 The proposition we want to provide is an application of the
461 cover relation we have abstracted in the context. The command
462 `napply`, if the given term has not the expected type (in that
463 case it is a product versus a proposition) it applies it to as many
464 implicit arguments as necessary (in that case `? ? ?`).
467 The system will now ask in turn the three implicit arguments
468 passed to cover. The syntax `##[` allows to start a branching
469 to tackle every sub proof individually, otherwise every command
470 is applied to every subrpoof. The command `##|` switches to the next
471 subproof and `##]` ends the branching.
479 The definition of fish works exactly the same way as for cover, except
480 that it is defined as a coinductive proposition.
483 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
488 notation "hvbox(a break ⋉ b)" non associative with precedence 45
489 for @{ 'fish $a $b }.
491 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
493 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
494 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
498 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
499 interpretation "fish" 'fish a U = (fish ? U a).
503 Introction rule for fish
504 ------------------------
506 Matita is able to generate elimination rules for inductive types,
507 but not introduction rules for the coinductive case.
511 (* ncheck cover_rect_CProp0. *)
515 We thus have to define the introduction rule for fish by corecursion.
516 Here we again use the proof mode of Matita to exhibit the body of the
517 corecursive function.
521 nlet corec fish_rec (A:Ax) (U: Ω^A)
523 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
524 (** screenshot "def-fish-rec-1". *)
525 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
526 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
527 napply H1; (** screenshot "def-fish-rec-3". *)
529 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
530 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
531 @; (** screenshot "def-fish-rec-6". *)
533 ##| @; (** screenshot "def-fish-rec-7". *)
535 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
544 Note the first item of the context, it is the corecursive function we are
545 defining. This item allows to perform the recursive call, but we will be
546 allowed to do such call only after having generated a constructor of
547 the fish coinductive type.
549 We introduce `a` and `p`, and then return the fish constructor `cfish`.
550 Since the constructor accepts two arguments, the system asks for them.
553 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
554 With the `nchange` tactic we change `H1` into an equivalent form (this step
555 can be skipped, since the system would be able to unfold the definition
556 of inclusion by itself)
559 It is now clear that `H1` can be applied. Again `napply` adds two
560 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
561 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
562 `a`, and it asks a proof that `a ∈ P`.
565 The `nassumption` tactic looks for the required proof in the context, and in
566 that cases finds it in the last context position.
568 We move now to the second branch of the proof, corresponding to the second
569 argument of the `cfish` constructor.
571 We introduce `i` and then we destruct `H2 a p i`, that being a proof
572 of an overlap predicate, give as an element and a proof that it is
573 both in `𝐂 a i` and `P`.
576 We then introduce `x`, break the conjunction (the `*;` command is the
577 equivalent of `ncases` but operates on the first hypothesis that can
578 be introduced. We then introduce the two sides of the conjunction.
581 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
582 We thus need to use the introduction rule for the existential quantifier.
583 In CIC it is a defined notion, that is an inductive type with just
584 one constructor (one introduction rule) holding the witness and the proof
585 that the witness satisfies a proposition.
589 Instead of trying to remember the name of the constructor, that should
590 be used as the argument of `napply`, we can ask the system to find by
591 itself the constructor name and apply it with the `@` tactic.
592 Note that some inductive predicates, like the disjunction, have multiple
593 introduction rules, and thus `@` can be followed by a number identifying
597 After choosing `x` as the witness, we have to prove a conjunction,
598 and we again apply the introduction rule for the inductively defined
602 The left hand side of the conjunction is trivial to prove, since it
603 is already in the context. The right hand side needs to perform
604 the co-recursive call.
607 The co-recursive call needs some arguments, but all of them live
608 in the context. Instead of explicitly mention them, we use the
609 `nassumption` tactic, that simply tries to apply every context item.
615 Subset of covered/fished points
616 -------------------------------
618 We now have to define the subset of `S` of points covered by `U`.
619 We also define a prefix notation for it. Remember that the precedence
620 of the prefix form of a symbol has to be lower than the precedence
625 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
627 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
629 interpretation "coverage cover" 'coverage U = (coverage ? U).
633 Here we define the equation characterizing the cover relation.
634 In the igft.ma file we proved that `◃U` is the minimum solution for
635 such equation, the interested reader should be able to reply the proof
640 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
641 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
643 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
645 ##[ nelim H; #b; (* manca clear *)
646 ##[ #bU; @1; nassumption;
647 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
649 ##| #_; napply CaiU; nassumption; ##] ##]
650 ##| ncases H; ##[ #E; @; nassumption]
651 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
655 ntheorem coverage_min_cover_equation :
656 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
657 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
658 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
659 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
665 We similarly define the subset of point fished by `F`, the
666 equation characterizing `⋉F` and prove that fish is
667 the biggest solution for such equation.
671 notation "⋉F" non associative with precedence 55
674 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
676 interpretation "fished fish" 'fished F = (fished ? F).
678 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
679 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
681 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
682 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
683 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
685 ##| #aF; #H1; @ aF; napply H1;
689 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
690 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
691 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
696 Part 2, the new set of axioms
697 -----------------------------
699 Since the name of objects (record included) has to unique
700 within the same script, we prefix every field name
701 in the new definition of the axiom set with `n`.
705 nrecord nAx : Type[2] ≝ {
708 nD: ∀a:nS. nI a → Type[0];
709 nd: ∀a:nS. ∀i:nI a. nD a i → nS
714 We again define a notation for the projections, making the
715 projected record an implicit argument. Note that since we already have
716 a notation for `𝐈` we just add another interpretation for it. The
717 system, looking at the argument of `𝐈`, will be able to use
718 the correct interpretation.
722 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
723 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
725 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
726 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
728 interpretation "D" 'D a i = (nD ? a i).
729 interpretation "d" 'd a i j = (nd ? a i j).
730 interpretation "new I" 'I a = (nI ? a).
734 The paper defines the image as
736 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
738 but this cannot be ..... MAIL
742 Allora ha una comoda interpretazione (che voi usate liberamente)
744 > ∀j:D(a,i). d(a,i,j) ∈ V
746 Ma se voglio usare Im per definire C, che è un subset di S, devo per
747 forza (almeno credo) definire un subset, ovvero dire che
749 > Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
751 Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
752 uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
753 scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
755 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
760 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
762 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
763 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
765 interpretation "image" 'Im a i = (image ? a i).
773 ndefinition Ax_of_nAx : nAx → Ax.
774 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
777 ndefinition nAx_of_Ax : Ax → nAx.
779 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
780 ##| #a; #i; *; #x; #_; napply x;
786 We then define the inductive type of ordinals, parametrized over an axiom
787 set. We also attach some notations to the constructors.
791 ninductive Ord (A : nAx) : Type[0] ≝
794 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
796 notation "0" non associative with precedence 90 for @{ 'oO }.
797 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
798 notation "x+1" non associative with precedence 50 for @{'oS $x }.
800 interpretation "ordinals Zero" 'oO = (oO ?).
801 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
802 interpretation "ordinals Succ" 'oS x = (oS ? x).
806 Note that Matita does not support notation in the left hand side
807 of a pattern match, and thus the names of the constructors have to
808 be spelled out verbatim.
810 BLA let rec. Bla let_in.
814 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
817 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
818 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
820 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
821 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
823 interpretation "famU" 'famU U x = (famU ? U x).
827 We attach as the input notation for U_x the similar `U⎽x` where underscore,
828 that is a character valid for identifier names, has been replaced by `⎽` that is
829 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
830 for `_` (i.e. pressing ALT-L after `_`).
832 The notion ◃(U) has to be defined as the subset of of y
833 belonging to U_x for some x. Moreover, we have to define the notion
834 of cover between sets again, since the one defined at the beginning
835 of the tutorial works only for the old axiom set definition.
839 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
841 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
842 ∀y.y ∈ C → y ∈ c A U.
844 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
845 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
846 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
850 Before proving that this cover relation validates the reflexivity and infinity
851 rules, we prove this little technical lemma that is used in the proof for the
857 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
858 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
863 The proof of infinity uses the following form of the Axiom of choice,
864 that cannot be prove inside Matita, since the existential quantifier
865 lives in the sort of predicative propositions while the sigma in the conclusion
866 lives in the sort of data types, and thus the former cannot be eliminated
867 to provide the second.
871 naxiom AC : ∀A,a,i,U.
872 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
876 In the proof of infinity, we have to rewrite under the ∈ predicate.
877 It is clearly possible to show that U_x is an extensional set:
879 > a=b → a ∈ U_x → b ∈ U_x
881 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
882 declared as morphisms. This poses to problem, but goes out of the scope of the
883 tutorial and we thus assume it.
887 naxiom setoidification :
888 ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
892 The reflexivity proof is trivial, it is enough to provide the ordinal 0
893 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
896 ntheorem new_coverage_reflexive:
897 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
898 #A; #U; #a; #H; @ (0); napply H;
903 We now proceed with the proof of the infinity rule.
907 alias symbol "covers" = "new covers set".
908 alias symbol "covers" = "new covers".
909 alias symbol "covers" = "new covers set".
910 alias symbol "covers" = "new covers".
911 alias symbol "covers" = "new covers set".
912 alias symbol "covers" = "new covers".
913 ntheorem new_coverage_infinity:
914 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
915 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
916 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
917 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
918 #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
919 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
920 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
921 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
922 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
923 @2; (** screenshot "n-cov-inf-8". *)
924 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
925 napply (setoidification … Hd); napply Hf';
930 We eliminate the existential, obtaining an `i` and a proof that the
931 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
932 form of `H`, thus expands the definition of cover between sets.
935 The paper proof considers `H` implicitly substitutes the equation assumed
936 by `H` in its conclusion. In Matita this step is not completely trivia.
937 We thus assert (`ncut`) the nicer form of `H`.
940 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
941 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
942 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
943 the `#` is a standard notation for the reflexivity property of the equality.
946 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
950 The paper proof does now a forward reasoning step, deriving (by the ord_subset
951 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
954 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
957 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
958 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
959 the second constructor `@2;` of the disjunction, we are left to prove that `a`
960 belongs to the right hand side.
963 We thus provide `i`, introduce the element being in the image and we are
964 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
965 to the image means that there exists an object in the domain… we eliminate the
966 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
969 We just need to use the equational definition of `x` to obtain a conclusion
970 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
971 every `x`, thus we are allowed to use `Hd` and close the proof.
977 The next proof is that ◃(U) is mininal. The hardest part of the proof
978 it to prepare the goal for the induction. The desiderata is to prove
979 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
980 unfolding all definitions:
982 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
986 nlemma new_coverage_min :
987 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
988 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
989 *; #o; (** screenshot "n-cov-min-3". *)
990 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
991 nelim o; (** screenshot "n-cov-min-5". *)
992 ##[ #b; #bU0; napply HUV; napply bU0;
993 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
994 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
995 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1000 After all the introductions, event the element hidden in the ⊆ definition,
1001 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1004 What is left is almost right, but the element `b` is already in the
1005 context. We thus generalize every occurrence of `b` in
1006 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1009 We then proceed by induction on `o` obtaining the following goals
1012 All of them can be proved using simple set theoretic arguments,
1013 the induction hypothesis and the assumption `Im`.
1024 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1027 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
1028 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1031 interpretation "famF" 'famU U x = (famF ? U x).
1033 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1035 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1036 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1040 The proof of compatibility uses this little result, that we
1044 nlemma co_ord_subset:
1045 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1046 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1051 We assume the dual of the axiom of choice, as in the paper proof.
1055 ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
1059 Proving the anti-reflexivity property is simce, since the
1060 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1061 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
1064 ntheorem new_fish_antirefl:
1065 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1066 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1074 ntheorem new_fish_compatible:
1075 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1076 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
1077 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
1078 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
1080 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1081 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
1082 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
1083 *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
1099 The proof that `⋉(F)` is maximal is exactly the dual one of the
1100 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1101 before doing the induction over `o`.
1104 ntheorem max_new_fished:
1105 ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1106 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1107 ngeneralize in match HbG; ngeneralize in match b;
1108 nchange with (G ⊆ F⎽o);
1111 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1112 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1114 alias symbol "prop2" = "prop21".
1115 napply (. Ed^-1‡#); napply cG;
1116 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1117 #b; #Hb; #d; napply (Hf d); napply Hb;
1123 <div id="appendix" class="anchor"></div>
1124 Appendix: tactics explanation
1125 -----------------------------
1127 In this appendix we try to give a description of tactics
1128 in terms of sequent calculus rules annotated with proofs.
1129 The `:` separator has to be read as _is a proof of_, in the spirit
1130 of the Curry-Howard isomorphism.
1132 Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
1133 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1134 Γ ⊢ (f ?1 … ?n ) : B
1136 Γ ⊢ ? : F → B Γ ⊢ f : F
1137 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1142 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1143 Γ ⊢ λx:T.? : ∀x:T.P(x)
1146 Γ ⊢ ?_i : args_i → P(k_i args_i)
1147 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1148 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1151 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1152 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1153 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1155 Where `T_rect_CProp0` is the induction principle for the
1159 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1162 Where the equivalence relation between types `≡` keeps into account
1163 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1164 definition unfolding), ι-reduction (pattern matching simplification),
1165 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1169 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1170 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1175 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1176 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1181 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1189 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf