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 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
122 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
125 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
126 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
129 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
130 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
133 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
134 sig_intro : ∀x:A.P x → sigma A P.
136 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
141 Some basic results that we will use are also part of the sets library:
143 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
144 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
149 A set of axioms is made of a set S, a family of sets I and a
150 family C of subsets of S indexed by elements a of S and I(a).
152 It is desirable to state theorems like "for every set of axioms, …"
153 without explicitly mentioning S, I and C. To do that, the three
154 components have to be grouped into a record (essentially a dependently
155 typed tuple). The system is able to generate the projections
156 of the record for free, and they are named as the fields of
157 the record. So, given a axiom set `A` we can obtain the set
158 with `S A`, the family of sets with `I A` and the family of subsets
163 nrecord Ax : Type[1] ≝ {
166 C : ∀a:S. I a → Ω ^ S
171 Forget for a moment the `:>` that will be detailed later, and focus on
172 the record definition. It is made of a list of pairs: a name, followed
173 by `:` and the its type. It is a dependently typed tuple, thus
174 already defined names (fields) can be used in the types that follow.
176 Note that `S` is declared to be a `setoid` and not a Type. The original
177 paper probably also considers I to generate setoids, and both I and C
178 to be morphisms. For the sake of simplicity, we will "cheat" and use
179 setoids only when strictly needed (i.e. where we want to talk about
180 equality). Setoids will play a role only when we will define
181 the alternative version of the axiom set.
183 Note that the field `S` was declared with `:>` instead of a simple `:`.
184 This declares the `S` projection to be a coercion. A coercion is
185 a function case the system automatically inserts when it is needed.
186 In that case, the projection `S` has type `Ax → setoid`, and whenever
187 the expected type of a term is `setoid` while its type is `Ax`, the
188 system inserts the coercion around it, to make the whole term well types.
190 When formalizing an algebraic structure, declaring the carrier as a
191 coercion is a common practice, since it allows to write statements like
193 ∀G:Group.∀x:G.x * x^-1 = 1
195 The quantification over `x` of type `G` is ill-typed, since `G` is a term
196 (of type `Group`) and thus not a type. Since the carrier projection
197 `carr` of `G` is a coercion, that maps a `Group` into the type of
198 its elements, the system automatically inserts `carr` around `G`,
199 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
200 when it displays a term.
202 In this particular case, the coercion `S` allows to write
206 Since `A` is not a type, but it can be turned into a `setoid` by `S`
207 and a `setoid` can be turned into a type by its `carr` projection, the
208 composed coercion `carr ∘ S` is silently inserted.
213 Something that is not still satisfactory, is that the dependent type
214 of `I` and `C` are abstracted over the Axiom set. To obtain the
215 precise type of a term, you can use the `ncheck` command as follows.
224 One would like to write `I a` and not `I A a` under a context where
225 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
226 mechanism simply `A`). In Matita, a question mark represents an implicit
227 argument, i.e. a missing piece of information the system is asked to
228 infer. Matita performs some sort of type inference, thus writing
229 `I ? a` is enough: since the second argument of `I` is typed by the
230 first one, the first one can be inferred just computing the type of `a`.
234 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
238 This is still not completely satisfactory, since you have always type
239 `?`; to fix this minor issue we have to introduce the notational
240 support built in Matita.
245 Matita is quipped with a quite complex notational support,
246 allowing the user to define and use mathematical notations
247 ([From Notation to Semantics: There and Back Again][1]).
249 Since notations are usually ambiguous (e.g. the frequent overloading of
250 symbols) Matita distinguishes between the term level, the
251 content level, and the presentation level, allowing multiple
252 mappings between the content and the term level.
254 The mapping between the presentation level (i.e. what is typed on the
255 keyboard and what is displayed in the sequent window) and the content
256 level is defined with the `notation` command. When followed by
257 `>`, it defines an input (only) notation.
261 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
262 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
266 The first notation defines the writing `𝐈 a` where `a` is a generic
267 term of precedence 90, the maximum one. This high precedence forces
268 parentheses around any term of a lower precedence. For example `𝐈 x`
269 would be accepted, since identifiers have precedence 90, but
270 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
271 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
273 To obtain the `𝐈` is enough to type `I` and then cycle between its
274 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
275 regular letters or the round parentheses, thus their variants (like the
276 bold ones) have to be used.
278 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
279 new content element to which a term `$a` is passed.
281 Content elements have to be interpreted, and possibly multiple,
282 incompatible, interpretations can be defined.
286 interpretation "I" 'I a = (I ? a).
287 interpretation "C" 'C a i = (C ? a i).
291 The `interpretation` command allows to define the mapping between
292 the content level and the terms level. Here we associate the `I` and
293 `C` projections of the Axiom set record, where the Axiom set is an implicit
294 argument `?` to be inferred by the system.
296 Interpretation are bi-directional, thus when displaying a term like
297 `C _ a i`, the system looks for a presentation for the content element
302 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
303 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
307 For output purposes we can define more complex notations, for example
308 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
309 the size of the arguments and lowering their baseline (i.e. putting them
310 as subscript), separating them with a comma followed by a little space.
312 The first (technical) definition
313 --------------------------------
315 Before defining the cover relation as an inductive predicate, one
316 has to notice that the infinity rule uses, in its hypotheses, the
317 cover relation between two subsets, while the inductive predicate
318 we are going to define relates an element and a subset.
320 An option would be to unfold the definition of cover between subsets,
321 but we prefer to define the abstract notion of cover between subsets
322 (so that we can attach a (ambiguous) notation to it).
324 Anyway, to ease the understanding of the definition of the cover relation
325 between subsets, we first define the inductive predicate unfolding the
326 definition, and we later refine it with.
330 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
331 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
332 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
336 We defined the xcover (x will be removed in the final version of the
337 definition) as an inductive predicate. The arity of the inductive
338 predicate has to be carefully analyzed:
340 > (A : Ax) (U : Ω^A) : A → CProp[0]
342 The syntax separates with `:` abstractions that are fixed for every
343 constructor (introduction rule) and abstractions that can change. In that
344 case the parameter `U` is abstracted once and forall in front of every
345 constructor, and every occurrence of the inductive predicate is applied to
346 `U` in a consistent way. Arguments abstracted on the right of `:` are not
347 constant, for example the xcinfinity constructor introduces `a ◃ U`,
348 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
349 had side of the predicate changes, thus it has to be abstracted (in the arity
350 of the inductive predicate) on the right of `:`.
354 (* ncheck xcreflexivity. *)
358 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
359 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
361 This notion has to be abstracted over the cover relation (whose
362 type is the arity of the inductive `xcover` predicate just defined).
364 Then it has to be abstracted over the arguments of that cover relation,
365 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
366 sitting on the left hand side of `◃`.
370 ndefinition cover_set :
371 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
373 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
377 The `ndefinition` command takes a name, a type and body (of that type).
378 The type can be omitted, and in that case it is inferred by the system.
379 If the type is given, the system uses it to infer implicit arguments
380 of the body. In that case all types are left implicit in the body.
382 We now define the notation `a ◃ b`. Here the keywork `hvbox`
383 and `break` tell the system how to wrap text when it does not
384 fit the screen (they can be safely ignore for the scope of
385 this tutorial). We also add an interpretation for that notation,
386 where the (abstracted) cover relation is implicit. The system
387 will not be able to infer it from the other arguments `C` and `U`
388 and will thus prompt the user for it. This is also why we named this
389 interpretation `covers set temp`: we will later define another
390 interpretation in which the cover relation is the one we are going to
395 notation "hvbox(a break ◃ b)" non associative with precedence 45
396 for @{ 'covers $a $b }.
398 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
405 We can now define the cover relation using the `◃` notation for
406 the premise of infinity.
410 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
411 | creflexivity : ∀a. a ∈ U → cover ? U a
412 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
413 (** screenshot "cover". *)
419 Note that the system accepts the definition
420 but prompts the user for the relation the `cover_set` notion is
425 The horizontal line separates the hypotheses from the conclusion.
426 The `napply cover` command tells the system that the relation
427 it is looking for is exactly our first context entry (i.e. the inductive
428 predicate we are defining, up to α-conversion); while the `nqed` command
429 ends a definition or proof.
431 We can now define the interpretation for the cover relation between an
432 element and a subset fist, then between two subsets (but this time
433 we fixed the relation `cover_set` is abstracted on).
437 interpretation "covers" 'covers a U = (cover ? U a).
438 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
442 We will proceed similarly for the fish relation, but before going
443 on it is better to give a short introduction to the proof mode of Matita.
444 We define again the `cover_set` term, but this time we will build
445 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
446 and terms share the same syntax, and it is thus possible to use the
447 commands devoted to build proof term to build regular definitions.
448 A tentative semantics for the proof mode commands (called tactics)
449 in terms of sequent calculus rules are given in the
450 <a href="#appendix">appendix</a>.
454 ndefinition xcover_set :
455 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
456 (** screenshot "xcover-set-1". *)
457 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
458 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
459 napply cover; (** screenshot "xcover-set-4". *)
467 The system asks for a proof of the full statement, in an empty context.
469 The `#` command is the ∀-introduction rule, it gives a name to an
470 assumption putting it in the context, and generates a λ-abstraction
474 We have now to provide a proposition, and we exhibit it. We left
475 a part of it implicit; since the system cannot infer it it will
476 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
480 The proposition we want to provide is an application of the
481 cover relation we have abstracted in the context. The command
482 `napply`, if the given term has not the expected type (in that
483 case it is a product versus a proposition) it applies it to as many
484 implicit arguments as necessary (in that case `? ? ?`).
487 The system will now ask in turn the three implicit arguments
488 passed to cover. The syntax `##[` allows to start a branching
489 to tackle every sub proof individually, otherwise every command
490 is applied to every subrpoof. The command `##|` switches to the next
491 subproof and `##]` ends the branching.
499 The definition of fish works exactly the same way as for cover, except
500 that it is defined as a coinductive proposition.
503 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
508 notation "hvbox(a break ⋉ b)" non associative with precedence 45
509 for @{ 'fish $a $b }.
511 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
513 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
514 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
518 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
519 interpretation "fish" 'fish a U = (fish ? U a).
523 Introction rule for fish
524 ------------------------
526 Matita is able to generate elimination rules for inductive types,
527 but not introduction rules for the coinductive case.
531 (* ncheck cover_rect_CProp0. *)
535 We thus have to define the introduction rule for fish by corecursion.
536 Here we again use the proof mode of Matita to exhibit the body of the
537 corecursive function.
541 nlet corec fish_rec (A:Ax) (U: Ω^A)
543 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
544 (** screenshot "def-fish-rec-1". *)
545 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
546 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
547 napply H1; (** screenshot "def-fish-rec-3". *)
549 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
550 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
551 @; (** screenshot "def-fish-rec-6". *)
553 ##| @; (** screenshot "def-fish-rec-7". *)
555 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
564 Note the first item of the context, it is the corecursive function we are
565 defining. This item allows to perform the recursive call, but we will be
566 allowed to do such call only after having generated a constructor of
567 the fish coinductive type.
569 We introduce `a` and `p`, and then return the fish constructor `cfish`.
570 Since the constructor accepts two arguments, the system asks for them.
573 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
574 With the `nchange` tactic we change `H1` into an equivalent form (this step
575 can be skipped, since the system would be able to unfold the definition
576 of inclusion by itself)
579 It is now clear that `H1` can be applied. Again `napply` adds two
580 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
581 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
582 `a`, and it asks a proof that `a ∈ P`.
585 The `nassumption` tactic looks for the required proof in the context, and in
586 that cases finds it in the last context position.
588 We move now to the second branch of the proof, corresponding to the second
589 argument of the `cfish` constructor.
591 We introduce `i` and then we destruct `H2 a p i`, that being a proof
592 of an overlap predicate, give as an element and a proof that it is
593 both in `𝐂 a i` and `P`.
596 We then introduce `x`, break the conjunction (the `*;` command is the
597 equivalent of `ncases` but operates on the first hypothesis that can
598 be introduced. We then introduce the two sides of the conjunction.
601 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
602 We thus need to use the introduction rule for the existential quantifier.
603 In CIC it is a defined notion, that is an inductive type with just
604 one constructor (one introduction rule) holding the witness and the proof
605 that the witness satisfies a proposition.
609 Instead of trying to remember the name of the constructor, that should
610 be used as the argument of `napply`, we can ask the system to find by
611 itself the constructor name and apply it with the `@` tactic.
612 Note that some inductive predicates, like the disjunction, have multiple
613 introduction rules, and thus `@` can be followed by a number identifying
617 After choosing `x` as the witness, we have to prove a conjunction,
618 and we again apply the introduction rule for the inductively defined
622 The left hand side of the conjunction is trivial to prove, since it
623 is already in the context. The right hand side needs to perform
624 the co-recursive call.
627 The co-recursive call needs some arguments, but all of them live
628 in the context. Instead of explicitly mention them, we use the
629 `nassumption` tactic, that simply tries to apply every context item.
635 Subset of covered/fished points
636 -------------------------------
638 We now have to define the subset of `S` of points covered by `U`.
639 We also define a prefix notation for it. Remember that the precedence
640 of the prefix form of a symbol has to be lower than the precedence
645 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
647 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
649 interpretation "coverage cover" 'coverage U = (coverage ? U).
653 Here we define the equation characterizing the cover relation.
654 In the igft.ma file we proved that `◃U` is the minimum solution for
655 such equation, the interested reader should be able to reply the proof
660 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
661 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
663 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
665 ##[ nelim H; #b; (* manca clear *)
666 ##[ #bU; @1; nassumption;
667 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
669 ##| #_; napply CaiU; nassumption; ##] ##]
670 ##| ncases H; ##[ #E; @; nassumption]
671 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
675 ntheorem coverage_min_cover_equation :
676 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
677 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
678 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
679 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
685 We similarly define the subset of point fished by `F`, the
686 equation characterizing `⋉F` and prove that fish is
687 the biggest solution for such equation.
691 notation "⋉F" non associative with precedence 55
694 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
696 interpretation "fished fish" 'fished F = (fished ? F).
698 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
699 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
701 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
702 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
703 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
705 ##| #aF; #H1; @ aF; napply H1;
709 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
710 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
711 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
716 Part 2, the new set of axioms
717 -----------------------------
719 Since the name of objects (record included) has to unique
720 within the same script, we prefix every field name
721 in the new definition of the axiom set with `n`.
725 nrecord nAx : Type[2] ≝ {
728 nD: ∀a:nS. nI a → Type[0];
729 nd: ∀a:nS. ∀i:nI a. nD a i → nS
734 We again define a notation for the projections, making the
735 projected record an implicit argument. Note that since we already have
736 a notation for `𝐈` we just add another interpretation for it. The
737 system, looking at the argument of `𝐈`, will be able to use
738 the correct interpretation.
742 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
743 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
745 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
746 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
748 interpretation "D" 'D a i = (nD ? a i).
749 interpretation "d" 'd a i j = (nd ? a i j).
750 interpretation "new I" 'I a = (nI ? a).
754 The paper defines the image as
756 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
758 but this cannot be ..... MAIL
762 Allora ha una comoda interpretazione (che voi usate liberamente)
764 > ∀j:D(a,i). d(a,i,j) ∈ V
766 Ma se voglio usare Im per definire C, che è un subset di S, devo per
767 forza (almeno credo) definire un subset, ovvero dire che
769 > Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
771 Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
772 uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
773 scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
775 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
780 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
782 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
783 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
785 interpretation "image" 'Im a i = (image ? a i).
793 ndefinition Ax_of_nAx : nAx → Ax.
794 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
797 ndefinition nAx_of_Ax : Ax → nAx.
799 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
800 ##| #a; #i; *; #x; #_; napply x;
806 We then define the inductive type of ordinals, parametrized over an axiom
807 set. We also attach some notations to the constructors.
811 ninductive Ord (A : nAx) : Type[0] ≝
814 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
816 notation "0" non associative with precedence 90 for @{ 'oO }.
817 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
818 notation "x+1" non associative with precedence 50 for @{'oS $x }.
820 interpretation "ordinals Zero" 'oO = (oO ?).
821 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
822 interpretation "ordinals Succ" 'oS x = (oS ? x).
826 Note that Matita does not support notation in the left hand side
827 of a pattern match, and thus the names of the constructors have to
828 be spelled out verbatim.
830 BLA let rec. Bla let_in.
834 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
837 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
838 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
840 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
841 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
843 interpretation "famU" 'famU U x = (famU ? U x).
847 We attach as the input notation for U_x the similar `U⎽x` where underscore,
848 that is a character valid for identifier names, has been replaced by `⎽` that is
849 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
850 for `_` (i.e. pressing ALT-L after `_`).
852 The notion ◃(U) has to be defined as the subset of of y
853 belonging to U_x for some x. Moreover, we have to define the notion
854 of cover between sets again, since the one defined at the beginning
855 of the tutorial works only for the old axiom set definition.
859 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
861 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
862 ∀y.y ∈ C → y ∈ c A U.
864 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
865 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
866 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
870 Before proving that this cover relation validates the reflexivity and infinity
871 rules, we prove this little technical lemma that is used in the proof for the
877 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
878 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
883 The proof of infinity uses the following form of the Axiom of choice,
884 that cannot be prove inside Matita, since the existential quantifier
885 lives in the sort of predicative propositions while the sigma in the conclusion
886 lives in the sort of data types, and thus the former cannot be eliminated
887 to provide the second.
891 naxiom AC : ∀A,a,i,U.
892 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
896 In the proof of infinity, we have to rewrite under the ∈ predicate.
897 It is clearly possible to show that U_x is an extensional set:
899 > a=b → a ∈ U_x → b ∈ U_x
901 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
902 declared as morphisms. This poses to problem, but goes out of the scope of the
903 tutorial and we thus assume it.
907 naxiom setoidification :
908 ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
912 The reflexivity proof is trivial, it is enough to provide the ordinal 0
913 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
916 ntheorem new_coverage_reflexive:
917 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
918 #A; #U; #a; #H; @ (0); napply H;
923 We now proceed with the proof of the infinity rule.
927 alias symbol "covers" = "new covers set".
928 alias symbol "covers" = "new covers".
929 alias symbol "covers" = "new covers set".
930 alias symbol "covers" = "new covers".
931 alias symbol "covers" = "new covers set".
932 alias symbol "covers" = "new covers".
933 ntheorem new_coverage_infinity:
934 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
935 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
936 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
937 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
938 #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
939 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
940 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
941 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
942 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
943 @2; (** screenshot "n-cov-inf-8". *)
944 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
945 napply (setoidification … Hd); napply Hf';
950 We eliminate the existential, obtaining an `i` and a proof that the
951 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
952 form of `H`, thus expands the definition of cover between sets.
955 The paper proof considers `H` implicitly substitutes the equation assumed
956 by `H` in its conclusion. In Matita this step is not completely trivia.
957 We thus assert (`ncut`) the nicer form of `H`.
960 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
961 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
962 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
963 the `#` is a standard notation for the reflexivity property of the equality.
966 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
970 The paper proof does now a forward reasoning step, deriving (by the ord_subset
971 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
974 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
977 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
978 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
979 the second constructor `@2;` of the disjunction, we are left to prove that `a`
980 belongs to the right hand side.
983 We thus provide `i`, introduce the element being in the image and we are
984 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
985 to the image means that there exists an object in the domain… we eliminate the
986 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
989 We just need to use the equational definition of `x` to obtain a conclusion
990 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
991 every `x`, thus we are allowed to use `Hd` and close the proof.
997 The next proof is that ◃(U) is mininal. The hardest part of the proof
998 it to prepare the goal for the induction. The desiderata is to prove
999 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
1000 unfolding all definitions:
1002 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
1006 nlemma new_coverage_min :
1007 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1008 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
1009 *; #o; (** screenshot "n-cov-min-3". *)
1010 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
1011 nelim o; (** screenshot "n-cov-min-5". *)
1012 ##[ #b; #bU0; napply HUV; napply bU0;
1013 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1014 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1015 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1020 After all the introductions, event the element hidden in the ⊆ definition,
1021 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1024 What is left is almost right, but the element `b` is already in the
1025 context. We thus generalize every occurrence of `b` in
1026 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1029 We then proceed by induction on `o` obtaining the following goals
1032 All of them can be proved using simple set theoretic arguments,
1033 the induction hypothesis and the assumption `Im`.
1044 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1047 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
1048 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1051 interpretation "famF" 'famU U x = (famF ? U x).
1053 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1055 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1056 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1060 The proof of compatibility uses this little result, that we
1064 nlemma co_ord_subset:
1065 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1066 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1071 We assume the dual of the axiom of choice, as in the paper proof.
1075 ∀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.
1079 Proving the anti-reflexivity property is simce, since the
1080 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1081 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
1084 ntheorem new_fish_antirefl:
1085 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1086 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1094 ntheorem new_fish_compatible:
1095 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1096 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
1097 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
1098 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
1100 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1101 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
1102 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
1103 *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
1119 The proof that `⋉(F)` is maximal is exactly the dual one of the
1120 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1121 before doing the induction over `o`.
1124 ntheorem max_new_fished:
1125 ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1126 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1127 ngeneralize in match HbG; ngeneralize in match b;
1128 nchange with (G ⊆ F⎽o);
1131 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1132 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1134 alias symbol "prop2" = "prop21".
1135 napply (. Ed^-1‡#); napply cG;
1136 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1137 #b; #Hb; #d; napply (Hf d); napply Hb;
1143 <div id="appendix" class="anchor"></div>
1144 Appendix: tactics explanation
1145 -----------------------------
1147 In this appendix we try to give a description of tactics
1148 in terms of sequent calculus rules annotated with proofs.
1149 The `:` separator has to be read as _is a proof of_, in the spirit
1150 of the Curry-Howard isomorphism.
1152 Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
1153 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1154 Γ ⊢ (f ?1 … ?n ) : B
1156 Γ ⊢ ? : F → B Γ ⊢ f : F
1157 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1162 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1163 Γ ⊢ λx:T.? : ∀x:T.P(x)
1166 Γ ⊢ ?_i : args_i → P(k_i args_i)
1167 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1168 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1171 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1172 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1173 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1175 Where `T_rect_CProp0` is the induction principle for the
1179 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1182 Where the equivalence relation between types `≡` keeps into account
1183 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1184 definition unfolding), ι-reduction (pattern matching simplification),
1185 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1189 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1190 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1195 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1196 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1201 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1209 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf