1 <?xml version="1.0" encoding="UTF-8"?>
4 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
5 <style type="text/css">
7 font-family: monospace;
15 padding-bottom: 0.2em;
47 p { text-align: justify; }
49 <script type="text/javascript" src="sh_main.js"></script>
50 <script type="text/javascript" src="sh_grafite.js"></script>
51 <link type="text/css" rel="stylesheet" href="sh_gedit.css">
52 <script type="text/javascript">
54 var pres=document.getElementsByTagName("pre")
55 for (i=0; i < pres.length; i++) {
56 pres[i].className="sh_grafite";
58 sh_highlightDocument();
62 <body onload="syntaxon();">
63 <h1>Inductively generated formal topologies in Matita</h1>
65 <p>This is a not so short introduction to <a href="http://matita.cs.unibo.it">Matita</a>, based on
66 the formalization of the paper</p>
69 <p>Between formal topology and game theory: an
70 explicit solution for the conditions for an
71 inductive generation of formal topologies</p>
74 <p>by Stefano Berardi and Silvio Valentini. </p>
76 <p>The tutorial and the formalization are by Enrico Tassi.</p>
78 <p>The reader should be familiar with inductively generated
79 formal topologies and have some basic knowledge of type theory and λ-calculus. </p>
81 <p>A considerable part of this tutorial is devoted to explain how to define
82 notations that resemble the ones used in the original paper. We believe
83 this is an important part of every formalization, not only from the aesthetic
84 point of view, but also from the practical point of view. Being
85 consistent allows to follow the paper in a pedantic way, and hopefully
86 to make the formalization (at least the definitions and proved
87 statements) readable to the author of the paper. </p>
89 <p>The formalization uses the "new generation" version of Matita
90 (that will be named 1.x when finally released).
91 Last stable release of the "old" system is named 0.5.7; the ng system
92 is coexisting with the old one in all development release
93 (named "nightly builds" in the download page of Matita)
94 with a version strictly greater than 0.5.7.</p>
96 <p>To read this tutorial in HTML format, you need a decent browser
97 equipped with a unicode capable font. Use the PDF format if some
98 symbols are not displayed correctly.</p>
100 <h2>Orienteering</h2>
102 <p>The graphical interface of Matita is composed of three windows:
103 the script window, on the left, is where you type; the sequent
104 window on the top right is where the system shows you the ongoing proof;
105 the error window, on the bottom right, is where the system complains.
106 On the top of the script window five buttons drive the processing of
107 the proof script. From left to right they request the system to:</p>
110 <li>go back to the beginning of the script</li>
111 <li>go back one step</li>
112 <li>go to the current cursor position</li>
113 <li>advance one step</li>
114 <li>advance to the end of the script</li>
117 <p>When the system processes a command, it locks the part of the script
118 corresponding to the command, such that you cannot edit it anymore
119 (without going back). Locked parts are coloured in blue.</p>
121 <p>The sequent window is hyper textual, i.e. you can click on symbols
122 to jump to their definition, or switch between different notations
123 for the same expression (for example, equality has two notations,
124 one of them makes the type of the arguments explicit). </p>
126 <p>Everywhere in the script you can use the <code>ncheck (term).</code> command to
127 ask for the type a given term. If you do that in the middle of a proof,
128 the term is assumed to live in the current proof context (i.e. can use
129 variables introduced so far).</p>
131 <p>To ease the typing of mathematical symbols, the script window
132 implements two unusual input facilities:</p>
135 <li><p>some TeX symbols can be typed using their TeX names, and are
136 automatically converted to UTF-8 characters. For a list of
137 the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
138 Moreover some ASCII-art is understood as well, like <code>=></code> and <code>-></code>
139 to mean double or single arrows.
140 Here we recall some of these "shortcuts":</p>
143 <li>∀ can be typed with <code>\forall</code></li>
144 <li>λ can be typed with <code>\lambda</code></li>
145 <li>≝ can be typed with <code>\def</code> or <code>:=</code></li>
146 <li>→ can be typed with <code>\to</code> or <code>-></code></li>
148 <li><p>some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
149 The user can cycle between variants typing one of them and then
150 pressing ALT-L. Note that also letters do have variants, for
151 example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
152 Variants are listed in the aforementioned TeX/UTF-8 table. </p></li>
155 <p>The syntax of terms (and types) is the one of the λ-calculus CIC
156 on which Matita is based. The main syntactical difference w.r.t.
157 the usual mathematical notation is the function application, written
158 <code>(f x y)</code> in place of <code>f(x,y)</code>. </p>
160 <p>Pressing <code>F1</code> opens the Matita manual.</p>
162 <h2>CIC (as <a href="http://www.cs.unibo.it/~tassi/smallcc.pdf">implemented in Matita</a>) in a nutshell</h2>
164 <p>CIC is a full and functional Pure Type System (all products do exist,
165 and their sort is is determined by the target) with an impredicative sort
166 Prop and a predicative sort Type. It features both dependent types and
167 polymorphism like the <a href="http://www.inria.fr/rrrt/rr-0530.html">Calculus of Constructions</a>. Proofs and terms share
168 the same syntax, and they can occur in types. </p>
170 <p>The environment used for in the typing judgement can be populated with
171 well typed definitions or theorems, (co)inductive types validating positivity
172 conditions and recursive functions provably total by simple syntactical
173 analysis (recursive calls are allowed only on structurally smaller subterms).
175 functions can be defined as well, and must satisfy the dual condition, i.e.
176 performing the recursive call only after having generated a constructor (a piece
179 <p>The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
180 types defined in the environment. This construct, together with the possibility to
181 definable total recursive functions, allows to define eliminators (or constructors)
182 for (co)inductive types. </p>
184 <p>Types are compare up to conversion. Since types may depend on terms, conversion
185 involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
186 definition unfolding), ι-reduction (pattern matching simplification),
187 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
190 <p>Since we are going to formalize constructive and predicative mathematics
191 in an intensional type theory like CIC, we try to establish some terminology.
192 Type is the sort of sets equipped with the <code>Id</code> equality (i.e. an intensional,
193 not quotiented set). </p>
195 <p>We write <code>Type[i]</code> to mention a Type in the predicative hierarchy
196 of types. To ease the comprehension we will use <code>Type[0]</code> for sets,
197 and <code>Type[1]</code> for classes. The index <code>i</code> is just a label: constraints among
198 universes are declared by the user. The standard library defines</p>
201 <p>Type[0] < Type[1] < Type[2]</p>
204 <p>Matita implements a variant of CIC in which constructive and predicative proposition
205 are distinguished from predicative data types.</p>
207 <p><object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/></p>
209 <p>For every <code>Type[i]</code> there is a corresponding level of predicative
210 propositions <code>CProp[i]</code> (the C initial is due to historical reasons, and
211 stands for constructive).
212 A predicative proposition cannot be eliminated toward
213 <code>Type[j]</code> unless it holds no computational content (i.e. it is an inductive proposition
214 with 0 or 1 constructors with propositional arguments, like <code>Id</code> and <code>And</code>
215 but not like <code>Or</code>). </p>
217 <p>The distinction between predicative propositions and predicative data types
218 is a peculiarity of Matita (for example in CIC as implemented by Coq they are the
219 same). The additional restriction of not allowing the elimination of a CProp
220 toward a Type makes the theory of Matita minimal in the following sense: </p>
222 <p><object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/></p>
224 <p>Theorems proved in CIC as implemented in Matita can be reused in a classical
225 and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
226 constructive propositions and assuming the excluded middle on them).
227 Alternatively, one can decide to collapse predicative propositions and
228 predicative data types recovering the Axiom of Choice in the sense of Martin Löf
229 (i.e. ∃ really holds a witness and can be eliminated to inhabit a type).</p>
231 <p>This implementation of CIC is the result of the collaboration with Maietti M.,
232 Sambin G. and Valentini S. of the University of Padua.</p>
234 <h2>Formalization choices</h2>
236 <p>There are many different ways of formalizing the same piece of mathematics
237 in CIC, depending on what our interests are. There is usually a trade-off
238 between the possibility of reuse the formalization we did and its complexity.</p>
240 <p>In this work, our decisions mainly regarded the following two areas</p>
243 <li>Axiom of Choice: controlled use or not</li>
244 <li>Equality: Id or not</li>
247 <h3>Axiom of Choice</h3>
249 <p>In this paper it is clear that the author is interested in using the Axiom
250 of Choice, thus choosing to identify ∃ and Σ (i.e. working in the
251 leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision
252 (that is, the author of the paper would not complain we formalized something
253 different from what he had in mind).</p>
255 <p>Anyway, we may benefit from the minimality of CIC as implemented in Matita,
256 "asking" the type system to ensure we do no use the Axiom of Choice elsewhere
257 in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
258 very beginning, the system will not complain if we use the Axiom of Choice at all.
259 Moreover, the elimination of an inductive type (like ∃) is a so common operation
260 that the syntax chosen for the elimination command is very compact and non
261 informative, hard to spot for a human being
262 (in fact it is just two characters long!). </p>
264 <p>We decided to formalize the whole paper without identifying
265 CProp and Type and assuming the Axiom of Choice as a real axiom
266 (i.e. a black hole with no computational content, a function with no body). </p>
268 <p>It is clear that this approach give us full control on when/where we really use
269 the Axiom of Choice. But, what are we loosing? What happens to the computational
270 content of the proofs if the Axiom of Choice gives no content back? </p>
273 depends on when we actually look at the computational content of the proof and
274 we "run" that program. We can extract the content and run it before or after
275 informing the system that our propositions are actually code (i.e. identifying
276 ∃ and Σ). If we run the program before, as soon as the computation reaches the
277 Axiom of Choice it stops, giving no output. If we tell the system that CProp and
278 Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
279 and the extracted code would compute an output. </p>
281 <p>Note that the computational
282 content is there even if the Axiom of Choice is an axiom, the difference is
283 just that we cannot use it (the typing rules inhibit the elimination of the
284 existential). This is possible only thanks to the minimality of CIC as implemented
289 <p>What we have to decide here is which models we admit. The paper does not
290 mention quotiented sets, thus using an intensional equality is enough
291 to capture the intended content of the paper. Nevertheless, the formalization
292 cannot be reused in a concrete example where the (families of) sets
293 that will build the axiom set are quotiented.</p>
295 <p>Matita gives support for setoid rewriting under a context built with
296 non dependent morphisms. As we will detail later, if we assume a generic
297 equality over the carrier of our axiom set, a non trivial inductive
298 construction over the ordinals has to be proved to respect extensionality
299 (i.e. if the input is an extensional set, also the output is).
300 The proof requires to rewrite under the context formed by the family of sets
301 <code>I</code> and <code>D</code>, that have a dependent type. Declaring them as dependently typed
302 morphisms is possible, but Matita does not provide an adequate support for them,
303 and would thus need more effort than formalizing the whole paper. </p>
305 <p>Anyway, in a preliminary attempt of formalization, we tried the setoid approach,
306 reaching the end of the formalization, but we had to assume the proof
307 of the extensionality of the <code>U_x</code> construction (while there is no
308 need to assume the same property for <code>F_x</code>!). </p>
310 <p>The current version of the formalization uses <code>Id</code>. </p>
312 <h2>The standard library and the <code>include</code> command</h2>
314 <p>Some basic notions, like subset, membership, intersection and union
315 are part of the standard library of Matita.</p>
317 <p>These notions come with some standard notation attached to them:</p>
320 <li>A ∪ B can be typed with <code>A \cup B</code></li>
321 <li>A ∩ B can be typed with <code>A \cap B</code> </li>
322 <li>A ≬ B can be typed with <code>A \between B</code></li>
323 <li>x ∈ A can be typed with <code>x \in A</code> </li>
324 <li>Ω^A, that is the type of the subsets of A, can be typed with <code>\Omega ^ A</code> </li>
327 <p>The <code>include</code> command tells Matita to load a part of the library,
328 in particular the part that we will use can be loaded as follows: </p>
330 <pre><code>include "sets/sets.ma".
333 <p>Some basic results that we will use are also part of the sets library:</p>
336 <li>subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W</li>
337 <li>subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V</li>
340 <h2>Defining Axiom set</h2>
342 <p>A set of axioms is made of a set <code>S</code>, a family of sets <code>I</code> and a
343 family <code>C</code> of subsets of <code>S</code> indexed by elements <code>a</code> of <code>S</code>
344 and elements of <code>I(a)</code>.</p>
346 <p>It is desirable to state theorems like "for every set of axioms, …"
347 without explicitly mentioning S, I and C. To do that, the three
348 components have to be grouped into a record (essentially a dependently
349 typed tuple). The system is able to generate the projections
350 of the record automatically, and they are named as the fields of
351 the record. So, given an axiom set <code>A</code> we can obtain the set
352 with <code>S A</code>, the family of sets with <code>I A</code> and the family of subsets
353 with <code>C A</code>.</p>
355 <pre><code>nrecord Ax : Type[1] ≝ {
362 <p>Forget for a moment the <code>:></code> that will be detailed later, and focus on
363 the record definition. It is made of a list of pairs: a name, followed
364 by <code>:</code> and the its type. It is a dependently typed tuple, thus
365 already defined names (fields) can be used in the types that follow. </p>
367 <p>Note that the field <code>S</code> was declared with <code>:></code> instead of a simple <code>:</code>.
368 This declares the <code>S</code> projection to be a coercion. A coercion is
369 a "cast" function the system automatically inserts when it is needed.
370 In that case, the projection <code>S</code> has type <code>Ax → setoid</code>, and whenever
371 the expected type of a term is <code>setoid</code> while its type is <code>Ax</code>, the
372 system inserts the coercion around it, to make the whole term well typed.</p>
374 <p>When formalizing an algebraic structure, declaring the carrier as a
375 coercion is a common practice, since it allows to write statements like</p>
377 <pre><code>∀G:Group.∀x:G.x * x^-1 = 1
380 <p>The quantification over <code>x</code> of type <code>G</code> is ill-typed, since <code>G</code> is a term
381 (of type <code>Group</code>) and thus not a type. Since the carrier projection
382 <code>carr</code> is a coercion, that maps a <code>Group</code> into the type of
383 its elements, the system automatically inserts <code>carr</code> around <code>G</code>,
384 obtaining <code>…∀x: carr G.…</code>. </p>
386 <p>Coercions are hidden by the system when it displays a term.
387 In this particular case, the coercion <code>S</code> allows to write (and read):</p>
389 <pre><code>∀A:Ax.∀a:A.…
392 <p>Since <code>A</code> is not a type, but it can be turned into a <code>setoid</code> by <code>S</code>
393 and a <code>setoid</code> can be turned into a type by its <code>carr</code> projection, the
394 composed coercion <code>carr ∘ S</code> is silently inserted.</p>
396 <h2>Implicit arguments</h2>
398 <p>Something that is not still satisfactory, is that the dependent type
399 of <code>I</code> and <code>C</code> are abstracted over the Axiom set. To obtain the
400 precise type of a term, you can use the <code>ncheck</code> command as follows.</p>
402 <pre><code>(** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *)
403 (** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *)
406 <p>One would like to write <code>I a</code> and not <code>I A a</code> under a context where
407 <code>A</code> is an axiom set and <code>a</code> has type <code>S A</code> (or thanks to the coercion
408 mechanism simply <code>A</code>). In Matita, a question mark represents an implicit
409 argument, i.e. a missing piece of information the system is asked to
410 infer. Matita performs Hindley-Milner-style type inference, thus writing
411 <code>I ? a</code> is enough: since the second argument of <code>I</code> is typed by the
412 first one, the first (omitted) argument can be inferred just
413 computing the type of <code>a</code> (that is <code>A</code>).</p>
415 <pre><code>(** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *)
418 <p>This is still not completely satisfactory, since you have always to type
419 <code>?</code>; to fix this minor issue we have to introduce the notational
420 support built in Matita.</p>
422 <h2>Notation for I and C</h2>
424 <p>Matita is quipped with a quite complex notational support,
425 allowing the user to define and use mathematical notations
426 (<a href="http://upsilon.cc/~zack/research/publications/notation.pdf">From Notation to Semantics: There and Back Again</a>). </p>
428 <p>Since notations are usually ambiguous (e.g. the frequent overloading of
429 symbols) Matita distinguishes between the term level, the
430 content level, and the presentation level, allowing multiple
431 mappings between the content and the term level. </p>
433 <p>The mapping between the presentation level (i.e. what is typed on the
434 keyboard and what is displayed in the sequent window) and the content
435 level is defined with the <code>notation</code> command. When followed by
436 <code>></code>, it defines an input (only) notation. </p>
438 <pre><code>notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
439 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
442 <p>The first notation defines the writing <code>𝐈 a</code> where <code>a</code> is a generic
443 term of precedence 90, the maximum one. This high precedence forces
444 parentheses around any term of a lower precedence. For example <code>𝐈 x</code>
445 would be accepted, since identifiers have precedence 90, but
446 <code>𝐈 f x</code> would be interpreted as <code>(𝐈 f) x</code>. In the latter case, parentheses
447 have to be put around <code>f x</code>, thus the accepted writing would be <code>𝐈 (f x)</code>.</p>
449 <p>To obtain the <code>𝐈</code> is enough to type <code>I</code> and then cycle between its
450 similar symbols with ALT-L. The same for <code>𝐂</code>. Notations cannot use
451 regular letters or the round parentheses, thus their variants (like the
452 bold ones) have to be used.</p>
454 <p>The first notation associates <code>𝐈 a</code> with <code>'I $a</code> where <code>'I</code> is a
455 new content element to which a term <code>$a</code> is passed.</p>
457 <p>Content elements have to be interpreted, and possibly multiple,
458 incompatible, interpretations can be defined.</p>
460 <pre><code>interpretation "I" 'I a = (I ? a).
461 interpretation "C" 'C a i = (C ? a i).
464 <p>The <code>interpretation</code> command allows to define the mapping between
465 the content level and the terms level. Here we associate the <code>I</code> and
466 <code>C</code> projections of the Axiom set record, where the Axiom set is an implicit
467 argument <code>?</code> to be inferred by the system.</p>
469 <p>Interpretation are bi-directional, thus when displaying a term like
470 <code>C _ a i</code>, the system looks for a presentation for the content element
471 <code>'C a i</code>. </p>
473 <pre><code>notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
474 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
477 <p>For output purposes we can define more complex notations, for example
478 we can put bold parentheses around the arguments of <code>𝐈</code> and <code>𝐂</code>, decreasing
479 the size of the arguments and lowering their baseline (i.e. putting them
480 as subscript), separating them with a comma followed by a little space.</p>
482 <h2>The first (technical) definition</h2>
484 <p>Before defining the cover relation as an inductive predicate, one
485 has to notice that the infinity rule uses, in its hypotheses, the
486 cover relation between two subsets, while the inductive predicate
487 we are going to define relates an element and a subset.</p>
489 <pre><code> a ∈ U i ∈ I(a) C(a,i) ◃ U
490 (reflexivity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼ (infinity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
494 <p>An option would be to unfold the definition of cover between subsets,
495 but we prefer to define the abstract notion of cover between subsets
496 (so that we can attach a (ambiguous) notation to it).</p>
498 <p>Anyway, to ease the understanding of the definition of the cover relation
499 between subsets, we first define the inductive predicate unfolding the
500 definition, and we later refine it with.</p>
502 <pre><code>ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
503 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
504 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
507 <p>We defined the xcover (x will be removed in the final version of the
508 definition) as an inductive predicate. The arity of the inductive
509 predicate has to be carefully analyzed:</p>
512 <p>(A : Ax) (U : Ω^A) : A → CProp[0]</p>
515 <p>The syntax separates with <code>:</code> abstractions that are fixed for every
516 constructor (introduction rule) and abstractions that can change. In that
517 case the parameter <code>U</code> is abstracted once and for all in front of every
518 constructor, and every occurrence of the inductive predicate is applied to
519 <code>U</code> in a consistent way. Arguments abstracted on the right of <code>:</code> are not
520 constant, for example the xcinfinity constructor introduces <code>a ◃ U</code>,
521 but under the assumption that (for every y) <code>y ◃ U</code>. In that rule, the left
522 had side of the predicate changes, thus it has to be abstracted (in the arity
523 of the inductive predicate) on the right of <code>:</code>.</p>
525 <p>The intuition Valentini suggests is that we are defining the unary predicate
526 "being covered by U" (i.e. <code>_ ◃ U</code>) and not "being covered" (i.e. <code>_ ◃ _</code>).
527 Unluckily, the syntax of Matita forces us to abstract <code>U</code> first, and
528 we will make it the second argument of the predicate using
529 the notational support Matita offers.</p>
531 <pre><code>(** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
534 <p>We want now to abstract out <code>(∀y.y ∈ 𝐂 a i → xcover A U y)</code> and define
535 a notion <code>cover_set</code> to which a notation <code>𝐂 a i ◃ U</code> can be attached.</p>
537 <p>This notion has to be abstracted over the cover relation (whose
538 type is the arity of the inductive <code>xcover</code> predicate just defined).</p>
540 <p>Then it has to be abstracted over the arguments of that cover relation,
541 i.e. the axiom set and the set <code>U</code>, and the subset (in that case <code>𝐂 a i</code>)
542 sitting on the left hand side of <code>◃</code>. </p>
544 <pre><code>ndefinition cover_set :
545 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
547 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
550 <p>The <code>ndefinition</code> command takes a name, a type and body (of that type).
551 The type can be omitted, and in that case it is inferred by the system.
552 If the type is given, the system uses it to infer implicit arguments
553 of the body. In that case all types are left implicit in the body.</p>
555 <p>We now define the notation <code>a ◃ b</code>. Here the keywork <code>hvbox</code>
556 and <code>break</code> tell the system how to wrap text when it does not
557 fit the screen (they can be safely ignored for the scope of
558 this tutorial). We also add an interpretation for that notation,
559 where the (abstracted) cover relation is implicit. The system
560 will not be able to infer it from the other arguments <code>C</code> and <code>U</code>
561 and will thus prompt the user for it. This is also why we named this
562 interpretation <code>covers set temp</code>: we will later define another
563 interpretation in which the cover relation is the one we are going to
566 <pre><code>notation "hvbox(a break ◃ b)" non associative with precedence 45
567 for @{ 'covers $a $b }.
569 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
572 <h2>The cover relation</h2>
574 <p>We can now define the cover relation using the <code>◃</code> notation for
575 the premise of infinity. </p>
577 <pre><code>ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
578 | creflexivity : ∀a. a ∈ U → cover A U a
579 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
582 <p><img src="cover.png" alt="cover" /></p>
584 <pre><code>napply cover;
588 <p>Note that the system accepts the definition
589 but prompts the user for the relation the <code>cover_set</code> notion is
592 <p>The horizontal line separates the hypotheses from the conclusion.
593 The <code>napply cover</code> command tells the system that the relation
594 it is looking for is exactly our first context entry (i.e. the inductive
595 predicate we are defining, up to α-conversion); while the <code>nqed</code> command
596 ends a definition or proof.</p>
598 <p>We can now define the interpretation for the cover relation between an
599 element and a subset first, then between two subsets (but this time
600 we fix the relation <code>cover_set</code> is abstracted on).</p>
602 <pre><code>interpretation "covers" 'covers a U = (cover ? U a).
603 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
606 <p>We will proceed similarly for the fish relation, but before going
607 on it is better to give a short introduction to the proof mode of Matita.
608 We define again the <code>cover_set</code> term, but this time we build
609 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
610 and terms share the same syntax, and it is thus possible to use the
611 commands devoted to build proof term also to build regular definitions.
612 A tentative semantics for the proof mode commands (called tactics)
613 in terms of sequent calculus rules are given in the
614 <a href="#appendix">appendix</a>.</p>
616 <pre><code>ndefinition xcover_set :
617 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
620 <p><img src="xcover-set-1.png" alt="xcover-set-1" /></p>
622 <p>The system asks for a proof of the full statement, in an empty context.</p>
624 <p>The <code>#</code> command is the ∀-introduction rule, it gives a name to an
625 assumption putting it in the context, and generates a λ-abstraction
626 in the proof term.</p>
628 <pre><code>#cover; #A; #C; #U;
631 <p><img src="xcover-set-2.png" alt="xcover-set-2" /></p>
633 <p>We have now to provide a proposition, and we exhibit it. We left
634 a part of it implicit; since the system cannot infer it it will
636 Note that the type of <code>∀y:A.y ∈ C → ?</code> is a proposition
637 whenever <code>?</code> is a proposition.</p>
639 <pre><code>napply (∀y:A.y ∈ C → ?);
642 <p><img src="xcover-set-3.png" alt="xcover-set-3" /></p>
644 <p>The proposition we want to provide is an application of the
645 cover relation we have abstracted in the context. The command
646 <code>napply</code>, if the given term has not the expected type (in that
647 case it is a product versus a proposition) it applies it to as many
648 implicit arguments as necessary (in that case <code>? ? ?</code>).</p>
650 <pre><code>napply cover;
653 <p><img src="xcover-set-4.png" alt="xcover-set-4" /></p>
655 <p>The system will now ask in turn the three implicit arguments
656 passed to cover. The syntax <code>##[</code> allows to start a branching
657 to tackle every sub proof individually, otherwise every command
658 is applied to every subproof. The command <code>##|</code> switches to the next
659 subproof and <code>##]</code> ends the branching. </p>
661 <pre><code>##[ napply A;
668 <h2>The fish relation</h2>
670 <p>The definition of fish works exactly the same way as for cover, except
671 that it is defined as a coinductive proposition.</p>
673 <pre><code>ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
678 notation "hvbox(a break ⋉ b)" non associative with precedence 45
679 for @{ 'fish $a $b }.
681 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
683 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
684 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
688 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
689 interpretation "fish" 'fish a U = (fish ? U a).
692 <h2>Introduction rule for fish</h2>
694 <p>Matita is able to generate elimination rules for inductive types</p>
696 <pre><code>(** ncheck cover_rect_CProp0. *)
699 <p>but not introduction rules for the coinductive case. </p>
701 <pre><code> P ⊆ U (∀x,j.x ∈ P → C(x,j) ≬ P) a ∈ P
702 (fish intro) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
706 <p>We thus have to define the introduction rule for fish by co-recursion.
707 Here we again use the proof mode of Matita to exhibit the body of the
708 corecursive function.</p>
710 <pre><code>nlet corec fish_rec (A:Ax) (U: Ω^A)
712 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
715 <p><img src="def-fish-rec-1.png" alt="def-fish-rec-1" /></p>
717 <p>Note the first item of the context, it is the corecursive function we are
718 defining. This item allows to perform the recursive call, but we will be
719 allowed to do such call only after having generated a constructor of
720 the fish coinductive type.</p>
722 <p>We introduce <code>a</code> and <code>p</code>, and then return the fish constructor <code>cfish</code>.
723 Since the constructor accepts two arguments, the system asks for them.</p>
725 <pre><code>#a; #a_in_P; napply cfish;
728 <p><img src="def-fish-rec-2.png" alt="def-fish-rec-2" /></p>
730 <p>The first one is a proof that <code>a ∈ U</code>. This can be proved using <code>H1</code> and <code>p</code>.
731 With the <code>nchange</code> tactic we change <code>H1</code> into an equivalent form (this step
732 can be skipped, since the system would be able to unfold the definition
733 of inclusion by itself)</p>
735 <pre><code>##[ nchange in H1 with (∀b.b∈P → b∈U);
738 <p><img src="def-fish-rec-2-1.png" alt="def-fish-rec-2-1" /></p>
740 <p>It is now clear that <code>H1</code> can be applied. Again <code>napply</code> adds two
741 implicit arguments to <code>H1 ? ?</code>, obtaining a proof of <code>? ∈ U</code> given a proof
742 that <code>? ∈ P</code>. Thanks to unification, the system understands that <code>?</code> is actually
743 <code>a</code>, and it asks a proof that <code>a ∈ P</code>.</p>
745 <pre><code> napply H1;
748 <p><img src="def-fish-rec-3.png" alt="def-fish-rec-3" /></p>
750 <p>The <code>nassumption</code> tactic looks for the required proof in the context, and in
751 that cases finds it in the last context position. </p>
753 <p>We move now to the second branch of the proof, corresponding to the second
754 argument of the <code>cfish</code> constructor.</p>
756 <p>We introduce <code>i</code> and then we destruct <code>H2 a p i</code>, that being a proof
757 of an overlap predicate, give as an element and a proof that it is
758 both in <code>𝐂 a i</code> and <code>P</code>.</p>
760 <pre><code> nassumption;
761 ##| #i; ncases (H2 a a_in_P i);
764 <p><img src="def-fish-rec-5.png" alt="def-fish-rec-5" /></p>
766 <p>We then introduce <code>x</code>, break the conjunction (the <code>*;</code> command is the
767 equivalent of <code>ncases</code> but operates on the first hypothesis that can
768 be introduced). We then introduce the two sides of the conjunction.</p>
770 <pre><code> #x; *; #xC; #xP;
773 <p><img src="def-fish-rec-5-1.png" alt="def-fish-rec-5-1" /></p>
775 <p>The goal is now the existence of a point in <code>𝐂 a i</code> fished by <code>U</code>.
776 We thus need to use the introduction rule for the existential quantifier.
777 In CIC it is a defined notion, that is an inductive type with just
778 one constructor (one introduction rule) holding the witness and the proof
779 that the witness satisfies a proposition.</p>
785 <p>Instead of trying to remember the name of the constructor, that should
786 be used as the argument of <code>napply</code>, we can ask the system to find by
787 itself the constructor name and apply it with the <code>@</code> tactic.
788 Note that some inductive predicates, like the disjunction, have multiple
789 introduction rules, and thus <code>@</code> can be followed by a number identifying
795 <p><img src="def-fish-rec-6.png" alt="def-fish-rec-6" /></p>
797 <p>After choosing <code>x</code> as the witness, we have to prove a conjunction,
798 and we again apply the introduction rule for the inductively defined
799 predicate <code>∧</code>.</p>
801 <pre><code> ##[ napply x
805 <p><img src="def-fish-rec-7.png" alt="def-fish-rec-7" /></p>
807 <p>The left hand side of the conjunction is trivial to prove, since it
808 is already in the context. The right hand side needs to perform
809 the co-recursive call.</p>
811 <pre><code> ##[ napply xC;
812 ##| napply (fish_rec ? U P);
815 <p><img src="def-fish-rec-9.png" alt="def-fish-rec-9" /></p>
817 <p>The co-recursive call needs some arguments, but all of them are
818 in the context. Instead of explicitly mention them, we use the
819 <code>nassumption</code> tactic, that simply tries to apply every context item.</p>
821 <pre><code> nassumption;
828 <h2>Subset of covered/fished points</h2>
830 <p>We now have to define the subset of <code>S</code> of points covered by <code>U</code>.
831 We also define a prefix notation for it. Remember that the precedence
832 of the prefix form of a symbol has to be higher than the precedence
833 of its infix form.</p>
835 <pre><code>ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
837 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
839 interpretation "coverage cover" 'coverage U = (coverage ? U).
842 <p>Here we define the equation characterizing the cover relation.
843 Even if it is not part of the paper, we proved that <code>◃(U)</code> is
844 the minimum solution for
845 such equation, the interested reader should be able to reply the proof
848 <pre><code>ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
849 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
851 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
854 ##[ #bU; @1; nassumption;
855 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
857 ##| #_; napply CaiU; nassumption; ##] ##]
858 ##| ncases H; ##[ #E; @; nassumption]
859 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
863 ntheorem coverage_min_cover_equation :
864 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
865 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
866 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
867 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
872 <p>We similarly define the subset of points "fished" by <code>F</code>, the
873 equation characterizing <code>⋉(F)</code> and prove that fish is
874 the biggest solution for such equation.</p>
876 <pre><code>notation "⋉F" non associative with precedence 55
879 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
881 interpretation "fished fish" 'fished F = (fished ? F).
883 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
884 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
886 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
887 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
888 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
890 ##| #aF; #H1; @ aF; napply H1;
894 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
895 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
896 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
900 <h2>Part 2, the new set of axioms</h2>
902 <p>Since the name of defined objects (record included) has to be unique
903 within the same file, we prefix every field name
904 in the new definition of the axiom set with <code>n</code>.</p>
906 <pre><code>nrecord nAx : Type[1] ≝ {
909 nD: ∀a:nS. nI a → Type[0];
910 nd: ∀a:nS. ∀i:nI a. nD a i → nS
914 <p>We again define a notation for the projections, making the
915 projected record an implicit argument. Note that, since we already have
916 a notation for <code>𝐈</code>, we just add another interpretation for it. The
917 system, looking at the argument of <code>𝐈</code>, will be able to choose
918 the correct interpretation. </p>
920 <pre><code>notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
921 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
923 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
924 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
926 interpretation "D" 'D a i = (nD ? a i).
927 interpretation "d" 'd a i j = (nd ? a i j).
928 interpretation "new I" 'I a = (nI ? a).
931 <p>The first result the paper presents to motivate the new formulation
932 of the axiom set is the possibility to define and old axiom set
933 starting from a new one and vice versa. The key definition for
934 such construction is the image of d(a,i).
935 The paper defines the image as</p>
938 <p>Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }</p>
941 <p>but this not so formal notation poses some problems. The image is
942 often used as the left hand side of the ⊆ predicate</p>
945 <p>Im[d(a,i)] ⊆ V</p>
948 <p>Of course this writing is interpreted by the authors as follows </p>
951 <p>∀j:D(a,i). d(a,i,j) ∈ V</p>
954 <p>If we need to use the image to define <code>𝐂</code> (a subset of <code>S</code>) we are obliged to
955 form a subset, i.e. to place a single variable <code>{ here | … }</code> of type <code>S</code>.</p>
958 <p>Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }</p>
961 <p>This poses no theoretical problems, since <code>S</code> is a Type and thus
962 equipped with the <code>Id</code> equality. If <code>S</code> was a setoid, here the equality
963 would have been the one of the setoid.</p>
965 <p>Unless we define two different images, one for stating that the image is ⊆ of
966 something and another one to define <code>𝐂</code>, we end up using always the latter.
967 Thus the statement <code>Im[d(a,i)] ⊆ V</code> unfolds to</p>
970 <p>∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V</p>
973 <p>That, up to rewriting with the equation defining <code>x</code>, is what we mean.
974 Since we decided to use <code>Id</code> the rewriting always work (the elimination
975 principle for <code>Id</code> is Leibnitz's equality, that is quantified over
978 <p>The problem that arises if we decide to make <code>S</code> a setoid is that
979 <code>V</code> has to be extensional w.r.t. the equality of <code>S</code> (i.e. the characteristic
980 functional proposition has to quotient its input with a relation bigger
981 than the one of <code>S</code>.</p>
984 <p>∀x,y:S. x = y → x ∈ V → y ∈ V</p>
987 <p>If <code>V</code> is a complex construction, the proof may not be trivial.</p>
989 <pre><code>include "logic/equality.ma".
991 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
993 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
994 notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
996 interpretation "image" 'Im a i = (image ? a i).
999 <p>Thanks to our definition of image, we can define a function mapping a
1000 new axiom set to an old one and vice versa. Note that in the second
1001 definition, when we give the <code>𝐝</code> component, the projection of the
1002 Σ-type is inlined (constructed on the fly by <code>*;</code>)
1003 while in the paper it was named <code>fst</code>.</p>
1005 <pre><code>ndefinition Ax_of_nAx : nAx → Ax.
1006 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
1009 ndefinition nAx_of_Ax : Ax → nAx.
1011 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
1012 ##| #a; #i; *; #x; #_; napply x;
1017 <p>We now prove that the two function above form a retraction pair for
1018 the <code>C</code> component of the axiom set. To prove that we face a little
1019 problem since CIC is not equipped with η-conversion. This means that
1020 the followin does not hold (where <code>A</code> is an axiom set).</p>
1023 <p>A = (S A, I A, C A)</p>
1026 <p>This can be proved only under a pattern mach over <code>A</code>, that means
1027 that the resulting computation content of the proof is a program
1028 that computes something only if <code>A</code> is a concrete axiom set.</p>
1030 <p>To state the lemma we have to drop notation, and explicitly
1031 give the axiom set in input to the <code>C</code> projection.</p>
1033 <pre><code>nlemma Ax_nAx_equiv :
1034 ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
1035 C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
1036 #A; #a; #i; @; #b; #H;
1039 <p><img src="retr-1.png" alt="retr-1" /></p>
1041 <p>Look for example the type of <code>a</code>. The command <code>nchange in a with A</code>
1042 would fail because of the missing η-conversion rule. We have thus
1043 to pattern match over <code>A</code> and introduce its pieces.</p>
1045 <pre><code>##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
1048 <p><img src="retr-2.png" alt="retr-2" /></p>
1050 <p>Now the system accepts that the type of <code>a</code> is the fist component
1051 of the axiom set, now called <code>S</code>. Unfolding definitions in <code>H</code> we discover
1052 there is still some work to do.</p>
1054 <pre><code> nchange in a with S; nwhd in H;
1057 <p><img src="retr-3.png" alt="retr-3" /></p>
1059 <p>To use the equation defining <code>b</code> we have to eliminate <code>H</code>. Unfolding
1060 definitions in <code>x</code> tell us there is still something to do. The <code>nrewrite</code>
1061 tactic is a shortcut for the elimination principle of the equality.
1062 It accepts an additional argument <code><</code> or <code>></code> to rewrite left-to-right
1063 or right-to-left. </p>
1065 <pre><code> ncases H; #x; #E; nrewrite > E; nwhd in x;
1068 <p><img src="retr-4.png" alt="retr-4" /></p>
1070 <p>We defined <code>𝐝</code> to be the first projection of <code>x</code>, thus we have to
1071 eliminate <code>x</code> to actually compute <code>𝐝</code>. </p>
1073 <p>The remaining part of the proof it not interesting and poses no
1076 <pre><code> ncases x; #b; #Hb; nnormalize; nassumption;
1077 ##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
1078 ##[ @ b; nassumption;
1079 ##| nnormalize; @; ##]
1084 <p>We then define the inductive type of ordinals, parametrized over an axiom
1085 set. We also attach some notations to the constructors.</p>
1087 <pre><code>ninductive Ord (A : nAx) : Type[0] ≝
1089 | oS : Ord A → Ord A
1090 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
1092 notation "0" non associative with precedence 90 for @{ 'oO }.
1093 notation "x+1" non associative with precedence 50 for @{'oS $x }.
1094 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
1096 interpretation "ordinals Zero" 'oO = (oO ?).
1097 interpretation "ordinals Succ" 'oS x = (oS ? x).
1098 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
1101 <p>The definition of <code>U⎽x</code> is by recursion over the ordinal <code>x</code>.
1102 We thus define a recursive function using the <code>nlet rec</code> command.
1103 The <code>on x</code> directive tells
1104 the system on which argument the function is (structurally) recursive.</p>
1106 <p>In the <code>oS</code> case we use a local definition to name the recursive call
1107 since it is used twice.</p>
1109 <p>Note that Matita does not support notation in the left hand side
1110 of a pattern match, and thus the names of the constructors have to
1111 be spelled out verbatim.</p>
1113 <pre><code>nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
1116 | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
1117 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
1119 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
1120 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
1122 interpretation "famU" 'famU U x = (famU ? U x).
1125 <p>We attach as the input notation for U_x the similar <code>U⎽x</code> where underscore,
1126 that is a character valid for identifier names, has been replaced by <code>⎽</code> that is
1127 not. The symbol <code>⎽</code> can act as a separator, and can be typed as an alternative
1128 for <code>_</code> (i.e. pressing ALT-L after <code>_</code>). </p>
1130 <p>The notion ◃(U) has to be defined as the subset of elements <code>y</code> <br />
1131 belonging to <code>U⎽x</code> for some <code>x</code>. Moreover, we have to define the notion
1132 of cover between sets again, since the one defined at the beginning
1133 of the tutorial works only for the old axiom set.</p>
1135 <pre><code>ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝
1136 λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
1138 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
1139 ∀y.y ∈ C → y ∈ c A U.
1141 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
1142 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
1143 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
1146 <p>Before proving that this cover relation validates the reflexivity and infinity
1147 rules, we prove this little technical lemma that is used in the proof for the
1150 <pre><code>nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
1151 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
1155 <p>The proof of infinity uses the following form of the Axiom of Choice,
1156 that cannot be proved inside Matita, since the existential quantifier
1157 lives in the sort of predicative propositions while the sigma in the conclusion
1158 lives in the sort of data types, and thus the former cannot be eliminated
1159 to provide the witness for the second.</p>
1161 <pre><code>naxiom AC : ∀A,a,i,U.
1162 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
1165 <p>Note that, if we will decide later to identify ∃ and Σ, <code>AC</code> is
1166 trivially provable</p>
1168 <pre><code>nlemma AC_exists_is_sigma : ∀A,a,i,U.
1169 (∀j:𝐃 a i.Σx:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
1170 #A; #a; #i; #U; #H; @;
1171 ##[ #j; ncases (H j); #x; #_; napply x;
1172 ##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
1176 <p>In case we made <code>S</code> a setoid, the following property has to be proved</p>
1179 <p>nlemma U<em>x</em>is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.</p>
1182 <p>Anyway this proof is a non trivial induction over x, that requires <code>𝐈</code> and <code>𝐃</code> to be
1183 declared as morphisms. </p>
1185 <p>The reflexivity proof is trivial, it is enough to provide the ordinal <code>0</code>
1186 as a witness, then <code>◃(U)</code> reduces to <code>U</code> by definition,
1187 hence the conclusion. Note that <code>0</code> is between <code>(</code> and <code>)</code> to
1188 make it clear that it is a term (an ordinal) and not the number
1189 of the constructor we want to apply (that is the first and only one
1190 of the existential inductive type).</p>
1192 <pre><code>ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
1193 #A; #U; #a; #H; @ (0); napply H;
1197 <p>We now proceed with the proof of the infinity rule.</p>
1199 <pre><code>alias symbol "covers" (instance 3) = "new covers set".
1200 ntheorem new_coverage_infinity:
1201 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
1205 <p><img src="n-cov-inf-1.png" alt="n-cov-inf-1" /></p>
1207 <p>We eliminate the existential, obtaining an <code>i</code> and a proof that the
1208 image of <code>𝐝 a i</code> is covered by U. The <code>nnormalize</code> tactic computes the normal
1209 form of <code>H</code>, thus expands the definition of cover between sets.</p>
1211 <pre><code>*; #i; #H; nnormalize in H;
1214 <p><img src="n-cov-inf-2.png" alt="n-cov-inf-2" /></p>
1216 <p>When the paper proof considers <code>H</code>, it implicitly substitutes assumed
1217 equation defining <code>y</code> in its conclusion.
1218 In Matita this step is not completely trivial.
1219 We thus assert (<code>ncut</code>) the nicer form of <code>H</code> and prove it.</p>
1221 <pre><code>ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
1224 <p><img src="n-cov-inf-3.png" alt="n-cov-inf-3" /></p>
1226 <p>After introducing <code>z</code>, <code>H</code> can be applied (choosing <code>𝐝 a i z</code> as <code>y</code>).
1227 What is the left to prove is that <code>∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j</code>, that
1228 becomes trivial if <code>j</code> is chosen to be <code>z</code>. </p>
1230 <pre><code> #z; napply H; @ z; @; ##] #H';
1233 <p><img src="n-cov-inf-4.png" alt="n-cov-inf-4" /></p>
1235 <p>Under <code>H'</code> the axiom of choice <code>AC</code> can be eliminated, obtaining the <code>f</code> and
1236 its property. Note that the axiom <code>AC</code> was abstracted over <code>A,a,i,U</code> before
1237 assuming <code>(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)</code>. Thus the term that can be eliminated
1238 is <code>AC ???? H'</code> where the system is able to infer every <code>?</code>. Matita provides
1239 a facility to specify a number of <code>?</code> in a compact way, i.e. <code>…</code>. The system
1240 expand <code>…</code> first to zero, then one, then two, three and finally four question
1241 marks, "guessing" how may of them are needed. </p>
1243 <pre><code>ncases (AC … H'); #f; #Hf;
1246 <p><img src="n-cov-inf-5.png" alt="n-cov-inf-5" /></p>
1248 <p>The paper proof does now a forward reasoning step, deriving (by the ord_subset
1249 lemma we proved above) <code>Hf'</code> i.e. 𝐝 a i j ∈ U⎽(Λf).</p>
1251 <pre><code>ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
1252 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
1255 <p><img src="n-cov-inf-6.png" alt="n-cov-inf-6" /></p>
1257 <p>To prove that <code>a◃U</code> we have to exhibit the ordinal x such that <code>a ∈ U⎽x</code>.</p>
1259 <pre><code>@ (Λ f+1);
1262 <p><img src="n-cov-inf-7.png" alt="n-cov-inf-7" /></p>
1264 <p>The definition of <code>U⎽(…+1)</code> expands to the union of two sets, and proving
1265 that <code>a ∈ X ∪ Y</code> is, by definition, equivalent to prove that <code>a</code> is in <code>X</code> or <code>Y</code>.
1266 Applying the second constructor <code>@2;</code> of the disjunction,
1267 we are left to prove that <code>a</code> belongs to the right hand side of the union.</p>
1272 <p><img src="n-cov-inf-8.png" alt="n-cov-inf-8" /></p>
1274 <p>We thus provide <code>i</code> as the witness of the existential, introduce the
1275 element being in the image and we are
1276 left to prove that it belongs to <code>U⎽(Λf)</code>. In the meanwhile, since belonging
1277 to the image means that there exists an object in the domain …, we eliminate the
1278 existential, obtaining <code>d</code> (of type <code>𝐃 a i</code>) and the equation defining <code>x</code>. </p>
1280 <pre><code>@i; #x; *; #d; #Hd;
1283 <p><img src="n-cov-inf-9.png" alt="n-cov-inf-9" /></p>
1285 <p>We just need to use the equational definition of <code>x</code> to obtain a conclusion
1286 that can be proved with <code>Hf'</code>. We assumed that <code>U⎽x</code> is extensional for
1287 every <code>x</code>, thus we are allowed to use <code>Hd</code> and close the proof.</p>
1289 <pre><code>nrewrite > Hd; napply Hf';
1293 <p>The next proof is that ◃(U) is minimal. The hardest part of the proof
1294 is to prepare the goal for the induction. The desiderata is to prove
1295 <code>U⎽o ⊆ V</code> by induction on <code>o</code>, but the conclusion of the lemma is,
1296 unfolding all definitions:</p>
1299 <p>∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V</p>
1302 <pre><code>nlemma new_coverage_min :
1303 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1304 #A; #U; #V; #HUV; #Im;#b;
1307 <p><img src="n-cov-min-2.png" alt="n-cov-min-2" /></p>
1309 <p>After all the introductions, event the element hidden in the ⊆ definition,
1310 we have to eliminate the existential quantifier, obtaining the ordinal <code>o</code></p>
1315 <p><img src="n-cov-min-3.png" alt="n-cov-min-3" /></p>
1317 <p>What is left is almost right, but the element <code>b</code> is already in the
1318 context. We thus generalize every occurrence of <code>b</code> in
1319 the current goal, obtaining <code>∀c.c ∈ U⎽o → c ∈ V</code> that is <code>U⎽o ⊆ V</code>.</p>
1321 <pre><code>ngeneralize in match b; nchange with (U⎽o ⊆ V);
1324 <p><img src="n-cov-min-4.png" alt="n-cov-min-4" /></p>
1326 <p>We then proceed by induction on <code>o</code> obtaining the following goals</p>
1331 <p><img src="n-cov-min-5.png" alt="n-cov-min-5" /></p>
1333 <p>All of them can be proved using simple set theoretic arguments,
1334 the induction hypothesis and the assumption <code>Im</code>.</p>
1336 <pre><code>##[ napply HUV;
1337 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1338 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1339 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1343 <p>The notion <code>F⎽x</code> is again defined by recursion over the ordinal <code>x</code>.</p>
1345 <pre><code>nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1348 | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
1349 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1352 interpretation "famF" 'famU U x = (famF ? U x).
1354 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1356 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1357 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1360 <p>The proof of compatibility uses this little result, that we
1361 proved outside the main proof. </p>
1363 <pre><code>nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1364 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1368 <p>We assume the dual of the axiom of choice, as in the paper proof.</p>
1370 <pre><code>naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
1371 (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x))
1372 → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
1375 <p>Proving the anti-reflexivity property is simple, since the
1376 assumption <code>a ⋉ F</code> states that for every ordinal <code>x</code> (and thus also 0)
1377 <code>a ∈ F⎽x</code>. If <code>x</code> is choose to be <code>0</code>, we obtain the thesis.</p>
1379 <pre><code>ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1380 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1384 <p>We now prove the compatibility property for the new fish relation.</p>
1386 <pre><code>ntheorem new_fish_compatible:
1387 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1388 #A; #F; #a; #aF; #i; nnormalize;
1391 <p><img src="n-f-compat-1.png" alt="n-f-compat-1" /></p>
1393 <p>After reducing to normal form the goal, we observe it is exactly the conclusion of
1394 the dual axiom of choice we just assumed. We thus apply it ad introduce the
1395 fcuntion <code>f</code>.</p>
1397 <pre><code>napply AC_dual; #f;
1400 <p><img src="n-f-compat-2.png" alt="n-f-compat-2" /></p>
1402 <p>The hypothesis <code>aF</code> states that <code>a⋉F⎽x</code> for every <code>x</code>, and we choose <code>Λf+1</code>.</p>
1404 <pre><code>nlapply (aF (Λf+1)); #aLf;
1407 <p><img src="n-f-compat-3.png" alt="n-f-compat-3" /></p>
1409 <p>Since F_(Λf+1) is defined by recursion and we actually have a concrete input
1410 <code>Λf+1</code> for that recursive function, it can be computed.
1411 Anyway, using the <code>nnormalize</code>
1412 tactic would reduce too much (both the <code>+1</code> and the <code>Λf</code> steps would be performed);
1413 we thus explicitly give a convertible type for that hypothesis, corresponding
1414 the computation of the <code>+1</code> step, plus the unfolding the definition of
1415 the intersection.</p>
1417 <pre><code>nchange in aLf with
1418 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
1421 <p><img src="n-f-compat-4.png" alt="n-f-compat-4" /></p>
1423 <p>We are interested in the right hand side of <code>aLf</code>, an in particular to
1424 its intance where the generic index in <code>𝐈 a</code> is <code>i</code>.</p>
1426 <pre><code>ncases aLf; #_; #H; nlapply (H i);
1429 <p><img src="n-f-compat-5.png" alt="n-f-compat-5" /></p>
1431 <p>We then eliminate the existential, obtaining <code>j</code> and its property <code>Hj</code>. We provide
1432 the same witness </p>
1434 <pre><code>*; #j; #Hj; @j;
1437 <p><img src="n-f-compat-6.png" alt="n-f-compat-6" /></p>
1439 <p>What is left to prove is exactly the <code>co_ord_subset</code> lemma we factored out
1440 of the main proof.</p>
1442 <pre><code>napply (co_ord_subset … Hj);
1446 <p>The proof that <code>⋉(F)</code> is maximal is exactly the dual one of the
1447 minimality of <code>◃(U)</code>. Thus the main problem is to obtain <code>G ⊆ F⎽o</code>
1448 before doing the induction over <code>o</code>.</p>
1450 <pre><code>ntheorem max_new_fished:
1451 ∀A:nAx.∀G:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1452 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1453 ngeneralize in match HbG; ngeneralize in match b;
1454 nchange with (G ⊆ F⎽o);
1457 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1458 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1462 <p><img src="n-f-max-1.png" alt="n-f-max-1" /></p>
1464 <p>Note that here the right hand side of <code>∈</code> is <code>G</code> and not <code>F⎽p</code> as
1465 in the dual proof. If <code>S</code> was declare to be a setoid, to finish this proof
1466 would be enough to assume <code>G</code> extensional, and no proof of the
1467 extensionality of <code>F⎽p</code> is required. </p>
1469 <div id="appendix" class="anchor"></div>
1471 <h2>Appendix: tactics explanation</h2>
1473 <p>In this appendix we try to give a description of tactics
1474 in terms of sequent calculus rules annotated with proofs.
1475 The <code>:</code> separator has to be read as <em>is a proof of</em>, in the spirit
1476 of the Curry-Howard isomorphism.</p>
1478 <pre><code> Γ ⊢ f : A_1 → … → A_n → B Γ ⊢ ?_i : A_i
1479 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1480 Γ ⊢ (f ?_1 … ?_n ) : B
1482 Γ ⊢ ? : F → B Γ ⊢ f : F
1483 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1488 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1489 Γ ⊢ λx:T.? : ∀x:T.P(x)
1492 Γ ⊢ ?_i : args_i → P(k_i args_i)
1493 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1494 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1497 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1498 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1499 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1502 <p>Where <code>T_rect_CProp0</code> is the induction principle for the
1503 inductive type <code>T</code>.</p>
1505 <pre><code> Γ ⊢ ? : Q Q ≡ P
1506 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1510 <p>Where the equivalence relation between types <code>≡</code> keeps into account
1511 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1512 definition unfolding), ι-reduction (pattern matching simplification),
1513 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1516 <pre><code> Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1517 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1521 Γ; H : Q; Δ ⊢ ? : G P →* Q
1522 nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1526 <p>Where <code>Q</code> is the normal form of <code>P</code> considering βδζιμν-reduction steps.</p>
1528 <pre><code> Γ ⊢ ? : Q P →* Q
1529 nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1533 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1534 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1539 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1543 nrewrite < Ed; napply cG;
1544 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1545 #b; #Hb; #d; napply (Hf d); napply Hb;
1551 Last updated: $Date: 2009-10-28 15:46:19 +0100 (Wed, 28 Oct 2009) $
projects / helm.git / blob