3 Inductively generated formal topologies in Matita
4 =================================================
6 This is a not so short introduction to [Matita][2], 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 Stefano Berardi and Silvio Valentini.
15 The tutorial is by Enrico Tassi.
17 The reader should be familiar with inductively generated
18 formal topologies and have some basic knowledge of type theory and λ-calculus.
20 A considerable part of this tutorial is devoted to explain how to define
21 notations that resemble the ones used in the original paper. We believe
22 this is an important part of every formalization, not only from the aesthetic
23 point of view, but also from the practical point of view. Being
24 consistent allows to follow the paper in a pedantic way, and hopefully
25 to make the formalization (at least the definitions and proved
26 statements) readable to the author of the paper.
28 The formalization uses the "new generation" version of Matita
29 (that will be named 1.x when finally released).
30 Last stable release of the "old" system is named 0.5.7; the ng system
31 is coexisting with the old one in all development release
32 (named "nightly builds" in the download page of Matita)
33 with a version strictly greater than 0.5.7.
35 To read this tutorial in HTML format, you need a decent browser
36 equipped with a unicode capable font. Use the PDF format if some
37 symbols are not displayed correctly.
42 The graphical interface of Matita is composed of three windows:
43 the script window, on the left, is where you type; the sequent
44 window on the top right is where the system shows you the ongoing proof;
45 the error window, on the bottom right, is where the system complains.
46 On the top of the script window five buttons drive the processing of
47 the proof script. From left to right they request the system to:
49 - go back to the beginning of the script
51 - go to the current cursor position
53 - advance to the end of the script
55 When the system processes a command, it locks the part of the script
56 corresponding to the command, such that you cannot edit it anymore
57 (without going back). Locked parts are coloured in blue.
59 The sequent window is hyper textual, i.e. you can click on symbols
60 to jump to their definition, or switch between different notations
61 for the same expression (for example, equality has two notations,
62 one of them makes the type of the arguments explicit).
64 Everywhere in the script you can use the `ncheck (term).` command to
65 ask for the type a given term. If you do that in the middle of a proof,
66 the term is assumed to live in the current proof context (i.e. can use
67 variables introduced so far).
69 To ease the typing of mathematical symbols, the script window
70 implements two unusual input facilities:
72 - some TeX symbols can be typed using their TeX names, and are
73 automatically converted to UTF-8 characters. For a list of
74 the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
75 Moreover some ASCII-art is understood as well, like `=>` and `->`
76 to mean double or single arrows.
77 Here we recall some of these "shortcuts":
79 - ∀ can be typed with `\forall`
80 - λ can be typed with `\lambda`
81 - ≝ can be typed with `\def` or `:=`
82 - → can be typed with `\to` or `->`
84 - some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
85 The user can cycle between variants typing one of them and then
86 pressing ALT-L. Note that also letters do have variants, for
87 example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
88 Variants are listed in the aforementioned TeX/UTF-8 table.
90 The syntax of terms (and types) is the one of the λ-calculus CIC
91 on which Matita is based. The main syntactical difference w.r.t.
92 the usual mathematical notation is the function application, written
93 `(f x y)` in place of `f(x,y)`.
95 Pressing `F1` opens the Matita manual.
97 CIC (as [implemented in Matita][3]) in a nutshell
98 -------------------------------------------------
100 CIC is a full and functional Pure Type System (all products do exist,
101 and their sort is is determined by the target) with an impredicative sort
102 Prop and a predicative sort Type. It features both dependent types and
103 polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
104 the same syntax, and they can occur in types.
106 The environment used for in the typing judgement can be populated with
107 well typed definitions or theorems, (co)inductive types validating positivity
108 conditions and recursive functions provably total by simple syntactical
109 analysis (recursive calls are allowed only on structurally smaller subterms).
111 functions can be defined as well, and must satisfy the dual condition, i.e.
112 performing the recursive call only after having generated a constructor (a piece
115 The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
116 types defined in the environment. This construct, together with the possibility to
117 definable total recursive functions, allows to define eliminators (or constructors)
118 for (co)inductive types. The λ-calculus is also equipped with explicitly typed
119 local definitions (let in) that in the degenerate case work as casts (i.e.
120 the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
122 Types are compare up to conversion. Since types may depend on terms, conversion
123 involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
124 definition unfolding), ι-reduction (pattern matching simplification),
125 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
128 Since we are going to formalize constructive and predicative mathematics
129 in an intensional type theory like CIC, we try to establish some terminology.
130 Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
133 We write `Type[i]` to mention a Type in the predicative hierarchy
134 of types. To ease the comprehension we will use `Type[0]` for sets,
135 and `Type[1]` for classes. The index `i` is just a label: constraints among
136 universes are declared by the user. The standard library defines
138 > Type[0] < Type[1] < Type[2]
140 <object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
142 For every `Type[i]` there is a corresponding level of predicative
143 propositions `CProp[i]` (the C initial is due to historical reasons, and
144 stands for constructive, `PProp` would be more appropriate).
145 A predicative proposition cannot be eliminated toward
146 `Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
147 with 0 or 1 constructors with propositional arguments, like `Id` and `And`
150 The distinction between predicative propositions and predicative data types
151 is a peculirity of Matita (for example in CIC as implemented by Coq they are the
152 same). The additional restriction of not allowing the elimination of a CProp
153 toward a Type makes the theory of Matita minimal in the following sense:
155 <object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
157 Theorems proved in CIC as implemented in Matita can be reused in a classical
158 and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
159 constructive propositions and assuming the excluded middle on them).
160 Alternatively, one can decide to collapse predicative propositions and
161 datatypes recovering the Axiom of Choice in the sense of Martin Löf
162 (i.e. ∃ really holds a witness and can be eliminated to inhabit a type).
164 This implementation of CIC is the result of the collaboration with Maietti M.,
165 Sambin G. and Valentini S. of the University of Padua.
167 Formalization choices
168 ---------------------
170 There are many different ways of formalizing the same piece of mathematics
171 in CIC, depending on what our interests are. There is usually a tradeoff
172 between the possibility of reuse the formalization we did and its complexity.
174 In this work, our decisions mainly regarded the following two areas
176 - Equality: Id or not
177 - Axiom of Choice: controlled use or not
182 We will avoid using `Id` (Leibniz equality),
183 thus we will explicitly equip a set with an equivalence relation when needed.
184 We will call this structure a _setoid_. Note that we will
185 attach the infix `=` symbol only to the equality of a setoid,
190 In this paper it is clear that the author is interested in using the Axiom
191 of Choice, thus choosing to identify ∃ and Σ (i.e. working in the
192 leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision
193 (that is, the author of the paper would not complain we formalized something
194 diffrent from what he had in mind).
196 Anyway, we may benefit from the minimality of CIC as implemented in Matita,
197 "asking" the type system to ensure we do no use the Axiom of Choice elswhere
198 in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
199 very beginnig, the system will not complain if we use the Axiom of Choice at all.
200 Moreover, the elimination of an inductive type (like ∃) is a so common operation
201 that the syntax chosen for the elimination command is very compact and non
202 informative, hard to spot for a human being
203 (in fact it is just two characters long!).
205 We decided to formalize the whole paper without identifying
206 CProp and Type and assuming the Axiom of Choice as a real axiom
207 (i.e. a black hole with no computational content, a function with no body).
209 It is clear that this approach give us full control on when/where we really use
210 the Axiom of Choice. But, what are we loosing? What happens to the computational
211 content of the proofs if the Axiom of Choice gives no content back?
214 depends on when we actually look at the computational content of the proof and
215 we "run" that program. We can extract the content and run it before or after
216 informing the system that our propositions are actually code (i.e. identifying
217 ∃ and Σ). If we run the program before, as soon as the computation reaches the
218 Axiom of Choice it stops, giving no output. If we tell the system that CProp and
219 Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
220 and the extracted code would compute an output.
222 Note that the computational
223 content is there even if the Axiom of Choice is an axiom, the difference is
224 just that we cannot use it (the typing rules inhibit the elimination of the
225 existential). This is possible only thanks to the minimality of CIC as implemented
228 The standard library and the `include` command
229 ----------------------------------------------
231 Some basic notions, like subset, membership, intersection and union
232 are part of the standard library of Matita.
234 These notions come with some standard notation attached to them:
236 - A ∪ B can be typed with `A \cup B`
237 - A ∩ B can be typed with `A \cap B`
238 - A ≬ B can be typed with `A \between B`
239 - x ∈ A can be typed with `x \in A`
240 - Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A`
242 The `include` command tells Matita to load a part of the library,
243 in particular the part that we will use can be loaded as follows:
247 include "sets/sets.ma".
251 Some basic results that we will use are also part of the sets library:
253 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
254 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
259 A set of axioms is made of a set(oid) `S`, a family of sets `I` and a
260 family `C` of subsets of `S` indexed by elements `a` of `S`
261 and elements of `I(a)`.
263 It is desirable to state theorems like "for every set of axioms, …"
264 without explicitly mentioning S, I and C. To do that, the three
265 components have to be grouped into a record (essentially a dependently
266 typed tuple). The system is able to generate the projections
267 of the record automatically, and they are named as the fields of
268 the record. So, given an axiom set `A` we can obtain the set
269 with `S A`, the family of sets with `I A` and the family of subsets
274 nrecord Ax : Type[1] ≝ {
282 Forget for a moment the `:>` that will be detailed later, and focus on
283 the record definition. It is made of a list of pairs: a name, followed
284 by `:` and the its type. It is a dependently typed tuple, thus
285 already defined names (fields) can be used in the types that follow.
287 Note that `S` is declared to be a `setoid` and not a Type. The original
288 paper probably also considers I to generate setoids, and both I and C
289 to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use
290 setoids only when strictly needed (i.e. where we want to talk about
291 equality). Setoids will play a role only when we will define
292 the alternative version of the axiom set.
294 Note that the field `S` was declared with `:>` instead of a simple `:`.
295 This declares the `S` projection to be a coercion. A coercion is
296 a "cast" function the system automatically inserts when it is needed.
297 In that case, the projection `S` has type `Ax → setoid`, and whenever
298 the expected type of a term is `setoid` while its type is `Ax`, the
299 system inserts the coercion around it, to make the whole term well typed.
301 When formalizing an algebraic structure, declaring the carrier as a
302 coercion is a common practice, since it allows to write statements like
304 ∀G:Group.∀x:G.x * x^-1 = 1
306 The quantification over `x` of type `G` is ill-typed, since `G` is a term
307 (of type `Group`) and thus not a type. Since the carrier projection
308 `carr` is a coercion, that maps a `Group` into the type of
309 its elements, the system automatically inserts `carr` around `G`,
310 obtaining `…∀x: carr G.…`.
312 Coercions are hidden by the system when it displays a term.
313 In this particular case, the coercion `S` allows to write (and read):
317 Since `A` is not a type, but it can be turned into a `setoid` by `S`
318 and a `setoid` can be turned into a type by its `carr` projection, the
319 composed coercion `carr ∘ S` is silently inserted.
324 Something that is not still satisfactory, is that the dependent type
325 of `I` and `C` are abstracted over the Axiom set. To obtain the
326 precise type of a term, you can use the `ncheck` command as follows.
330 (** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *)
331 (** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *)
335 One would like to write `I a` and not `I A a` under a context where
336 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
337 mechanism simply `A`). In Matita, a question mark represents an implicit
338 argument, i.e. a missing piece of information the system is asked to
339 infer. Matita performs Hindley-Milner-style type inference, thus writing
340 `I ? a` is enough: since the second argument of `I` is typed by the
341 first one, the first (omitted) argument can be inferred just
342 computing the type of `a` (that is `A`).
346 (** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *)
350 This is still not completely satisfactory, since you have always to type
351 `?`; to fix this minor issue we have to introduce the notational
352 support built in Matita.
357 Matita is quipped with a quite complex notational support,
358 allowing the user to define and use mathematical notations
359 ([From Notation to Semantics: There and Back Again][1]).
361 Since notations are usually ambiguous (e.g. the frequent overloading of
362 symbols) Matita distinguishes between the term level, the
363 content level, and the presentation level, allowing multiple
364 mappings between the content and the term level.
366 The mapping between the presentation level (i.e. what is typed on the
367 keyboard and what is displayed in the sequent window) and the content
368 level is defined with the `notation` command. When followed by
369 `>`, it defines an input (only) notation.
373 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
374 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
378 The first notation defines the writing `𝐈 a` where `a` is a generic
379 term of precedence 90, the maximum one. This high precedence forces
380 parentheses around any term of a lower precedence. For example `𝐈 x`
381 would be accepted, since identifiers have precedence 90, but
382 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
383 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
385 To obtain the `𝐈` is enough to type `I` and then cycle between its
386 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
387 regular letters or the round parentheses, thus their variants (like the
388 bold ones) have to be used.
390 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
391 new content element to which a term `$a` is passed.
393 Content elements have to be interpreted, and possibly multiple,
394 incompatible, interpretations can be defined.
398 interpretation "I" 'I a = (I ? a).
399 interpretation "C" 'C a i = (C ? a i).
403 The `interpretation` command allows to define the mapping between
404 the content level and the terms level. Here we associate the `I` and
405 `C` projections of the Axiom set record, where the Axiom set is an implicit
406 argument `?` to be inferred by the system.
408 Interpretation are bi-directional, thus when displaying a term like
409 `C _ a i`, the system looks for a presentation for the content element
414 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
415 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
419 For output purposes we can define more complex notations, for example
420 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
421 the size of the arguments and lowering their baseline (i.e. putting them
422 as subscript), separating them with a comma followed by a little space.
424 The first (technical) definition
425 --------------------------------
427 Before defining the cover relation as an inductive predicate, one
428 has to notice that the infinity rule uses, in its hypotheses, the
429 cover relation between two subsets, while the inductive predicate
430 we are going to define relates an element and a subset.
432 An option would be to unfold the definition of cover between subsets,
433 but we prefer to define the abstract notion of cover between subsets
434 (so that we can attach a (ambiguous) notation to it).
436 Anyway, to ease the understanding of the definition of the cover relation
437 between subsets, we first define the inductive predicate unfolding the
438 definition, and we later refine it with.
442 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
443 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
444 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
448 We defined the xcover (x will be removed in the final version of the
449 definition) as an inductive predicate. The arity of the inductive
450 predicate has to be carefully analyzed:
452 > (A : Ax) (U : Ω^A) : A → CProp[0]
454 The syntax separates with `:` abstractions that are fixed for every
455 constructor (introduction rule) and abstractions that can change. In that
456 case the parameter `U` is abstracted once and for all in front of every
457 constructor, and every occurrence of the inductive predicate is applied to
458 `U` in a consistent way. Arguments abstracted on the right of `:` are not
459 constant, for example the xcinfinity constructor introduces `a ◃ U`,
460 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
461 had side of the predicate changes, thus it has to be abstracted (in the arity
462 of the inductive predicate) on the right of `:`.
466 (** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
470 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
471 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
473 This notion has to be abstracted over the cover relation (whose
474 type is the arity of the inductive `xcover` predicate just defined).
476 Then it has to be abstracted over the arguments of that cover relation,
477 i.e. the axiom set and the set `U`, and the subset (in that case `𝐂 a i`)
478 sitting on the left hand side of `◃`.
482 ndefinition cover_set :
483 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
485 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
489 The `ndefinition` command takes a name, a type and body (of that type).
490 The type can be omitted, and in that case it is inferred by the system.
491 If the type is given, the system uses it to infer implicit arguments
492 of the body. In that case all types are left implicit in the body.
494 We now define the notation `a ◃ b`. Here the keywork `hvbox`
495 and `break` tell the system how to wrap text when it does not
496 fit the screen (they can be safely ignored for the scope of
497 this tutorial). We also add an interpretation for that notation,
498 where the (abstracted) cover relation is implicit. The system
499 will not be able to infer it from the other arguments `C` and `U`
500 and will thus prompt the user for it. This is also why we named this
501 interpretation `covers set temp`: we will later define another
502 interpretation in which the cover relation is the one we are going to
507 notation "hvbox(a break ◃ b)" non associative with precedence 45
508 for @{ 'covers $a $b }.
510 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
517 We can now define the cover relation using the `◃` notation for
518 the premise of infinity.
522 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
523 | creflexivity : ∀a. a ∈ U → cover A U a
524 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
525 (** screenshot "cover". *)
531 Note that the system accepts the definition
532 but prompts the user for the relation the `cover_set` notion is
537 The horizontal line separates the hypotheses from the conclusion.
538 The `napply cover` command tells the system that the relation
539 it is looking for is exactly our first context entry (i.e. the inductive
540 predicate we are defining, up to α-conversion); while the `nqed` command
541 ends a definition or proof.
543 We can now define the interpretation for the cover relation between an
544 element and a subset first, then between two subsets (but this time
545 we fix the relation `cover_set` is abstracted on).
549 interpretation "covers" 'covers a U = (cover ? U a).
550 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
554 We will proceed similarly for the fish relation, but before going
555 on it is better to give a short introduction to the proof mode of Matita.
556 We define again the `cover_set` term, but this time we build
557 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
558 and terms share the same syntax, and it is thus possible to use the
559 commands devoted to build proof term also to build regular definitions.
560 A tentative semantics for the proof mode commands (called tactics)
561 in terms of sequent calculus rules are given in the
562 <a href="#appendix">appendix</a>.
566 ndefinition xcover_set :
567 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
568 (** screenshot "xcover-set-1". *)
569 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
570 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
571 napply cover; (** screenshot "xcover-set-4". *)
579 The system asks for a proof of the full statement, in an empty context.
581 The `#` command is the ∀-introduction rule, it gives a name to an
582 assumption putting it in the context, and generates a λ-abstraction
586 We have now to provide a proposition, and we exhibit it. We left
587 a part of it implicit; since the system cannot infer it it will
589 Note that the type of `∀y:A.y ∈ C → ?` is a proposition
590 whenever `?` is a proposition.
593 The proposition we want to provide is an application of the
594 cover relation we have abstracted in the context. The command
595 `napply`, if the given term has not the expected type (in that
596 case it is a product versus a proposition) it applies it to as many
597 implicit arguments as necessary (in that case `? ? ?`).
600 The system will now ask in turn the three implicit arguments
601 passed to cover. The syntax `##[` allows to start a branching
602 to tackle every sub proof individually, otherwise every command
603 is applied to every subproof. The command `##|` switches to the next
604 subproof and `##]` ends the branching.
612 The definition of fish works exactly the same way as for cover, except
613 that it is defined as a coinductive proposition.
616 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
621 notation "hvbox(a break ⋉ b)" non associative with precedence 45
622 for @{ 'fish $a $b }.
624 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
626 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
627 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
631 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
632 interpretation "fish" 'fish a U = (fish ? U a).
636 Introduction rule for fish
637 ---------------------------
639 Matita is able to generate elimination rules for inductive types,
640 but not introduction rules for the coinductive case.
644 (** ncheck cover_rect_CProp0. *)
648 We thus have to define the introduction rule for fish by co-recursion.
649 Here we again use the proof mode of Matita to exhibit the body of the
650 corecursive function.
654 nlet corec fish_rec (A:Ax) (U: Ω^A)
656 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
657 (** screenshot "def-fish-rec-1". *)
658 #a; #a_in_P; napply cfish; (** screenshot "def-fish-rec-2". *)
659 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
660 napply H1; (** screenshot "def-fish-rec-3". *)
662 ##| #i; ncases (H2 a a_in_P i); (** screenshot "def-fish-rec-5". *)
663 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
664 @; (** screenshot "def-fish-rec-6". *)
666 ##| @; (** screenshot "def-fish-rec-7". *)
668 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
677 Note the first item of the context, it is the corecursive function we are
678 defining. This item allows to perform the recursive call, but we will be
679 allowed to do such call only after having generated a constructor of
680 the fish coinductive type.
682 We introduce `a` and `p`, and then return the fish constructor `cfish`.
683 Since the constructor accepts two arguments, the system asks for them.
686 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
687 With the `nchange` tactic we change `H1` into an equivalent form (this step
688 can be skipped, since the system would be able to unfold the definition
689 of inclusion by itself)
692 It is now clear that `H1` can be applied. Again `napply` adds two
693 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
694 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
695 `a`, and it asks a proof that `a ∈ P`.
698 The `nassumption` tactic looks for the required proof in the context, and in
699 that cases finds it in the last context position.
701 We move now to the second branch of the proof, corresponding to the second
702 argument of the `cfish` constructor.
704 We introduce `i` and then we destruct `H2 a p i`, that being a proof
705 of an overlap predicate, give as an element and a proof that it is
706 both in `𝐂 a i` and `P`.
709 We then introduce `x`, break the conjunction (the `*;` command is the
710 equivalent of `ncases` but operates on the first hypothesis that can
711 be introduced). We then introduce the two sides of the conjunction.
714 The goal is now the existence of a point in `𝐂 a i` fished by `U`.
715 We thus need to use the introduction rule for the existential quantifier.
716 In CIC it is a defined notion, that is an inductive type with just
717 one constructor (one introduction rule) holding the witness and the proof
718 that the witness satisfies a proposition.
722 Instead of trying to remember the name of the constructor, that should
723 be used as the argument of `napply`, we can ask the system to find by
724 itself the constructor name and apply it with the `@` tactic.
725 Note that some inductive predicates, like the disjunction, have multiple
726 introduction rules, and thus `@` can be followed by a number identifying
730 After choosing `x` as the witness, we have to prove a conjunction,
731 and we again apply the introduction rule for the inductively defined
735 The left hand side of the conjunction is trivial to prove, since it
736 is already in the context. The right hand side needs to perform
737 the co-recursive call.
740 The co-recursive call needs some arguments, but all of them are
741 in the context. Instead of explicitly mention them, we use the
742 `nassumption` tactic, that simply tries to apply every context item.
748 Subset of covered/fished points
749 -------------------------------
751 We now have to define the subset of `S` of points covered by `U`.
752 We also define a prefix notation for it. Remember that the precedence
753 of the prefix form of a symbol has to be higher than the precedence
758 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
760 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
762 interpretation "coverage cover" 'coverage U = (coverage ? U).
766 Here we define the equation characterizing the cover relation.
767 Even if it is not part of the paper, we proved that `◃(U)` is
768 the minimum solution for
769 such equation, the interested reader should be able to reply the proof
774 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
775 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
777 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
780 ##[ #bU; @1; nassumption;
781 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
783 ##| #_; napply CaiU; nassumption; ##] ##]
784 ##| ncases H; ##[ #E; @; nassumption]
785 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
789 ntheorem coverage_min_cover_equation :
790 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
791 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
792 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
793 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
799 We similarly define the subset of points "fished" by `F`, the
800 equation characterizing `⋉(F)` and prove that fish is
801 the biggest solution for such equation.
805 notation "⋉F" non associative with precedence 55
808 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
810 interpretation "fished fish" 'fished F = (fished ? F).
812 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
813 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
815 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
816 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
817 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
819 ##| #aF; #H1; @ aF; napply H1;
823 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
824 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
825 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
830 Part 2, the new set of axioms
831 -----------------------------
833 Since the name of defined objects (record included) has to be unique
834 within the same file, we prefix every field name
835 in the new definition of the axiom set with `n`.
839 nrecord nAx : Type[1] ≝ {
842 nD: ∀a:nS. nI a → Type[0];
843 nd: ∀a:nS. ∀i:nI a. nD a i → nS
848 We again define a notation for the projections, making the
849 projected record an implicit argument. Note that, since we already have
850 a notation for `𝐈`, we just add another interpretation for it. The
851 system, looking at the argument of `𝐈`, will be able to choose
852 the correct interpretation.
856 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
857 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
859 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
860 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
862 interpretation "D" 'D a i = (nD ? a i).
863 interpretation "d" 'd a i j = (nd ? a i j).
864 interpretation "new I" 'I a = (nI ? a).
868 The first result the paper presents to motivate the new formulation
869 of the axiom set is the possibility to define and old axiom set
870 starting from a new one and vice versa. The key definition for
871 such construction is the image of d(a,i).
872 The paper defines the image as
874 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
876 but this not so formal notation poses some problems. The image is
877 often used as the left hand side of the ⊆ predicate
881 Of course this writing is interpreted by the authors as follows
883 > ∀j:D(a,i). d(a,i,j) ∈ V
885 If we need to use the image to define `𝐂 ` (a subset of `S`) we are obliged to
886 form a subset, i.e. to place a single variable `{ here | … }` of type `S`.
888 > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
890 This poses no theoretical problems, since `S` is a setoid and thus equipped
893 Unless we define two different images, one for stating that the image is ⊆ of
894 something and another one to define `𝐂`, we end up using always the latter.
895 Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
897 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
899 That, up to rewriting with the equation defining `x`, is what we mean.
900 The technical problem arises later, when `V` will be a complex
901 construction that has to be proved extensional
902 (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
906 include "logic/equality.ma".
908 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
910 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
911 notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
913 interpretation "image" 'Im a i = (image ? a i).
917 Thanks to our definition of image, we can define a function mapping a
918 new axiom set to an old one and vice versa. Note that in the second
919 definition, when we give the `𝐝` component, the projection of the
920 Σ-type is inlined (constructed on the fly by `*;`)
921 while in the paper it was named `fst`.
925 ndefinition Ax_of_nAx : nAx → Ax.
926 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
929 ndefinition nAx_of_Ax : Ax → nAx.
931 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
932 ##| #a; #i; *; #x; #_; napply x;
936 nlemma Ax_nAx_equiv :
937 ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
938 C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
939 #A; #a; #i; @; #b; #H;
940 ##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
941 nwhd in H; ncases H; #x; #E; nrewrite > E;
942 ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
943 ##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
944 ##[ @ b; nassumption;
945 ##| nnormalize; @; ##]
951 We then define the inductive type of ordinals, parametrized over an axiom
952 set. We also attach some notations to the constructors.
956 ninductive Ord (A : nAx) : Type[0] ≝
959 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
961 notation "0" non associative with precedence 90 for @{ 'oO }.
962 notation "x+1" non associative with precedence 50 for @{'oS $x }.
963 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
965 interpretation "ordinals Zero" 'oO = (oO ?).
966 interpretation "ordinals Succ" 'oS x = (oS ? x).
967 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
971 The definition of `U⎽x` is by recursion over the ordinal `x`.
972 We thus define a recursive function using the `nlet rec` command.
973 The `on x` directive tells
974 the system on which argument the function is (structurally) recursive.
976 In the `oS` case we use a local definition to name the recursive call
977 since it is used twice.
979 Note that Matita does not support notation in the left hand side
980 of a pattern match, and thus the names of the constructors have to
981 be spelled out verbatim.
985 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
988 | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
989 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
991 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
992 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
994 interpretation "famU" 'famU U x = (famU ? U x).
998 We attach as the input notation for U_x the similar `U⎽x` where underscore,
999 that is a character valid for identifier names, has been replaced by `⎽` that is
1000 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
1001 for `_` (i.e. pressing ALT-L after `_`).
1003 The notion ◃(U) has to be defined as the subset of elements `y`
1004 belonging to `U⎽x` for some `x`. Moreover, we have to define the notion
1005 of cover between sets again, since the one defined at the beginning
1006 of the tutorial works only for the old axiom set.
1010 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝
1011 λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
1013 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
1014 ∀y.y ∈ C → y ∈ c A U.
1016 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
1017 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
1018 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
1022 Before proving that this cover relation validates the reflexivity and infinity
1023 rules, we prove this little technical lemma that is used in the proof for the
1028 nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
1029 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
1034 The proof of infinity uses the following form of the Axiom of Choice,
1035 that cannot be proved inside Matita, since the existential quantifier
1036 lives in the sort of predicative propositions while the sigma in the conclusion
1037 lives in the sort of data types, and thus the former cannot be eliminated
1038 to provide the witness for the second.
1042 nlemma AC_fake : ∀A,a,i,U.
1043 (∀j:𝐃 a i.Σx:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
1044 #A; #a; #i; #U; #H; @;
1045 ##[ #j; ncases (H j); #x; #_; napply x;
1046 ##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
1049 naxiom AC : ∀A,a,i,U.
1050 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
1054 In the proof of infinity, we have to rewrite under the ∈ predicate.
1055 It is clearly possible to show that `U⎽x` is an extensional set:
1057 > a = b → a ∈ U⎽x → b ∈ U⎽x
1059 Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be
1060 declared as morphisms. This poses no problem, but goes out of the scope of the
1061 tutorial, since dependent morphisms are hard to manipulate, and we thus assume it.
1065 naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
1069 The reflexivity proof is trivial, it is enough to provide the ordinal `0`
1070 as a witness, then `◃(U)` reduces to `U` by definition,
1071 hence the conclusion. Note that `0` is between `(` and `)` to
1072 make it clear that it is a term (an ordinal) and not the number
1073 of the constructor we want to apply (that is the first and only one
1074 of the existential inductive type).
1077 ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
1078 #A; #U; #a; #H; @ (0); napply H;
1083 We now proceed with the proof of the infinity rule.
1088 alias symbol "exists" (instance 1) = "exists".
1089 alias symbol "covers" = "new covers set".
1090 alias symbol "covers" = "new covers".
1091 alias symbol "covers" = "new covers set".
1092 alias symbol "covers" = "new covers".
1093 alias symbol "covers" = "new covers set".
1094 alias symbol "covers" = "new covers".
1095 ntheorem new_coverage_infinity:
1096 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
1097 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
1098 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
1099 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
1100 #z; napply H; @ z; @; ##] #H'; (** screenshot "n-cov-inf-4". *)
1101 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
1102 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
1103 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
1104 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
1105 @2; (** screenshot "n-cov-inf-8". *)
1106 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
1107 nrewrite > Hd; napply Hf';
1112 We eliminate the existential, obtaining an `i` and a proof that the
1113 image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal
1114 form of `H`, thus expands the definition of cover between sets.
1117 When the paper proof considers `H`, it implicitly substitutes assumed
1118 equation defining `y` in its conclusion.
1119 In Matita this step is not completely trivial.
1120 We thus assert (`ncut`) the nicer form of `H` and prove it.
1123 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
1124 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
1125 becomes trivial if `j` is chosen to be `z`.
1128 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
1129 its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before
1130 assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated
1131 is `AC ???? H'` where the system is able to infer every `?`. Matita provides
1132 a facility to specify a number of `?` in a compact way, i.e. `…`. The system
1133 expand `…` first to zero, then one, then two, three and finally four question
1134 marks, "guessing" how may of them are needed.
1137 The paper proof does now a forward reasoning step, deriving (by the ord_subset
1138 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
1141 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
1144 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
1145 that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`.
1146 Applying the second constructor `@2;` of the disjunction,
1147 we are left to prove that `a` belongs to the right hand side of the union.
1150 We thus provide `i` as the witness of the existential, introduce the
1151 element being in the image and we are
1152 left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging
1153 to the image means that there exists an object in the domain …, we eliminate the
1154 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
1157 We just need to use the equational definition of `x` to obtain a conclusion
1158 that can be proved with `Hf'`. We assumed that `U⎽x` is extensional for
1159 every `x`, thus we are allowed to use `Hd` and close the proof.
1165 The next proof is that ◃(U) is minimal. The hardest part of the proof
1166 is to prepare the goal for the induction. The desiderata is to prove
1167 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
1168 unfolding all definitions:
1170 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
1174 nlemma new_coverage_min :
1175 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1176 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
1177 *; #o; (** screenshot "n-cov-min-3". *)
1178 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
1179 nelim o; (** screenshot "n-cov-min-5". *)
1181 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1182 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1183 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1188 After all the introductions, event the element hidden in the ⊆ definition,
1189 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1192 What is left is almost right, but the element `b` is already in the
1193 context. We thus generalize every occurrence of `b` in
1194 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1197 We then proceed by induction on `o` obtaining the following goals
1200 All of them can be proved using simple set theoretic arguments,
1201 the induction hypothesis and the assumption `Im`.
1208 The notion `F⎽x` is again defined by recursion over the ordinal `x`.
1212 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1215 | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
1216 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1219 interpretation "famF" 'famU U x = (famF ? U x).
1221 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1223 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1224 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1228 The proof of compatibility uses this little result, that we
1229 proved outside the main proof.
1232 nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1233 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1238 We assume the dual of the axiom of choice, as in the paper proof.
1241 naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
1242 (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x))
1243 → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
1247 Proving the anti-reflexivity property is simple, since the
1248 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1249 `a ∈ F⎽x`. If `x` is choose to be `0`, we obtain the thesis.
1252 ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1253 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1258 We now prove the compatibility property for the new fish relation.
1261 ntheorem new_fish_compatible:
1262 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1263 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
1264 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
1265 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
1267 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1268 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
1269 *; #j; #Hj; @j; (** screenshot "n-f-compat-6". *)
1270 napply (co_ord_subset … Hj);
1275 After reducing to normal form the goal, we observe it is exactly the conclusion of
1276 the dual axiom of choice we just assumed. We thus apply it ad introduce the
1280 The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`.
1283 Since F_(Λf+1) is defined by recursion and we actually have a concrete input
1284 `Λf+1` for that recursive function, it can be computed.
1285 Anyway, using the `nnormalize`
1286 tactic would reduce too much (both the `+1` and the `Λf` steps would be performed);
1287 we thus explicitly give a convertible type for that hypothesis, corresponding
1288 the computation of the `+1` step, plus the unfolding the definition of
1292 We are interested in the right hand side of `aLf`, an in particular to
1293 its intance where the generic index in `𝐈 a` is `i`.
1296 We then eliminate the existential, obtaining `j` and its property `Hj`. We provide
1300 What is left to prove is exactly the `co_ord_subset` lemma we factored out
1307 The proof that `⋉(F)` is maximal is exactly the dual one of the
1308 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1309 before doing the induction over `o`.
1311 Note that `G` is assumed to be of type `𝛀^A`, that means an extensional
1312 subset of `S`, while `Ω^A` means just a subset (note that the former is bold).
1315 ntheorem max_new_fished:
1316 ∀A:nAx.∀G:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1317 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1318 ngeneralize in match HbG; ngeneralize in match b;
1319 nchange with (G ⊆ F⎽o);
1322 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1323 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1324 @d; napply IH; (** screenshot "n-f-max-1". *)
1325 nrewrite < Ed; napply cG;
1326 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1327 #b; #Hb; #d; napply (Hf d); napply Hb;
1333 Here the situation looks really similar to the one of the dual proof where
1334 we had to apply the assumption `U_x_is_ext`, but here the set is just `G`
1335 not `F_x`. Since we assumed `G` to be extensional we can
1336 exploit the facilities
1337 Matita provides to perform rewriting in the general setting of setoids.
1339 The `.` notation simply triggers the mechanism, while the given argument has to
1340 mimic the context under which the rewriting has to happen. In that case
1341 we want to rewrite the left hand side of the binary morphism `∈`.
1343 to represent the context of a binary morphism is `‡`. The right hand side
1344 has to be left untouched, and the identity rewriting step is represented with
1345 `#` (actually a reflexivity proof for the subterm identified by the context).
1347 We want to rewrite the left hand side using `Ed` right-to-left (the default
1348 is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`.
1350 The complete command is `napply (. Ed^-1‡#)` that has to be read like:
1352 > perform some rewritings under a binary morphism,
1353 > on the right do nothing,
1354 > on the left rewrite with Ed right-to-left.
1356 After the rewriting step the goal is exactly the `cG` assumption.
1362 <div id="appendix" class="anchor"></div>
1363 Appendix: tactics explanation
1364 -----------------------------
1366 In this appendix we try to give a description of tactics
1367 in terms of sequent calculus rules annotated with proofs.
1368 The `:` separator has to be read as _is a proof of_, in the spirit
1369 of the Curry-Howard isomorphism.
1371 Γ ⊢ f : A_1 → … → A_n → B Γ ⊢ ?_i : A_i
1372 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1373 Γ ⊢ (f ?_1 … ?_n ) : B
1375 Γ ⊢ ? : F → B Γ ⊢ f : F
1376 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1381 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1382 Γ ⊢ λx:T.? : ∀x:T.P(x)
1385 Γ ⊢ ?_i : args_i → P(k_i args_i)
1386 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1387 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1390 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1391 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1392 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1394 Where `T_rect_CProp0` is the induction principle for the
1399 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1402 Where the equivalence relation between types `≡` keeps into account
1403 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1404 definition unfolding), ι-reduction (pattern matching simplification),
1405 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1409 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1410 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1414 Γ; H : Q; Δ ⊢ ? : G P →* Q
1415 nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1418 Where `Q` is the normal form of `P` considering βδζιμν-reduction steps.
1422 nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1426 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1427 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1432 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1441 Last updated: $Date$
1444 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf
1445 [2]: http://matita.cs.unibo.it
1446 [3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
1447 [4]: http://www.inria.fr/rrrt/rr-0530.html