]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/topology/igft.ma
06f2c08e5d18f019b6c5fe9fde0c7ebec68f4ada
[helm.git] / helm / software / matita / nlibrary / topology / igft.ma
1 (*D
2
3 Matita Tutorial: inductively generated formal topologies
4 ======================================================== 
5
6 This is a not so short introduction to [Matita][2], based on
7 the formalization of the paper
8
9 > Between formal topology and game theory: an
10 > explicit solution for the conditions for an
11 > inductive generation of formal topologies
12
13 by Stefano Berardi and Silvio Valentini. 
14
15 The tutorial is by Enrico Tassi. 
16
17 The tutorial spends a considerable amount of effort in defining 
18 notations that resemble the ones used in the original paper. We believe
19 this is a important part of every formalization, not only from the aesthetic 
20 point of view, but also from the practical point of view. Being 
21 consistent allows to follow the paper in a pedantic way, and hopefully
22 to make the formalization (at least the definitions and proved
23 statements) readable to the author of the paper. 
24
25 The formalization uses the ng (new generation) version of Matita
26 (that will be named 1.x when finally released). 
27 Last stable release of the "old" system is named 0.5.7; the ng system
28 is coexisting with the old one in every development release with a 
29 version strictly greater than 0.5.7.
30
31 Orienteering
32 ------------
33
34 The graphical interface of Matita is composed of three windows:
35 the script window, on the left, is where you type; the sequent
36 window on the top right is where the system shows you the ongoing proof;
37 the error window, on the bottom right, is where the system complains.
38 On the top of the script window five buttons drive the processing of
39 the proof script. From left to right they request the system to:
40
41 - go back to the beginning of the script
42 - go back one step
43 - go to the current cursor position
44 - advance one step
45 - advance to the end of the script
46
47 When the system processes a command, it locks the part of the script
48 corresponding to the command, such that you cannot edit it anymore 
49 (without going back). Locked parts are coloured in blue.
50
51 The sequent window is hyper textual, i.e. you can click on symbols
52 to jump to their definition, or switch between different notations
53 for the same expression (for example, equality has two notations,
54 one of them makes the type of the arguments explicit).  
55
56 Everywhere in the script you can use the `ncheck (term).` command to
57 ask for the type a given term. If you do that in the middle of a proof,
58 the term is assumed to live in the current proof context (i.e. can use
59 variables introduced so far).
60
61 To ease the typing of mathematical symbols, the script window
62 implements two unusual input facilities:
63
64 - some TeX symbols can be typed using their TeX names, and are 
65   automatically converted to UTF-8 characters. For a list of 
66   the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
67   Moreover some ASCII-art is understood as well, like `=>` and `->`
68   to mean double or single arrows.
69   Here we recall some of these "shortcuts":
70
71   - ∀ can be typed with `\forall`
72   - λ can be typed with `\lambda`
73   - ≝ can be typed with `\def` or `:=`
74   - → can be typed with `\to` or `->`
75   
76 - some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
77   The user can cycle between variants typing one of them and then
78   pressing ALT-L. Note that also letters do have variants, for
79   example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … 
80   Variants are listed in the aforementioned TeX/UTF-8 table. 
81
82 The syntax of terms (and types) is the one of the λ-calculus CIC
83 on which Matita is based. The main syntactical difference w.r.t. 
84 the usual mathematical notation is the function application, written
85 `(f x y)` in place of `f(x,y)`. 
86
87 Pressing `F1` opens the Matita manual.
88
89 CIC (as [implemented in Matita][3]) in a nutshell
90 ------------------------------------------------- 
91
92 CIC is a full and functional Pure Type System (all products do exist,
93 and their sort is is determined by the target) with an impredicative sort
94 Prop and a predicative sort Type. It features both dependent types and 
95 polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
96 the same syntax, and they can occur in types. 
97
98 The environment used for in the typing judgement can be populated with
99 well typed definitions or theorems, (co)inductive types validating positivity
100 conditions and recursive functions provably total by simple syntactical 
101 analysis (recursive calls are allowed only on structurally smaller subterms). 
102 Co-recursive 
103 functions can be defined as well, and must satisfy the dual condition, i.e.
104 performing the recursive call only after having generated a constructor (a piece
105 of output).
106
107 The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
108 types defined in the environment. This construct, together with the possibility to
109 definable total recursive functions, allows to define eliminators (or constructors)
110 for (co)inductive types. The λ-calculus is also equipped with explicitly typed 
111 local definitions (let in) that in the degenerate case work as casts (i.e.
112 the type annotation `(t : T)`  is implemented as `let x : T ≝ t in x`). 
113
114 Types are compare up to conversion. Since types may depend on terms, conversion
115 involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
116 definition unfolding), ι-reduction (pattern matching simplification),
117 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
118 computation).
119
120 Since we are going to formalize constructive and predicative mathematics
121 in an intensional type theory like CIC, we try to establish some terminology. 
122 Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
123 not quotiented set). We will avoid using `Id` (Leibniz equality), 
124 thus we will explicitly equip a set with an equivalence relation when needed.
125 We will call this structure a _setoid_. Note that we will
126 attach the infix `=` symbol only to the equality of a setoid,
127 not to Id.
128
129 We write `Type[i]` to mention a Type in the predicative hierarchy 
130 of types. To ease the comprehension we will use `Type[0]` for sets, 
131 and `Type[1]` for classes. The index `i` is just a label: constraints among
132 universes are declared by the user. The standard library defines
133
134 > Type[0] < Type[1] < Type[2]
135
136 For every `Type[i]` there is a corresponding level of predicative
137 propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
138 `Type[j]` unless it holds no computational content (i.e. it is an inductive type
139 with 0 or 1 constructors with propositional arguments, like `Id` and `And` 
140 but not like `Or`). 
141
142
143 The standard library and the `include` command
144 ----------------------------------------------
145
146 Some basic notions, like subset, membership, intersection and union
147 are part of the standard library of Matita.
148
149 These notions come with some standard notation attached to them:
150
151 - A ∪ B can be typed with `A \cup B`
152 - A ∩ B can be typed with `A \cap B` 
153 - A ≬ B can be typed with `A \between B`
154 - x ∈ A can be typed with `x \in A` 
155 - Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A` 
156
157 The `include` command tells Matita to load a part of the library, 
158 in particular the part that we will use can be loaded as follows: 
159
160 D*)
161
162 include "sets/sets.ma".
163
164 (*D
165
166 Some basic results that we will use are also part of the sets library:
167
168 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
169 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
170
171 Defining Axiom set
172 ------------------
173
174 A set of axioms is made of a set(oid) `S`, a family of sets `I` and a 
175 family `C` of subsets of `S` indexed by elements `a` of `S` 
176 and elements of `I(a)`.
177
178 It is desirable to state theorems like "for every set of axioms, …"
179 without explicitly mentioning S, I and C. To do that, the three 
180 components have to be grouped into a record (essentially a dependently
181 typed tuple). The system is able to generate the projections
182 of the record automatically, and they are named as the fields of
183 the record. So, given an axiom set `A` we can obtain the set
184 with `S A`, the family of sets with `I A` and the family of subsets
185 with `C A`.
186
187 D*)
188
189 nrecord Ax : Type[1] ≝ { 
190   S :> setoid;
191   I :  S → Type[0];
192   C :  ∀a:S. I a → Ω ^ S
193 }.
194
195 (*D
196
197 Forget for a moment the `:>` that will be detailed later, and focus on
198 the record definition. It is made of a list of pairs: a name, followed
199 by `:` and the its type. It is a dependently typed tuple, thus
200 already defined names (fields) can be used in the types that follow. 
201
202 Note that `S` is declared to be a `setoid` and not a Type. The original
203 paper probably also considers I to generate setoids, and both I and C
204 to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use
205 setoids only when strictly needed (i.e. where we want to talk about 
206 equality). Setoids will play a role only when we will define
207 the alternative version of the axiom set.
208
209 Note that the field `S` was declared with `:>` instead of a simple `:`.
210 This declares the `S` projection to be a coercion. A coercion is 
211 a "cast" function the system automatically inserts when it is needed.
212 In that case, the projection `S` has type `Ax → setoid`, and whenever
213 the expected type of a term is `setoid` while its type is `Ax`, the 
214 system inserts the coercion around it, to make the whole term well typed.
215
216 When formalizing an algebraic structure, declaring the carrier as a 
217 coercion is a common practice, since it allows to write statements like
218
219     ∀G:Group.∀x:G.x * x^-1 = 1 
220
221 The quantification over `x` of type `G` is ill-typed, since `G` is a term
222 (of type `Group`) and thus not a type. Since the carrier projection 
223 `carr` is a coercion, that maps a `Group` into the type of 
224 its elements, the system automatically inserts `carr` around `G`, 
225 obtaining `…∀x: carr G.…`. 
226
227 Coercions are hidden by the system when it displays a term.
228 In this particular case, the coercion `S` allows to write (and read):
229
230     ∀A:Ax.∀a:A.…
231
232 Since `A` is not a type, but it can be turned into a `setoid` by `S`
233 and a `setoid` can be turned into a type by its `carr` projection, the 
234 composed coercion `carr ∘ S` is silently inserted.
235
236 Implicit arguments
237 ------------------
238
239 Something that is not still satisfactory, is that the dependent type
240 of `I` and `C` are abstracted over the Axiom set. To obtain the
241 precise type of a term, you can use the `ncheck` command as follows.
242
243 D*) 
244
245 (** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *)
246 (** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *)
247
248 (*D
249
250 One would like to write `I a` and not `I A a` under a context where
251 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
252 mechanism simply `A`). In Matita, a question mark represents an implicit
253 argument, i.e. a missing piece of information the system is asked to
254 infer. Matita performs Hindley-Milner-style type inference, thus writing
255 `I ? a` is enough: since the second argument of `I` is typed by the 
256 first one, the first (omitted) argument can be inferred just 
257 computing the type of `a` (that is `A`).
258
259 D*) 
260
261 (** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *)
262
263 (*D
264
265 This is still not completely satisfactory, since you have always to type 
266 `?`; to fix this minor issue we have to introduce the notational
267 support built in Matita.
268
269 Notation for I and C
270 --------------------
271
272 Matita is quipped with a quite complex notational support,
273 allowing the user to define and use mathematical notations 
274 ([From Notation to Semantics: There and Back Again][1]). 
275
276 Since notations are usually ambiguous (e.g. the frequent overloading of 
277 symbols) Matita distinguishes between the term level, the 
278 content level, and the presentation level, allowing multiple 
279 mappings between the content and the term level. 
280
281 The mapping between the presentation level (i.e. what is typed on the 
282 keyboard and what is displayed in the sequent window) and the content
283 level is defined with the `notation` command. When followed by
284 `>`, it defines an input (only) notation.   
285
286 D*)
287
288 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
289 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
290
291 (*D
292
293 The first notation defines the writing `𝐈 a` where `a` is a generic
294 term of precedence 90, the maximum one. This high precedence forces
295 parentheses around any term of a lower precedence. For example `𝐈 x`
296 would be accepted, since identifiers have precedence 90, but
297 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
298 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
299
300 To obtain the `𝐈` is enough to type `I` and then cycle between its
301 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
302 regular letters or the round parentheses, thus their variants (like the 
303 bold ones) have to be used.
304
305 The first notation associates `𝐈 a` with `'I $a` where `'I` is a 
306 new content element to which a term `$a` is passed.
307
308 Content elements have to be interpreted, and possibly multiple, 
309 incompatible, interpretations can be defined.
310
311 D*)
312
313 interpretation "I" 'I a = (I ? a).
314 interpretation "C" 'C a i = (C ? a i).
315
316 (*D
317
318 The `interpretation` command allows to define the mapping between
319 the content level and the terms level. Here we associate the `I` and
320 `C` projections of the Axiom set record, where the Axiom set is an implicit 
321 argument `?` to be inferred by the system.
322
323 Interpretation are bi-directional, thus when displaying a term like 
324 `C _ a i`, the system looks for a presentation for the content element
325 `'C a i`. 
326
327 D*)
328
329 notation < "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
330 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
331
332 (*D
333
334 For output purposes we can define more complex notations, for example
335 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
336 the size of the arguments and lowering their baseline (i.e. putting them
337 as subscript), separating them with a comma followed by a little space.
338
339 The first (technical) definition
340 --------------------------------
341
342 Before defining the cover relation as an inductive predicate, one
343 has to notice that the infinity rule uses, in its hypotheses, the 
344 cover relation between two subsets, while the inductive predicate 
345 we are going to define relates an element and a subset.
346
347 An option would be to unfold the definition of cover between subsets,
348 but we prefer to define the abstract notion of cover between subsets
349 (so that we can attach a (ambiguous) notation to it).
350
351 Anyway, to ease the understanding of the definition of the cover relation 
352 between subsets, we first define the inductive predicate unfolding the 
353 definition, and we later refine it with.
354
355 D*)
356
357 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
358 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
359 | xcinfinity    : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
360
361 (*D
362
363 We defined the xcover (x will be removed in the final version of the 
364 definition) as an inductive predicate. The arity of the inductive
365 predicate has to be carefully analyzed:
366
367 >  (A : Ax) (U : Ω^A) : A → CProp[0]
368
369 The syntax separates with `:` abstractions that are fixed for every
370 constructor (introduction rule) and abstractions that can change. In that 
371 case the parameter `U` is abstracted once and for all in front of every 
372 constructor, and every occurrence of the inductive predicate is applied to
373 `U` in a consistent way. Arguments abstracted on the right of `:` are not
374 constant, for example the xcinfinity constructor introduces `a ◃ U`,
375 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
376 had side of the predicate changes, thus it has to be abstracted (in the arity
377 of the inductive predicate) on the right of `:`.
378
379 D*)
380
381 (** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
382
383 (*D
384
385 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
386 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
387
388 This notion has to be abstracted over the cover relation (whose
389 type is the arity of the inductive `xcover` predicate just defined).
390
391 Then it has to be abstracted over the arguments of that cover relation,
392 i.e. the axiom set and the set `U`, and the subset (in that case `𝐂 a i`)
393 sitting on the left hand side of `◃`. 
394
395 D*)
396
397 ndefinition cover_set : 
398   ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0] 
399 ≝ 
400   λcover.                           λA,    C,U.     ∀y.y ∈ C → cover A U y.
401
402 (*D
403
404 The `ndefinition` command takes a name, a type and body (of that type).
405 The type can be omitted, and in that case it is inferred by the system.
406 If the type is given, the system uses it to infer implicit arguments
407 of the body. In that case all types are left implicit in the body.
408
409 We now define the notation `a ◃ b`. Here the keywork `hvbox`
410 and `break` tell the system how to wrap text when it does not
411 fit the screen (they can be safely ignored for the scope of
412 this tutorial). We also add an interpretation for that notation, 
413 where the (abstracted) cover relation is implicit. The system
414 will not be able to infer it from the other arguments `C` and `U`
415 and will thus prompt the user for it. This is also why we named this 
416 interpretation `covers set temp`: we will later define another 
417 interpretation in which the cover relation is the one we are going to 
418 define.
419
420 D*)
421
422 notation "hvbox(a break ◃ b)" non associative with precedence 45
423 for @{ 'covers $a $b }.
424
425 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
426
427 (*D
428
429 The cover relation
430 ------------------
431
432 We can now define the cover relation using the `◃` notation for 
433 the premise of infinity. 
434
435 D*)
436
437 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
438 | creflexivity : ∀a. a ∈ U → cover ? U a
439 | cinfinity    : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
440 (** screenshot "cover". *) 
441 napply cover;
442 nqed.
443
444 (*D
445
446 Note that the system accepts the definition
447 but prompts the user for the relation the `cover_set` notion is
448 abstracted on.
449
450
451
452 The horizontal line separates the hypotheses from the conclusion.
453 The `napply cover` command tells the system that the relation
454 it is looking for is exactly our first context entry (i.e. the inductive
455 predicate we are defining, up to α-conversion); while the `nqed` command
456 ends a definition or proof.
457
458 We can now define the interpretation for the cover relation between an
459 element and a subset first, then between two subsets (but this time
460 we fix the relation `cover_set` is abstracted on).
461
462 D*)
463
464 interpretation "covers" 'covers a U = (cover ? U a).
465 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
466
467 (*D
468
469 We will proceed similarly for the fish relation, but before going
470 on it is better to give a short introduction to the proof mode of Matita.
471 We define again the `cover_set` term, but this time we build
472 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
473 and terms share the same syntax, and it is thus possible to use the
474 commands devoted to build proof term also to build regular definitions.
475 A tentative semantics for the proof mode commands (called tactics)
476 in terms of sequent calculus rules are given in the
477 <a href="#appendix">appendix</a>.
478
479 D*)
480
481 ndefinition xcover_set : 
482   ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]. 
483                          (** screenshot "xcover-set-1". *)
484 #cover; #A; #C; #U;      (** screenshot "xcover-set-2". *) 
485 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
486 napply cover;            (** screenshot "xcover-set-4". *)
487 ##[ napply A;
488 ##| napply U;
489 ##| napply y;
490 ##]
491 nqed.
492
493 (*D[xcover-set-1]
494 The system asks for a proof of the full statement, in an empty context.
495
496 The `#` command is the ∀-introduction rule, it gives a name to an 
497 assumption putting it in the context, and generates a λ-abstraction
498 in the proof term.
499
500 D[xcover-set-2]
501 We have now to provide a proposition, and we exhibit it. We left
502 a part of it implicit; since the system cannot infer it it will
503 ask for it later. 
504 Note that the type of `∀y:A.y ∈ C → ?` is a proposition
505 whenever `?` is a proposition.
506
507 D[xcover-set-3]
508 The proposition we want to provide is an application of the
509 cover relation we have abstracted in the context. The command
510 `napply`, if the given term has not the expected type (in that
511 case it is a product versus a proposition) it applies it to as many 
512 implicit arguments as necessary (in that case `? ? ?`).
513
514 D[xcover-set-4]
515 The system will now ask in turn the three implicit arguments 
516 passed to cover. The syntax `##[` allows to start a branching
517 to tackle every sub proof individually, otherwise every command
518 is applied to every subproof. The command `##|` switches to the next
519 subproof and `##]` ends the branching.  
520 D*)
521
522 (*D
523
524 The fish relation
525 -----------------
526
527 The definition of fish works exactly the same way as for cover, except 
528 that it is defined as a coinductive proposition.
529 D*)
530
531 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
532  λA,U,V.
533   ∃a.a ∈ V ∧ f A U a.
534
535 (* a \ltimes b *)
536 notation "hvbox(a break ⋉ b)" non associative with precedence 45
537 for @{ 'fish $a $b }. 
538
539 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
540
541 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝ 
542 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂  a i ⋉ F) → fish A F a.
543 napply fish;
544 nqed.
545
546 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
547 interpretation "fish" 'fish a U = (fish ? U a).
548
549 (*D
550
551 Introduction rule for fish
552 ---------------------------
553
554 Matita is able to generate elimination rules for inductive types,
555 but not introduction rules for the coinductive case. 
556
557 D*)
558
559 (** ncheck cover_rect_CProp0. *) 
560
561 (*D
562
563 We thus have to define the introduction rule for fish by co-recursion.
564 Here we again use the proof mode of Matita to exhibit the body of the
565 corecursive function.
566
567 D*)
568
569 nlet corec fish_rec (A:Ax) (U: Ω^A)
570  (P: Ω^A) (H1: P ⊆ U)
571   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
572                                        (** screenshot "def-fish-rec-1".   *)
573 #a; #p; napply cfish;                  (** screenshot "def-fish-rec-2".   *)
574 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) 
575     napply H1;                         (** screenshot "def-fish-rec-3".   *) 
576     nassumption;
577 ##| #i; ncases (H2 a p i);             (** screenshot "def-fish-rec-5".   *) 
578     #x; *; #xC; #xP;                   (** screenshot "def-fish-rec-5-1". *) 
579     @;                                 (** screenshot "def-fish-rec-6".   *)
580     ##[ napply x
581     ##| @;                             (** screenshot "def-fish-rec-7".   *)
582         ##[ napply xC; 
583         ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9".   *)
584             nassumption;
585         ##]
586     ##]
587 ##]
588 nqed.
589
590 (*D
591 D[def-fish-rec-1]
592 Note the first item of the context, it is the corecursive function we are 
593 defining. This item allows to perform the recursive call, but we will be
594 allowed to do such call only after having generated a constructor of
595 the fish coinductive type.
596
597 We introduce `a` and `p`, and then return the fish constructor `cfish`.
598 Since the constructor accepts two arguments, the system asks for them.
599
600 D[def-fish-rec-2]
601 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
602 With the `nchange` tactic we change `H1` into an equivalent form (this step
603 can be skipped, since the system would be able to unfold the definition
604 of inclusion by itself)
605
606 D[def-fish-rec-2-1]
607 It is now clear that `H1` can be applied. Again `napply` adds two 
608 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
609 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
610 `a`, and it asks a proof that `a ∈ P`.
611
612 D[def-fish-rec-3]
613 The `nassumption` tactic looks for the required proof in the context, and in
614 that cases finds it in the last context position. 
615
616 We move now to the second branch of the proof, corresponding to the second
617 argument of the `cfish` constructor.
618
619 We introduce `i` and then we destruct `H2 a p i`, that being a proof
620 of an overlap predicate, give as an element and a proof that it is 
621 both in `𝐂 a i` and `P`.
622
623 D[def-fish-rec-5]
624 We then introduce `x`, break the conjunction (the `*;` command is the
625 equivalent of `ncases` but operates on the first hypothesis that can
626 be introduced). We then introduce the two sides of the conjunction.
627
628 D[def-fish-rec-5-1]
629 The goal is now the existence of a point in `𝐂 a i` fished by `U`.
630 We thus need to use the introduction rule for the existential quantifier.
631 In CIC it is a defined notion, that is an inductive type with just
632 one constructor (one introduction rule) holding the witness and the proof
633 that the witness satisfies a proposition.
634
635 > ncheck Ex.
636
637 Instead of trying to remember the name of the constructor, that should
638 be used as the argument of `napply`, we can ask the system to find by
639 itself the constructor name and apply it with the `@` tactic. 
640 Note that some inductive predicates, like the disjunction, have multiple
641 introduction rules, and thus `@` can be followed by a number identifying
642 the constructor.
643
644 D[def-fish-rec-6]
645 After choosing `x` as the witness, we have to prove a conjunction,
646 and we again apply the introduction rule for the inductively defined
647 predicate `∧`.
648
649 D[def-fish-rec-7]
650 The left hand side of the conjunction is trivial to prove, since it 
651 is already in the context. The right hand side needs to perform
652 the co-recursive call.
653
654 D[def-fish-rec-9]
655 The co-recursive call needs some arguments, but all of them are
656 in the context. Instead of explicitly mention them, we use the
657 `nassumption` tactic, that simply tries to apply every context item.
658
659 D*)
660
661 (*D
662
663 Subset of covered/fished points
664 -------------------------------
665
666 We now have to define the subset of `S` of points covered by `U`.
667 We also define a prefix notation for it. Remember that the precedence
668 of the prefix form of a symbol has to be higher than the precedence 
669 of its infix form.
670
671 D*)
672
673 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
674
675 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
676
677 interpretation "coverage cover" 'coverage U = (coverage ? U).
678
679 (*D
680
681 Here we define the equation characterizing the cover relation. 
682 Even if it is not part of the paper, we proved that `◃(U)` is 
683 the minimum solution for
684 such equation, the interested reader should be able to reply the proof
685 with Matita.
686
687 D*)
688
689 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝  λA,U,X. 
690   ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).  
691
692 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
693 #A; #U; #a; @; #H;
694 ##[ nelim H; #b; 
695     ##[ #bU; @1; nassumption;
696     ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
697         ##[ #E; @; napply E;
698         ##| #_; napply CaiU; nassumption; ##] ##]
699 ##| ncases H; ##[ #E; @; nassumption]
700     *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
701 ##]
702 nqed. 
703
704 ntheorem coverage_min_cover_equation : 
705   ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
706 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
707 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
708 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
709 ##]
710 nqed.
711
712 (*D
713
714 We similarly define the subset of points "fished" by `F`, the 
715 equation characterizing `⋉(F)` and prove that fish is
716 the biggest solution for such equation.
717
718 D*) 
719
720 notation "⋉F" non associative with precedence 55
721 for @{ 'fished $F }.
722
723 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
724
725 interpretation "fished fish" 'fished F = (fished ? F).
726
727 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
728   ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X. 
729   
730 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
731 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
732 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
733     napply cF;  
734 ##| #aF; #H1; @ aF; napply H1;
735 ##]
736 nqed.
737
738 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
739 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
740 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; 
741 nqed. 
742
743 (*D
744
745 Part 2, the new set of axioms
746 -----------------------------
747
748 Since the name of defined objects (record included) has to be unique
749 within the same file, we prefix every field name
750 in the new definition of the axiom set with `n`.
751
752 D*)
753
754 nrecord nAx : Type[2] ≝ { 
755   nS:> setoid; 
756   nI: nS → Type[0];
757   nD: ∀a:nS. nI a → Type[0];
758   nd: ∀a:nS. ∀i:nI a. nD a i → nS
759 }.
760
761 (*D
762
763 We again define a notation for the projections, making the 
764 projected record an implicit argument. Note that, since we already have
765 a notation for `𝐈`, we just add another interpretation for it. The
766 system, looking at the argument of `𝐈`, will be able to choose
767 the correct interpretation. 
768
769 D*)
770
771 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
772 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
773
774 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
775 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
776
777 interpretation "D" 'D a i = (nD ? a i).
778 interpretation "d" 'd a i j = (nd ? a i j).
779 interpretation "new I" 'I a = (nI ? a).
780
781 (*D
782
783 The first result the paper presents to motivate the new formulation
784 of the axiom set is the possibility to define and old axiom set
785 starting from a new one and vice versa. The key definition for
786 such construction is the image of d(a,i).
787 The paper defines the image as
788
789 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
790
791 but this not so formal notation poses some problems. The image is
792 often used as the left hand side of the ⊆ predicate
793
794 > Im[d(a,i)] ⊆ V
795
796 Of course this writing is interpreted by the authors as follows 
797
798 > ∀j:D(a,i). d(a,i,j) ∈ V
799
800 If we need to use the image to define `𝐂 ` (a subset of `S`) we are obliged to
801 form a subset, i.e. to place a single variable `{ here | … }` of type `S`.
802
803 > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
804
805 This poses no theoretical problems, since `S` is a setoid and thus equipped
806 with an equality.
807
808 Unless we define two different images, one for stating that the image is ⊆ of
809 something and another one to define `𝐂`, we end up using always the latter.
810 Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
811
812 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
813
814 That, up to rewriting with the equation defining `x`, is what we mean. 
815 The technical problem arises later, when `V` will be a complex 
816 construction that has to be proved extensional 
817 (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
818
819 D*)
820
821 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
822
823 notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
824 notation < "𝐈𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
825
826 interpretation "image" 'Im a i = (image ? a i).
827
828 (*D
829
830 Thanks to our definition of image, we can define a function mapping a
831 new axiom set to an old one and vice versa. Note that in the second
832 definition, when we give the `𝐝` component, the projection of the 
833 Σ-type is inlined (constructed on the fly by `*;`) 
834 while in the paper it was named `fst`.
835
836 D*)
837
838 ndefinition Ax_of_nAx : nAx → Ax.
839 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
840 nqed.
841
842 ndefinition nAx_of_Ax : Ax → nAx.
843 #A; @ A (I ?);
844 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
845 ##| #a; #i; *; #x; #_; napply x;
846 ##]
847 nqed.
848
849 (*D
850
851 We then define the inductive type of ordinals, parametrized over an axiom
852 set. We also attach some notations to the constructors.
853
854 D*)
855
856 ninductive Ord (A : nAx) : Type[0] ≝ 
857  | oO : Ord A
858  | oS : Ord A → Ord A
859  | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
860
861 notation "0" non associative with precedence 90 for @{ 'oO }.
862 notation "x+1" non associative with precedence 50 for @{'oS $x }.
863 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
864
865 interpretation "ordinals Zero" 'oO = (oO ?).
866 interpretation "ordinals Succ" 'oS x = (oS ? x).
867 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
868
869 (*D
870
871 The definition of `U⎽x` is by recursion over the ordinal `x`. 
872 We thus define a recursive function using the `nlet rec` command. 
873 The `on x` directive tells
874 the system on which argument the function is (structurally) recursive.
875
876 In the `oS` case we use a local definition to name the recursive call
877 since it is used twice.
878
879 Note that Matita does not support notation in the left hand side
880 of a pattern match, and thus the names of the constructors have to 
881 be spelled out verbatim.
882
883 D*)
884
885 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ 
886   match x with
887   [ oO ⇒ U
888   | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n} 
889   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
890   
891 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
892 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
893
894 interpretation "famU" 'famU U x = (famU ? U x).
895
896 (*D
897
898 We attach as the input notation for U_x the similar `U⎽x` where underscore,
899 that is a character valid for identifier names, has been replaced by `⎽` that is
900 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
901 for `_` (i.e. pressing ALT-L after `_`). 
902
903 The notion ◃(U) has to be defined as the subset of elements `y`  
904 belonging to `U⎽x` for some `x`. Moreover, we have to define the notion
905 of cover between sets again, since the one defined at the beginning
906 of the tutorial works only for the old axiom set.
907
908 D*)
909   
910 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
911
912 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
913   ∀y.y ∈ C → y ∈ c A U.
914
915 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
916 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
917 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
918
919 (*D
920
921 Before proving that this cover relation validates the reflexivity and infinity
922 rules, we prove this little technical lemma that is used in the proof for the 
923 infinity rule.
924
925 D*)
926
927 nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
928 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
929 nqed.
930
931 (*D
932
933 The proof of infinity uses the following form of the Axiom of Choice,
934 that cannot be proved inside Matita, since the existential quantifier
935 lives in the sort of predicative propositions while the sigma in the conclusion
936 lives in the sort of data types, and thus the former cannot be eliminated
937 to provide the witness for the second.
938
939 D*)
940
941 naxiom AC : ∀A,a,i,U.
942   (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
943
944 (*D
945
946 In the proof of infinity, we have to rewrite under the ∈ predicate.
947 It is clearly possible to show that `U⎽x` is an extensional set:
948
949 > a = b → a ∈ U⎽x → b ∈ U⎽x
950
951 Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be
952 declared as morphisms. This poses no problem, but goes out of the scope of the 
953 tutorial, since dependent morphisms are hard to manipulate, and we thus assume it.
954
955 D*)
956
957 naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
958
959 (*D
960
961 The reflexivity proof is trivial, it is enough to provide the ordinal `0`
962 as a witness, then `◃(U)` reduces to `U` by definition, 
963 hence the conclusion. Note that `0` is between `(` and `)` to
964 make it clear that it is a term (an ordinal) and not the number
965 of the constructor we want to apply (that is the first and only one
966 of the existential inductive type).
967
968 D*)
969 ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
970 #A; #U; #a; #H; @ (0); napply H;
971 nqed.
972
973 (*D
974
975 We now proceed with the proof of the infinity rule.
976
977 D*)
978
979
980 alias symbol "covers" = "new covers set".
981 ntheorem new_coverage_infinity:
982   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
983 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  
984 *; #i; #H; nnormalize in H;                   (** screenshot "n-cov-inf-2". *)
985 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[    (** screenshot "n-cov-inf-3". *)
986   #z; napply H; @ z; napply #; ##] #H';       (** screenshot "n-cov-inf-4". *)
987 ncases (AC … H'); #f; #Hf;                    (** screenshot "n-cov-inf-5". *)
988 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
989   ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
990 @ (Λ f+1);                                    (** screenshot "n-cov-inf-7". *)
991 @2;                                           (** screenshot "n-cov-inf-8". *) 
992 @i; #x; *; #d; #Hd;                           (** screenshot "n-cov-inf-9". *)  
993 napply (U_x_is_ext … Hd); napply Hf';
994 nqed.
995
996 (*D
997 D[n-cov-inf-1]
998 We eliminate the existential, obtaining an `i` and a proof that the 
999 image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal
1000 form of `H`, thus expands the definition of cover between sets.
1001
1002 D[n-cov-inf-2]
1003 When the paper proof considers `H`, it implicitly substitutes assumed 
1004 equation defining `y` in its conclusion. 
1005 In Matita this step is not completely trivial.
1006 We thus assert (`ncut`) the nicer form of `H` and prove it.
1007
1008 D[n-cov-inf-3]
1009 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`). 
1010 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that 
1011 becomes trivial if `j` is chosen to be `z`. In the command `napply #`,
1012 the `#` is a standard notation for the reflexivity property of the equality. 
1013
1014 D[n-cov-inf-4]
1015 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and 
1016 its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before
1017 assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated
1018 is `AC ???? H'` where the system is able to infer every `?`. Matita provides
1019 a facility to specify a number of `?` in a compact way, i.e. `…`. The system
1020 expand `…` first to zero, then one, then two, three and finally four question 
1021 marks, "guessing" how may of them are needed. 
1022
1023 D[n-cov-inf-5]
1024 The paper proof does now a forward reasoning step, deriving (by the ord_subset 
1025 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
1026
1027 D[n-cov-inf-6]
1028 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
1029
1030 D[n-cov-inf-7]
1031 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
1032 that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`. 
1033 Applying the second constructor `@2;` of the disjunction, 
1034 we are left to prove that `a` belongs to the right hand side of the union.
1035
1036 D[n-cov-inf-8]
1037 We thus provide `i` as the witness of the existential, introduce the 
1038 element being in the image and we are
1039 left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging 
1040 to the image means that there exists an object in the domain …, we eliminate the
1041 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.  
1042
1043 D[n-cov-inf-9]
1044 We just need to use the equational definition of `x` to obtain a conclusion
1045 that can be proved with `Hf'`. We assumed that `U⎽x` is extensional for
1046 every `x`, thus we are allowed to use `Hd` and close the proof.
1047
1048 D*)
1049
1050 (*D
1051
1052 The next proof is that ◃(U) is minimal. The hardest part of the proof
1053 is to prepare the goal for the induction. The desiderata is to prove
1054 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
1055 unfolding all definitions:
1056
1057 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
1058
1059 D*)
1060
1061 nlemma new_coverage_min :  
1062   ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1063 #A; #U; #V; #HUV; #Im;#b;                       (** screenshot "n-cov-min-2". *)
1064 *; #o;                                          (** screenshot "n-cov-min-3". *)
1065 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
1066 nelim o;                                        (** screenshot "n-cov-min-5". *) 
1067 ##[ #b; #bU0; napply HUV; napply bU0;
1068 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1069     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1070 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1071 nqed.
1072
1073 (*D
1074 D[n-cov-min-2]
1075 After all the introductions, event the element hidden in the ⊆ definition,
1076 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1077
1078 D[n-cov-min-3]
1079 What is left is almost right, but the element `b` is already in the
1080 context. We thus generalize every occurrence of `b` in 
1081 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1082
1083 D[n-cov-min-4]
1084 We then proceed by induction on `o` obtaining the following goals
1085
1086 D[n-cov-min-5]
1087 All of them can be proved using simple set theoretic arguments,
1088 the induction hypothesis and the assumption `Im`.
1089
1090 D*)
1091
1092
1093 (*D
1094
1095 The notion `F⎽x` is again defined by recursion over the ordinal `x`.
1096
1097 D*)
1098
1099 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
1100   match x with
1101   [ oO ⇒ F
1102   | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o } 
1103   | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1104   ].
1105
1106 interpretation "famF" 'famU U x = (famF ? U x).
1107
1108 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1109
1110 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1111 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1112
1113 (*D
1114
1115 The proof of compatibility uses this little result, that we 
1116 proved outside the main proof. 
1117
1118 D*)
1119 nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1120 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1121 nqed.
1122
1123 (*D
1124
1125 We assume the dual of the axiom of choice, as in the paper proof.
1126
1127 D*)
1128 naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F. 
1129  (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
1130
1131 (*D
1132
1133 Proving the anti-reflexivity property is simple, since the
1134 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1135 `a ∈ F⎽x`. If `x` is choose to be `0`, we obtain the thesis.
1136
1137 D*)
1138 ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1139 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1140 nqed.
1141
1142 (*D
1143
1144 We now prove the compatibility property for the new fish relation.
1145
1146 D*)
1147 ntheorem new_fish_compatible: 
1148  ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1149 #A; #F; #a; #aF; #i; nnormalize;               (** screenshot "n-f-compat-1". *)
1150 napply AC_dual; #f;                            (** screenshot "n-f-compat-2". *)
1151 nlapply (aF (Λf+1)); #aLf;                     (** screenshot "n-f-compat-3". *)
1152 nchange in aLf with 
1153   (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1154 ncases aLf; #_; #H; nlapply (H i);                 (** screenshot "n-f-compat-5". *)
1155 *; #j; #Hj; @j;                                    (** screenshot "n-f-compat-6". *)
1156 napply (co_ord_subset … Hj);
1157 nqed.
1158
1159 (*D
1160 D[n-f-compat-1]
1161 After reducing to normal form the goal, we observe it is exactly the conclusion of
1162 the dual axiom of choice we just assumed. We thus apply it ad introduce the 
1163 fcuntion `f`.
1164
1165 D[n-f-compat-2]
1166 The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`.
1167
1168 D[n-f-compat-3]
1169 Since F_(Λf+1) is defined by recursion and we actually have a concrete input
1170 `Λf+1` for that recursive function, it can be computed. 
1171 Anyway, using the `nnormalize`
1172 tactic would reduce too much (both the `+1` and the `Λf` steps would be performed);
1173 we thus explicitly give a convertible type for that hypothesis, corresponding 
1174 the computation of the `+1` step, plus the unfolding the definition of
1175 the intersection.
1176
1177 D[n-f-compat-4]
1178 We are interested in the right hand side of `aLf`, an in particular to
1179 its intance where the generic index in `𝐈 a` is `i`.
1180
1181 D[n-f-compat-5]
1182 We then eliminate the existential, obtaining `j` and its property `Hj`. We provide
1183 the same witness 
1184
1185 D[n-f-compat-6]
1186 What is left to prove is exactly the `co_ord_subset` lemma we factored out
1187 of the main proof.
1188
1189 D*)
1190
1191 (*D
1192
1193 The proof that `⋉(F)` is maximal is exactly the dual one of the
1194 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1195 before doing the induction over `o`.
1196
1197 Note that `G` is assumed to be of type `𝛀^A`, that means an extensional
1198 subset of `S`, while `Ω^A` means just a subset (note that the former is bold). 
1199
1200 D*)
1201 ntheorem max_new_fished: 
1202   ∀A:nAx.∀G:𝛀^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1203 #A; #G; #F; #GF; #H; #b; #HbG; #o; 
1204 ngeneralize in match HbG; ngeneralize in match b;
1205 nchange with (G ⊆ F⎽o);
1206 nelim o;
1207 ##[ napply GF;
1208 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1209     #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1210     @d; napply IH;                                (** screenshot "n-f-max-1". *)
1211     alias symbol "prop2" = "prop21".
1212     napply (. Ed^-1‡#); napply cG;    
1213 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
1214     #b; #Hb; #d; napply (Hf d); napply Hb;
1215 ##]
1216 nqed.
1217
1218 (*D
1219 D[n-f-max-1]
1220 Here the situation looks really similar to the one of the dual proof where 
1221 we had to apply the assumption `U_x_is_ext`, but here the set is just `G`
1222 not `F_x`. Since we assumed `G` to be extensional we can 
1223 exploit the facilities
1224 Matita provides to perform rewriting in the general setting of setoids.
1225
1226 The `.` notation simply triggers the mechanism, while the given argument has to
1227 mimic the context under which the rewriting has to happen. In that case
1228 we want to rewrite the left hand side of the binary morphism `∈`. 
1229 The infix notation
1230 to represent the context of a binary morphism is `‡`. The right hand side 
1231 has to be left untouched, and the identity rewriting step is represented with 
1232 `#` (actually a reflexivity proof for the subterm identified by the context). 
1233
1234 We want to rewrite the left hand side using `Ed` right-to-left (the default
1235 is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`. 
1236
1237 The complete command is `napply (. Ed^-1‡#)` that has to be read like:
1238
1239 > perform some rewritings under a binary morphism, 
1240 > on the right do nothing, 
1241 > on the left rewrite with Ed right-to-left.
1242
1243 After the rewriting step the goal is exactly the `cG` assumption.
1244
1245 D*)
1246
1247
1248 (*D
1249 <div id="appendix" class="anchor"></div>
1250 Appendix: tactics explanation
1251 -----------------------------
1252
1253 In this appendix we try to give a description of tactics
1254 in terms of sequent calculus rules annotated with proofs.
1255 The `:` separator has to be read as _is a proof of_, in the spirit
1256 of the Curry-Howard isomorphism.
1257
1258                   Γ ⊢  f  :  A1 → … → An → B    Γ ⊢ ?1 : A1 … ?n  :  An 
1259     napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1260                            Γ ⊢ (f ?1 … ?n )  :  B
1261  
1262                    Γ ⊢  ?  :  F → B       Γ ⊢ f  :  F 
1263     nlapply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1264                              Γ ⊢ (? f)  :  B
1265
1266
1267                  Γ; x : T  ⊢ ?  :  P(x) 
1268     #x;      ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1269                 Γ ⊢ λx:T.?  :  ∀x:T.P(x)
1270
1271                        
1272                        Γ ⊢ ?_i  :  args_i → P(k_i args_i)          
1273     ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1274                 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ]  :  P(x)                    
1275
1276
1277                       Γ ⊢ ?i  :  ∀t. P(t) → P(k_i … t …)          
1278     nelim x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1279                    Γ ⊢ (T_rect_CProp0 ?_1 … ?_n)  :  P(x)                    
1280
1281 Where `T_rect_CProp0` is the induction principle for the 
1282 inductive type `T`.
1283
1284
1285                           Γ ⊢ ?  :  Q     Q ≡ P          
1286     nchange with Q;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1287                           Γ ⊢ ?  :  P                    
1288
1289 Where the equivalence relation between types `≡` keeps into account
1290 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1291 definition unfolding), ι-reduction (pattern matching simplification),
1292 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1293 computation).
1294
1295
1296                                Γ; H : Q; Δ ⊢ ?  :  G     Q ≡ P          
1297     nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1298                                Γ; H : P; Δ ⊢ ?  :  G                    
1299
1300
1301                                Γ; H : Q; Δ ⊢ ?  :  G     P →* Q           
1302     nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1303                                Γ; H : P; Δ ⊢ ?  :  G                    
1304
1305 Where `Q` is the normal form of `P` considering βδζιμν-reduction steps.
1306
1307
1308                        Γ ⊢ ?  :  Q     P →* Q          
1309     nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1310                        Γ ⊢ ?  :  P                    
1311
1312
1313                     Γ ⊢ ?_2  :  T → G    Γ ⊢ ?_1  :  T
1314     ncut T;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1315                                Γ ⊢ (?_2 ?_1)  :  G                    
1316
1317
1318                                 Γ ⊢ ?  :  ∀x.P(x)
1319     ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1320                                 Γ ⊢ (? t)  :  P(t)
1321                                 
1322 D*)
1323
1324
1325 (*D
1326
1327 <date>
1328 Last updated: $Date$
1329 </date>
1330
1331 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
1332 [2]: http://matita.cs.unibo.it
1333 [3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
1334 [4]: http://www.inria.fr/rrrt/rr-0530.html
1335
1336 D*)