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.
26 buttons, PG-interaction-model, sequent window, script window
28 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
29 Symbols (see menu: View ▹ TeX/UTF-8 Table):
36 Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
38 The standard library and the `include` command
39 ----------------------------------------------
41 Some basic notions, like subset, membership, intersection and union
42 are part of the standard library of Matita.
44 These notions come with
45 some notation attached to them:
49 - A ≬ B `A \between B`
51 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
53 The `include` command tells Matita to load a part of the library,
54 in particular the part that we will use can be loaded as follows:
58 include "sets/sets.ma".
62 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
63 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
66 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
67 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
70 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
71 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
77 Some basic results that we will use are also part of the sets library:
79 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
80 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
85 records, projections, types of projections..
89 nrecord Ax : Type[1] ≝ {
97 Note that the field `S` was declared with `:>` instead of a simple `:`.
98 This declares the `S` projection to be a coercion. A coercion is
99 a function case the system automatically inserts when it is needed.
100 In that case, the projection `S` has type `Ax → setoid`, and whenever
101 the expected type of a term is `setoid` while its type is `Ax`, the
102 system inserts the coercion around it, to make the whole term well types.
104 When formalizing an algebraic structure, declaring the carrier as a
105 coercion is a common practice, since it allows to write statements like
107 ∀G:Group.∀x:G.x * x^-1 = 1
109 The quantification over `x` of type `G` is illtyped, since `G` is a term
110 (of type `Group`) and thus not a type. Since the carrier projection
111 `carr` of `G` is a coercion, that maps a `Group` into the type of
112 its elements, the system automatically inserts `carr` around `G`,
113 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
114 when it displays a term.
116 In this particular case, the coercion `S` allows to write
120 Since `A` is not a type, but it can be turned into a `setoid` by `S`
121 and a `setoid` can be turned into a type by its `carr` projection, the
122 composed coercion `carr ∘ S` is silently inserted.
127 Something that is not still satisfactory, in that the dependent type
128 of `I` and `C` are abstracted over the Axiom set. To obtain the
129 precise type of a term, you can use the `ncheck` command as follows.
138 One would like to write `I a` and not `I A a` under a context where
139 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
140 mecanism simply `A`). In Matita, a question mark represents an implicit
141 argument, i.e. a missing piece of information the system is asked to
142 infer. Matita performs some sort of type inference, thus writing
143 `I ? a` is enough: since the second argument of `I` is typed by the
144 first one, the first one can be inferred just computing the type of `a`.
148 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
152 This is still not completely satisfactory, since you have always type
153 `?`; to fix this minor issue we have to introduce the notational
154 support built in Matita.
159 Matita is quipped with a quite complex notational support,
160 allowing the user to define and use mathematical notations
161 ([From Notation to Semantics: There and Back Again][1]).
163 Since notations are usually ambiguous (e.g. the frequent overloading of
164 symbols) Matita distinguishes between the term level, the
165 content level, and the presentation level, allowing multiple
166 mappings between the contenet and the term level.
168 The mapping between the presentation level (i.e. what is typed on the
169 keyboard and what is displayed in the sequent window) and the content
170 level is defined with the `notation` command. When followed by
171 `>`, it defines an input (only) notation.
175 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
176 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
180 The forst notation defines the writing `𝐈 a` where `a` is a generic
181 term of precedence 90, the maximum one. This high precedence forces
182 parentheses around any term of a lower precedence. For example `𝐈 x`
183 would be accepted, since identifiers have precedence 90, but
184 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
185 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
187 To obtain the `𝐈` is enough to type `I` and then cycle between its
188 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
189 regular letters or the round parentheses, thus their variants (like the
190 bold ones) have to be used.
192 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
193 new content element to which a term `$a` is passed.
195 Content elements have to be interpreted, and possibly multiple,
196 incompatible, interpretations can be defined.
200 interpretation "I" 'I a = (I ? a).
201 interpretation "C" 'C a i = (C ? a i).
205 The `interpretation` command allows to define the mapping between
206 the content level and the terms level. Here we associate the `I` and
207 `C` projections of the Axiom set record, where the Axiom set is an implicit
208 argument `?` to be inferred by the system.
210 Interpretation are bi-directional, thus when displaying a term like
211 `C _ a i`, the system looks for a presentation for the content element
216 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
217 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
221 For output purposes we can define more complex notations, for example
222 we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
223 the size of the arguments and lowering their baseline (i.e. putting them
224 as subscript), separating them with a comma followed by a little space.
226 The first (technical) definition
227 --------------------------------
229 Before defining the cover relation as an inductive predicate, one
230 has to notice that the infinity rule uses, in its hypotheses, the
231 cover relation between two subsets, while the inductive predicate
232 we are going to define relates an element and a subset.
234 An option would be to unfold the definition of cover between subsets,
235 but we prefer to define the abstract notion of cover between subsets
236 (so that we can attach a (ambiguous) notation to it).
238 Anyway, to ease the understaing of the definition of the cover relation
239 between subsets, we first define the inductive predicate unfolding the
240 definition, and we later refine it with.
244 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
245 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
246 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
250 We defined the xcover (x will be removed in the final version of the
251 definition) as an inductive predicate. The arity of the inductive
252 predicate has to be carefully analyzed:
254 > (A : Ax) (U : Ω^A) : A → CProp[0]
256 The syntax separates with `:` abstractions that are fixed for every
257 constructor (introduction rule) and abstractions that can change. In that
258 case the parameter `U` is abstracted once and forall in front of every
259 constructor, and every occurrence of the inductive predicate is applied to
260 `U` in a consistent way. Arguments abstracted on the right of `:` are not
261 constant, for example the xcinfinity constructor introduces `a ◃ U`,
262 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
263 had side of the predicate changes, thus it has to be abstrated (in the arity
264 of the inductive predicate) on the right of `:`.
268 (* ncheck xcreflexivity. *)
272 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
273 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
275 This notion has to be abstracted over the cover relation (whose
276 type is the arity of the inductive `xcover` predicate just defined).
278 Then it has to be abstracted over the arguments of that cover relation,
279 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
280 sitting on the left hand side of `◃`.
284 ndefinition cover_set :
285 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
287 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
291 The `ndefinition` command takes a name, a type and body (of that type).
292 The type can be omitted, and in that case it is inferred by the system.
293 If the type is given, the system uses it to infer implicit arguments
294 of the body. In that case all types are left implicit in the body.
296 We now define the notation `a ◃ b`. Here the keywork `hvbox`
297 and `break` tell the system how to wrap text when it does not
298 fit the screen (they can be safely ignore for the scope of
299 this tutorial). we also add an interpretation for that notation,
300 where the (abstracted) cover relation is implicit. The system
301 will not be able to infer it from the other arguments `C` and `U`
302 and will thus prompt the user for it. This is also why we named this
303 interpretation `covers set temp`: we will later define another
304 interpretation in which the cover relation is the one we are going to
309 notation "hvbox(a break ◃ b)" non associative with precedence 45
310 for @{ 'covers $a $b }.
312 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
316 We can now define the cover relation using the `◃` notation for
317 the premise of infinity.
321 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
322 | creflexivity : ∀a. a ∈ U → cover ? U a
323 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
324 (** screenshot "cover". *)
330 Note that the system accepts the definition
331 but prompts the user for the relation the `cover_set` notion is
334 ![The system asks for a cover relation][cover]
336 The orizontal line separates the hypotheses from the conclusion.
337 The `napply cover` command tells the system that the relation
338 it is looking for is exactly our first context entry (i.e. the inductive
339 predicate we are defining, up to α-conversion); while the `nqed` command
340 ends a definition or proof.
342 We can now define the interpretation for the cover relation between an
343 element and a subset fist, then between two subsets (but this time
344 we fixed the relation `cover_set` is abstracted on).
348 interpretation "covers" 'covers a U = (cover ? U a).
349 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
353 We will proceed similarly for the fish relation, but before going
354 on it is better to give a short introduction to the proof mode of Matita.
355 We define again the `cover_set` term, but this time we will build
356 its body interactively. In λ-calculus Matita is based on, CIC, proofs
357 and terms share the same syntax, and it thus possible to use the
358 commands devoted to build proof term to build regular definitions.
363 ndefinition xcover_set :
364 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
365 (** screenshot "xcover-set-1". *)
367 The system asks for a proof of the full statement, in an empty context.
368 ![xcover_set proof step ][xcover-set-1]
369 The `#` command in the ∀-introduction rule, it gives a name to an
370 assumption putting it in the context, and generates a λ-abstraction
373 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
375 ![xcover_set proof step ][xcover-set-2]
376 We have now to provide a proposition, and we exhibit it. We left
377 a part of it implicit; since the system cannot infer it it will
378 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
381 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
383 ![xcover_set proof step ][xcover-set-3]
384 The proposition we want to provide is an application of the
385 cover relation we have abstracted in the context. The command
386 `napply`, if the given term has not the expected type (in that
387 case it is a product versus a proposition) it applies it to as many
388 implicit arguments as necessary (in that case `? ? ?`).
390 napply cover; (** screenshot "xcover-set-4". *)
392 ![xcover_set proof step ][xcover-set-4]
393 The system will now ask in turn the three implicit arguments
394 passed to cover. The syntax `##[` allows to start a branching
395 to tackle every sub proof individually, otherwise every command
396 is applied to every subrpoof. The command `##|` switches to the next
397 subproof and `##]` ends the branching.
406 The definition of fish works exactly the same way as for cover, except
407 that it is defined as a coinductive proposition.
410 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
415 notation "hvbox(a break ⋉ b)" non associative with precedence 45
416 for @{ 'fish $a $b }.
418 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
420 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
421 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
425 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
426 interpretation "fish" 'fish a U = (fish ? U a).
430 Matita is able to generate elimination rules for inductive types,
431 but not introduction rules for the coinductive case.
435 (* ncheck cover_rect_CProp0. *)
439 We thus have to define the introduction rule for fish by corecursion.
440 Here we again use the proof mode of Matita to exhibit the body of the
441 corecursive function.
445 nlet corec fish_rec (A:Ax) (U: Ω^A)
447 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
448 (** screenshot "def-fish-rec-1". *)
449 #a; #p; napply cfish;
450 ##[ (** screenshot "def-fish-rec-2". *) napply H1;
451 (** screenshot "def-fish-rec-3". *) napply p;
452 ##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i);
453 (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP;
454 (** screenshot "def-fish-rec-5". *) @;
455 ##[ (** screenshot "def-fish-rec-6". *) napply x
456 ##| (** screenshot "def-fish-rec-7". *)
458 ##| (** screenshot "def-fish-rec-8". *)
459 napply (fish_rec ? U P);
467 ![fish proof step][def-fish-rec-1]
468 ![fish proof step][def-fish-rec-2]
469 ![fish proof step][def-fish-rec-3]
470 ![fish proof step][def-fish-rec-4]
471 ![fish proof step][def-fish-rec-5]
472 ![fish proof step][def-fish-rec-6]
473 ![fish proof step][def-fish-rec-7]
474 ![fish proof step][def-fish-rec-8]
477 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
479 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
481 interpretation "coverage cover" 'coverage U = (coverage ? U).
483 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
484 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
486 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
488 ##[ nelim H; #b; (* manca clear *)
489 ##[ #bU; @1; nassumption;
490 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
492 ##| #_; napply CaiU; nassumption; ##] ##]
493 ##| ncases H; ##[ #E; @; nassumption]
494 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
498 ntheorem coverage_min_cover_equation :
499 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
500 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
501 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
502 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
506 notation "⋉F" non associative with precedence 55
509 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
511 interpretation "fished fish" 'fished F = (fished ? F).
513 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
514 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
516 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
517 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
518 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
520 ##| #aF; #H1; @ aF; napply H1;
524 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
525 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
526 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
529 nrecord nAx : Type[2] ≝ {
530 nS:> setoid; (*Type[0];*)
532 nD: ∀a:nS. nI a → Type[0];
533 nd: ∀a:nS. ∀i:nI a. nD a i → nS
537 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
542 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
543 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
545 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
546 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
548 interpretation "D" 'D a i = (nD ? a i).
549 interpretation "d" 'd a i j = (nd ? a i j).
550 interpretation "new I" 'I a = (nI ? a).
552 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
554 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
555 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
557 interpretation "image" 'Im a i = (image ? a i).
559 ndefinition Ax_of_nAx : nAx → Ax.
560 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
563 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
564 sig_intro : ∀x:A.P x → sigma A P.
566 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
568 ndefinition nAx_of_Ax : Ax → nAx.
570 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
571 ##| #a; #i; *; #x; #_; napply x;
575 ninductive Ord (A : nAx) : Type[0] ≝
578 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
580 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
581 notation "x+1" non associative with precedence 50 for @{'oS $x }.
583 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
584 interpretation "ordinals Succ" 'oS x = (oS ? x).
586 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
589 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
590 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
592 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
593 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
595 interpretation "famU" 'famU U x = (famU ? U x).
597 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
599 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
600 ∀y.y ∈ C → y ∈ c A U.
602 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
603 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
604 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
606 ntheorem new_coverage_reflexive:
607 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
608 #A; #U; #a; #H; @ (oO A); napply H;
612 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
613 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
616 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)).
618 naxiom setoidification :
619 ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
628 alias symbol "covers" = "new covers".
629 alias symbol "covers" = "new covers set".
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 ntheorem new_coverage_infinity:
638 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
639 #A; #U; #a;(** screenshot "figure1". *)
640 *; #i; #H; nnormalize in H;
641 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
642 #y; napply H; @ y; napply #; ##] #H';
643 ncases (AC … H'); #f; #Hf;
644 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
645 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
646 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
647 napply (setoidification … Hd); napply Hf';
650 nlemma new_coverage_min :
651 ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
652 #A; #U; #V; #HUV; #Im; #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
654 ##[ #b; #bU0; napply HUV; napply bU0;
655 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
656 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
657 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
660 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
663 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
664 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
667 interpretation "famF" 'famU U x = (famF ? U x).
669 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
671 interpretation "fished new fish" 'fished U = (ord_fished ? U).
672 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
674 ntheorem new_fish_antirefl:
675 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
676 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
679 nlemma co_ord_subset:
680 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
681 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
685 ∀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.
688 ntheorem new_fish_compatible:
689 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
690 #A; #F; #a; #aF; #i; nnormalize;
692 nlapply (aF (Λf+1)); #aLf;
693 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
694 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
695 ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
699 ntheorem max_new_fished:
700 ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
701 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
702 nchange with (G ⊆ F⎽o);
705 ##| #p; #IH; napply (subseteq_intersection_r … IH);
706 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
707 @d; napply IH; napply (setoidification … Ed^-1); napply cG;
708 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
709 #b; #Hb; #d; napply (Hf d); napply Hb;
715 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf