Matita Tutorial: inductively generated formal topologies
========================================================
-This is a not so short introduction to Matita, based on
+This is a not so short introduction to [Matita][2], based on
the formalization of the paper
> Between formal topology and game theory: an
> explicit solution for the conditions for an
> inductive generation of formal topologies
-by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
+by Stefano Berardi and Silvio Valentini.
+The tutorial is by Enrico Tassi.
The tutorial spends a considerable amount of effort in defining
notations that resemble the ones used in the original paper. We believe
-this a important part of every formalization, not only for the aesthetic
+this is a important part of every formalization, not only from the aesthetic
point of view, but also from the practical point of view. Being
consistent allows to follow the paper in a pedantic way, and hopefully
to make the formalization (at least the definitions and proved
window on the top right is where the system shows you the ongoing proof;
the error window, on the bottom right, is where the system complains.
On the top of the script window five buttons drive the processing of
-the proof script. From left to right the requesting the system to:
+the proof script. From left to right they request the system to:
- go back to the beginning of the script
- go back one step
When the system processes a command, it locks the part of the script
corresponding to the command, such that you cannot edit it anymore
-(without to go back). Locked parts are coloured in blue.
+(without going back). Locked parts are coloured in blue.
The sequent window is hyper textual, i.e. you can click on symbols
-to jump to their definition, or switch between different notation
+to jump to their definition, or switch between different notations
for the same expression (for example, equality has two notations,
one of them makes the type of the arguments explicit).
Everywhere in the script you can use the `ncheck (term).` command to
-ask for the type a given term. If you that in the middle of a proof,
+ask for the type a given term. If you do that in the middle of a proof,
the term is assumed to live in the current proof context (i.e. can use
variables introduced so far).
to mean double or single arrows.
Here we recall some of these "shortcuts":
- - ∀ can be typed with `\Forall`
+ - ∀ can be typed with `\forall`
- λ can be typed with `\lambda`
- ≝ can be typed with `\def` or `:=`
- - → can be typed with `to` or `->`
+ - → can be typed with `\to` or `->`
- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
The user can cycle between variants typing one of them and then
example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
Variants are listed in the aforementioned TeX/UTF-8 table.
-CIC (as implemented in Matita) in a nutshell
---------------------------------------------
-
-...
+Pressing `F1` opens the Matita manual.
+
+CIC (as [implemented in Matita][3]) in a nutshell
+-------------------------------------------------
+
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. It features both dependent types and
+polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
+the same syntax, and they can occurr in types.
+
+The environment used for in the typing judgement can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive calls are allowed only on structurally smaller subterms).
+Co-recursive
+functions can be defined as well, and must satisfy the dual condition, i.e.
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment. This construct, together with the possibility to
+definable total recursive functions, allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly typed
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
-Type is a set equipped with the Id equality (i.e. an intensional,
-not quotiented set). We will avoid using Leibnitz equality Id,
-thus we will explicitly equip a set with an equality when needed.
-We will call this structure `setoid`. Note that we will
-attach the infix = symbols only to the equality of a setoid,
+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology.
+Type is the sort of sets equipped with the `Id `equality (i.e. an intensional,
+not quotiented set). We will avoid using `Id` (Leibnitz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
not to Id.
-...
+We write `Type[i]` to mention a Type in the predicative hierarchy
+of types. To ease the comprehension we will use `Type[0]` for sets,
+and `Type[1]` for classes. The index `i` is just a lable: constraints among
+universes are declared by the user. The standard library defines
-We write Type[i] to mention a Type in the predicative hierarchy
-of types. To ease the comprehension we will use Type[0] for sets,
-and Type[1] for classes.
+> Type[0] < Type[1] < Type[2]
-For every Type[i] there is a corresponding level of predicative
-propositions CProp[i].
+For every `Type[i]` there is a corresponding level of predicative
+propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+with 0 or 1 constructors with propositional arguments, like `Id` and `And`
+but not like `Or`).
-CIC is also equipped with an impredicative sort Prop that we will not
-use in this tutorial.
The standard library and the `include` command
----------------------------------------------
These notions come with some standard notation attached to them:
-- A ∪ B `A \cup B`
-- A ∩ B `A \cap B`
-- A ≬ B `A \between B`
-- x ∈ A `x \in A`
-- Ω^A, that is the type of the subsets of A, `\Omega ^ A`
+- A ∪ B can be typed with `A \cup B`
+- A ∩ B can be typed with `A \cap B`
+- A ≬ B can be typed with `A \between B`
+- x ∈ A can be typed with `x \in A`
+- Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A`
The `include` command tells Matita to load a part of the library,
in particular the part that we will use can be loaded as follows:
Defining Axiom set
------------------
-A set of axioms is made of a set S, a family of sets I and a
-family C of subsets of S indexed by elements a of S and I(a).
+A set of axioms is made of a set(oid) `S`, a family of sets `I` and a
+family `C` of subsets of `S` indexed by elements `a` of `S`
+and elements of `I(a)`.
It is desirable to state theorems like "for every set of axioms, …"
without explicitly mentioning S, I and C. To do that, the three
components have to be grouped into a record (essentially a dependently
typed tuple). The system is able to generate the projections
-of the record for free, and they are named as the fields of
-the record. So, given a axiom set `A` we can obtain the set
+of the record automatically, and they are named as the fields of
+the record. So, given an axiom set `A` we can obtain the set
with `S A`, the family of sets with `I A` and the family of subsets
with `C A`.
Note that `S` is declared to be a `setoid` and not a Type. The original
paper probably also considers I to generate setoids, and both I and C
-to be morphisms. For the sake of simplicity, we will "cheat" and use
+to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use
setoids only when strictly needed (i.e. where we want to talk about
equality). Setoids will play a role only when we will define
the alternative version of the axiom set.
nlet corec fish_rec (A:Ax) (U: Ω^A)
(P: Ω^A) (H1: P ⊆ U)
(H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
- (** screenshot "def-fish-rec-1". *)
-#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
+ (** screenshot "def-fish-rec-1". *)
+#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
- napply H1; (** screenshot "def-fish-rec-3". *)
+ napply H1; (** screenshot "def-fish-rec-3". *)
nassumption;
-##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
+##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
#x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
- @; (** screenshot "def-fish-rec-6". *)
+ @; (** screenshot "def-fish-rec-6". *)
##[ napply x
- ##| @; (** screenshot "def-fish-rec-7". *)
+ ##| @; (** screenshot "def-fish-rec-7". *)
##[ napply xC;
- ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
+ ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
nassumption;
##]
##]
ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
#A; #U; #a; @; #H;
-##[ nelim H; #b; (* manca clear *)
+##[ nelim H; #b;
##[ #bU; @1; nassumption;
##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
##[ #E; @; napply E;
> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
-but this cannot be ..... MAIL
+but this not so formal notation poses some problems. The image is
+often used as the left hand side of the ⊆ predicate
> Im[d(a,i)] ⊆ V
-Allora ha una comoda interpretazione (che voi usate liberamente)
+Of course this writing is interpreted by the authors as follows
> ∀j:D(a,i). d(a,i,j) ∈ V
-Ma se voglio usare Im per definire C, che è un subset di S, devo per
-forza (almeno credo) definire un subset, ovvero dire che
+If we need to use the image to define 𝐂 (a subset of S) we are obliged to
+form a subset, i.e. to place a single variable `{ here | … }`.
+
+> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
-> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+This poses no theoretical problems, since `S` is a setoid and thus equipped
+with an equality.
-Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
-uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
-scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
+Unless we difene two different images, one for stating the image is ⊆ of
+something and another one to define 𝐂, we end up using always the latter.
+Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
> ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
+That up to rewriting with the equation defining `x` is what we mean. The
+technical problem arises when `V` is a complex construction that has to
+be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
D*)
(*D
-
+Thanks to our definition of image, we ca trivially a function mapping a
+new axiom set to an old one and viceversa. Note that in the second
+definition, when defining 𝐝, the projection of the Σ type is inlined
+(constructed on the fly by `*;`) while in the paper it was named `fst`.
D*)
(*D
+The dfinition of `U_x` is by recursion over the ordinal `x`.
+We thus define a recursive function. The `on x` directive tells
+the system on which argument the function is (structurally) recursive.
+
+In the `oS` case we use a local definition to name the recursive call
+since it is used twice.
+
Note that Matita does not support notation in the left hand side
of a pattern match, and thus the names of the constructors have to
be spelled out verbatim.
-BLA let rec. Bla let_in.
-
D*)
nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ U
- | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
+ | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
| oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
D*)
-nlemma ord_subset:
- ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
+nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
#A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
nqed.
(*D
In the proof of infinity, we have to rewrite under the ∈ predicate.
-It is clearly possible to show that U_x is an extensional set:
+It is clearly possible to show that U⎽x is an extensional set:
-> a=b → a ∈ U_x → b ∈ U_x
+> a = b → a ∈ U⎽x → b ∈ U⎽x
Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
declared as morphisms. This poses to problem, but goes out of the scope of the
D*)
-naxiom setoidification :
- ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
+naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
(*D
as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
D*)
-ntheorem new_coverage_reflexive:
- ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
#A; #U; #a; #H; @ (0); napply H;
nqed.
alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)
@ (Λ f+1); (** screenshot "n-cov-inf-7". *)
@2; (** screenshot "n-cov-inf-8". *)
@i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
-napply (setoidification … Hd); napply Hf';
+napply (U_x_is_ext … Hd); napply Hf';
nqed.
(*D
D[n-cov-inf-4]
Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
-its property.
+its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before
+assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated
+is `AC ???? H'` where the system is able to infer every `?`. Matita provides
+a facility to specify a number of `?` in a compact way, i.e. `…`. The system
+expand `…` first to zero, then one, then two, three and finally four question
+marks, "guessing" how may of them are needed.
D[n-cov-inf-5]
The paper proof does now a forward reasoning step, deriving (by the ord_subset
D[n-cov-inf-9]
We just need to use the equational definition of `x` to obtain a conclusion
-that can be proved with `Hf'`. We assumed that `U_x` is extensional for
+that can be proved with `Hf'`. We assumed that `U⎽x` is extensional for
every `x`, thus we are allowed to use `Hd` and close the proof.
D*)
(*D
The next proof is that ◃(U) is mininal. The hardest part of the proof
-it to prepare the goal for the induction. The desiderata is to prove
+is to prepare the goal for the induction. The desiderata is to prove
`U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
unfolding all definitions:
(*D
-bla bla
+The notion `F⎽x` is again defined by recursion over the ordinal `x`.
D*)
nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ F
- | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
+ | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
| oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
].
(*D
The proof of compatibility uses this little result, that we
-factored out.
+proved outside the mail proof.
D*)
-nlemma co_ord_subset:
- ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
+nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
#A; #F; #a; #i; #f; #j; #x; #H; napply H;
nqed.
We assume the dual of the axiom of choice, as in the paper proof.
D*)
-naxiom AC_dual :
- ∀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.
+naxiom AC_dual: ∀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.
(*D
-Proving the anti-reflexivity property is simce, since the
+Proving the anti-reflexivity property is simple, since the
assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
`a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
D*)
-ntheorem new_fish_antirefl:
- ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
#A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
nqed.
(*D
-bar
+We now prove the compatibility property for the new fish relation.
D*)
ntheorem new_fish_compatible:
nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
nchange in aLf with
(a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
-ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
- ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
- *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
-napply aLf';
+ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
+*; #j; #Hj; @j; (** screenshot "n-f-compat-6". *)
+napply (co_ord_subset … Hj);
nqed.
(*D
D[n-f-compat-1]
+After reducing to normal form the goal, we obseve it is exactly the conlusion of
+the dual axiom of choice we just assumed. We thus apply it ad introduce the
+fcuntion `f`.
+
D[n-f-compat-2]
+The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`.
+
D[n-f-compat-3]
+Since F_(Λf+1) is defined by recursion and we actually have a concrete input
+`Λf+1` for that recursive function, it can compute. Anyway, using the `nnormalize`
+tactic would reduce too much (both the `+1` and the `Λf` steps would be prformed);
+we thus explicitly give a convertible type for that hypothesis, corresponding
+the computation of the `+1` step, plus the unfolding of `∩`.
+
D[n-f-compat-4]
+We are interested in the right hand side of `aLf`, an in particular to
+its intance where the generic index in `𝐈 a` is `i`.
+
D[n-f-compat-5]
+We then eliminate the existential, obtaining `j` and its property `Hj`. We provide
+the same witness
+
D[n-f-compat-6]
+What is left to prove is exactly the `co_ord_subset` lemma we factored out
+of the main proof.
D*)
minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
before doing the induction over `o`.
+Note that `G` is assumed to be of type `𝛀^A`, that means an extensional
+subset of `S`, while `Ω^A` means just a subset (note that the former is bold).
+
D*)
ntheorem max_new_fished:
- ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+ ∀A:nAx.∀G:𝛀^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
#A; #G; #F; #GF; #H; #b; #HbG; #o;
ngeneralize in match HbG; ngeneralize in match b;
nchange with (G ⊆ F⎽o);
##[ napply GF;
##| #p; #IH; napply (subseteq_intersection_r … IH);
#x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
- @d; napply IH;
+ @d; napply IH; (** screenshot "n-f-max-1". *)
alias symbol "prop2" = "prop21".
-napply (. Ed^-1‡#); napply cG;
+ napply (. Ed^-1‡#); napply cG;
##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
#b; #Hb; #d; napply (Hf d); napply Hb;
##]
nqed.
+(*D
+D[n-f-max-1]
+Here the situacion look really similar to the one of the dual proof where
+we had to apply the assumption `U_x_is_ext`, but here the set is just `G`
+not `F_x`. Since we assumed `G` to be extensional we can employ the facilities
+Matita provides to perform rewriting in the general setting of setoids.
+
+The lemma `.` simply triggers the mechanism, and the given argument has to
+mimick the context under which the rewriting has to happen. In that case
+we want to rewrite to the left of the binary morphism `∈`. The infix notation
+to represent the context of a binary morphism is `‡`. The right hand side
+has to be left untouched, and the identity rewriting step is represented with
+`#` (actually a reflexivity proof for the subterm identified by the context).
+
+We want to rewrite the left hand side using `Ed` right-to-left (the default
+is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`.
+
+The complete command is `napply (. Ed^-1‡#)` that has to be read like:
+
+> perform some rewritings under a binary morphism,
+> on the right do nothing,
+> on the left rewrite with Ed right-to-left.
+
+After the rewriting step the goal is exactly the `cG` assumption.
+
+D*)
+
(*D
<div id="appendix" class="anchor"></div>
Where `T_rect_CProp0` is the induction principle for the
inductive type `T`.
+
Γ ⊢ ? : Q Q ≡ P
nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
Γ ⊢ ? : P
Γ; H : P; Δ ⊢ ? : G
+ Γ; H : Q; Δ ⊢ ? : G P →* Q
+ nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ; H : P; Δ ⊢ ? : G
+
+Where `Q` is the normal form of `P` considering βδζιμν-reduction steps.
+
+
+ Γ ⊢ ? : Q P →* Q
+ nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ ? : P
+
Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
(*D
+<date>
+Last updated: $Date$
+</date>
+
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
+[2]: http://matita.cs.unibo.it
+[3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
+[4]: http://www.inria.fr/rrrt/rr-0530.html
D*)
projects / helm.git / blobdiff