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.
30 buttons, PG-interaction-model, sequent window, script window, ncheck
32 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
33 Symbols (see menu: View ▹ TeX/UTF-8 Table):
40 Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
42 The standard library and the `include` command
43 ----------------------------------------------
45 Some basic notions, like subset, membership, intersection and union
46 are part of the standard library of Matita.
48 These notions come with
49 some notation attached to them:
53 - A ≬ B `A \between B`
55 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
57 The `include` command tells Matita to load a part of the library,
58 in particular the part that we will use can be loaded as follows:
62 include "sets/sets.ma".
66 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
67 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
70 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
71 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
74 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
75 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
81 Some basic results that we will use are also part of the sets library:
83 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
84 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
89 records, projections, types of projections..
93 nrecord Ax : Type[1] ≝ {
101 Note that the field `S` was declared with `:>` instead of a simple `:`.
102 This declares the `S` projection to be a coercion. A coercion is
103 a function case the system automatically inserts when it is needed.
104 In that case, the projection `S` has type `Ax → setoid`, and whenever
105 the expected type of a term is `setoid` while its type is `Ax`, the
106 system inserts the coercion around it, to make the whole term well types.
108 When formalizing an algebraic structure, declaring the carrier as a
109 coercion is a common practice, since it allows to write statements like
111 ∀G:Group.∀x:G.x * x^-1 = 1
113 The quantification over `x` of type `G` is illtyped, since `G` is a term
114 (of type `Group`) and thus not a type. Since the carrier projection
115 `carr` of `G` is a coercion, that maps a `Group` into the type of
116 its elements, the system automatically inserts `carr` around `G`,
117 obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
118 when it displays a term.
120 In this particular case, the coercion `S` allows to write
124 Since `A` is not a type, but it can be turned into a `setoid` by `S`
125 and a `setoid` can be turned into a type by its `carr` projection, the
126 composed coercion `carr ∘ S` is silently inserted.
131 Something that is not still satisfactory, in that the dependent type
132 of `I` and `C` are abstracted over the Axiom set. To obtain the
133 precise type of a term, you can use the `ncheck` command as follows.
142 One would like to write `I a` and not `I A a` under a context where
143 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
144 mecanism simply `A`). In Matita, a question mark represents an implicit
145 argument, i.e. a missing piece of information the system is asked to
146 infer. Matita performs some sort of type inference, thus writing
147 `I ? a` is enough: since the second argument of `I` is typed by the
148 first one, the first one can be inferred just computing the type of `a`.
152 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
156 This is still not completely satisfactory, since you have always type
157 `?`; to fix this minor issue we have to introduce the notational
158 support built in Matita.
163 Matita is quipped with a quite complex notational support,
164 allowing the user to define and use mathematical notations
165 ([From Notation to Semantics: There and Back Again][1]).
167 Since notations are usually ambiguous (e.g. the frequent overloading of
168 symbols) Matita distinguishes between the term level, the
169 content level, and the presentation level, allowing multiple
170 mappings between the contenet and the term level.
172 The mapping between the presentation level (i.e. what is typed on the
173 keyboard and what is displayed in the sequent window) and the content
174 level is defined with the `notation` command. When followed by
175 `>`, it defines an input (only) notation.
179 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
180 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
184 The forst notation defines the writing `𝐈 a` where `a` is a generic
185 term of precedence 90, the maximum one. This high precedence forces
186 parentheses around any term of a lower precedence. For example `𝐈 x`
187 would be accepted, since identifiers have precedence 90, but
188 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
189 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
191 To obtain the `𝐈` is enough to type `I` and then cycle between its
192 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
193 regular letters or the round parentheses, thus their variants (like the
194 bold ones) have to be used.
196 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
197 new content element to which a term `$a` is passed.
199 Content elements have to be interpreted, and possibly multiple,
200 incompatible, interpretations can be defined.
204 interpretation "I" 'I a = (I ? a).
205 interpretation "C" 'C a i = (C ? a i).
209 The `interpretation` command allows to define the mapping between
210 the content level and the terms level. Here we associate the `I` and
211 `C` projections of the Axiom set record, where the Axiom set is an implicit
212 argument `?` to be inferred by the system.
214 Interpretation are bi-directional, thus when displaying a term like
215 `C _ a i`, the system looks for a presentation for the content element
220 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
221 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
225 For output purposes we can define more complex notations, for example
226 we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
227 the size of the arguments and lowering their baseline (i.e. putting them
228 as subscript), separating them with a comma followed by a little space.
230 The first (technical) definition
231 --------------------------------
233 Before defining the cover relation as an inductive predicate, one
234 has to notice that the infinity rule uses, in its hypotheses, the
235 cover relation between two subsets, while the inductive predicate
236 we are going to define relates an element and a subset.
238 An option would be to unfold the definition of cover between subsets,
239 but we prefer to define the abstract notion of cover between subsets
240 (so that we can attach a (ambiguous) notation to it).
242 Anyway, to ease the understaing of the definition of the cover relation
243 between subsets, we first define the inductive predicate unfolding the
244 definition, and we later refine it with.
248 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
249 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
250 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
254 We defined the xcover (x will be removed in the final version of the
255 definition) as an inductive predicate. The arity of the inductive
256 predicate has to be carefully analyzed:
258 > (A : Ax) (U : Ω^A) : A → CProp[0]
260 The syntax separates with `:` abstractions that are fixed for every
261 constructor (introduction rule) and abstractions that can change. In that
262 case the parameter `U` is abstracted once and forall in front of every
263 constructor, and every occurrence of the inductive predicate is applied to
264 `U` in a consistent way. Arguments abstracted on the right of `:` are not
265 constant, for example the xcinfinity constructor introduces `a ◃ U`,
266 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
267 had side of the predicate changes, thus it has to be abstrated (in the arity
268 of the inductive predicate) on the right of `:`.
272 (* ncheck xcreflexivity. *)
276 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
277 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
279 This notion has to be abstracted over the cover relation (whose
280 type is the arity of the inductive `xcover` predicate just defined).
282 Then it has to be abstracted over the arguments of that cover relation,
283 i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
284 sitting on the left hand side of `◃`.
288 ndefinition cover_set :
289 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
291 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
295 The `ndefinition` command takes a name, a type and body (of that type).
296 The type can be omitted, and in that case it is inferred by the system.
297 If the type is given, the system uses it to infer implicit arguments
298 of the body. In that case all types are left implicit in the body.
300 We now define the notation `a ◃ b`. Here the keywork `hvbox`
301 and `break` tell the system how to wrap text when it does not
302 fit the screen (they can be safely ignore for the scope of
303 this tutorial). we also add an interpretation for that notation,
304 where the (abstracted) cover relation is implicit. The system
305 will not be able to infer it from the other arguments `C` and `U`
306 and will thus prompt the user for it. This is also why we named this
307 interpretation `covers set temp`: we will later define another
308 interpretation in which the cover relation is the one we are going to
313 notation "hvbox(a break ◃ b)" non associative with precedence 45
314 for @{ 'covers $a $b }.
316 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
323 We can now define the cover relation using the `◃` notation for
324 the premise of infinity.
328 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
329 | creflexivity : ∀a. a ∈ U → cover ? U a
330 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
331 (** screenshot "cover". *)
337 Note that the system accepts the definition
338 but prompts the user for the relation the `cover_set` notion is
343 The orizontal line separates the hypotheses from the conclusion.
344 The `napply cover` command tells the system that the relation
345 it is looking for is exactly our first context entry (i.e. the inductive
346 predicate we are defining, up to α-conversion); while the `nqed` command
347 ends a definition or proof.
349 We can now define the interpretation for the cover relation between an
350 element and a subset fist, then between two subsets (but this time
351 we fixed the relation `cover_set` is abstracted on).
355 interpretation "covers" 'covers a U = (cover ? U a).
356 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
360 We will proceed similarly for the fish relation, but before going
361 on it is better to give a short introduction to the proof mode of Matita.
362 We define again the `cover_set` term, but this time we will build
363 its body interactively. In λ-calculus Matita is based on, CIC, proofs
364 and terms share the same syntax, and it thus possible to use the
365 commands devoted to build proof term to build regular definitions.
369 ndefinition xcover_set :
370 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
371 (** screenshot "xcover-set-1". *)
372 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
373 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
374 napply cover; (** screenshot "xcover-set-4". *)
382 The system asks for a proof of the full statement, in an empty context.
384 The `#` command is the ∀-introduction rule, it gives a name to an
385 assumption putting it in the context, and generates a λ-abstraction
389 We have now to provide a proposition, and we exhibit it. We left
390 a part of it implicit; since the system cannot infer it it will
391 ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
395 The proposition we want to provide is an application of the
396 cover relation we have abstracted in the context. The command
397 `napply`, if the given term has not the expected type (in that
398 case it is a product versus a proposition) it applies it to as many
399 implicit arguments as necessary (in that case `? ? ?`).
402 The system will now ask in turn the three implicit arguments
403 passed to cover. The syntax `##[` allows to start a branching
404 to tackle every sub proof individually, otherwise every command
405 is applied to every subrpoof. The command `##|` switches to the next
406 subproof and `##]` ends the branching.
414 The definition of fish works exactly the same way as for cover, except
415 that it is defined as a coinductive proposition.
418 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
423 notation "hvbox(a break ⋉ b)" non associative with precedence 45
424 for @{ 'fish $a $b }.
426 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
428 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
429 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
433 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
434 interpretation "fish" 'fish a U = (fish ? U a).
438 Introction rule for fish
439 ------------------------
441 Matita is able to generate elimination rules for inductive types,
442 but not introduction rules for the coinductive case.
446 (* ncheck cover_rect_CProp0. *)
450 We thus have to define the introduction rule for fish by corecursion.
451 Here we again use the proof mode of Matita to exhibit the body of the
452 corecursive function.
456 nlet corec fish_rec (A:Ax) (U: Ω^A)
458 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
459 (** screenshot "def-fish-rec-1". *)
460 #a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
461 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
462 napply H1; (** screenshot "def-fish-rec-3". *)
464 ##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
465 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
466 @; (** screenshot "def-fish-rec-6". *)
468 ##| @; (** screenshot "def-fish-rec-7". *)
470 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
479 Note the first item of the context, it is the corecursive function we are
480 defining. This item allows to perform the recursive call, but we will be
481 allowed to do such call only after having generated a constructor of
482 the fish coinductive type.
484 We introduce `a` and `p`, and then return the fish constructor `cfish`.
485 Since the constructor accepts two arguments, the system asks for them.
488 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
489 With the `nchange` tactic we change `H1` into an equivalent form (this step
490 can be skipped, since the systeem would be able to unfold the definition
491 of inclusion by itself)
494 It is now clear that `H1` can be applied. Again `napply` adds two
495 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
496 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
497 `a`, and it asks a proof that `a ∈ P`.
500 The `nassumption` tactic looks for the required proof in the context, and in
501 that cases finds it in the last context position.
503 We move now to the second branch of the proof, corresponding to the second
504 argument of the `cfish` constructor.
506 We introduce `i` and then we destruct `H2 a p i`, that being a proof
507 of an overlap predicate, give as an element and a proof that it is
508 both in `𝐂 a i` and `P`.
511 We then introduce `x`, break the conjunction (the `*;` command is the
512 equivalent of `ncases` but operates on the first hypothesis that can
513 be introduced. We then introduce the two sides of the conjuction.
516 The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
517 We thus need to use the introduction rulle for the existential quantifier.
518 In CIC it is a defined notion, that is an inductive type with just
519 one constructor (one introduction rule) holding the witness and the proof
520 that the witness satisfies a proposition.
524 Instead of trying to remember the name of the constructor, that should
525 be used as the argument of `napply`, we can ask the system to find by
526 itself the constructor name and apply it with the `@` tactic.
527 Note that some inductive predicates, like the disjunction, have multiple
528 introduction rules, and thus `@` can be followed by a number identifying
532 After choosing `x` as the witness, we have to prove a conjunction,
533 and we again apply the introduction rule for the inductively defined
537 The left hand side of the conjunction is trivial to prove, since it
538 is already in the context. The right hand side needs to perform
539 the co-recursive call.
542 The co-recursive call needs some arguments, but all of them live
543 in the context. Instead of explicitly mention them, we use the
544 `nassumption` tactic, that simply tries to apply every context item.
550 Subset of covered/fished points
551 -------------------------------
553 We now have to define the subset of `S` of points covered by `U`.
554 We also define a prefix notation for it. Remember that the precedence
555 of the prefix form of a symbol has to be lower than the precedence
560 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
562 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
564 interpretation "coverage cover" 'coverage U = (coverage ? U).
568 Here we define the equation characterizing the cover relation.
569 In the igft.ma file we proved that `◃U` is the minimum solution for
570 such equation, the interested reader should be able to reply the proof
575 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
576 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
578 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
580 ##[ nelim H; #b; (* manca clear *)
581 ##[ #bU; @1; nassumption;
582 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
584 ##| #_; napply CaiU; nassumption; ##] ##]
585 ##| ncases H; ##[ #E; @; nassumption]
586 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
590 ntheorem coverage_min_cover_equation :
591 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
592 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
593 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
594 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
600 We similarly define the subset of point fished by `F`, the
601 equation characterizing `⋉F` and prove that fish is
602 the biggest solution for such equation.
606 notation "⋉F" non associative with precedence 55
609 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
611 interpretation "fished fish" 'fished F = (fished ? F).
613 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
614 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
616 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
617 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
618 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
620 ##| #aF; #H1; @ aF; napply H1;
624 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
625 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
626 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
631 Part 2, the new set of axioms
632 -----------------------------
636 nrecord nAx : Type[2] ≝ {
639 nD: ∀a:nS. nI a → Type[0];
640 nd: ∀a:nS. ∀i:nI a. nD a i → nS
644 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
649 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
650 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
652 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
653 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
655 interpretation "D" 'D a i = (nD ? a i).
656 interpretation "d" 'd a i j = (nd ? a i j).
657 interpretation "new I" 'I a = (nI ? a).
659 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
661 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
662 notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
664 interpretation "image" 'Im a i = (image ? a i).
666 ndefinition Ax_of_nAx : nAx → Ax.
667 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
670 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
671 sig_intro : ∀x:A.P x → sigma A P.
673 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
675 ndefinition nAx_of_Ax : Ax → nAx.
677 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
678 ##| #a; #i; *; #x; #_; napply x;
682 ninductive Ord (A : nAx) : Type[0] ≝
685 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
687 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
688 notation "x+1" non associative with precedence 50 for @{'oS $x }.
690 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
691 interpretation "ordinals Succ" 'oS x = (oS ? x).
693 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
696 | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
697 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
699 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
700 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
702 interpretation "famU" 'famU U x = (famU ? U x).
704 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
706 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
707 ∀y.y ∈ C → y ∈ c A U.
709 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
710 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
711 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
713 ntheorem new_coverage_reflexive:
714 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
715 #A; #U; #a; #H; @ (oO A); napply H;
719 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
720 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
723 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)).
725 naxiom setoidification :
726 ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
735 alias symbol "covers" = "new covers".
736 alias symbol "covers" = "new covers set".
737 alias symbol "covers" = "new covers".
738 alias symbol "covers" = "new covers set".
739 alias symbol "covers" = "new covers".
740 alias symbol "covers" = "new covers set".
741 alias symbol "covers" = "new covers".
742 alias symbol "covers" = "new covers set".
743 alias symbol "covers" = "new covers".
744 ntheorem new_coverage_infinity:
745 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
746 #A; #U; #a;(** screenshot "figure1". *)
747 *; #i; #H; nnormalize in H;
748 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
749 #y; napply H; @ y; napply #; ##] #H';
750 ncases (AC … H'); #f; #Hf;
751 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
752 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
753 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
754 napply (setoidification … Hd); napply Hf';
757 nlemma new_coverage_min :
758 ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
759 #A; #U; #V; #HUV; #Im; #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
761 ##[ #b; #bU0; napply HUV; napply bU0;
762 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
763 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
764 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
767 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
770 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
771 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
774 interpretation "famF" 'famU U x = (famF ? U x).
776 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
778 interpretation "fished new fish" 'fished U = (ord_fished ? U).
779 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
781 ntheorem new_fish_antirefl:
782 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
783 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
786 nlemma co_ord_subset:
787 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
788 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
792 ∀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.
795 ntheorem new_fish_compatible:
796 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
797 #A; #F; #a; #aF; #i; nnormalize;
799 nlapply (aF (Λf+1)); #aLf;
800 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
801 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
802 ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
806 ntheorem max_new_fished:
807 ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
808 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
809 nchange with (G ⊆ F⎽o);
812 ##| #p; #IH; napply (subseteq_intersection_r … IH);
813 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
814 @d; napply IH; napply (setoidification … Ed^-1); napply cG;
815 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
816 #b; #Hb; #d; napply (Hf d); napply Hb;
822 Appendix: natural deduction like tactics explanation
823 -----------------------------------------------------
825 In this appendix we try to give a description of tactics
826 in terms of natural deduction rules annotated with proofs.
827 The `:` separator has to be read as _is a proof of_, in the spirit
828 of the Curry-Howard isomorphism.
830 f : A1 → … → An → B ?1 : A1 … ?n : An
831 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
839 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
844 (?1 args1) : P(k1 args1) … (?n argsn) : P(kn argsn)
845 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
846 match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x)
852 x : T ?1 : P(k1) … ?n : P(kn t)
853 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
854 (T_rect_CProp0 ?1 … ?n) : P(x)
856 Where `T_rect_CProp0` is the induction principle for the
860 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
863 Where the equivalence relation between types `≡` keeps into account
864 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
865 definition unfolding), ι-reduction (pattern matching simplification),
866 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
874 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf