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.
26 apply (f : A -> B): --------------------
29 f: A1 -> ... -> An -> B ?1: A1 ... ?n: An
30 apply (f : A -> B): ------------------------------------------------
31 apply f == f \ldots == f ? ... ? : B
35 buttons, PG-interaction-model, sequent window, script window, ncheck
37 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
38 Symbols (see menu: View ▹ TeX/UTF-8 Table):
45 Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
47 The standard library and the `include` command
48 ----------------------------------------------
50 Some basic notions, like subset, membership, intersection and union
51 are part of the standard library of Matita.
53 These notions come with
54 some notation attached to them:
58 - A ≬ B `A \between B`
60 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
62 The `include` command tells Matita to load a part of the library,
63 in particular the part that we will use can be loaded as follows:
67 include "sets/sets.ma".
71 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
72 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
75 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
76 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
79 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
80 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
86 Some basic results that we will use are also part of the sets library:
88 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
89 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
94 records, projections, types of projections..
98 nrecord Ax : Type[1] ≝ {
101 C : ∀a:S. I a → Ω ^ S
106 Note that the field `S` was declared with `:>` instead of a simple `:`.
107 This declares the `S` projection to be a coercion. A coercion is
108 a function case the system automatically inserts when it is needed.
109 In that case, the projection `S` has type `Ax → setoid`, and whenever
110 the expected type of a term is `setoid` while its type is `Ax`, the
111 system inserts the coercion around it, to make the whole term well types.
113 When formalizing an algebraic structure, declaring the carrier as a
114 coercion is a common practice, since it allows to write statements like
116 ∀G:Group.∀x:G.x * x^-1 = 1
118 The quantification over `x` of type `G` is illtyped, since `G` is a term
119 (of type `Group`) and thus not a type. Since the carrier projection
120 `carr` of `G` is a coercion, that maps a `Group` into the type of
121 its elements, the system automatically inserts `carr` around `G`,
122 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
123 when it displays a term.
125 In this particular case, the coercion `S` allows to write
129 Since `A` is not a type, but it can be turned into a `setoid` by `S`
130 and a `setoid` can be turned into a type by its `carr` projection, the
131 composed coercion `carr ∘ S` is silently inserted.
136 Something that is not still satisfactory, in that the dependent type
137 of `I` and `C` are abstracted over the Axiom set. To obtain the
138 precise type of a term, you can use the `ncheck` command as follows.
147 One would like to write `I a` and not `I A a` under a context where
148 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
149 mecanism simply `A`). In Matita, a question mark represents an implicit
150 argument, i.e. a missing piece of information the system is asked to
151 infer. Matita performs some sort of type inference, thus writing
152 `I ? a` is enough: since the second argument of `I` is typed by the
153 first one, the first one can be inferred just computing the type of `a`.
157 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
161 This is still not completely satisfactory, since you have always type
162 `?`; to fix this minor issue we have to introduce the notational
163 support built in Matita.
168 Matita is quipped with a quite complex notational support,
169 allowing the user to define and use mathematical notations
170 ([From Notation to Semantics: There and Back Again][1]).
172 Since notations are usually ambiguous (e.g. the frequent overloading of
173 symbols) Matita distinguishes between the term level, the
174 content level, and the presentation level, allowing multiple
175 mappings between the contenet and the term level.
177 The mapping between the presentation level (i.e. what is typed on the
178 keyboard and what is displayed in the sequent window) and the content
179 level is defined with the `notation` command. When followed by
180 `>`, it defines an input (only) notation.
184 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
185 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
189 The forst notation defines the writing `𝐈 a` where `a` is a generic
190 term of precedence 90, the maximum one. This high precedence forces
191 parentheses around any term of a lower precedence. For example `𝐈 x`
192 would be accepted, since identifiers have precedence 90, but
193 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
194 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
196 To obtain the `𝐈` is enough to type `I` and then cycle between its
197 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
198 regular letters or the round parentheses, thus their variants (like the
199 bold ones) have to be used.
201 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
202 new content element to which a term `$a` is passed.
204 Content elements have to be interpreted, and possibly multiple,
205 incompatible, interpretations can be defined.
209 interpretation "I" 'I a = (I ? a).
210 interpretation "C" 'C a i = (C ? a i).
214 The `interpretation` command allows to define the mapping between
215 the content level and the terms level. Here we associate the `I` and
216 `C` projections of the Axiom set record, where the Axiom set is an implicit
217 argument `?` to be inferred by the system.
219 Interpretation are bi-directional, thus when displaying a term like
220 `C _ a i`, the system looks for a presentation for the content element
225 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
226 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
230 For output purposes we can define more complex notations, for example
231 we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
232 the size of the arguments and lowering their baseline (i.e. putting them
233 as subscript), separating them with a comma followed by a little space.
235 The first (technical) definition
236 --------------------------------
238 Before defining the cover relation as an inductive predicate, one
239 has to notice that the infinity rule uses, in its hypotheses, the
240 cover relation between two subsets, while the inductive predicate
241 we are going to define relates an element and a subset.
243 An option would be to unfold the definition of cover between subsets,
244 but we prefer to define the abstract notion of cover between subsets
245 (so that we can attach a (ambiguous) notation to it).
247 Anyway, to ease the understaing of the definition of the cover relation
248 between subsets, we first define the inductive predicate unfolding the
249 definition, and we later refine it with.
253 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
254 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
255 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
259 We defined the xcover (x will be removed in the final version of the
260 definition) as an inductive predicate. The arity of the inductive
261 predicate has to be carefully analyzed:
263 > (A : Ax) (U : Ω^A) : A → CProp[0]
265 The syntax separates with `:` abstractions that are fixed for every
266 constructor (introduction rule) and abstractions that can change. In that
267 case the parameter `U` is abstracted once and forall in front of every
268 constructor, and every occurrence of the inductive predicate is applied to
269 `U` in a consistent way. Arguments abstracted on the right of `:` are not
270 constant, for example the xcinfinity constructor introduces `a ◃ U`,
271 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
272 had side of the predicate changes, thus it has to be abstrated (in the arity
273 of the inductive predicate) on the right of `:`.
277 (* ncheck xcreflexivity. *)
281 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
282 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
284 This notion has to be abstracted over the cover relation (whose
285 type is the arity of the inductive `xcover` predicate just defined).
287 Then it has to be abstracted over the arguments of that cover relation,
288 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
289 sitting on the left hand side of `◃`.
293 ndefinition cover_set :
294 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
296 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
300 The `ndefinition` command takes a name, a type and body (of that type).
301 The type can be omitted, and in that case it is inferred by the system.
302 If the type is given, the system uses it to infer implicit arguments
303 of the body. In that case all types are left implicit in the body.
305 We now define the notation `a ◃ b`. Here the keywork `hvbox`
306 and `break` tell the system how to wrap text when it does not
307 fit the screen (they can be safely ignore for the scope of
308 this tutorial). we also add an interpretation for that notation,
309 where the (abstracted) cover relation is implicit. The system
310 will not be able to infer it from the other arguments `C` and `U`
311 and will thus prompt the user for it. This is also why we named this
312 interpretation `covers set temp`: we will later define another
313 interpretation in which the cover relation is the one we are going to
318 notation "hvbox(a break ◃ b)" non associative with precedence 45
319 for @{ 'covers $a $b }.
321 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
325 We can now define the cover relation using the `◃` notation for
326 the premise of infinity.
330 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
331 | creflexivity : ∀a. a ∈ U → cover ? U a
332 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
333 (** screenshot "cover". *)
339 Note that the system accepts the definition
340 but prompts the user for the relation the `cover_set` notion is
345 The orizontal line separates the hypotheses from the conclusion.
346 The `napply cover` command tells the system that the relation
347 it is looking for is exactly our first context entry (i.e. the inductive
348 predicate we are defining, up to α-conversion); while the `nqed` command
349 ends a definition or proof.
351 We can now define the interpretation for the cover relation between an
352 element and a subset fist, then between two subsets (but this time
353 we fixed the relation `cover_set` is abstracted on).
357 interpretation "covers" 'covers a U = (cover ? U a).
358 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
362 We will proceed similarly for the fish relation, but before going
363 on it is better to give a short introduction to the proof mode of Matita.
364 We define again the `cover_set` term, but this time we will build
365 its body interactively. In λ-calculus Matita is based on, CIC, proofs
366 and terms share the same syntax, and it thus possible to use the
367 commands devoted to build proof term to build regular definitions.
371 ndefinition xcover_set :
372 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
373 (** screenshot "xcover-set-1". *)
374 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
375 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
376 napply cover; (** screenshot "xcover-set-4". *)
384 The system asks for a proof of the full statement, in an empty context.
386 The `#` command is the ∀-introduction rule, it gives a name to an
387 assumption putting it in the context, and generates a λ-abstraction
391 We have now to provide a proposition, and we exhibit it. We left
392 a part of it implicit; since the system cannot infer it it will
393 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
397 The proposition we want to provide is an application of the
398 cover relation we have abstracted in the context. The command
399 `napply`, if the given term has not the expected type (in that
400 case it is a product versus a proposition) it applies it to as many
401 implicit arguments as necessary (in that case `? ? ?`).
404 The system will now ask in turn the three implicit arguments
405 passed to cover. The syntax `##[` allows to start a branching
406 to tackle every sub proof individually, otherwise every command
407 is applied to every subrpoof. The command `##|` switches to the next
408 subproof and `##]` ends the branching.
412 The definition of fish works exactly the same way as for cover, except
413 that it is defined as a coinductive proposition.
416 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
421 notation "hvbox(a break ⋉ b)" non associative with precedence 45
422 for @{ 'fish $a $b }.
424 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
426 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
427 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
431 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
432 interpretation "fish" 'fish a U = (fish ? U a).
436 Matita is able to generate elimination rules for inductive types,
437 but not introduction rules for the coinductive case.
441 (* ncheck cover_rect_CProp0. *)
445 We thus have to define the introduction rule for fish by corecursion.
446 Here we again use the proof mode of Matita to exhibit the body of the
447 corecursive function.
451 nlet corec fish_rec (A:Ax) (U: Ω^A)
453 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
454 (** screenshot "def-fish-rec-1". *)
455 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
456 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
457 napply H1; (** screenshot "def-fish-rec-3". *)
459 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
460 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
461 @; (** screenshot "def-fish-rec-6". *)
463 ##| @; (** screenshot "def-fish-rec-7". *)
465 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
474 Note the first item of the context, it is the corecursive function we are
475 defining. This item allows to perform the recursive call, but we will be
476 allowed to do such call only after having generated a constructor of
477 the fish coinductive type.
479 We introduce `a` and `p`, and then return the fish constructor `cfish`.
480 Since the constructor accepts two arguments, the system asks for them.
483 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
484 With the `nchange` tactic we change `H1` into an equivalent form (this step
485 can be skipped, since the systeem would be able to unfold the definition
486 of inclusion by itself)
489 It is now clear that `H1` can be applied. Again `napply` adds two
490 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
491 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
492 `a`, and it asks a proof that `a ∈ P`.
495 The `nassumption` tactic looks for the required proof in the context, and in
496 that cases finds it in the last context position.
498 We move now to the second branch of the proof, corresponding to the second
499 argument of the `cfish` constructor.
501 We introduce `i` and then we destruct `H2 a p i`, that being a proof
502 of an overlap predicate, give as an element and a proof that it is
503 both in `𝐂 a i` and `P`.
506 We then introduce `x`, break the conjunction (the `*;` command is the
507 equivalent of `ncases` but operates on the first hypothesis that can
508 be introduced. We then introduce the two sides of the conjuction.
511 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
512 We thus need to use the introduction rulle for the existential quantifier.
513 In CIC it is a defined notion, that is an inductive type with just
514 one constructor (one introduction rule) holding the witness and the proof
515 that the witness satisfies a proposition.
519 Instead of trying to remember the name of the constructor, that should
520 be used as the argument of `napply`, we can ask the system to find by
521 itself the constructor name and apply it with the `@` tactic.
522 Note that some inductive predicates, like the disjunction, have multiple
523 introduction rules, and thus `@` can be followed by a number identifying
527 After choosing `x` as the witness, we have to prove a conjunction,
528 and we again apply the introduction rule for the inductively defined
532 The left hand side of the conjunction is trivial to prove, since it
533 is already in the context. The right hand side needs to perform
534 the co-recursive call.
537 The co-recursive call needs some arguments, but all of them live
538 in the context. Instead of explicitly mention them, we use the
539 `nassumption` tactic, that simply tries to apply every context item.
543 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
545 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
547 interpretation "coverage cover" 'coverage U = (coverage ? U).
549 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
550 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
552 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
554 ##[ nelim H; #b; (* manca clear *)
555 ##[ #bU; @1; nassumption;
556 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
558 ##| #_; napply CaiU; nassumption; ##] ##]
559 ##| ncases H; ##[ #E; @; nassumption]
560 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
564 ntheorem coverage_min_cover_equation :
565 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
566 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
567 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
568 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
572 notation "⋉F" non associative with precedence 55
575 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
577 interpretation "fished fish" 'fished F = (fished ? F).
579 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
580 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
582 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
583 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
584 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
586 ##| #aF; #H1; @ aF; napply H1;
590 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
591 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
592 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
595 nrecord nAx : Type[2] ≝ {
596 nS:> setoid; (*Type[0];*)
598 nD: ∀a:nS. nI a → Type[0];
599 nd: ∀a:nS. ∀i:nI a. nD a i → nS
603 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
608 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
609 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
611 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
612 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
614 interpretation "D" 'D a i = (nD ? a i).
615 interpretation "d" 'd a i j = (nd ? a i j).
616 interpretation "new I" 'I a = (nI ? a).
618 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
620 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
621 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
623 interpretation "image" 'Im a i = (image ? a i).
625 ndefinition Ax_of_nAx : nAx → Ax.
626 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
629 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
630 sig_intro : ∀x:A.P x → sigma A P.
632 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
634 ndefinition nAx_of_Ax : Ax → nAx.
636 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
637 ##| #a; #i; *; #x; #_; napply x;
641 ninductive Ord (A : nAx) : Type[0] ≝
644 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
646 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
647 notation "x+1" non associative with precedence 50 for @{'oS $x }.
649 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
650 interpretation "ordinals Succ" 'oS x = (oS ? x).
652 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
655 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
656 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
658 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
659 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
661 interpretation "famU" 'famU U x = (famU ? U x).
663 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
665 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
666 ∀y.y ∈ C → y ∈ c A U.
668 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
669 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
670 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
672 ntheorem new_coverage_reflexive:
673 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
674 #A; #U; #a; #H; @ (oO A); napply H;
678 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
679 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
682 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)).
684 naxiom setoidification :
685 ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
694 alias symbol "covers" = "new covers".
695 alias symbol "covers" = "new covers set".
696 alias symbol "covers" = "new covers".
697 alias symbol "covers" = "new covers set".
698 alias symbol "covers" = "new covers".
699 alias symbol "covers" = "new covers set".
700 alias symbol "covers" = "new covers".
701 alias symbol "covers" = "new covers set".
702 alias symbol "covers" = "new covers".
703 ntheorem new_coverage_infinity:
704 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
705 #A; #U; #a;(** screenshot "figure1". *)
706 *; #i; #H; nnormalize in H;
707 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
708 #y; napply H; @ y; napply #; ##] #H';
709 ncases (AC … H'); #f; #Hf;
710 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
711 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
712 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
713 napply (setoidification … Hd); napply Hf';
716 nlemma new_coverage_min :
717 ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
718 #A; #U; #V; #HUV; #Im; #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
720 ##[ #b; #bU0; napply HUV; napply bU0;
721 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
722 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
723 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
726 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
729 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
730 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
733 interpretation "famF" 'famU U x = (famF ? U x).
735 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
737 interpretation "fished new fish" 'fished U = (ord_fished ? U).
738 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
740 ntheorem new_fish_antirefl:
741 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
742 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
745 nlemma co_ord_subset:
746 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
747 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
751 ∀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.
754 ntheorem new_fish_compatible:
755 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
756 #A; #F; #a; #aF; #i; nnormalize;
758 nlapply (aF (Λf+1)); #aLf;
759 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
760 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
761 ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
765 ntheorem max_new_fished:
766 ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
767 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
768 nchange with (G ⊆ F⎽o);
771 ##| #p; #IH; napply (subseteq_intersection_r … IH);
772 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
773 @d; napply IH; napply (setoidification … Ed^-1); napply cG;
774 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
775 #b; #Hb; #d; napply (Hf d); napply Hb;
781 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf