3 Matita Tutorial: inductively generated formal topologies
4 ========================================================
6 This is a not so short introduction to [Matita][2], 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 Stefano Berardi and Silvio Valentini.
15 The tutorial is by Enrico Tassi.
17 The tutorial spends a considerable amount of effort in defining
18 notations that resemble the ones used in the original paper. We believe
19 this is a important part of every formalization, not only from the aesthetic
20 point of view, but also from the practical point of view. Being
21 consistent allows to follow the paper in a pedantic way, and hopefully
22 to make the formalization (at least the definitions and proved
23 statements) readable to the author of the paper.
25 The formalization uses the ng (new generation) version of Matita
26 (that will be named 1.x when finally released).
27 Last stable release of the "old" system is named 0.5.7; the ng system
28 is coexisting with the old one in every development release
29 (named "nightly builds" in the download page of Matita)
30 with a version strictly greater than 0.5.7.
32 To read this tutorial in HTML format, you need a decent browser
33 equipped with a unicode capable font. Use the PDF format if some
34 symbols are not displayed correctly.
39 The graphical interface of Matita is composed of three windows:
40 the script window, on the left, is where you type; the sequent
41 window on the top right is where the system shows you the ongoing proof;
42 the error window, on the bottom right, is where the system complains.
43 On the top of the script window five buttons drive the processing of
44 the proof script. From left to right they request the system to:
46 - go back to the beginning of the script
48 - go to the current cursor position
50 - advance to the end of the script
52 When the system processes a command, it locks the part of the script
53 corresponding to the command, such that you cannot edit it anymore
54 (without going back). Locked parts are coloured in blue.
56 The sequent window is hyper textual, i.e. you can click on symbols
57 to jump to their definition, or switch between different notations
58 for the same expression (for example, equality has two notations,
59 one of them makes the type of the arguments explicit).
61 Everywhere in the script you can use the `ncheck (term).` command to
62 ask for the type a given term. If you do that in the middle of a proof,
63 the term is assumed to live in the current proof context (i.e. can use
64 variables introduced so far).
66 To ease the typing of mathematical symbols, the script window
67 implements two unusual input facilities:
69 - some TeX symbols can be typed using their TeX names, and are
70 automatically converted to UTF-8 characters. For a list of
71 the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
72 Moreover some ASCII-art is understood as well, like `=>` and `->`
73 to mean double or single arrows.
74 Here we recall some of these "shortcuts":
76 - ∀ can be typed with `\forall`
77 - λ can be typed with `\lambda`
78 - ≝ can be typed with `\def` or `:=`
79 - → can be typed with `\to` or `->`
81 - some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
82 The user can cycle between variants typing one of them and then
83 pressing ALT-L. Note that also letters do have variants, for
84 example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
85 Variants are listed in the aforementioned TeX/UTF-8 table.
87 The syntax of terms (and types) is the one of the λ-calculus CIC
88 on which Matita is based. The main syntactical difference w.r.t.
89 the usual mathematical notation is the function application, written
90 `(f x y)` in place of `f(x,y)`.
92 Pressing `F1` opens the Matita manual.
94 CIC (as [implemented in Matita][3]) in a nutshell
95 -------------------------------------------------
97 CIC is a full and functional Pure Type System (all products do exist,
98 and their sort is is determined by the target) with an impredicative sort
99 Prop and a predicative sort Type. It features both dependent types and
100 polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
101 the same syntax, and they can occur in types.
103 The environment used for in the typing judgement can be populated with
104 well typed definitions or theorems, (co)inductive types validating positivity
105 conditions and recursive functions provably total by simple syntactical
106 analysis (recursive calls are allowed only on structurally smaller subterms).
108 functions can be defined as well, and must satisfy the dual condition, i.e.
109 performing the recursive call only after having generated a constructor (a piece
112 The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
113 types defined in the environment. This construct, together with the possibility to
114 definable total recursive functions, allows to define eliminators (or constructors)
115 for (co)inductive types. The λ-calculus is also equipped with explicitly typed
116 local definitions (let in) that in the degenerate case work as casts (i.e.
117 the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
119 Types are compare up to conversion. Since types may depend on terms, conversion
120 involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
121 definition unfolding), ι-reduction (pattern matching simplification),
122 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
125 Since we are going to formalize constructive and predicative mathematics
126 in an intensional type theory like CIC, we try to establish some terminology.
127 Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
130 We write `Type[i]` to mention a Type in the predicative hierarchy
131 of types. To ease the comprehension we will use `Type[0]` for sets,
132 and `Type[1]` for classes. The index `i` is just a label: constraints among
133 universes are declared by the user. The standard library defines
135 > Type[0] < Type[1] < Type[2]
137 <object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
139 For every `Type[i]` there is a corresponding level of predicative
140 propositions `CProp[i]` (the C initial is due to historical reasons, and
141 stands for constructive, `PProp` would be more appropriate).
142 A predicative proposition cannot be eliminated toward
143 `Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
144 with 0 or 1 constructors with propositional arguments, like `Id` and `And`
147 The distintion between predicative propositions and predicative data types
148 is a peculirity of Matita (for example in CIC as implemented by Coq they are the
149 same). The additional restriction of not allowing the elimination of a CProp
150 toward a Type makes the theory of Matita minimal in the following sense:
152 <object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
154 Theorems proved in this setting can be reused in a classical framwork (forcing
155 Matita to collapse the hierarchy of constructive propositions). Alternatively,
156 one can decide to collapse predicative propositions and datatypes recovering the
157 Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
158 provide a witness for a Σ).
160 Formalization choices
161 ---------------------
163 We will avoid using `Id` (Leibniz equality),
164 thus we will explicitly equip a set with an equivalence relation when needed.
165 We will call this structure a _setoid_. Note that we will
166 attach the infix `=` symbol only to the equality of a setoid,
171 The standard library and the `include` command
172 ----------------------------------------------
174 Some basic notions, like subset, membership, intersection and union
175 are part of the standard library of Matita.
177 These notions come with some standard notation attached to them:
179 - A ∪ B can be typed with `A \cup B`
180 - A ∩ B can be typed with `A \cap B`
181 - A ≬ B can be typed with `A \between B`
182 - x ∈ A can be typed with `x \in A`
183 - Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A`
185 The `include` command tells Matita to load a part of the library,
186 in particular the part that we will use can be loaded as follows:
190 include "sets/sets.ma".
194 Some basic results that we will use are also part of the sets library:
196 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
197 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
202 A set of axioms is made of a set(oid) `S`, a family of sets `I` and a
203 family `C` of subsets of `S` indexed by elements `a` of `S`
204 and elements of `I(a)`.
206 It is desirable to state theorems like "for every set of axioms, …"
207 without explicitly mentioning S, I and C. To do that, the three
208 components have to be grouped into a record (essentially a dependently
209 typed tuple). The system is able to generate the projections
210 of the record automatically, and they are named as the fields of
211 the record. So, given an axiom set `A` we can obtain the set
212 with `S A`, the family of sets with `I A` and the family of subsets
217 nrecord Ax : Type[1] ≝ {
225 Forget for a moment the `:>` that will be detailed later, and focus on
226 the record definition. It is made of a list of pairs: a name, followed
227 by `:` and the its type. It is a dependently typed tuple, thus
228 already defined names (fields) can be used in the types that follow.
230 Note that `S` is declared to be a `setoid` and not a Type. The original
231 paper probably also considers I to generate setoids, and both I and C
232 to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use
233 setoids only when strictly needed (i.e. where we want to talk about
234 equality). Setoids will play a role only when we will define
235 the alternative version of the axiom set.
237 Note that the field `S` was declared with `:>` instead of a simple `:`.
238 This declares the `S` projection to be a coercion. A coercion is
239 a "cast" function the system automatically inserts when it is needed.
240 In that case, the projection `S` has type `Ax → setoid`, and whenever
241 the expected type of a term is `setoid` while its type is `Ax`, the
242 system inserts the coercion around it, to make the whole term well typed.
244 When formalizing an algebraic structure, declaring the carrier as a
245 coercion is a common practice, since it allows to write statements like
247 ∀G:Group.∀x:G.x * x^-1 = 1
249 The quantification over `x` of type `G` is ill-typed, since `G` is a term
250 (of type `Group`) and thus not a type. Since the carrier projection
251 `carr` is a coercion, that maps a `Group` into the type of
252 its elements, the system automatically inserts `carr` around `G`,
253 obtaining `…∀x: carr G.…`.
255 Coercions are hidden by the system when it displays a term.
256 In this particular case, the coercion `S` allows to write (and read):
260 Since `A` is not a type, but it can be turned into a `setoid` by `S`
261 and a `setoid` can be turned into a type by its `carr` projection, the
262 composed coercion `carr ∘ S` is silently inserted.
267 Something that is not still satisfactory, is that the dependent type
268 of `I` and `C` are abstracted over the Axiom set. To obtain the
269 precise type of a term, you can use the `ncheck` command as follows.
273 (** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *)
274 (** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *)
278 One would like to write `I a` and not `I A a` under a context where
279 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
280 mechanism simply `A`). In Matita, a question mark represents an implicit
281 argument, i.e. a missing piece of information the system is asked to
282 infer. Matita performs Hindley-Milner-style type inference, thus writing
283 `I ? a` is enough: since the second argument of `I` is typed by the
284 first one, the first (omitted) argument can be inferred just
285 computing the type of `a` (that is `A`).
289 (** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *)
293 This is still not completely satisfactory, since you have always to type
294 `?`; to fix this minor issue we have to introduce the notational
295 support built in Matita.
300 Matita is quipped with a quite complex notational support,
301 allowing the user to define and use mathematical notations
302 ([From Notation to Semantics: There and Back Again][1]).
304 Since notations are usually ambiguous (e.g. the frequent overloading of
305 symbols) Matita distinguishes between the term level, the
306 content level, and the presentation level, allowing multiple
307 mappings between the content and the term level.
309 The mapping between the presentation level (i.e. what is typed on the
310 keyboard and what is displayed in the sequent window) and the content
311 level is defined with the `notation` command. When followed by
312 `>`, it defines an input (only) notation.
316 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
317 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
321 The first notation defines the writing `𝐈 a` where `a` is a generic
322 term of precedence 90, the maximum one. This high precedence forces
323 parentheses around any term of a lower precedence. For example `𝐈 x`
324 would be accepted, since identifiers have precedence 90, but
325 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
326 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
328 To obtain the `𝐈` is enough to type `I` and then cycle between its
329 similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
330 regular letters or the round parentheses, thus their variants (like the
331 bold ones) have to be used.
333 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
334 new content element to which a term `$a` is passed.
336 Content elements have to be interpreted, and possibly multiple,
337 incompatible, interpretations can be defined.
341 interpretation "I" 'I a = (I ? a).
342 interpretation "C" 'C a i = (C ? a i).
346 The `interpretation` command allows to define the mapping between
347 the content level and the terms level. Here we associate the `I` and
348 `C` projections of the Axiom set record, where the Axiom set is an implicit
349 argument `?` to be inferred by the system.
351 Interpretation are bi-directional, thus when displaying a term like
352 `C _ a i`, the system looks for a presentation for the content element
357 notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
358 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
362 For output purposes we can define more complex notations, for example
363 we can put bold parentheses around the arguments of `𝐈` and `𝐂`, decreasing
364 the size of the arguments and lowering their baseline (i.e. putting them
365 as subscript), separating them with a comma followed by a little space.
367 The first (technical) definition
368 --------------------------------
370 Before defining the cover relation as an inductive predicate, one
371 has to notice that the infinity rule uses, in its hypotheses, the
372 cover relation between two subsets, while the inductive predicate
373 we are going to define relates an element and a subset.
375 An option would be to unfold the definition of cover between subsets,
376 but we prefer to define the abstract notion of cover between subsets
377 (so that we can attach a (ambiguous) notation to it).
379 Anyway, to ease the understanding of the definition of the cover relation
380 between subsets, we first define the inductive predicate unfolding the
381 definition, and we later refine it with.
385 ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
386 | xcreflexivity : ∀a:A. a ∈ U → xcover A U a
387 | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.
391 We defined the xcover (x will be removed in the final version of the
392 definition) as an inductive predicate. The arity of the inductive
393 predicate has to be carefully analyzed:
395 > (A : Ax) (U : Ω^A) : A → CProp[0]
397 The syntax separates with `:` abstractions that are fixed for every
398 constructor (introduction rule) and abstractions that can change. In that
399 case the parameter `U` is abstracted once and for all in front of every
400 constructor, and every occurrence of the inductive predicate is applied to
401 `U` in a consistent way. Arguments abstracted on the right of `:` are not
402 constant, for example the xcinfinity constructor introduces `a ◃ U`,
403 but under the assumption that (for every y) `y ◃ U`. In that rule, the left
404 had side of the predicate changes, thus it has to be abstracted (in the arity
405 of the inductive predicate) on the right of `:`.
409 (** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
413 We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
414 a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.
416 This notion has to be abstracted over the cover relation (whose
417 type is the arity of the inductive `xcover` predicate just defined).
419 Then it has to be abstracted over the arguments of that cover relation,
420 i.e. the axiom set and the set `U`, and the subset (in that case `𝐂 a i`)
421 sitting on the left hand side of `◃`.
425 ndefinition cover_set :
426 ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
428 λcover. λA, C,U. ∀y.y ∈ C → cover A U y.
432 The `ndefinition` command takes a name, a type and body (of that type).
433 The type can be omitted, and in that case it is inferred by the system.
434 If the type is given, the system uses it to infer implicit arguments
435 of the body. In that case all types are left implicit in the body.
437 We now define the notation `a ◃ b`. Here the keywork `hvbox`
438 and `break` tell the system how to wrap text when it does not
439 fit the screen (they can be safely ignored for the scope of
440 this tutorial). We also add an interpretation for that notation,
441 where the (abstracted) cover relation is implicit. The system
442 will not be able to infer it from the other arguments `C` and `U`
443 and will thus prompt the user for it. This is also why we named this
444 interpretation `covers set temp`: we will later define another
445 interpretation in which the cover relation is the one we are going to
450 notation "hvbox(a break ◃ b)" non associative with precedence 45
451 for @{ 'covers $a $b }.
453 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
460 We can now define the cover relation using the `◃` notation for
461 the premise of infinity.
465 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
466 | creflexivity : ∀a. a ∈ U → cover A U a
467 | cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
468 (** screenshot "cover". *)
474 Note that the system accepts the definition
475 but prompts the user for the relation the `cover_set` notion is
480 The horizontal line separates the hypotheses from the conclusion.
481 The `napply cover` command tells the system that the relation
482 it is looking for is exactly our first context entry (i.e. the inductive
483 predicate we are defining, up to α-conversion); while the `nqed` command
484 ends a definition or proof.
486 We can now define the interpretation for the cover relation between an
487 element and a subset first, then between two subsets (but this time
488 we fix the relation `cover_set` is abstracted on).
492 interpretation "covers" 'covers a U = (cover ? U a).
493 interpretation "covers set" 'covers a U = (cover_set cover ? a U).
497 We will proceed similarly for the fish relation, but before going
498 on it is better to give a short introduction to the proof mode of Matita.
499 We define again the `cover_set` term, but this time we build
500 its body interactively. In the λ-calculus Matita is based on, CIC, proofs
501 and terms share the same syntax, and it is thus possible to use the
502 commands devoted to build proof term also to build regular definitions.
503 A tentative semantics for the proof mode commands (called tactics)
504 in terms of sequent calculus rules are given in the
505 <a href="#appendix">appendix</a>.
509 ndefinition xcover_set :
510 ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
511 (** screenshot "xcover-set-1". *)
512 #cover; #A; #C; #U; (** screenshot "xcover-set-2". *)
513 napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
514 napply cover; (** screenshot "xcover-set-4". *)
522 The system asks for a proof of the full statement, in an empty context.
524 The `#` command is the ∀-introduction rule, it gives a name to an
525 assumption putting it in the context, and generates a λ-abstraction
529 We have now to provide a proposition, and we exhibit it. We left
530 a part of it implicit; since the system cannot infer it it will
532 Note that the type of `∀y:A.y ∈ C → ?` is a proposition
533 whenever `?` is a proposition.
536 The proposition we want to provide is an application of the
537 cover relation we have abstracted in the context. The command
538 `napply`, if the given term has not the expected type (in that
539 case it is a product versus a proposition) it applies it to as many
540 implicit arguments as necessary (in that case `? ? ?`).
543 The system will now ask in turn the three implicit arguments
544 passed to cover. The syntax `##[` allows to start a branching
545 to tackle every sub proof individually, otherwise every command
546 is applied to every subproof. The command `##|` switches to the next
547 subproof and `##]` ends the branching.
555 The definition of fish works exactly the same way as for cover, except
556 that it is defined as a coinductive proposition.
559 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
564 notation "hvbox(a break ⋉ b)" non associative with precedence 45
565 for @{ 'fish $a $b }.
567 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
569 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
570 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂 a i ⋉ F) → fish A F a.
574 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
575 interpretation "fish" 'fish a U = (fish ? U a).
579 Introduction rule for fish
580 ---------------------------
582 Matita is able to generate elimination rules for inductive types,
583 but not introduction rules for the coinductive case.
587 (** ncheck cover_rect_CProp0. *)
591 We thus have to define the introduction rule for fish by co-recursion.
592 Here we again use the proof mode of Matita to exhibit the body of the
593 corecursive function.
597 nlet corec fish_rec (A:Ax) (U: Ω^A)
599 (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
600 (** screenshot "def-fish-rec-1". *)
601 #a; #a_in_P; napply cfish; (** screenshot "def-fish-rec-2". *)
602 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
603 napply H1; (** screenshot "def-fish-rec-3". *)
605 ##| #i; ncases (H2 a a_in_P i); (** screenshot "def-fish-rec-5". *)
606 #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
607 @; (** screenshot "def-fish-rec-6". *)
609 ##| @; (** screenshot "def-fish-rec-7". *)
611 ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
620 Note the first item of the context, it is the corecursive function we are
621 defining. This item allows to perform the recursive call, but we will be
622 allowed to do such call only after having generated a constructor of
623 the fish coinductive type.
625 We introduce `a` and `p`, and then return the fish constructor `cfish`.
626 Since the constructor accepts two arguments, the system asks for them.
629 The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
630 With the `nchange` tactic we change `H1` into an equivalent form (this step
631 can be skipped, since the system would be able to unfold the definition
632 of inclusion by itself)
635 It is now clear that `H1` can be applied. Again `napply` adds two
636 implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
637 that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
638 `a`, and it asks a proof that `a ∈ P`.
641 The `nassumption` tactic looks for the required proof in the context, and in
642 that cases finds it in the last context position.
644 We move now to the second branch of the proof, corresponding to the second
645 argument of the `cfish` constructor.
647 We introduce `i` and then we destruct `H2 a p i`, that being a proof
648 of an overlap predicate, give as an element and a proof that it is
649 both in `𝐂 a i` and `P`.
652 We then introduce `x`, break the conjunction (the `*;` command is the
653 equivalent of `ncases` but operates on the first hypothesis that can
654 be introduced). We then introduce the two sides of the conjunction.
657 The goal is now the existence of a point in `𝐂 a i` fished by `U`.
658 We thus need to use the introduction rule for the existential quantifier.
659 In CIC it is a defined notion, that is an inductive type with just
660 one constructor (one introduction rule) holding the witness and the proof
661 that the witness satisfies a proposition.
665 Instead of trying to remember the name of the constructor, that should
666 be used as the argument of `napply`, we can ask the system to find by
667 itself the constructor name and apply it with the `@` tactic.
668 Note that some inductive predicates, like the disjunction, have multiple
669 introduction rules, and thus `@` can be followed by a number identifying
673 After choosing `x` as the witness, we have to prove a conjunction,
674 and we again apply the introduction rule for the inductively defined
678 The left hand side of the conjunction is trivial to prove, since it
679 is already in the context. The right hand side needs to perform
680 the co-recursive call.
683 The co-recursive call needs some arguments, but all of them are
684 in the context. Instead of explicitly mention them, we use the
685 `nassumption` tactic, that simply tries to apply every context item.
691 Subset of covered/fished points
692 -------------------------------
694 We now have to define the subset of `S` of points covered by `U`.
695 We also define a prefix notation for it. Remember that the precedence
696 of the prefix form of a symbol has to be higher than the precedence
701 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
703 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
705 interpretation "coverage cover" 'coverage U = (coverage ? U).
709 Here we define the equation characterizing the cover relation.
710 Even if it is not part of the paper, we proved that `◃(U)` is
711 the minimum solution for
712 such equation, the interested reader should be able to reply the proof
717 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X.
718 ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
720 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
723 ##[ #bU; @1; nassumption;
724 ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
726 ##| #_; napply CaiU; nassumption; ##] ##]
727 ##| ncases H; ##[ #E; @; nassumption]
728 *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
732 ntheorem coverage_min_cover_equation :
733 ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
734 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
735 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
736 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
742 We similarly define the subset of points "fished" by `F`, the
743 equation characterizing `⋉(F)` and prove that fish is
744 the biggest solution for such equation.
748 notation "⋉F" non associative with precedence 55
751 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
753 interpretation "fished fish" 'fished F = (fished ? F).
755 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
756 ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
758 ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
759 #A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
760 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
762 ##| #aF; #H1; @ aF; napply H1;
766 ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
767 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
768 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
773 Part 2, the new set of axioms
774 -----------------------------
776 Since the name of defined objects (record included) has to be unique
777 within the same file, we prefix every field name
778 in the new definition of the axiom set with `n`.
782 nrecord nAx : Type[1] ≝ {
785 nD: ∀a:nS. nI a → Type[0];
786 nd: ∀a:nS. ∀i:nI a. nD a i → nS
791 We again define a notation for the projections, making the
792 projected record an implicit argument. Note that, since we already have
793 a notation for `𝐈`, we just add another interpretation for it. The
794 system, looking at the argument of `𝐈`, will be able to choose
795 the correct interpretation.
799 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
800 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
802 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
803 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
805 interpretation "D" 'D a i = (nD ? a i).
806 interpretation "d" 'd a i j = (nd ? a i j).
807 interpretation "new I" 'I a = (nI ? a).
811 The first result the paper presents to motivate the new formulation
812 of the axiom set is the possibility to define and old axiom set
813 starting from a new one and vice versa. The key definition for
814 such construction is the image of d(a,i).
815 The paper defines the image as
817 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
819 but this not so formal notation poses some problems. The image is
820 often used as the left hand side of the ⊆ predicate
824 Of course this writing is interpreted by the authors as follows
826 > ∀j:D(a,i). d(a,i,j) ∈ V
828 If we need to use the image to define `𝐂 ` (a subset of `S`) we are obliged to
829 form a subset, i.e. to place a single variable `{ here | … }` of type `S`.
831 > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
833 This poses no theoretical problems, since `S` is a setoid and thus equipped
836 Unless we define two different images, one for stating that the image is ⊆ of
837 something and another one to define `𝐂`, we end up using always the latter.
838 Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
840 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
842 That, up to rewriting with the equation defining `x`, is what we mean.
843 The technical problem arises later, when `V` will be a complex
844 construction that has to be proved extensional
845 (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
849 include "logic/equality.ma".
851 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
853 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
854 notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
856 interpretation "image" 'Im a i = (image ? a i).
860 Thanks to our definition of image, we can define a function mapping a
861 new axiom set to an old one and vice versa. Note that in the second
862 definition, when we give the `𝐝` component, the projection of the
863 Σ-type is inlined (constructed on the fly by `*;`)
864 while in the paper it was named `fst`.
868 ndefinition Ax_of_nAx : nAx → Ax.
869 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
872 ndefinition nAx_of_Ax : Ax → nAx.
874 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
875 ##| #a; #i; *; #x; #_; napply x;
879 nlemma Ax_nAx_equiv :
880 ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
881 C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
882 #A; #a; #i; @; #b; #H;
883 ##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
884 nwhd in H; ncases H; #x; #E; nrewrite > E;
885 ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
886 ##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
887 ##[ @ b; nassumption;
888 ##| nnormalize; @; ##]
894 We then define the inductive type of ordinals, parametrized over an axiom
895 set. We also attach some notations to the constructors.
899 ninductive Ord (A : nAx) : Type[0] ≝
902 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
904 notation "0" non associative with precedence 90 for @{ 'oO }.
905 notation "x+1" non associative with precedence 50 for @{'oS $x }.
906 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
908 interpretation "ordinals Zero" 'oO = (oO ?).
909 interpretation "ordinals Succ" 'oS x = (oS ? x).
910 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
914 The definition of `U⎽x` is by recursion over the ordinal `x`.
915 We thus define a recursive function using the `nlet rec` command.
916 The `on x` directive tells
917 the system on which argument the function is (structurally) recursive.
919 In the `oS` case we use a local definition to name the recursive call
920 since it is used twice.
922 Note that Matita does not support notation in the left hand side
923 of a pattern match, and thus the names of the constructors have to
924 be spelled out verbatim.
928 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
931 | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
932 | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
934 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
935 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
937 interpretation "famU" 'famU U x = (famU ? U x).
941 We attach as the input notation for U_x the similar `U⎽x` where underscore,
942 that is a character valid for identifier names, has been replaced by `⎽` that is
943 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
944 for `_` (i.e. pressing ALT-L after `_`).
946 The notion ◃(U) has to be defined as the subset of elements `y`
947 belonging to `U⎽x` for some `x`. Moreover, we have to define the notion
948 of cover between sets again, since the one defined at the beginning
949 of the tutorial works only for the old axiom set.
953 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝
954 λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
956 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
957 ∀y.y ∈ C → y ∈ c A U.
959 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
960 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
961 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
965 Before proving that this cover relation validates the reflexivity and infinity
966 rules, we prove this little technical lemma that is used in the proof for the
971 nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
972 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
977 The proof of infinity uses the following form of the Axiom of Choice,
978 that cannot be proved inside Matita, since the existential quantifier
979 lives in the sort of predicative propositions while the sigma in the conclusion
980 lives in the sort of data types, and thus the former cannot be eliminated
981 to provide the witness for the second.
985 nlemma AC_fake : ∀A,a,i,U.
986 (∀j:𝐃 a i.Σx:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
987 #A; #a; #i; #U; #H; @;
988 ##[ #j; ncases (H j); #x; #_; napply x;
989 ##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
992 naxiom AC : ∀A,a,i,U.
993 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
997 In the proof of infinity, we have to rewrite under the ∈ predicate.
998 It is clearly possible to show that `U⎽x` is an extensional set:
1000 > a = b → a ∈ U⎽x → b ∈ U⎽x
1002 Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be
1003 declared as morphisms. This poses no problem, but goes out of the scope of the
1004 tutorial, since dependent morphisms are hard to manipulate, and we thus assume it.
1008 naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
1012 The reflexivity proof is trivial, it is enough to provide the ordinal `0`
1013 as a witness, then `◃(U)` reduces to `U` by definition,
1014 hence the conclusion. Note that `0` is between `(` and `)` to
1015 make it clear that it is a term (an ordinal) and not the number
1016 of the constructor we want to apply (that is the first and only one
1017 of the existential inductive type).
1020 ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
1021 #A; #U; #a; #H; @ (0); napply H;
1026 We now proceed with the proof of the infinity rule.
1031 alias symbol "exists" (instance 1) = "exists".
1032 alias symbol "covers" = "new covers set".
1033 alias symbol "covers" = "new covers".
1034 alias symbol "covers" = "new covers set".
1035 alias symbol "covers" = "new covers".
1036 alias symbol "covers" = "new covers set".
1037 ntheorem new_coverage_infinity:
1038 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
1039 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
1040 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
1041 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
1042 #z; napply H; @ z; @; ##] #H'; (** screenshot "n-cov-inf-4". *)
1043 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
1044 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
1045 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
1046 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
1047 @2; (** screenshot "n-cov-inf-8". *)
1048 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
1049 nrewrite > Hd; napply Hf';
1054 We eliminate the existential, obtaining an `i` and a proof that the
1055 image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal
1056 form of `H`, thus expands the definition of cover between sets.
1059 When the paper proof considers `H`, it implicitly substitutes assumed
1060 equation defining `y` in its conclusion.
1061 In Matita this step is not completely trivial.
1062 We thus assert (`ncut`) the nicer form of `H` and prove it.
1065 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
1066 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
1067 becomes trivial if `j` is chosen to be `z`.
1070 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
1071 its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before
1072 assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated
1073 is `AC ???? H'` where the system is able to infer every `?`. Matita provides
1074 a facility to specify a number of `?` in a compact way, i.e. `…`. The system
1075 expand `…` first to zero, then one, then two, three and finally four question
1076 marks, "guessing" how may of them are needed.
1079 The paper proof does now a forward reasoning step, deriving (by the ord_subset
1080 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
1083 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
1086 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
1087 that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`.
1088 Applying the second constructor `@2;` of the disjunction,
1089 we are left to prove that `a` belongs to the right hand side of the union.
1092 We thus provide `i` as the witness of the existential, introduce the
1093 element being in the image and we are
1094 left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging
1095 to the image means that there exists an object in the domain …, we eliminate the
1096 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
1099 We just need to use the equational definition of `x` to obtain a conclusion
1100 that can be proved with `Hf'`. We assumed that `U⎽x` is extensional for
1101 every `x`, thus we are allowed to use `Hd` and close the proof.
1107 The next proof is that ◃(U) is minimal. The hardest part of the proof
1108 is to prepare the goal for the induction. The desiderata is to prove
1109 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
1110 unfolding all definitions:
1112 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
1116 nlemma new_coverage_min :
1117 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
1118 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
1119 *; #o; (** screenshot "n-cov-min-3". *)
1120 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
1121 nelim o; (** screenshot "n-cov-min-5". *)
1123 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
1124 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
1125 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
1130 After all the introductions, event the element hidden in the ⊆ definition,
1131 we have to eliminate the existential quantifier, obtaining the ordinal `o`
1134 What is left is almost right, but the element `b` is already in the
1135 context. We thus generalize every occurrence of `b` in
1136 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
1139 We then proceed by induction on `o` obtaining the following goals
1142 All of them can be proved using simple set theoretic arguments,
1143 the induction hypothesis and the assumption `Im`.
1150 The notion `F⎽x` is again defined by recursion over the ordinal `x`.
1154 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
1157 | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
1158 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
1161 interpretation "famF" 'famU U x = (famF ? U x).
1163 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
1165 interpretation "fished new fish" 'fished U = (ord_fished ? U).
1166 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
1170 The proof of compatibility uses this little result, that we
1171 proved outside the main proof.
1174 nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
1175 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
1180 We assume the dual of the axiom of choice, as in the paper proof.
1183 naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
1184 (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x))
1185 → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
1189 Proving the anti-reflexivity property is simple, since the
1190 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
1191 `a ∈ F⎽x`. If `x` is choose to be `0`, we obtain the thesis.
1194 ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
1195 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
1200 We now prove the compatibility property for the new fish relation.
1203 ntheorem new_fish_compatible:
1204 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
1205 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
1206 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
1207 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
1209 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
1210 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
1211 *; #j; #Hj; @j; (** screenshot "n-f-compat-6". *)
1212 napply (co_ord_subset … Hj);
1217 After reducing to normal form the goal, we observe it is exactly the conclusion of
1218 the dual axiom of choice we just assumed. We thus apply it ad introduce the
1222 The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`.
1225 Since F_(Λf+1) is defined by recursion and we actually have a concrete input
1226 `Λf+1` for that recursive function, it can be computed.
1227 Anyway, using the `nnormalize`
1228 tactic would reduce too much (both the `+1` and the `Λf` steps would be performed);
1229 we thus explicitly give a convertible type for that hypothesis, corresponding
1230 the computation of the `+1` step, plus the unfolding the definition of
1234 We are interested in the right hand side of `aLf`, an in particular to
1235 its intance where the generic index in `𝐈 a` is `i`.
1238 We then eliminate the existential, obtaining `j` and its property `Hj`. We provide
1242 What is left to prove is exactly the `co_ord_subset` lemma we factored out
1249 The proof that `⋉(F)` is maximal is exactly the dual one of the
1250 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
1251 before doing the induction over `o`.
1253 Note that `G` is assumed to be of type `𝛀^A`, that means an extensional
1254 subset of `S`, while `Ω^A` means just a subset (note that the former is bold).
1257 ntheorem max_new_fished:
1258 ∀A:nAx.∀G:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
1259 #A; #G; #F; #GF; #H; #b; #HbG; #o;
1260 ngeneralize in match HbG; ngeneralize in match b;
1261 nchange with (G ⊆ F⎽o);
1264 ##| #p; #IH; napply (subseteq_intersection_r … IH);
1265 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
1266 @d; napply IH; (** screenshot "n-f-max-1". *)
1267 nrewrite < Ed; napply cG;
1268 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
1269 #b; #Hb; #d; napply (Hf d); napply Hb;
1275 Here the situation looks really similar to the one of the dual proof where
1276 we had to apply the assumption `U_x_is_ext`, but here the set is just `G`
1277 not `F_x`. Since we assumed `G` to be extensional we can
1278 exploit the facilities
1279 Matita provides to perform rewriting in the general setting of setoids.
1281 The `.` notation simply triggers the mechanism, while the given argument has to
1282 mimic the context under which the rewriting has to happen. In that case
1283 we want to rewrite the left hand side of the binary morphism `∈`.
1285 to represent the context of a binary morphism is `‡`. The right hand side
1286 has to be left untouched, and the identity rewriting step is represented with
1287 `#` (actually a reflexivity proof for the subterm identified by the context).
1289 We want to rewrite the left hand side using `Ed` right-to-left (the default
1290 is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`.
1292 The complete command is `napply (. Ed^-1‡#)` that has to be read like:
1294 > perform some rewritings under a binary morphism,
1295 > on the right do nothing,
1296 > on the left rewrite with Ed right-to-left.
1298 After the rewriting step the goal is exactly the `cG` assumption.
1304 <div id="appendix" class="anchor"></div>
1305 Appendix: tactics explanation
1306 -----------------------------
1308 In this appendix we try to give a description of tactics
1309 in terms of sequent calculus rules annotated with proofs.
1310 The `:` separator has to be read as _is a proof of_, in the spirit
1311 of the Curry-Howard isomorphism.
1313 Γ ⊢ f : A_1 → … → A_n → B Γ ⊢ ?_i : A_i
1314 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1315 Γ ⊢ (f ?_1 … ?_n ) : B
1317 Γ ⊢ ? : F → B Γ ⊢ f : F
1318 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1323 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1324 Γ ⊢ λx:T.? : ∀x:T.P(x)
1327 Γ ⊢ ?_i : args_i → P(k_i args_i)
1328 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1329 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
1332 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
1333 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1334 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
1336 Where `T_rect_CProp0` is the induction principle for the
1341 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1344 Where the equivalence relation between types `≡` keeps into account
1345 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
1346 definition unfolding), ι-reduction (pattern matching simplification),
1347 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
1351 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
1352 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1356 Γ; H : Q; Δ ⊢ ? : G P →* Q
1357 nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1360 Where `Q` is the normal form of `P` considering βδζιμν-reduction steps.
1364 nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1368 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
1369 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1374 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
1383 Last updated: $Date$
1386 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf
1387 [2]: http://matita.cs.unibo.it
1388 [3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
1389 [4]: http://www.inria.fr/rrrt/rr-0530.html