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).
328 We can now define the cover relation using the `◃` notation for
329 the premise of infinity.
333 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
334 | creflexivity : ∀a. a ∈ U → cover ? U a
335 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
336 (** screenshot "cover". *)
342 Note that the system accepts the definition
343 but prompts the user for the relation the `cover_set` notion is
348 The orizontal line separates the hypotheses from the conclusion.
349 The `napply cover` command tells the system that the relation
350 it is looking for is exactly our first context entry (i.e. the inductive
351 predicate we are defining, up to α-conversion); while the `nqed` command
352 ends a definition or proof.
354 We can now define the interpretation for the cover relation between an
355 element and a subset fist, then between two subsets (but this time
356 we fixed the relation `cover_set` is abstracted on).
360 interpretation "covers" 'covers a U = (cover ? U a).
361 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
365 We will proceed similarly for the fish relation, but before going
366 on it is better to give a short introduction to the proof mode of Matita.
367 We define again the `cover_set` term, but this time we will build
368 its body interactively. In λ-calculus Matita is based on, CIC, proofs
369 and terms share the same syntax, and it thus possible to use the
370 commands devoted to build proof term to build regular definitions.
374 ndefinition xcover_set :
375 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
376 (** screenshot "xcover-set-1". *)
377 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
378 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
379 napply cover; (** screenshot "xcover-set-4". *)
387 The system asks for a proof of the full statement, in an empty context.
389 The `#` command is the ∀-introduction rule, it gives a name to an
390 assumption putting it in the context, and generates a λ-abstraction
394 We have now to provide a proposition, and we exhibit it. We left
395 a part of it implicit; since the system cannot infer it it will
396 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
400 The proposition we want to provide is an application of the
401 cover relation we have abstracted in the context. The command
402 `napply`, if the given term has not the expected type (in that
403 case it is a product versus a proposition) it applies it to as many
404 implicit arguments as necessary (in that case `? ? ?`).
407 The system will now ask in turn the three implicit arguments
408 passed to cover. The syntax `##[` allows to start a branching
409 to tackle every sub proof individually, otherwise every command
410 is applied to every subrpoof. The command `##|` switches to the next
411 subproof and `##]` ends the branching.
419 The definition of fish works exactly the same way as for cover, except
420 that it is defined as a coinductive proposition.
423 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
428 notation "hvbox(a break ⋉ b)" non associative with precedence 45
429 for @{ 'fish $a $b }.
431 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
433 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
434 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
438 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
439 interpretation "fish" 'fish a U = (fish ? U a).
443 Introction rule for fish
444 ------------------------
446 Matita is able to generate elimination rules for inductive types,
447 but not introduction rules for the coinductive case.
451 (* ncheck cover_rect_CProp0. *)
455 We thus have to define the introduction rule for fish by corecursion.
456 Here we again use the proof mode of Matita to exhibit the body of the
457 corecursive function.
461 nlet corec fish_rec (A:Ax) (U: Ω^A)
463 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
464 (** screenshot "def-fish-rec-1". *)
465 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
466 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
467 napply H1; (** screenshot "def-fish-rec-3". *)
469 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
470 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
471 @; (** screenshot "def-fish-rec-6". *)
473 ##| @; (** screenshot "def-fish-rec-7". *)
475 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
484 Note the first item of the context, it is the corecursive function we are
485 defining. This item allows to perform the recursive call, but we will be
486 allowed to do such call only after having generated a constructor of
487 the fish coinductive type.
489 We introduce `a` and `p`, and then return the fish constructor `cfish`.
490 Since the constructor accepts two arguments, the system asks for them.
493 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
494 With the `nchange` tactic we change `H1` into an equivalent form (this step
495 can be skipped, since the systeem would be able to unfold the definition
496 of inclusion by itself)
499 It is now clear that `H1` can be applied. Again `napply` adds two
500 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
501 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
502 `a`, and it asks a proof that `a ∈ P`.
505 The `nassumption` tactic looks for the required proof in the context, and in
506 that cases finds it in the last context position.
508 We move now to the second branch of the proof, corresponding to the second
509 argument of the `cfish` constructor.
511 We introduce `i` and then we destruct `H2 a p i`, that being a proof
512 of an overlap predicate, give as an element and a proof that it is
513 both in `𝐂 a i` and `P`.
516 We then introduce `x`, break the conjunction (the `*;` command is the
517 equivalent of `ncases` but operates on the first hypothesis that can
518 be introduced. We then introduce the two sides of the conjuction.
521 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
522 We thus need to use the introduction rulle for the existential quantifier.
523 In CIC it is a defined notion, that is an inductive type with just
524 one constructor (one introduction rule) holding the witness and the proof
525 that the witness satisfies a proposition.
529 Instead of trying to remember the name of the constructor, that should
530 be used as the argument of `napply`, we can ask the system to find by
531 itself the constructor name and apply it with the `@` tactic.
532 Note that some inductive predicates, like the disjunction, have multiple
533 introduction rules, and thus `@` can be followed by a number identifying
537 After choosing `x` as the witness, we have to prove a conjunction,
538 and we again apply the introduction rule for the inductively defined
542 The left hand side of the conjunction is trivial to prove, since it
543 is already in the context. The right hand side needs to perform
544 the co-recursive call.
547 The co-recursive call needs some arguments, but all of them live
548 in the context. Instead of explicitly mention them, we use the
549 `nassumption` tactic, that simply tries to apply every context item.
555 Subset of covered/fished points
556 -------------------------------
558 We now have to define the subset of `S` of points covered by `U`.
559 We also define a prefix notation for it. Remember that the precedence
560 of the prefix form of a symbol has to be lower than the precedence
565 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
567 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
569 interpretation "coverage cover" 'coverage U = (coverage ? U).
573 Here we define the equation characterizing the cover relation.
574 In the igft.ma file we proved that `◃U` is the minimum solution for
575 such equation, the interested reader should be able to reply the proof
580 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
581 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
583 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
585 ##[ nelim H; #b; (* manca clear *)
586 ##[ #bU; @1; nassumption;
587 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
589 ##| #_; napply CaiU; nassumption; ##] ##]
590 ##| ncases H; ##[ #E; @; nassumption]
591 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
595 ntheorem coverage_min_cover_equation :
596 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
597 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
598 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
599 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
605 We similarly define the subset of point fished by `F`, the
606 equation characterizing `⋉F` and prove that fish is
607 the biggest solution for such equation.
611 notation "⋉F" non associative with precedence 55
614 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
616 interpretation "fished fish" 'fished F = (fished ? F).
618 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
619 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
621 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
622 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
623 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
625 ##| #aF; #H1; @ aF; napply H1;
629 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
630 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
631 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
636 Part 2, the new set of axioms
637 -----------------------------
641 nrecord nAx : Type[2] ≝ {
644 nD: ∀a:nS. nI a → Type[0];
645 nd: ∀a:nS. ∀i:nI a. nD a i → nS
649 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
654 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
655 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
657 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
658 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
660 interpretation "D" 'D a i = (nD ? a i).
661 interpretation "d" 'd a i j = (nd ? a i j).
662 interpretation "new I" 'I a = (nI ? a).
664 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
666 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
667 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
669 interpretation "image" 'Im a i = (image ? a i).
671 ndefinition Ax_of_nAx : nAx → Ax.
672 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
675 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
676 sig_intro : ∀x:A.P x → sigma A P.
678 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
680 ndefinition nAx_of_Ax : Ax → nAx.
682 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
683 ##| #a; #i; *; #x; #_; napply x;
687 ninductive Ord (A : nAx) : Type[0] ≝
690 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
692 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
693 notation "x+1" non associative with precedence 50 for @{'oS $x }.
695 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
696 interpretation "ordinals Succ" 'oS x = (oS ? x).
698 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
701 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
702 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
704 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
705 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
707 interpretation "famU" 'famU U x = (famU ? U x).
709 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
711 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
712 ∀y.y ∈ C → y ∈ c A U.
714 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
715 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
716 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
718 ntheorem new_coverage_reflexive:
719 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
720 #A; #U; #a; #H; @ (oO A); napply H;
724 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
725 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
728 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)).
730 naxiom setoidification :
731 ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
740 alias symbol "covers" = "new covers".
741 alias symbol "covers" = "new covers set".
742 alias symbol "covers" = "new covers".
743 alias symbol "covers" = "new covers set".
744 alias symbol "covers" = "new covers".
745 alias symbol "covers" = "new covers set".
746 alias symbol "covers" = "new covers".
747 alias symbol "covers" = "new covers set".
748 alias symbol "covers" = "new covers".
749 ntheorem new_coverage_infinity:
750 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
751 #A; #U; #a;(** screenshot "figure1". *)
752 *; #i; #H; nnormalize in H;
753 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
754 #y; napply H; @ y; napply #; ##] #H';
755 ncases (AC … H'); #f; #Hf;
756 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
757 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
758 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
759 napply (setoidification … Hd); napply Hf';
762 nlemma new_coverage_min :
763 ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
764 #A; #U; #V; #HUV; #Im; #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
766 ##[ #b; #bU0; napply HUV; napply bU0;
767 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
768 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
769 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
772 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
775 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
776 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
779 interpretation "famF" 'famU U x = (famF ? U x).
781 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
783 interpretation "fished new fish" 'fished U = (ord_fished ? U).
784 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
786 ntheorem new_fish_antirefl:
787 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
788 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
791 nlemma co_ord_subset:
792 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
793 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
797 ∀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.
800 ntheorem new_fish_compatible:
801 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
802 #A; #F; #a; #aF; #i; nnormalize;
804 nlapply (aF (Λf+1)); #aLf;
805 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
806 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
807 ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
811 ntheorem max_new_fished:
812 ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
813 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
814 nchange with (G ⊆ F⎽o);
817 ##| #p; #IH; napply (subseteq_intersection_r … IH);
818 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
819 @d; napply IH; napply (setoidification … Ed^-1); napply cG;
820 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
821 #b; #Hb; #d; napply (Hf d); napply Hb;
827 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf