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 is a important part of every formalization, not only from 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 --------------------------------------------
77 CIC is a full and functional Pure Type System (all products do exist,
78 and their sort is is determined by the target) with an impedicative sort
79 Prop and a predicative sort Type. The environment can be populated with
80 well typed definitions or theorems, (co)inductive types validating positivity
81 conditions and recursive functions provably total by simple syntactical
82 analysis (recursive call on structurally smaller subterms). Co-recursive
83 functions can be defined as well, and must satisfy a dual condition, that is
84 performing the recursive call only after having generated a constructor (a piece
87 The λ-calculus is equipped with a pattern matching construct (match) on inductive
88 types defined in the environment that combined with the definable total
89 structural recursive functions allows to define eliminators (or constructors)
90 for (co)inductive types. The λ-calculus is also equipped with explicitly types
91 local definitions (let in) that in the degenerate case work as casts (i.e.
92 the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
94 Types are compare up to conversion. Since types may depend on terms, conversion
95 involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
96 definition unfolding), ι-reduction (pattern matching simplification),
97 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
100 Since we are going to formalize constructive and predicative mathematics
101 in an intensional type theory like CIC, we try to establish some terminology.
102 Type is the sort of sets equipped with the Id equality (i.e. an intensional,
103 not quotiented set). We will avoid using Leibnitz equality Id,
104 thus we will explicitly equip a set with an equality when needed.
105 We will call this structure `setoid`. Note that we will
106 attach the infix = symbol only to the equality of a setoid,
109 We write Type[i] to mention a Type in the predicative hierarchy
110 of types. To ease the comprehension we will use Type[0] for sets,
111 and Type[1] for classes.
113 For every Type[i] there is a corresponding level of predicative
114 propositions CProp[i].
117 The standard library and the `include` command
118 ----------------------------------------------
120 Some basic notions, like subset, membership, intersection and union
121 are part of the standard library of Matita.
123 These notions come with some standard notation attached to them:
125 - A ∪ B can be typed with `A \cup B`
126 - A ∩ B can be typed with `A \cap B`
127 - A ≬ B can be typed with `A \between B`
128 - x ∈ A can be typed with `x \in A`
129 - Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A`
131 The `include` command tells Matita to load a part of the library,
132 in particular the part that we will use can be loaded as follows:
136 include "sets/sets.ma".
140 Some basic results that we will use are also part of the sets library:
142 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
143 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
148 A set of axioms is made of a set S, a family of sets I and a
149 family C of subsets of S indexed by elements a of S and I(a).
151 It is desirable to state theorems like "for every set of axioms, …"
152 without explicitly mentioning S, I and C. To do that, the three
153 components have to be grouped into a record (essentially a dependently
154 typed tuple). The system is able to generate the projections
155 of the record for free, and they are named as the fields of
156 the record. So, given a axiom set `A` we can obtain the set
157 with `S A`, the family of sets with `I A` and the family of subsets
162 nrecord Ax : Type[1] ≝ {
165 C : ∀a:S. I a → Ω ^ S
170 Forget for a moment the `:>` that will be detailed later, and focus on
171 the record definition. It is made of a list of pairs: a name, followed
172 by `:` and the its type. It is a dependently typed tuple, thus
173 already defined names (fields) can be used in the types that follow.
175 Note that `S` is declared to be a `setoid` and not a Type. The original
176 paper probably also considers I to generate setoids, and both I and C
177 to be morphisms. For the sake of simplicity, we will "cheat" and use
178 setoids only when strictly needed (i.e. where we want to talk about
179 equality). Setoids will play a role only when we will define
180 the alternative version of the axiom set.
182 Note that the field `S` was declared with `:>` instead of a simple `:`.
183 This declares the `S` projection to be a coercion. A coercion is
184 a function case the system automatically inserts when it is needed.
185 In that case, the projection `S` has type `Ax → setoid`, and whenever
186 the expected type of a term is `setoid` while its type is `Ax`, the
187 system inserts the coercion around it, to make the whole term well types.
189 When formalizing an algebraic structure, declaring the carrier as a
190 coercion is a common practice, since it allows to write statements like
192 ∀G:Group.∀x:G.x * x^-1 = 1
194 The quantification over `x` of type `G` is ill-typed, since `G` is a term
195 (of type `Group`) and thus not a type. Since the carrier projection
196 `carr` of `G` is a coercion, that maps a `Group` into the type of
197 its elements, the system automatically inserts `carr` around `G`,
198 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
199 when it displays a term.
201 In this particular case, the coercion `S` allows to write
205 Since `A` is not a type, but it can be turned into a `setoid` by `S`
206 and a `setoid` can be turned into a type by its `carr` projection, the
207 composed coercion `carr ∘ S` is silently inserted.
212 Something that is not still satisfactory, is that the dependent type
213 of `I` and `C` are abstracted over the Axiom set. To obtain the
214 precise type of a term, you can use the `ncheck` command as follows.
223 One would like to write `I a` and not `I A a` under a context where
224 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
225 mechanism simply `A`). In Matita, a question mark represents an implicit
226 argument, i.e. a missing piece of information the system is asked to
227 infer. Matita performs some sort of type inference, thus writing
228 `I ? a` is enough: since the second argument of `I` is typed by the
229 first one, the first one can be inferred just computing the type of `a`.
233 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
237 This is still not completely satisfactory, since you have always type
238 `?`; to fix this minor issue we have to introduce the notational
239 support built in Matita.
244 Matita is quipped with a quite complex notational support,
245 allowing the user to define and use mathematical notations
246 ([From Notation to Semantics: There and Back Again][1]).
248 Since notations are usually ambiguous (e.g. the frequent overloading of
249 symbols) Matita distinguishes between the term level, the
250 content level, and the presentation level, allowing multiple
251 mappings between the content and the term level.
253 The mapping between the presentation level (i.e. what is typed on the
254 keyboard and what is displayed in the sequent window) and the content
255 level is defined with the `notation` command. When followed by
256 `>`, it defines an input (only) notation.
260 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
261 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
265 The first notation defines the writing `𝐈 a` where `a` is a generic
266 term of precedence 90, the maximum one. This high precedence forces
267 parentheses around any term of a lower precedence. For example `𝐈 x`
268 would be accepted, since identifiers have precedence 90, but
269 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
270 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
272 To obtain the `𝐈` is enough to type `I` and then cycle between its
273 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
274 regular letters or the round parentheses, thus their variants (like the
275 bold ones) have to be used.
277 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
278 new content element to which a term `$a` is passed.
280 Content elements have to be interpreted, and possibly multiple,
281 incompatible, interpretations can be defined.
285 interpretation "I" 'I a = (I ? a).
286 interpretation "C" 'C a i = (C ? a i).
290 The `interpretation` command allows to define the mapping between
291 the content level and the terms level. Here we associate the `I` and
292 `C` projections of the Axiom set record, where the Axiom set is an implicit
293 argument `?` to be inferred by the system.
295 Interpretation are bi-directional, thus when displaying a term like
296 `C _ a i`, the system looks for a presentation for the content element
301 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
302 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
306 For output purposes we can define more complex notations, for example
307 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
308 the size of the arguments and lowering their baseline (i.e. putting them
309 as subscript), separating them with a comma followed by a little space.
311 The first (technical) definition
312 --------------------------------
314 Before defining the cover relation as an inductive predicate, one
315 has to notice that the infinity rule uses, in its hypotheses, the
316 cover relation between two subsets, while the inductive predicate
317 we are going to define relates an element and a subset.
319 An option would be to unfold the definition of cover between subsets,
320 but we prefer to define the abstract notion of cover between subsets
321 (so that we can attach a (ambiguous) notation to it).
323 Anyway, to ease the understanding of the definition of the cover relation
324 between subsets, we first define the inductive predicate unfolding the
325 definition, and we later refine it with.
329 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
330 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
331 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
335 We defined the xcover (x will be removed in the final version of the
336 definition) as an inductive predicate. The arity of the inductive
337 predicate has to be carefully analyzed:
339 > (A : Ax) (U : Ω^A) : A → CProp[0]
341 The syntax separates with `:` abstractions that are fixed for every
342 constructor (introduction rule) and abstractions that can change. In that
343 case the parameter `U` is abstracted once and forall in front of every
344 constructor, and every occurrence of the inductive predicate is applied to
345 `U` in a consistent way. Arguments abstracted on the right of `:` are not
346 constant, for example the xcinfinity constructor introduces `a ◃ U`,
347 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
348 had side of the predicate changes, thus it has to be abstracted (in the arity
349 of the inductive predicate) on the right of `:`.
353 (* ncheck xcreflexivity. *)
357 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
358 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
360 This notion has to be abstracted over the cover relation (whose
361 type is the arity of the inductive `xcover` predicate just defined).
363 Then it has to be abstracted over the arguments of that cover relation,
364 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
365 sitting on the left hand side of `◃`.
369 ndefinition cover_set :
370 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
372 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
376 The `ndefinition` command takes a name, a type and body (of that type).
377 The type can be omitted, and in that case it is inferred by the system.
378 If the type is given, the system uses it to infer implicit arguments
379 of the body. In that case all types are left implicit in the body.
381 We now define the notation `a ◃ b`. Here the keywork `hvbox`
382 and `break` tell the system how to wrap text when it does not
383 fit the screen (they can be safely ignore for the scope of
384 this tutorial). We also add an interpretation for that notation,
385 where the (abstracted) cover relation is implicit. The system
386 will not be able to infer it from the other arguments `C` and `U`
387 and will thus prompt the user for it. This is also why we named this
388 interpretation `covers set temp`: we will later define another
389 interpretation in which the cover relation is the one we are going to
394 notation "hvbox(a break ◃ b)" non associative with precedence 45
395 for @{ 'covers $a $b }.
397 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
404 We can now define the cover relation using the `◃` notation for
405 the premise of infinity.
409 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
410 | creflexivity : ∀a. a ∈ U → cover ? U a
411 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
412 (** screenshot "cover". *)
418 Note that the system accepts the definition
419 but prompts the user for the relation the `cover_set` notion is
424 The horizontal line separates the hypotheses from the conclusion.
425 The `napply cover` command tells the system that the relation
426 it is looking for is exactly our first context entry (i.e. the inductive
427 predicate we are defining, up to α-conversion); while the `nqed` command
428 ends a definition or proof.
430 We can now define the interpretation for the cover relation between an
431 element and a subset fist, then between two subsets (but this time
432 we fixed the relation `cover_set` is abstracted on).
436 interpretation "covers" 'covers a U = (cover ? U a).
437 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
441 We will proceed similarly for the fish relation, but before going
442 on it is better to give a short introduction to the proof mode of Matita.
443 We define again the `cover_set` term, but this time we will build
444 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
445 and terms share the same syntax, and it is thus possible to use the
446 commands devoted to build proof term to build regular definitions.
447 A tentative semantics for the proof mode commands (called tactics)
448 in terms of sequent calculus rules are given in the
449 <a href="#appendix">appendix</a>.
453 ndefinition xcover_set :
454 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
455 (** screenshot "xcover-set-1". *)
456 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
457 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
458 napply cover; (** screenshot "xcover-set-4". *)
466 The system asks for a proof of the full statement, in an empty context.
468 The `#` command is the ∀-introduction rule, it gives a name to an
469 assumption putting it in the context, and generates a λ-abstraction
473 We have now to provide a proposition, and we exhibit it. We left
474 a part of it implicit; since the system cannot infer it it will
475 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
479 The proposition we want to provide is an application of the
480 cover relation we have abstracted in the context. The command
481 `napply`, if the given term has not the expected type (in that
482 case it is a product versus a proposition) it applies it to as many
483 implicit arguments as necessary (in that case `? ? ?`).
486 The system will now ask in turn the three implicit arguments
487 passed to cover. The syntax `##[` allows to start a branching
488 to tackle every sub proof individually, otherwise every command
489 is applied to every subrpoof. The command `##|` switches to the next
490 subproof and `##]` ends the branching.
498 The definition of fish works exactly the same way as for cover, except
499 that it is defined as a coinductive proposition.
502 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
507 notation "hvbox(a break ⋉ b)" non associative with precedence 45
508 for @{ 'fish $a $b }.
510 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
512 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
513 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
517 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
518 interpretation "fish" 'fish a U = (fish ? U a).
522 Introction rule for fish
523 ------------------------
525 Matita is able to generate elimination rules for inductive types,
526 but not introduction rules for the coinductive case.
530 (* ncheck cover_rect_CProp0. *)
534 We thus have to define the introduction rule for fish by corecursion.
535 Here we again use the proof mode of Matita to exhibit the body of the
536 corecursive function.
540 nlet corec fish_rec (A:Ax) (U: Ω^A)
542 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
543 (** screenshot "def-fish-rec-1". *)
544 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
545 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
546 napply H1; (** screenshot "def-fish-rec-3". *)
548 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
549 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
550 @; (** screenshot "def-fish-rec-6". *)
552 ##| @; (** screenshot "def-fish-rec-7". *)
554 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
563 Note the first item of the context, it is the corecursive function we are
564 defining. This item allows to perform the recursive call, but we will be
565 allowed to do such call only after having generated a constructor of
566 the fish coinductive type.
568 We introduce `a` and `p`, and then return the fish constructor `cfish`.
569 Since the constructor accepts two arguments, the system asks for them.
572 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
573 With the `nchange` tactic we change `H1` into an equivalent form (this step
574 can be skipped, since the system would be able to unfold the definition
575 of inclusion by itself)
578 It is now clear that `H1` can be applied. Again `napply` adds two
579 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
580 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
581 `a`, and it asks a proof that `a ∈ P`.
584 The `nassumption` tactic looks for the required proof in the context, and in
585 that cases finds it in the last context position.
587 We move now to the second branch of the proof, corresponding to the second
588 argument of the `cfish` constructor.
590 We introduce `i` and then we destruct `H2 a p i`, that being a proof
591 of an overlap predicate, give as an element and a proof that it is
592 both in `𝐂 a i` and `P`.
595 We then introduce `x`, break the conjunction (the `*;` command is the
596 equivalent of `ncases` but operates on the first hypothesis that can
597 be introduced. We then introduce the two sides of the conjunction.
600 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
601 We thus need to use the introduction rule for the existential quantifier.
602 In CIC it is a defined notion, that is an inductive type with just
603 one constructor (one introduction rule) holding the witness and the proof
604 that the witness satisfies a proposition.
608 Instead of trying to remember the name of the constructor, that should
609 be used as the argument of `napply`, we can ask the system to find by
610 itself the constructor name and apply it with the `@` tactic.
611 Note that some inductive predicates, like the disjunction, have multiple
612 introduction rules, and thus `@` can be followed by a number identifying
616 After choosing `x` as the witness, we have to prove a conjunction,
617 and we again apply the introduction rule for the inductively defined
621 The left hand side of the conjunction is trivial to prove, since it
622 is already in the context. The right hand side needs to perform
623 the co-recursive call.
626 The co-recursive call needs some arguments, but all of them live
627 in the context. Instead of explicitly mention them, we use the
628 `nassumption` tactic, that simply tries to apply every context item.
634 Subset of covered/fished points
635 -------------------------------
637 We now have to define the subset of `S` of points covered by `U`.
638 We also define a prefix notation for it. Remember that the precedence
639 of the prefix form of a symbol has to be lower than the precedence
644 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
646 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
648 interpretation "coverage cover" 'coverage U = (coverage ? U).
652 Here we define the equation characterizing the cover relation.
653 In the igft.ma file we proved that `◃U` is the minimum solution for
654 such equation, the interested reader should be able to reply the proof
659 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
660 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
662 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
665 ##[ #bU; @1; nassumption;
666 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
668 ##| #_; napply CaiU; nassumption; ##] ##]
669 ##| ncases H; ##[ #E; @; nassumption]
670 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
674 ntheorem coverage_min_cover_equation :
675 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
676 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
677 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
678 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
684 We similarly define the subset of point fished by `F`, the
685 equation characterizing `⋉F` and prove that fish is
686 the biggest solution for such equation.
690 notation "⋉F" non associative with precedence 55
693 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
695 interpretation "fished fish" 'fished F = (fished ? F).
697 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
698 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
700 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
701 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
702 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
704 ##| #aF; #H1; @ aF; napply H1;
708 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
709 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
710 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
715 Part 2, the new set of axioms
716 -----------------------------
718 Since the name of objects (record included) has to unique
719 within the same script, we prefix every field name
720 in the new definition of the axiom set with `n`.
724 nrecord nAx : Type[2] ≝ {
727 nD: ∀a:nS. nI a → Type[0];
728 nd: ∀a:nS. ∀i:nI a. nD a i → nS
733 We again define a notation for the projections, making the
734 projected record an implicit argument. Note that since we already have
735 a notation for `𝐈` we just add another interpretation for it. The
736 system, looking at the argument of `𝐈`, will be able to use
737 the correct interpretation.
741 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
742 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
744 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
745 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
747 interpretation "D" 'D a i = (nD ? a i).
748 interpretation "d" 'd a i j = (nd ? a i j).
749 interpretation "new I" 'I a = (nI ? a).
753 The paper defines the image as
755 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
757 but this not so formal notation poses some problems. The image is
758 often used as the left hand side of the ⊆ predicate
762 Of course this writing is interpreted by the authors as follows
764 > ∀j:D(a,i). d(a,i,j) ∈ V
766 If we need to use the image to define 𝐂 (a subset of S) we are obliged to
767 form a subset, i.e. to place a single variable `{ here | … }`.
769 > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
771 This poses no theoretical problems, since `S` is a setoid and thus equipped
774 Unless we difene two different images, one for stating the image is ⊆ of
775 something and another one to define 𝐂, we end up using always the latter.
776 Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
778 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
780 That up to rewriting with the equation defining `x` is what we mean. The
781 technical problem arises when `V` is a complex construction that has to
782 be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
786 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
788 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
789 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
791 interpretation "image" 'Im a i = (image ? a i).
795 Thanks to our definition of image, we ca trivially a function mapping a
796 new axiom set to an old one and viceversa. Note that in the second
797 definition, when defining 𝐝, the projection of the Σ type is inlined
798 (constructed on the fly by `*;`) while in the paper it was named `fst`.
802 ndefinition Ax_of_nAx : nAx → Ax.
803 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
806 ndefinition nAx_of_Ax : Ax → nAx.
808 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
809 ##| #a; #i; *; #x; #_; napply x;
815 We then define the inductive type of ordinals, parametrized over an axiom
816 set. We also attach some notations to the constructors.
820 ninductive Ord (A : nAx) : Type[0] ≝
823 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
825 notation "0" non associative with precedence 90 for @{ 'oO }.
826 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
827 notation "x+1" non associative with precedence 50 for @{'oS $x }.
829 interpretation "ordinals Zero" 'oO = (oO ?).
830 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
831 interpretation "ordinals Succ" 'oS x = (oS ? x).
835 The dfinition of `U_x` is by recursion over the ordinal `x`.
836 We thus define a recursive function. The `on x` directive tells
837 the system on which argument the function is (structurally) recursive.
839 In the `oS` case we use a local definition to name the recursive call
840 since it is used twice.
842 Note that Matita does not support notation in the left hand side
843 of a pattern match, and thus the names of the constructors have to
844 be spelled out verbatim.
848 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
851 | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
852 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
854 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
855 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
857 interpretation "famU" 'famU U x = (famU ? U x).
861 We attach as the input notation for U_x the similar `U⎽x` where underscore,
862 that is a character valid for identifier names, has been replaced by `⎽` that is
863 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
864 for `_` (i.e. pressing ALT-L after `_`).
866 The notion ◃(U) has to be defined as the subset of of y
867 belonging to U_x for some x. Moreover, we have to define the notion
868 of cover between sets again, since the one defined at the beginning
869 of the tutorial works only for the old axiom set definition.
873 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
875 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
876 ∀y.y ∈ C → y ∈ c A U.
878 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
879 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
880 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
884 Before proving that this cover relation validates the reflexivity and infinity
885 rules, we prove this little technical lemma that is used in the proof for the
890 nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
891 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
896 The proof of infinity uses the following form of the Axiom of choice,
897 that cannot be prove inside Matita, since the existential quantifier
898 lives in the sort of predicative propositions while the sigma in the conclusion
899 lives in the sort of data types, and thus the former cannot be eliminated
900 to provide the second.
904 naxiom AC : ∀A,a,i,U.
905 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
909 In the proof of infinity, we have to rewrite under the ∈ predicate.
910 It is clearly possible to show that U_x is an extensional set:
912 > a = b → a ∈ U_x → b ∈ U_x
914 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
915 declared as morphisms. This poses to problem, but goes out of the scope of the
916 tutorial and we thus assume it.
920 naxiom setoidification: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
924 The reflexivity proof is trivial, it is enough to provide the ordinal 0
925 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
928 ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
929 #A; #U; #a; #H; @ (0); napply H;
934 We now proceed with the proof of the infinity rule.
938 alias symbol "covers" = "new covers set".
939 alias symbol "covers" = "new covers".
940 alias symbol "covers" = "new covers set".
941 alias symbol "covers" = "new covers".
942 alias symbol "covers" = "new covers set".
943 alias symbol "covers" = "new covers".
944 alias symbol "covers" = "new covers set".
945 ntheorem new_coverage_infinity:
946 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
947 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
948 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
949 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
950 #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
951 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
952 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
953 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
954 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
955 @2; (** screenshot "n-cov-inf-8". *)
956 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
957 napply (setoidification … Hd); napply Hf';
962 We eliminate the existential, obtaining an `i` and a proof that the
963 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
964 form of `H`, thus expands the definition of cover between sets.
967 The paper proof considers `H` implicitly substitutes the equation assumed
968 by `H` in its conclusion. In Matita this step is not completely trivia.
969 We thus assert (`ncut`) the nicer form of `H`.
972 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
973 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
974 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
975 the `#` is a standard notation for the reflexivity property of the equality.
978 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
982 The paper proof does now a forward reasoning step, deriving (by the ord_subset
983 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
986 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
989 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
990 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
991 the second constructor `@2;` of the disjunction, we are left to prove that `a`
992 belongs to the right hand side.
995 We thus provide `i`, introduce the element being in the image and we are
996 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
997 to the image means that there exists an object in the domain… we eliminate the
998 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
1001 We just need to use the equational definition of `x` to obtain a conclusion
1002 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
1003 every `x`, thus we are allowed to use `Hd` and close the proof.
1009 The next proof is that ◃(U) is mininal. The hardest part of the proof
1010 is to prepare the goal for the induction. The desiderata is to prove
1011 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
1012 unfolding all definitions:
1014 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
1018 nlemma new_coverage_min :
1019 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1020 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
1021 *; #o; (** screenshot "n-cov-min-3". *)
1022 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
1023 nelim o; (** screenshot "n-cov-min-5". *)
1024 ##[ #b; #bU0; napply HUV; napply bU0;
1025 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1026 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1027 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1032 After all the introductions, event the element hidden in the ⊆ definition,
1033 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1036 What is left is almost right, but the element `b` is already in the
1037 context. We thus generalize every occurrence of `b` in
1038 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1041 We then proceed by induction on `o` obtaining the following goals
1044 All of them can be proved using simple set theoretic arguments,
1045 the induction hypothesis and the assumption `Im`.
1052 The notion `F_x` is again defined by recursion over the ordinal `x`.
1056 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1059 | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
1060 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1063 interpretation "famF" 'famU U x = (famF ? U x).
1065 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1067 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1068 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1072 The proof of compatibility uses this little result, that we
1073 proved outside the mail proof.
1076 nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1077 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1082 We assume the dual of the axiom of choice, as in the paper proof.
1085 naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
1086 (∀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.
1090 Proving the anti-reflexivity property is simple, since the
1091 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1092 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
1095 ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1096 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1104 ntheorem new_fish_compatible:
1105 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1106 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
1107 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
1108 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
1110 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1111 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
1112 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
1113 *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
1129 The proof that `⋉(F)` is maximal is exactly the dual one of the
1130 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1131 before doing the induction over `o`.
1134 ntheorem max_new_fished:
1135 ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1136 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1137 ngeneralize in match HbG; ngeneralize in match b;
1138 nchange with (G ⊆ F⎽o);
1141 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1142 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1144 alias symbol "prop2" = "prop21".
1145 napply (. Ed^-1‡#); napply cG;
1146 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1147 #b; #Hb; #d; napply (Hf d); napply Hb;
1153 <div id="appendix" class="anchor"></div>
1154 Appendix: tactics explanation
1155 -----------------------------
1157 In this appendix we try to give a description of tactics
1158 in terms of sequent calculus rules annotated with proofs.
1159 The `:` separator has to be read as _is a proof of_, in the spirit
1160 of the Curry-Howard isomorphism.
1162 Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
1163 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1164 Γ ⊢ (f ?1 … ?n ) : B
1166 Γ ⊢ ? : F → B Γ ⊢ f : F
1167 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1172 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1173 Γ ⊢ λx:T.? : ∀x:T.P(x)
1176 Γ ⊢ ?_i : args_i → P(k_i args_i)
1177 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1178 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1181 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1182 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1183 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1185 Where `T_rect_CProp0` is the induction principle for the
1189 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1192 Where the equivalence relation between types `≡` keeps into account
1193 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1194 definition unfolding), ι-reduction (pattern matching simplification),
1195 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1199 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1200 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1205 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1206 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1211 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1219 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf