5 include "basics/logic.ma".
7 (* In the previous section, we introduced many interesting logical connectives
8 by means of inductive definitions in the sort Prop. Do the same constructions
9 make any sense in Type? The answer is yes! Not only they make sense, but they
10 are indeed very familiar constructions: cartesian product, disjoint sum, empty
11 and singleton types, and ``sigma types'' (disjoint union of families of types
12 indexed over a given base type). This is not a coincidence, but a consequence of
13 a strong principle known under the name of ``Propositions as Types analogy'' (or
14 Curry-Howard correspondence).
16 We shall first discuss the constructions, and then we shall come back on the
19 (***************************** Cartesian Product ******************************)
21 (* The cartesian product of two types A and B is defined as follows: *)
23 inductive Prod (A,B:Type[0]) : Type[0] ≝
24 pair : A → B → Prod A B.
26 (* Observe that the definition is identical to the definition of the logical
27 conjunction, but for the fact that the sort Prop has been replaced by Type[0].
29 The following declarations allows us to use the canonical notations A × B for
30 the product and 〈a,b〉 for the pair of the two elements a and b. *)
32 notation "hvbox(x break × y)" with precedence 70 for @{ 'product $x $y}.
33 interpretation "Cartesian product" 'product A B = (Prod A B).
35 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
36 with precedence 90 for @{ 'pair $a $b}.
37 interpretation "Pair construction" 'pair x y = (pair ?? x y).
39 (* We can define the two projections fst and snd by a simple case analysis of
42 definition fst ≝ λA,B.λp:A×B. match p with [pair a b ⇒ a].
43 definition snd ≝ λA,B.λp:A×B. match p with [pair a b ⇒ b].
45 (* As in the case of inductive propositions, Matita automatically generates
46 elimination principles for A × B. In this case, however, it becomes interesting
47 to consider the possibility that the proposition towards which we are
48 eliminating a given pair p:A × B$ contains a copy of p itself. In other words,
49 if we have p:A × B in the current context, it is possible that p also occurs in
50 the current goal, that is that the current goal "depends" on p.
52 A typical example is in the proof of the so called ``surjective pairing''
55 lemma surjective_pair: ∀A,B.∀p:A×B. p = 〈fst ?? p, snd ?? p〉.
57 (* where p explicitly occurs in the conclusion. The proof is straightforward: we
58 introduce A, B and p and proceed by cases on p: since p is a pair, the only
59 possible case is that it is of the form 〈a,b〉 for some a and b.*)
61 #A #B #p cases p #a #b
63 (* At this point the goal looks like
64 〈a,b〉 = 〈fst A B 〈a,b〉, snd A B 〈a,b〉〉
65 and the two sides of the equation are convertible. *)
68 (* When we call cases p we are actually applying the dependent elimination
69 principle Prod_ind for the product, so it becomes interesting to have a look at
70 it (we shall postpone the discussion of the way it is generated in a later
73 ∀A,B.∀P:A×B →Prop.(∀a:A,∀b:B. P 〈a,b〉) → ∀x:A×B.P x
75 The previous principle has a very natural backward reading: in order to prove
76 that the property (P x) holds for any x of type A×B it is enough to prove P〈a,b〉
77 for any a:A and b:B. *)
79 (******************************* Disjoint Sum *********************************)
81 (* By reflecting in Type the definition of the logical disjunction we obtain the
82 disjoint union (the sum) of two types: *)
84 inductive Sum (A,B:Type[0]) : Type[0] ≝
88 notation "hvbox(a break + b)"
89 left associative with precedence 55 for @{ 'plus $a $b }.
91 interpretation "Disjoint union" 'plus A B = (Sum A B).
93 (* The two constructors are the left and right injections. The dependent
94 elimination principle Sum_ind has the following shape:
97 (∀a:A.P (inl A B a)) → (∀b:B.P (inr A B b)) → ∀x:A×B.P x
99 that is, in order to prove the property (P x) for any x:A+B it is enough to
100 prove P (inl A B a) and P (inr A B b) for all a:A and b:B. *)
102 (************************* Empty Type and Unit Type ***************************)
104 (* The counterparts of False and True are, respectively, an empty type and a
107 inductive void : Type[0] ≝.
108 inductive unit : Type[0] ≝ it: unit.
110 (* The elimination principle void_ind for void is simply
112 ∀P:void→Prop.∀x:void.P x
114 stating that any property is true for an element of type void (since we have no
117 Similarly, the elimination principle for the unit type is:
119 ∀P:unit→Prop. P it → ∀x:unit.P x
121 Indeed, in order to prove that a property is true for any element of the unit
122 type, it is enough to prove it for the unique (canonical) inhabitant "it".
124 As an exercise, let us prove that all inhabitants of unit are equal to each
127 lemma eq_unit: ∀a,b:unit. a = b.
129 (* The idea is to proceed by cases on a and b: we have only one possibility,
130 namely a=it and b=it, hence we end up to prove it=it, that is trivial. Here is
133 #a cases a #b cases b // qed. (* also: * * // qed. *)
135 (* It is interesting to observe that we get exactly the same behavior by
136 directly applying unit_ind instead of proceeding by cases. In fact, this is an
137 alternative proof: *)
139 lemma eq_unit_again: ∀a,b:unit. a = b.
140 @unit_ind @unit_ind // qed.
142 (********************* Sigma Types and dependent matching *********************)
144 (* As a final example, let us consider ``type'' variants of the existential
145 quantifier; in this case we have two interesting possibilities: *)
147 inductive Sig (A:Type[0]) (Q:A → Prop) : Type[0] ≝
148 Sig_intro: ∀x:A. Q x → Sig A Q.
150 inductive DPair (A:Type[0]) (Q:A → Type[0]) : Type[0] ≝
151 DPair_intro: ∀x:A. Q x → DPair A Q.
153 (* We shall use the notation Σx:A.Q x for the sigma type, and the similar
154 notation ∑x:A.Q x for dependent pairs. *)
156 notation "hvbox(\Sigma ident i : ty break . p)"
157 left associative with precedence 20
158 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
160 notation "hvbox(\Sigma ident i break . p)"
161 with precedence 20 for @{'sigma (\lambda ${ident i}. $p) }.
163 interpretation "Sigma" 'sigma x = (Sig ? x).
165 notation "hvbox(∑ ident i : ty break . p)"
166 left associative with precedence 20
167 for @{'dpair (\lambda ${ident i} : $ty. $p) }.
169 notation "hvbox(∑ ident i break . p)"
170 with precedence 20 for @{'dpair (\lambda ${ident i}. $p) }.
172 interpretation "Sum" 'dpair x = (DPair ? x).
174 (* In the first case (traditionally called sigma type), an element of type
175 (Sig A P) is a pair (Sig_intro ?? a h) where a is an element of type A and h is a
176 proof that the property (P a) holds.
178 A suggestive reading of (Sig A P) is as the subset of A enjoying the property P,
179 that is {a:A | P(a)}.
181 In the second case, an element of DPair A B is a "dependent" pair
182 (DPair_intro ?? a h) where a is element of type A and h maps a into an element in
183 (B a); the intuition is to look at DProd A B as a (disjoint) family of sets B_a
184 indexed over elements a:A.
186 In both case it is possible to define projections extracting the two components
187 of the pair. Let us discuss the case of the sigma type (the other one is
190 Extracting the first component (the element) is easy: *)
192 definition Sig_fst ≝ λA:Type[0].λP:A→Prop.λx:Sig A P.
193 match x with [Sig_intro a h ⇒ a].
195 (* Getting the second component is a bit trickier. The first problem is
196 the type of the result: given a pair (Sig_intro ?? a h): Sig A P, the type of
197 h is (P a), that is P applied to the first argument of the pair of which we want
198 to extract the second component!
199 Luckily, in a language with dependent types, it is not a problem to write such a
202 definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ ...
204 A subtler problem is met when we define the body. If we just write
206 definition Sig_snd : ∀A,P.∀x.Sig A P → P (Sig_fst A P x) ≝ λA,P,x.
207 match x with [Sig_intro a h ⇒ h].
209 the system will complain about the type of h. The point is that the type of this
210 term depends on a, that is, in a not so trivial way, from the input argument x.
211 In this situations, the type inference algorithm of Matita requires a little
212 help: in particular the user is asked to explicitly provide the return type of
213 the match expression, that is a map uniformly expressing the type of all
214 branches of the case as a function of the matched expression.
215 In our case we only have one branch and the return type is
217 λx.P (Sig\_fst A P x)
219 We declare such a type immediately after the match, introduces by the keyword
222 definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
223 match x return λx.P (Sig_fst A P x) with [Sig_intro a h ⇒ h].
225 (* Similarly, we have: *)
227 definition DPair_fst ≝ λA:Type[0].λP:A→Type[0].λx:DPair A P.
228 match x with [DPair_intro a h ⇒ a].
230 definition DPair_snd : ∀A,P.∀x:DPair A P.P (DPair_fst A P x) ≝ λA,P,x.
231 match x return λx.P (DPair_fst A P x) with [DPair_intro a h ⇒ h].
233 (* Remark: The careful reader may have possibly remarked that we also did a
234 systematic abuse of the arrow symbol: the expression A → B was sometimes
235 interpreted as the "implication" between A and B and sometimes as the "function
236 space" between A and B. The reason of this fact is that, actually, in a
237 foundational system like the Calculus of Construction, they are the very same
238 notion: we only distinguish them according to the sort of the resulting
240 Similarly for the dependent product ∏x:A.B: if the resulting expression is of
241 sort Prop we shall look at it as a "universal quantification" (using the
242 notation ∀x:A.B), while if it is in Type we shall typically regard it as a
243 generalized cartesian product of a family of types B indexed over a base type A.
246 (************************ Kolmogorov interpretation ***************************)
248 (* The previous analogy between propositions and types is a consequence of a
249 deep philosophical interpretation of the notion of proof in terms of a
250 constructive procedure that transforms proofs of the premises into a proof of
251 the conclusion. This usually referred to as Kolmogorov interpretation, or
252 Brouwer–Heyting–Kolmogorov (BHK) interpretation.
254 The interpretation states what is intended to be a proof of a given formula φ,
255 and is specified by induction on the structure of A:
257 - a proof of P∧Q is a pair 〈a,b〉 where a is a proof of P and b is a proof of Q;
258 - a proof of P∨Q is a pair 〈a,b〉 where either a is 0 and b is a proof of P, or
259 a=1 and b is a proof of Q;
260 - a proof of P→Q is a function f which transforms a proof of x:P into a proof of
262 - a proof of ∃x:S.φ(x) is a pair 〈a,b〉 where a is an element of S, and b is a
264 - a proof of ∀x:S.ϕ(x) is a function f which transforms an element x of S into a
266 - the formula ¬P is defined as P → False, so a proof of it is a function f which
267 transforms a proof of P into a proof of False;
268 - there is no proof of False.
270 For instance, a proof of the formula P → P is a function transforming a proof of
271 P into a proof of P: but we can just take the identity!
273 You can explicitly exploit this idea for writing proofs in Matita. Instead of
274 declaring a lemma and proving it interactively, you may define your lemma as if
275 it was the type of an expression, and directly proceed to inhabit it with its
278 definition trivial: ∀P:Prop.P→P ≝ λP,h.h.
280 (* It is interesting to observe that this is really the very same proof
281 (intensionally!!) that would be produce interactively, as testified by the
282 following fragment of code: *)
284 lemma trivial1: ∀P:Prop.P→P. #P #h @h qed.
285 lemma same_proofs: trivial = trivial1. @refl qed.
287 (* Even more interestingly, we can do the opposite, namely define functions
289 Suppose for instance that we need to define a function with the following
290 type: ∀A,B,C:Type[0]. (A → B → C) → A× B → C.
291 If we just declare the type of the function followed by a fullstop, Matita will
292 start an interactive session completely analogous to a proof session, and we can
293 use the usual tactics to ``close the goal'', that is to inhabit the type. *)
295 definition uncurrying: ∀A,B,C:Type[0]. (A→B→C)→A×B→C.
296 #A #B #C #f * @f qed.
298 (********************** The Curry-Howard correspondence ***********************)
300 (* The philosophical ideas contained in the BHK interpretation of a proof as a
301 constructive procedure building a proof of the conclusion from proofs of the
302 hypothesis get a precise syntactical systematization via the so called
303 Curry-Howard correspondence, expressing a direct relationship between computer
305 The Curry-Howard correspondence, also known as proofs-as-programs analogy, is a
306 generalization of a syntactic analogy between systems of formal logic and
307 computational calculi first observed by Curry for Combinatory Logic and Hilbert-
308 style deduction systems, and later by Howard for λ-calculus and Natural
309 Deduction: in both cases the formation rules for well typed terms have precisely
310 the same shape of the logical rules of introduction of the correspondent
313 As a consequence, the expression
317 really has a double possible reading:
319 - M is a term of type A
320 - M is a proof of the proposition A
322 In both cases, M is a witness that the object A is "inhabited". A free variable
323 x:A is an assumption about the validity of A (we assumeto have an unknown proof
324 named x). Let us consider the cases of the introduction and elimination rule of
325 the implication in natural deduction, that are particularly interesting:
327 Γ,A ⊢ B Γ ⊢ A → B Γ ⊢ A
328 ---------- -------------------
331 The first step is to enrich the representation by decorating formulae with
332 explicit proof terms. In particular, formulae in the context, being assumptions,
333 will be decorated with free variables (different form each others), while the
334 conclusion will be decorated with a term expression with free variables
335 appearing in the context.
337 Suppose Γ,x:A ⊢ M:B. What is the expected decoration for A → B?
338 According to Kolmogorov interpretation, M is a procedure transforming the proof
339 x:A into a proof of M:B; the proof of A → B is hence the function that, taken x
340 as input, returns M, and our canonical notation for expressing such a function
341 is λx:A.M. Hence we get:
347 that is precisely the typing rule for functions.
349 Similarly, let us suppose that Γ ⊢ M:A → B, and Γ ⊢ N:A, and let us derive a
350 natural proof decoration for the arrow elimination rule (that is just the well
351 known modus ponens rule). Again, we get inspiration from Kolmogorov
352 interpretation: a proof M:A → B is a function transforming a proof of A into a
353 proof of B hence, since we have a proof N:A in order to get a proof of B it is
354 enough to apply M to the argument N:
356 Γ ⊢ M: A → B Γ ⊢ N: A
357 --------------------------
360 But this is nothing else than the typing rule for the application!
362 There is still a point that deserve discussion: the most interesting point of p
363 rograms is that they can be executed (in a functional setting, terms can be
364 reduced to a normal form). By the Curry-Howard correspondence, this should
365 correspond to a normalization procedure over proofs: does this operation make
366 any sense at the logical level? Again the answer is yes: not only it makes
367 sense, but it was independently investigated in the field of proof theory. A
368 reducible expression corresponds to what is traditionally called a "cut". A cut
369 is a logical ``detour'' typically arising by an introduction rule immediately
370 followed by an elimination rule for the same connective, as in a beta-redex, where
371 we have a direct "interaction" between an application and a λ-abstraction:
373 (beta-rule) λx.M N → M[N/x]
375 One of the main meta-theoretical results that is usually investigated on proof
376 systems is if they enjoy the so called "cut-elimination" principle, that is if
377 the cut-rule is "admissible": any proof that makes use of cuts can be turned
378 into a cut-free proof. Since a cut is redex, a cut-free proof is a term that
379 does not contain any redex, that is a term in normal form.
380 Hence, the system enjoys cut-elimination if and only if the corresponding
381 calculus is normalizing.
383 Cut-elimination is a major tool of proof theory, with important implications on
384 e.g. "consistency", "automation" and "interpolation".
386 Let us make a final remark. If a program is a proof, then what does it
387 correspond to the act of verifying the correctness of a proof M of some
388 proposition A? Well, M is just an expression that is supposed to have type A, so
389 "proof verification" is nothing else that "type checking"!
391 This should also clarify that proof verification is a much easier task than
392 proof search. While the former corresponds to type checking, the second
393 one corresponds to the automatic synthesis of a program from a specification!
395 The main ideas behind the Curry-Howard correspondence are summarized in the
398 Curry-Howard Correspondence
404 cut | reducible expression (redex)
405 cut free | normal form
406 cut elimination | normalization
407 correctness | type checking
410 (******************************* Prop vs. Type ********************************)
412 (* In view of the Curry-Howard analogy, the reader could wonder if there is any
413 actual difference between the two sorts Prop and Type in a system like the
414 Calculus of Constructions, or if it just a matter of flavour.
416 In fact there is a subtle difference concerning the type of product types over
417 the given sorts. Consider for instance a higher order sentence of
418 the kind ∀P:Prop.P: this is just a sentence asserting that any proposition is
419 true, and it looks natural to look at it as an object of sort Prop. However, if
420 this is the case, when we are quantifying over ``all propositions' we are also
421 implicitly quantifying over the proposition we are in the act of defining, that
422 creates a strange and possibly dangerous circularity.
424 In mathematics, definitions of this kind, where the definition (directly or
425 indirectly) mentions or quantifies over the entity being defined are called
428 The opposite notion of impredicativity is "predicativity", which essentially
429 entails building stratified (or ramified) theories where quantification over
430 lower levels results in objects of some new type.
432 Impredicativity can be dangerous: a well known example is Russel's ``set of all
433 sets'' resulting in famous logical paradox: does such a set contain itself as an
434 element? If it does then by definition it should not, and if it does not then by
435 definition it should.
437 A predicative approach would consist in distinguishing e.g. between ``small''
438 sets and ``large'' sets (collections), where the set of all small sets would
439 result in a large set.
441 In fact, if we look at ∀P:Type[0].P$ as a dependent product, and we identify
442 Type[0] as a universe of (small) ``sets'', it would seem strange to conclude
443 that quantifying over all (small) sets we could obtain another (small) set.
445 In Matita, ∀P:Type[0].P has in fact type Type[1] and not Type[0], where Type[1]
446 is also the type of Type[0].
448 So, while Prop is impredicative, sorts of the kind Type[i] define a potentially
449 infinite hierarchy of predicative sorts.
451 The difference between predicative and impredicative sorts is in the typing rule
452 for the product ∏x:A.B: if the sort of B is Prop then ∏x:A.B has type Prop
453 whatever the sort of A is; if A:Type[i] and B:Type[j], then ∏x:A.B:Type[k] where
454 Type[k] is the smallest sort strictly larger than Type[i] and Type[j]:
456 Γ ⊢ A : s Γ,x:A ⊢ B:Prop Γ ⊢ A : Type[i] Γ,x:A ⊢ B:Type[j]
457 --------------------------- ------------------------------------
458 Γ ⊢ ∏x:A.B : Prop Γ ⊢ ∏x:A.B : Type[k]
462 It is worth to observe that in Matita, the index i is just a label: constraints
463 among universes are declared by the user. The standard library (see
464 "basics/pts.ma" declares a few of them, with the following relations:
466 Type[0] < Type[1] < Type[2] < …
468 The impredicativity of Prop is not a problem from the point of view of the
469 logical consistency, but there is a price to be paid for this: we are not
470 allowed to eliminate Prop vs. Type[i]. In concrete terms this means that while
471 we are allowed to build terms, types or even propositions by structural
472 induction on terms, the only think we can do by structural induction/case
473 analysis on proofs is to build other proofs.
475 For instance, we know that a proof of p:A∨B is either a proof of A or a proof B,
476 and one could be tempted to define a function that returns the boolean true in
477 the first case and false otherwise, by performing a simple case analysis on p:
479 definition discriminate_to_bool ≝ λA,B:Prop.λp:A∨B.
485 If you type the previous definition, Matita will complain with the following
486 error message: ``TypeChecker failure: Sort elimination not allowed: Prop towards
488 Even returning the two propositions True and False intead of two booleans would
491 definition discriminate_to_Prop ≝ λA,B:Prop.λp:A∨B.
494 | or_intror b ⇒ False
497 The error message is the same as before: in both cases the sort of the branches
498 is Type[0]. The only thing we can do is to return other proofs, like in the
499 following example: *)
501 definition or_elim ≝ λA,B,C:Prop.λp:A∨B.λf:A→C.λg:B→C.
507 (* Exercise: repeat the previous examples in interactive mode, eliminating the
510 (**************************** The axiom of choice *****************************)
512 (* The axiom of choice says that given a collection of non-empty sets S_i
513 indexed over a base set I, it is possible to make a selection of exactly one
515 In type theory, this can be expressed in the following terms: *)
517 axiom choice_ax: ∀I:Type[0].∀S:I→Type[0].∀A:(∀i:I.S i → Type[0]).
518 (∀i:I.(∑x:S i.A i x)) → ∑f:∀i:I.S i.∀i:I.A i (f i).
520 (* The axiom of choice is independent from the traditional basic axioms of set
521 theory, like Zermelo–Fraenkel set theory, hence, if required, must be explicitly
522 added to the theory. This extension of ZF, known as ZFC, provides the "standard"
523 axiomatization of set theory.
525 The controversial nature of the axiom of choice is related to the effectiveness
526 of performing the selection claimed by the axiom of choice; for this reasons the
527 axiom of choice is usually rejected by constructive mathematicians.
529 However, if the proof of the existence on an inhabitant x_i for each type S_i is
530 itself constructive, then this proof already provides a method that, when
531 applied to an element i∈I returns the witness x_i. In other words, not only the
532 above axiom "choice" is perfectly acceptable, but it is actually provable! *)
534 theorem choice: ∀I:Type[0].∀S:I→Type[0].∀A.
535 (∀i:I.∑x:S i.A i x) → ∑f:∀i:I.S i.∀i:I.A i (f i).
538 ∑f:∀i:I.S i.(∀i:I.A i (f i))
539 We need to provide the function f:∀i:I.S i, and the proof that for any i:I,
540 A i (f i). The hypothesis H tells us that for any i we can build an object
541 (H i): ∑x:S i.A i x. The first projection of (H i) is an element of type (S i),
542 and we may define f ≝ λi. DPair_fst … (H i).The second projection of (H i) is
543 a witness of A i (DPair_fst … (H i)), that is, according to our defintion
544 of f, a witness of A i (f i). Hence, λi.DPair_snd ?? (H i): ∀i:I.A i (f i). *)
545 %{(λi.DPair_fst ?? (H i)) (λi.DPair_snd ?? (H i))}
548 (* It is worth to observe that if we try to repeat the same proof with either
549 the existential of the sigma type it will not work. For instance, the
550 following property is not provable: *)
552 axiom Pchoice: ∀I:Type[0].∀S:I→Type[0].∀A.
553 (∀i:I.∃x:S i.A i x) → ∃f:∀i:I.S i.∀i:I.A i (f i).
555 (* The point is that the proof would require to extract from a non-informative
556 content, namely the fact that there exists an x such that (A i x), the actual
557 witness x, that is an informative notion, and we know that this is forbidden for
558 consistency reasons. *)