3 Matita Tutorial: inductively generated formal topologies
4 ========================================================
6 This is a not so short introduction to Matita, based on
7 the formalization of the paper
9 > Between formal topology and game theory: an
10 > explicit solution for the conditions for an
11 > inductive generation of formal topologies
13 by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
15 The tutorial spends a considerable amount of effort in defining
16 notations that resemble the ones used in the original paper. We believe
17 this a important part of every formalization, not only for the estetic
18 point of view, but also from the practical point of view. Being
19 consistent allows to follow the paper in a pedantic way, and hopefully
20 to make the formalization (at least the definitions and proved
21 statements) readable to the author of the paper.
28 buttons, PG-interaction-model, sequent window, script window, ncheck
30 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
31 Symbols (see menu: View ▹ TeX/UTF-8 Table):
38 Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
40 The standard library and the `include` command
41 ----------------------------------------------
43 Some basic notions, like subset, membership, intersection and union
44 are part of the standard library of Matita.
46 These notions come with
47 some notation attached to them:
51 - A ≬ B `A \between B`
53 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
55 The `include` command tells Matita to load a part of the library,
56 in particular the part that we will use can be loaded as follows:
60 include "sets/sets.ma".
64 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
65 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
68 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
69 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
72 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
73 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
79 Some basic results that we will use are also part of the sets library:
81 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
82 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
87 records, projections, types of projections..
91 nrecord Ax : Type[1] ≝ {
99 Note that the field `S` was declared with `:>` instead of a simple `:`.
100 This declares the `S` projection to be a coercion. A coercion is
101 a function case the system automatically inserts when it is needed.
102 In that case, the projection `S` has type `Ax → setoid`, and whenever
103 the expected type of a term is `setoid` while its type is `Ax`, the
104 system inserts the coercion around it, to make the whole term well types.
106 When formalizing an algebraic structure, declaring the carrier as a
107 coercion is a common practice, since it allows to write statements like
109 ∀G:Group.∀x:G.x * x^-1 = 1
111 The quantification over `x` of type `G` is illtyped, since `G` is a term
112 (of type `Group`) and thus not a type. Since the carrier projection
113 `carr` of `G` is a coercion, that maps a `Group` into the type of
114 its elements, the system automatically inserts `carr` around `G`,
115 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
116 when it displays a term.
118 In this particular case, the coercion `S` allows to write
122 Since `A` is not a type, but it can be turned into a `setoid` by `S`
123 and a `setoid` can be turned into a type by its `carr` projection, the
124 composed coercion `carr ∘ S` is silently inserted.
129 Something that is not still satisfactory, in that the dependent type
130 of `I` and `C` are abstracted over the Axiom set. To obtain the
131 precise type of a term, you can use the `ncheck` command as follows.
140 One would like to write `I a` and not `I A a` under a context where
141 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
142 mecanism simply `A`). In Matita, a question mark represents an implicit
143 argument, i.e. a missing piece of information the system is asked to
144 infer. Matita performs some sort of type inference, thus writing
145 `I ? a` is enough: since the second argument of `I` is typed by the
146 first one, the first one can be inferred just computing the type of `a`.
150 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
154 This is still not completely satisfactory, since you have always type
155 `?`; to fix this minor issue we have to introduce the notational
156 support built in Matita.
161 Matita is quipped with a quite complex notational support,
162 allowing the user to define and use mathematical notations
163 ([From Notation to Semantics: There and Back Again][1]).
165 Since notations are usually ambiguous (e.g. the frequent overloading of
166 symbols) Matita distinguishes between the term level, the
167 content level, and the presentation level, allowing multiple
168 mappings between the contenet and the term level.
170 The mapping between the presentation level (i.e. what is typed on the
171 keyboard and what is displayed in the sequent window) and the content
172 level is defined with the `notation` command. When followed by
173 `>`, it defines an input (only) notation.
177 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
178 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
182 The forst notation defines the writing `𝐈 a` where `a` is a generic
183 term of precedence 90, the maximum one. This high precedence forces
184 parentheses around any term of a lower precedence. For example `𝐈 x`
185 would be accepted, since identifiers have precedence 90, but
186 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
187 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
189 To obtain the `𝐈` is enough to type `I` and then cycle between its
190 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
191 regular letters or the round parentheses, thus their variants (like the
192 bold ones) have to be used.
194 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
195 new content element to which a term `$a` is passed.
197 Content elements have to be interpreted, and possibly multiple,
198 incompatible, interpretations can be defined.
202 interpretation "I" 'I a = (I ? a).
203 interpretation "C" 'C a i = (C ? a i).
207 The `interpretation` command allows to define the mapping between
208 the content level and the terms level. Here we associate the `I` and
209 `C` projections of the Axiom set record, where the Axiom set is an implicit
210 argument `?` to be inferred by the system.
212 Interpretation are bi-directional, thus when displaying a term like
213 `C _ a i`, the system looks for a presentation for the content element
218 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
219 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
223 For output purposes we can define more complex notations, for example
224 we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
225 the size of the arguments and lowering their baseline (i.e. putting them
226 as subscript), separating them with a comma followed by a little space.
228 The first (technical) definition
229 --------------------------------
231 Before defining the cover relation as an inductive predicate, one
232 has to notice that the infinity rule uses, in its hypotheses, the
233 cover relation between two subsets, while the inductive predicate
234 we are going to define relates an element and a subset.
236 An option would be to unfold the definition of cover between subsets,
237 but we prefer to define the abstract notion of cover between subsets
238 (so that we can attach a (ambiguous) notation to it).
240 Anyway, to ease the understaing of the definition of the cover relation
241 between subsets, we first define the inductive predicate unfolding the
242 definition, and we later refine it with.
246 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
247 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
248 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
252 We defined the xcover (x will be removed in the final version of the
253 definition) as an inductive predicate. The arity of the inductive
254 predicate has to be carefully analyzed:
256 > (A : Ax) (U : Ω^A) : A → CProp[0]
258 The syntax separates with `:` abstractions that are fixed for every
259 constructor (introduction rule) and abstractions that can change. In that
260 case the parameter `U` is abstracted once and forall in front of every
261 constructor, and every occurrence of the inductive predicate is applied to
262 `U` in a consistent way. Arguments abstracted on the right of `:` are not
263 constant, for example the xcinfinity constructor introduces `a ◃ U`,
264 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
265 had side of the predicate changes, thus it has to be abstrated (in the arity
266 of the inductive predicate) on the right of `:`.
270 (* ncheck xcreflexivity. *)
274 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
275 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
277 This notion has to be abstracted over the cover relation (whose
278 type is the arity of the inductive `xcover` predicate just defined).
280 Then it has to be abstracted over the arguments of that cover relation,
281 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
282 sitting on the left hand side of `◃`.
286 ndefinition cover_set :
287 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
289 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
293 The `ndefinition` command takes a name, a type and body (of that type).
294 The type can be omitted, and in that case it is inferred by the system.
295 If the type is given, the system uses it to infer implicit arguments
296 of the body. In that case all types are left implicit in the body.
298 We now define the notation `a ◃ b`. Here the keywork `hvbox`
299 and `break` tell the system how to wrap text when it does not
300 fit the screen (they can be safely ignore for the scope of
301 this tutorial). we also add an interpretation for that notation,
302 where the (abstracted) cover relation is implicit. The system
303 will not be able to infer it from the other arguments `C` and `U`
304 and will thus prompt the user for it. This is also why we named this
305 interpretation `covers set temp`: we will later define another
306 interpretation in which the cover relation is the one we are going to
311 notation "hvbox(a break ◃ b)" non associative with precedence 45
312 for @{ 'covers $a $b }.
314 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
318 We can now define the cover relation using the `◃` notation for
319 the premise of infinity.
323 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
324 | creflexivity : ∀a. a ∈ U → cover ? U a
325 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
326 (** screenshot "cover". *)
332 Note that the system accepts the definition
333 but prompts the user for the relation the `cover_set` notion is
336 ![The system asks for a cover relation][cover]
338 The orizontal line separates the hypotheses from the conclusion.
339 The `napply cover` command tells the system that the relation
340 it is looking for is exactly our first context entry (i.e. the inductive
341 predicate we are defining, up to α-conversion); while the `nqed` command
342 ends a definition or proof.
344 We can now define the interpretation for the cover relation between an
345 element and a subset fist, then between two subsets (but this time
346 we fixed the relation `cover_set` is abstracted on).
350 interpretation "covers" 'covers a U = (cover ? U a).
351 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
355 We will proceed similarly for the fish relation, but before going
356 on it is better to give a short introduction to the proof mode of Matita.
357 We define again the `cover_set` term, but this time we will build
358 its body interactively. In λ-calculus Matita is based on, CIC, proofs
359 and terms share the same syntax, and it thus possible to use the
360 commands devoted to build proof term to build regular definitions.
365 ndefinition xcover_set :
366 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
367 (** screenshot "xcover-set-1". *)
369 The system asks for a proof of the full statement, in an empty context.
370 ![xcover_set proof step ][xcover-set-1]
371 The `#` command in the ∀-introduction rule, it gives a name to an
372 assumption putting it in the context, and generates a λ-abstraction
375 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
377 ![xcover_set proof step ][xcover-set-2]
378 We have now to provide a proposition, and we exhibit it. We left
379 a part of it implicit; since the system cannot infer it it will
380 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
383 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
385 ![xcover_set proof step ][xcover-set-3]
386 The proposition we want to provide is an application of the
387 cover relation we have abstracted in the context. The command
388 `napply`, if the given term has not the expected type (in that
389 case it is a product versus a proposition) it applies it to as many
390 implicit arguments as necessary (in that case `? ? ?`).
392 napply cover; (** screenshot "xcover-set-4". *)
394 ![xcover_set proof step ][xcover-set-4]
395 The system will now ask in turn the three implicit arguments
396 passed to cover. The syntax `##[` allows to start a branching
397 to tackle every sub proof individually, otherwise every command
398 is applied to every subrpoof. The command `##|` switches to the next
399 subproof and `##]` ends the branching.
408 The definition of fish works exactly the same way as for cover, except
409 that it is defined as a coinductive proposition.
412 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
417 notation "hvbox(a break ⋉ b)" non associative with precedence 45
418 for @{ 'fish $a $b }.
420 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
422 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
423 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
427 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
428 interpretation "fish" 'fish a U = (fish ? U a).
432 Matita is able to generate elimination rules for inductive types,
433 but not introduction rules for the coinductive case.
437 (* ncheck cover_rect_CProp0. *)
441 We thus have to define the introduction rule for fish by corecursion.
442 Here we again use the proof mode of Matita to exhibit the body of the
443 corecursive function.
447 nlet corec fish_rec (A:Ax) (U: Ω^A)
449 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
450 (** screenshot "def-fish-rec-1". *)
451 #a; #p; napply cfish;
452 ##[ (** screenshot "def-fish-rec-2". *) napply H1;
453 (** screenshot "def-fish-rec-3". *) napply p;
454 ##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i);
455 (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP;
456 (** screenshot "def-fish-rec-5". *) @;
457 ##[ (** screenshot "def-fish-rec-6". *) napply x
458 ##| (** screenshot "def-fish-rec-7". *)
460 ##| (** screenshot "def-fish-rec-8". *)
461 napply (fish_rec ? U P);
469 ![fish proof step][def-fish-rec-1]
470 ![fish proof step][def-fish-rec-2]
471 ![fish proof step][def-fish-rec-3]
472 ![fish proof step][def-fish-rec-4]
473 ![fish proof step][def-fish-rec-5]
474 ![fish proof step][def-fish-rec-6]
475 ![fish proof step][def-fish-rec-7]
476 ![fish proof step][def-fish-rec-8]
479 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
481 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
483 interpretation "coverage cover" 'coverage U = (coverage ? U).
485 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
486 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
488 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
490 ##[ nelim H; #b; (* manca clear *)
491 ##[ #bU; @1; nassumption;
492 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
494 ##| #_; napply CaiU; nassumption; ##] ##]
495 ##| ncases H; ##[ #E; @; nassumption]
496 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
500 ntheorem coverage_min_cover_equation :
501 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
502 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
503 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
504 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
508 notation "⋉F" non associative with precedence 55
511 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
513 interpretation "fished fish" 'fished F = (fished ? F).
515 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
516 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
518 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
519 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
520 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
522 ##| #aF; #H1; @ aF; napply H1;
526 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
527 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
528 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
531 nrecord nAx : Type[2] ≝ {
532 nS:> setoid; (*Type[0];*)
534 nD: ∀a:nS. nI a → Type[0];
535 nd: ∀a:nS. ∀i:nI a. nD a i → nS
539 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
544 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
545 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
547 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
548 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
550 interpretation "D" 'D a i = (nD ? a i).
551 interpretation "d" 'd a i j = (nd ? a i j).
552 interpretation "new I" 'I a = (nI ? a).
554 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
556 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
557 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
559 interpretation "image" 'Im a i = (image ? a i).
561 ndefinition Ax_of_nAx : nAx → Ax.
562 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
565 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
566 sig_intro : ∀x:A.P x → sigma A P.
568 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
570 ndefinition nAx_of_Ax : Ax → nAx.
572 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
573 ##| #a; #i; *; #x; #_; napply x;
577 ninductive Ord (A : nAx) : Type[0] ≝
580 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
582 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
583 notation "x+1" non associative with precedence 50 for @{'oS $x }.
585 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
586 interpretation "ordinals Succ" 'oS x = (oS ? x).
588 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
591 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
592 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
594 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
595 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
597 interpretation "famU" 'famU U x = (famU ? U x).
599 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
601 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
602 ∀y.y ∈ C → y ∈ c A U.
604 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
605 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
606 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
608 ntheorem new_coverage_reflexive:
609 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
610 #A; #U; #a; #H; @ (oO A); napply H;
614 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
615 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
618 naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
620 naxiom setoidification :
621 ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
630 alias symbol "covers" = "new covers".
631 alias symbol "covers" = "new covers set".
632 alias symbol "covers" = "new covers".
633 alias symbol "covers" = "new covers set".
634 alias symbol "covers" = "new covers".
635 alias symbol "covers" = "new covers set".
636 alias symbol "covers" = "new covers".
637 alias symbol "covers" = "new covers set".
638 alias symbol "covers" = "new covers".
639 ntheorem new_coverage_infinity:
640 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
641 #A; #U; #a;(** screenshot "figure1". *)
642 *; #i; #H; nnormalize in H;
643 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
644 #y; napply H; @ y; napply #; ##] #H';
645 ncases (AC … H'); #f; #Hf;
646 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
647 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
648 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
649 napply (setoidification … Hd); napply Hf';
652 nlemma new_coverage_min :
653 ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
654 #A; #U; #V; #HUV; #Im; #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
656 ##[ #b; #bU0; napply HUV; napply bU0;
657 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
658 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
659 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
662 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
665 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
666 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
669 interpretation "famF" 'famU U x = (famF ? U x).
671 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
673 interpretation "fished new fish" 'fished U = (ord_fished ? U).
674 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
676 ntheorem new_fish_antirefl:
677 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
678 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
681 nlemma co_ord_subset:
682 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
683 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
687 ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
690 ntheorem new_fish_compatible:
691 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
692 #A; #F; #a; #aF; #i; nnormalize;
694 nlapply (aF (Λf+1)); #aLf;
695 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
696 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
697 ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
701 ntheorem max_new_fished:
702 ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
703 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
704 nchange with (G ⊆ F⎽o);
707 ##| #p; #IH; napply (subseteq_intersection_r … IH);
708 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
709 @d; napply IH; napply (setoidification … Ed^-1); napply cG;
710 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
711 #b; #Hb; #d; napply (Hf d); napply Hb;
717 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf