-(*
-Naif Set Theory
-
+(*
+ Propositions as Types
*)
-include "basics/types.ma".
-include "basics/bool.ma".
-(*
-In this Chapter we shall develop a naif theory of sets represented as
-characteristic predicates over some universe A, that is as objects of type
-A→Prop.
-For instance the empty set is defined by the always false function: *)
-definition empty_set ≝ λA:Type[0].λa:A.False.
-notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
-interpretation "empty set" 'empty_set = (empty_set ?).
+include "tutorial/chapter3.ma".
+include "basics/logic.ma".
-(* Similarly, a singleton set contaning containing an element a, is defined
-by by the characteristic function asserting equality with a *)
+(* In the previous section, we introduced many interesting logical connectives
+by means of inductive definitions in the sort Prop. Do the same constructions
+make any sense in Type? The answer is yes! Not only they make sense, but they
+are indeed very familiar constructions: cartesian product, disjoint sum, empty
+and singleton types, and ``sigma types'' (disjoint union of families of types
+indexed over a given base type). This is not a coincidence, but a consequence of
+a strong principle known under the name of ``Propositions as Types analogy'' (or
+Curry-Howard correspondence).
-definition singleton ≝ λA.λx,a:A.x=a.
-(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
-interpretation "singleton" 'singl x = (singleton ? x).
+We shall first discuss the constructions, and then we shall come back on the
+general analogy.*)
-(* The membership relation between an element of type A and a set S:A →Prop is
-simply the predicate resulting from the application of S to a.
-The operations of union, intersection, complement and substraction
-are easily defined in terms of the propositional connectives of dijunction,
-conjunction and negation *)
+(***************************** Cartesian Product ******************************)
-definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
-interpretation "union" 'union a b = (union ? a b).
+(* The cartesian product of two types A and B is defined as follows: *)
-definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
-interpretation "intersection" 'intersects a b = (intersection ? a b).
+inductive Prod (A,B:Type[0]) : Type[0] ≝
+ pair : A → B → Prod A B.
+
+(* Observe that the definition is identical to the definition of the logical
+conjunction, but for the fact that the sort Prop has been replaced by Type[0].
-definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
-interpretation "complement" 'not a = (complement ? a).
+The following declarations allows us to use the canonical notations A × B for
+the product and 〈a,b〉 for the pair of the two elements a and b. *)
-definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
-interpretation "substraction" 'minus a b = (substraction ? a b).
+notation "hvbox(x break × y)" with precedence 70 for @{ 'product $x $y}.
+interpretation "Cartesian product" 'product A B = (Prod A B).
-(* Finally, we use implication to define the inclusion relation between
-sets *)
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+ with precedence 90 for @{ 'pair $a $b}.
+interpretation "Pair construction" 'pair x y = (pair ?? x y).
-definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
-interpretation "subset" 'subseteq a b = (subset ? a b).
+(* We can define the two projections fst and snd by a simple case analysis of
+the term: *)
-(*
-Set Equality
+definition fst ≝ λA,B.λp:A×B. match p with [pair a b ⇒ a].
+definition snd ≝ λA,B.λp:A×B. match p with [pair a b ⇒ b].
-Two sets are equals if and only if they have the same elements, that is,
-if the two characteristic functions are extensionally equivalent: *)
+(* As in the case of inductive propositions, Matita automatically generates
+elimination principles for A × B. In this case, however, it becomes interesting
+to consider the possibility that the proposition towards which we are
+eliminating a given pair p:A × B$ contains a copy of p itself. In other words,
+if we have p:A × B in the current context, it is possible that p also occurs in
+the current goal, that is that the current goal "depends" on p.
-definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
-interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+A typical example is in the proof of the so called ``surjective pairing''
+property: *)
-(*
-This notion of equality is different from the intensional equality of
-functions; the fact it defines an equivalence relation must be explicitly
-proved: *)
+lemma surjective_pair: ∀A,B.∀p:A×B. p = 〈fst ?? p, snd ?? p〉.
-lemma eqP_sym: ∀U.∀A,B:U →Prop.
- A =1 B → B =1 A.
-#U #A #B #eqAB #a @iff_sym @eqAB qed.
-
-lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
- A =1 B → B =1 C → A =1 C.
-#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+(* where p explicitly occurs in the conclusion. The proof is straightforward: we
+introduce A, B and p and proceed by cases on p: since p is a pair, the only
+possible case is that it is of the form 〈a,b〉 for some a and b.*)
-(* For the same reason, we must also prove that all the operations behave well
-with respect to eqP: *)
+#A #B #p cases p #a #b
-lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∪ B =1 C ∪ B.
-#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
-
-lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∪ B =1 A ∪ C.
-#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
-
-lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∩ B =1 C ∩ B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
-
-lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∩ B =1 A ∩ C.
-#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+(* At this point the goal looks like
+ 〈a,b〉 = 〈fst A B 〈a,b〉, snd A B 〈a,b〉〉
+and the two sides of the equation are convertible. *)
+// qed.
+
+(* When we call cases p we are actually applying the dependent elimination
+principle Prod_ind for the product, so it becomes interesting to have a look at
+it (we shall postpone the discussion of the way it is generated in a later
+section):
-lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A - B =1 C - B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+ ∀A,B.∀P:A×B →Prop.(∀a:A,∀b:B. P 〈a,b〉) → ∀x:A×B.P x
-lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A - B =1 A - C.
-#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+The previous principle has a very natural backward reading: in order to prove
+that the property (P x) holds for any x of type A×B it is enough to prove P〈a,b〉
+for any a:A and b:B. *)
-(*
-Simple properties of sets
+(******************************* Disjoint Sum *********************************)
-We can now prove several properties of the previous set-theoretic operations.
-In particular, union is commutative and associative, and the empty set is an
-identity element: *)
+(* By reflecting in Type the definition of the logical disjunction we obtain the
+disjoint union (the sum) of two types: *)
-lemma union_empty_r: ∀U.∀A:U→Prop.
- A ∪ ∅ =1 A.
-#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
-qed.
+inductive Sum (A,B:Type[0]) : Type[0] ≝
+ inl : A → Sum A B
+| inr : B → Sum A B.
-lemma union_comm : ∀U.∀A,B:U →Prop.
- A ∪ B =1 B ∪ A.
-#U #A #B #a % * /2/ qed.
+notation "hvbox(a break + b)"
+ left associative with precedence 55 for @{ 'plus $a $b }.
-lemma union_assoc: ∀U.∀A,B,C:U → Prop.
- A ∪ B ∪ C =1 A ∪ (B ∪ C).
-#S #A #B #C #w % [* [* /3/ | /3/ ] | * [/3/ | * /3/]
-qed.
+interpretation "Disjoint union" 'plus A B = (Sum A B).
-(* In the same way we prove commutativity and associativity for set
-interesection *)
+(* The two constructors are the left and right injections. The dependent
+elimination principle Sum_ind has the following shape:
-lemma cap_comm : ∀U.∀A,B:U →Prop.
- A ∩ B =1 B ∩ A.
-#U #A #B #a % * /2/ qed.
+ ∀A,B.∀P:A+B →Prop.
+ (∀a:A.P (inl A B a)) → (∀b:B.P (inr A B b)) → ∀x:A×B.P x
+
+that is, in order to prove the property (P x) for any x:A+B it is enough to
+prove P (inl A B a) and P (inr A B b) for all a:A and b:B. *)
+
+(************************* Empty Type and Unit Type ***************************)
-lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
- A ∩ (B ∩ C) =1 (A ∩ B) ∩ C.
-#U #A #B #C #w % [ * #Aw * /3/ | * * /3/ ]
-qed.
+(* The counterparts of False and True are, respectively, an empty type and a
+singleton type: *)
-(* We can also easily prove idempotency for union and intersection *)
+inductive void : Type[0] ≝.
+inductive unit : Type[0] ≝ it: unit.
-lemma union_idemp: ∀U.∀A:U →Prop.
- A ∪ A =1 A.
-#U #A #a % [* // | /2/] qed.
+(* The elimination principle void_ind for void is simply
-lemma cap_idemp: ∀U.∀A:U →Prop.
- A ∩ A =1 A.
-#U #A #a % [* // | /2/] qed.
+ ∀P:void→Prop.∀x:void.P x
+
+stating that any property is true for an element of type void (since we have no
+such element).
-(* We conclude our examples with a couple of distributivity theorems, and a
-characterization of substraction in terms of interesection and complementation. *)
+Similarly, the elimination principle for the unit type is:
-lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
-qed.
+ ∀P:unit→Prop. P it → ∀x:unit.P x
-lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) - C =1 (A - C) ∪ (B - C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
-qed.
+Indeed, in order to prove that a property is true for any element of the unit
+type, it is enough to prove it for the unique (canonical) inhabitant "it".
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
-#U #A #B #w normalize /2/
-qed.
+As an exercise, let us prove that all inhabitants of unit are equal to each
+other: *)
-(*
-Bool vs. Prop
+lemma eq_unit: ∀a,b:unit. a = b.
-In several situation it is important to assume to have a decidable equality
-between elements of a set U, namely a boolean function eqb: U→U→bool such that
-for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
-A set equipped with such an equality is called a DeqSet: *)
+(* The idea is to proceed by cases on a and b: we have only one possibility,
+namely a=it and b=it, hence we end up to prove it=it, that is trivial. Here is
+the proof: *)
-record DeqSet : Type[1] ≝ { carr :> Type[0];
- eqb: carr → carr → bool;
- eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
-}.
+#a cases a #b cases b // qed. (* also: * * // qed. *)
-(* We use the notation == to denote the decidable equality, to distinguish it
-from the propositional equality. In particular, a term of the form a==b is a
-boolean, while a=b is a proposition. *)
+(* It is interesting to observe that we get exactly the same behavior by
+directly applying unit_ind instead of proceeding by cases. In fact, this is an
+alternative proof: *)
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
+lemma eq_unit_again: ∀a,b:unit. a = b.
+@unit_ind @unit_ind // qed.
-(*
-Small Scale Reflection
+(********************* Sigma Types and dependent matching *********************)
-It is convenient to have a simple way to reflect a proof of the fact
-that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
-we introduce two operators "\P" and "\b". *)
+(* As a final example, let us consider ``type'' variants of the existential
+quantifier; in this case we have two interesting possibilities: *)
-notation "\P H" non associative with precedence 90
- for @{(proj1 … (eqb_true ???) $H)}.
+inductive Sig (A:Type[0]) (Q:A → Prop) : Type[0] ≝
+ Sig_intro: ∀x:A. Q x → Sig A Q.
-notation "\b H" non associative with precedence 90
- for @{(proj2 … (eqb_true ???) $H)}.
-
-(* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
-\b h: eqb a b = true. Let us see an example of their use: the following
-statement asserts that we can reflect a proof that eqb a b is false into
-a proof of the proposition a ≠ b. *)
+inductive DPair (A:Type[0]) (Q:A → Type[0]) : Type[0] ≝
+ DPair_intro: ∀x:A. Q x → DPair A Q.
+
+(* In the first case (traditionally called sigma type), an element of type
+(Sig A P) is a pair (Sig_intro ?? a h) where a is an element of type A and h is a
+proof that the property (P a) holds.
+
+A suggestive reading of (Sig A P) is as the subset of A enjoying the property P,
+that is {a:A | P(a)}.
+
+In the second case, an element of DPair A B is a "dependent" pair
+(DPair_intro ?? a h) where a is element of type A and h maps a into an element in
+(B a); the intuition is to look at DProd A B as a (disjoint) family of sets B_a
+indexed over elements a:A.
+
+In both case it is possible to define projections extracting the two components
+of the pair. Let us discuss the case of the sigma type (the other one is
+analogous).
+
+Extracting the first component (the element) is easy: *)
+
+definition Sig_fst ≝ λA:Type[0].λP:A→Prop.λx:Sig A P.
+ match x with [Sig_intro a h ⇒ a].
-lemma eqb_false: ∀S:DeqSet.∀a,b:S.
- (eqb ? a b) = false ↔ a ≠ b.
+(* Getting the second component is a bit trickier. The first problem is
+the type of the result: given a pair (Sig_intro ?? a h): Sig A P, the type of
+h is (P a), that is P applied to the first argument of the pair of which we want
+to extract the second component!
+Luckily, in a language with dependent types, it is not a problem to write such a
+a type:
-(* We start the proof introducing the hypothesis, and then split the "if" and
-"only if" cases *)
+ definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ ...
+
+A subtler problem is met when we define the body. If we just write
+
+ definition Sig_snd : ∀A,P.∀x.Sig A P → P (Sig_fst A P x) ≝ λA,P,x.
+ match x with [Sig_intro a h ⇒ h].
+
+the system will complain about the type of h. The point is that the type of this
+term depends on a, that is, in a not so trivial way, from the input argument x.
+In this situations, the type inference algorithm of Matita requires a little
+help: in particular the user is asked to explicitly provide the return type of
+the match expression, that is a map uniformly expressing the type of all
+branches of the case as a function of the matched expression.
+In our case we only have one branch and the return type is
+
+ λx.P (Sig\_fst A P x)
+
+We declare such a type immediately after the match, introduces by the keyword
+``return'': *)
+
+definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
+ match x return λx.P (Sig_fst A P x) with [Sig_intro a h ⇒ h].
+
+(* Remark: The careful reader may have possibly remarked that we also did a
+systematic abuse of the arrow symbol: the expression A → B was sometimes
+interpreted as the "implication" between A and B and sometimes as the "function
+space" between A and B. The reason of this fact is that, actually, in a
+foundational system like the Calculus of Construction, they are the very same
+notion: we only distinguish them according to the sort of the resulting
+expression.
+Similarly for the dependent product ∏x:A.B: if the resulting expression is of
+sort Prop we shall look at it as a "universal quantification" (using the
+notation ∀x:A.B), while if it is in Type we shall typically regard it as a
+generalized cartesian product of a family of types B indexed over a base type A.
+*)
+
+(************************ Kolmogorov interpretation ***************************)
+
+(* The previous analogy between propositions and types is a consequence of a
+deep philosophical interpretation of the notion of proof in terms of a
+constructive procedure that transforms proofs of the premises into a proof of
+the conclusion. This usually referred to as Kolmogorov interpretation, or
+Brouwer–Heyting–Kolmogorov (BHK) interpretation.
+
+The interpretation states what is intended to be a proof of a given formula φ,
+and is specified by induction on the structure of A:
+
+- a proof of P∧Q is a pair 〈a,b〉 where a is a proof of P and b is a proof of Q;
+- a proof of P∨Q is a pair 〈a,b〉 where either a is 0 and b is a proof of P, or
+ a=1 and b is a proof of Q;
+- a proof of P→Q is a function f which transforms a proof of x:P into a proof of
+ (f x):Q;
+- a proof of ∃x:S.φ(x) is a pair 〈a,b〉 where a is an element of S, and b is a
+ proof of φ(a);
+- a proof of ∀x:S.ϕ(x) is a function f which transforms an element x of S into a
+ proof of \varphi(a);
+- the formula ¬P is defined as P → False, so a proof of it is a function f which
+ transforms a proof of P into a proof of False;
+- there is no proof of False.
+
+For instance, a proof of the formula P → P is a function transforming a proof of
+P into a proof of P: but we can just take the identity!
+
+You can explicitly exploit this idea for writing proofs in Matita. Instead of
+declaring a lemma and proving it interactively, you may define your lemma as if
+it was the type of an expression, and directly proceed to inhabit it with its
+proof: *)
+
+definition trivial: ∀P:Prop.P→P ≝ λP,h.h.
+
+(* It is interesting to observe that this is really the very same proof
+(intensionally!!) that would be produce interactively, as testified by the
+following fragment of code: *)
+
+lemma trivial1: ∀P:Prop.P→P. #P #h @h qed.
+lemma same_proofs: trivial = trivial1. @refl qed.
+
+(* Even more interestingly, we can do the opposite, namely define functions
+interactively.
+Suppose for instance that we need to define a function with the following
+type: ∀A,B,C:Type[0]. (A → B → C) → A× B → C.
+If we just declare the type of the function followed by a fullstop, Matita will
+start an interactive session completely analogous to a proof session, and we can
+use the usual tactics to ``close the goal'', that is to inhabit the type. *)
+
+definition uncurrying: ∀A,B,C:Type[0]. (A→B→C)→A×B→C.
+#A #B #C #f * @f qed.
+
+(********************** The Curry-Howard correspondence ***********************)
+
+(* The philosophical ideas contained in the BHK interpretation of a proof as a
+constructive procedure building a proof of the conclusion from proofs of the
+hypothesis get a precise syntactical systematization via the so called
+Curry-Howard correspondence, expressing a direct relationship between computer
+programs and proofs.
+The Curry-Howard correspondence, also known as proofs-as-programs analogy, is a
+generalization of a syntactic analogy between systems of formal logic and
+computational calculi first observed by Curry for Combinatory Logic and Hilbert-
+style deduction systems, and later by Howard for λ-calculus and Natural
+Deduction: in both cases the formation rules for well typed terms have precisely
+the same shape of the logical rules of introduction of the correspondent
+connective.
-#S #a #b % #H
+As a consequence, the expression
-(* The latter is easily reduced to prove the goal true=false under the assumption
-H1: a = b *)
- [@(not_to_not … not_eq_true_false) #H1
-
-(* since by assumption H false is equal to (a==b), by rewriting we obtain the goal
-true=(a==b) that is just the boolean version of H1 *)
+ M:A
+
+really has a double possible reading:
+
+- M is a term of type A
+- M is a proof of the proposition A
- <H @sym_eq @(\b H1)
+In both cases, M is a witness that the object A is "inhabited". A free variable
+x:A is an assumption about the validity of A (we assumeto have an unknown proof
+named x). Let us consider the cases of the introduction and elimination rule of
+the implication in natural deduction, that are particularly interesting:
-(* In the "if" case, we proceed by cases over the boolean equality (a==b); if
-(a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
-true, then by reflection a=b, while by hypothesis a≠b *)
+ Γ,A ⊢ B Γ ⊢ A → B Γ ⊢ A
+ ---------- -------------------
+ Γ ⊢ A → B Γ ⊢ B
- |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
- ]
-qed.
-
-(* We also introduce two operators "\Pf" and "\bf" to reflect a proof
-of (a==b)=false into a proof of a≠b, and vice-versa *)
-
-notation "\Pf H" non associative with precedence 90
- for @{(proj1 … (eqb_false ???) $H)}.
-
-notation "\bf H" non associative with precedence 90
- for @{(proj2 … (eqb_false ???) $H)}.
-
-(* The following statement proves that propositional equality in a
-DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
-
- lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
-#S #a #b cases (true_or_false (eqb ? a b)) #H
- [%1 @(\P H) | %2 @(\Pf H)]
-qed.
-
-(*
-Unification Hints
-
-A simple example of a set with a decidable equality is bool. We first define
-the boolean equality beqb, that is just the xand function, then prove that
-beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
-instantiating the DeqSet record with the previous information *)
-
-definition beqb ≝ λb1,b2.
- match b1 with [ true ⇒ b2 | false ⇒ notb b2].
-
-notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
-
-lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
-#b1 #b2 cases b1 cases b2 normalize /2/
-qed.
-
-definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
-
-(* At this point, we would expect to be able to prove things like the
-following: for any boolean b, if b==false is true then b=false.
-Unfortunately, this would not work, unless we declare b of type
-DeqBool (change the type in the following statement and see what
-happens). *)
-
-example exhint: ∀b:DeqBool. (b==false) = true → b=false.
-#b #H @(\P H)
-qed.
-
-(* The point is that == expects in input a pair of objects whose type must be the
-carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
-system has no knowledge of it (it is an information that has been supplied by the
-user, and stored somewhere in the library). More explicitly, the type inference
-inference system, would face an unification problem consisting to unify bool
-against the carrier of something (a metavaribale) and it has no way to synthetize
-the answer. To solve this kind of situations, matita provides a mechanism to hint
-the system the expected solution. A unification hint is a kind of rule, whose rhd
-is the unification problem, containing some metavariables X1, ..., Xn, and whose
-left hand side is the solution suggested to the system, in the form of equations
-Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
-is, if it is a unifier for the given problem.
-To make an example, in the previous case, the unification problem is bool = carr X,
-and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
-bool is convertible with (carr (mk_DeqSet bool beb true)). *)
-
-alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
-
-unification hint 0 ≔ ;
- X ≟ mk_DeqSet bool beqb beqb_true
-(* ---------------------------------------- *) ⊢
- bool ≡ carr X.
+The first step is to enrich the representation by decorating formulae with
+explicit proof terms. In particular, formulae in the context, being assumptions,
+will be decorated with free variables (different form each others), while the
+conclusion will be decorated with a term expression with free variables
+appearing in the context.
+
+Suppose Γ,x:A ⊢ M:B. What is the expected decoration for A → B?
+According to Kolmogorov interpretation, M is a procedure transforming the proof
+x:A into a proof of M:B; the proof of A → B is hence the function that, taken x
+as input, returns M, and our canonical notation for expressing such a function
+is λx:A.M. Hence we get:
+
+ Γ,x:A ⊢ M:B
+ -----------------
+ Γ ⊢ λx:A.M: A → B
-unification hint 0 ≔ b1,b2:bool;
- X ≟ mk_DeqSet bool beqb beqb_true
-(* ---------------------------------------- *) ⊢
- beqb b1 b2 ≡ eqb X b1 b2.
+that is precisely the typing rule for functions.
+
+Similarly, let us suppose that Γ ⊢ M:A → B, and Γ ⊢ N:A, and let us derive a
+natural proof decoration for the arrow elimination rule (that is just the well
+known modus ponens rule). Again, we get inspiration from Kolmogorov
+interpretation: a proof M:A → B is a function transforming a proof of A into a
+proof of B hence, since we have a proof N:A in order to get a proof of B it is
+enough to apply M to the argument N:
+
+ Γ ⊢ M: A → B Γ ⊢ N: A
+ --------------------------
+ Γ ⊢ (M N):B
+
+But this is nothing else than the typing rule for the application!
+
+There is still a point that deserve discussion: the most interesting point of p
+rograms is that they can be executed (in a functional setting, terms can be
+reduced to a normal form). By the Curry-Howard correspondence, this should
+correspond to a normalization procedure over proofs: does this operation make
+any sense at the logical level? Again the answer is yes: not only it makes
+sense, but it was independently investigated in the field of proof theory. A
+reducible expression corresponds to what is traditionally called a "cut". A cut
+is a logical ``detour'' typically arising by an introduction rule immediately
+followed by an elimination rule for the same connective, as in a beta-redex, where
+we have a direct "interaction" between an application and a λ-abstraction:
+
+ (beta-rule) λx.M N → M[N/x]
-(* After having provided the previous hints, we may rewrite example exhint
-declaring b of type bool. *)
+One of the main meta-theoretical results that is usually investigated on proof
+systems is if they enjoy the so called "cut-elimination" principle, that is if
+the cut-rule is "admissible": any proof that makes use of cuts can be turned
+into a cut-free proof. Since a cut is redex, a cut-free proof is a term that
+does not contain any redex, that is a term in normal form.
+Hence, the system enjoys cut-elimination if and only if the corresponding
+calculus is normalizing.
+
+Cut-elimination is a major tool of proof theory, with important implications on
+e.g. "consistency", "automation" and "interpolation".
+
+Let us make a final remark. If a program is a proof, then what does it
+correspond to the act of verifying the correctness of a proof M of some
+proposition A? Well, M is just an expression that is supposed to have type A, so
+"proof verification" is nothing else that "type checking"!
+
+This should also clarify that proof verification is a much easier task than
+proof search. While the former corresponds to type checking, the second
+one corresponds to the automatic synthesis of a program from a specification!
+
+The main ideas behind the Curry-Howard correspondence are summarized in the
+following Picture:
+
+ Curry-Howard Correspondence
+
+ Logic | Programming
+ |
+ proposition | type
+ proof | program
+ cut | reducible expression (redex)
+ cut free | normal form
+ cut elimination | normalization
+ correctness |type checking
+*)
+
+(******************************* Prop vs. Type ********************************)
+
+(* In view of the Curry-Howard analogy, the reader could wonder if there is any
+actual difference between the two sorts Prop and Type in a system like the
+Calculus of Constructions, or if it just a matter of flavour.
+
+In fact there is a subtle difference concerning the type of product types over
+the given sorts. Consider for instance a higher order sentence of
+the kind ∀P:Prop.P: this is just a sentence asserting that any proposition is
+true, and it looks natural to look at it as an object of sort Prop. However, if
+this is the case, when we are quantifying over ``all propositions' we are also
+implicitly quantifying over the proposition we are in the act of defining, that
+creates a strange and possibly dangerous circularity.
+
+In mathematics, definitions of this kind, where the definition (directly or
+indirectly) mentions or quantifies over the entity being defined are called
+"impredicative".
+
+The opposite notion of impredicativity is "predicativity", which essentially
+entails building stratified (or ramified) theories where quantification over
+lower levels results in objects of some new type.
+
+Impredicativity can be dangerous: a well known example is Russel's ``set of all
+sets'' resulting in famous logical paradox: does such a set contain itself as an
+element? If it does then by definition it should not, and if it does not then by
+definition it should.
+
+A predicative approach would consist in distinguishing e.g. between ``small''
+sets and ``large'' sets (collections), where the set of all small sets would
+result in a large set.
+
+In fact, if we look at ∀P:Type[0].P$ as a dependent product, and we identify
+Type[0] as a universe of (small) ``sets'', it would seem strange to conclude
+that quantifying over all (small) sets we could obtain another (small) set.
+
+In Matita, ∀P:Type[0].P has in fact type Type[1] and not Type[0], where Type[1]
+is also the type of Type[0].
+
+So, while Prop is impredicative, sorts of the kind Type[i] define a potentially
+infinite hierarchy of predicative sorts.
+
+The difference between predicative and impredicative sorts is in the typing rule
+for the product ∏x:A.B: if the sort of B is Prop then ∏x:A.B has type Prop
+whatever the sort of A is; if A:Type[i] and B:Type[j], then ∏x:A.B:Type[k] where
+Type[k] is the smallest sort strictly larger than Type[i] and Type[j]:
+
+ Γ ⊢ A : s Γ,x:A ⊢ B:Prop Γ ⊢ A : Type[i] Γ,x:A ⊢ B:Type[j]
+ --------------------------- ------------------------------------
+ Γ ⊢ ∏x:A.B : Prop Γ ⊢ ∏x:A.B : Type[k]
+
+for k = max{i,j}+1.
+
+It is worth to observe that in Matita, the index i is just a label: constraints
+among universes are declared by the user. The standard library (see
+"basics/pts.ma" declares a few of them, with the following relations:
+
+ Type[0] < Type[1] < Type[2] < …
+
+The impredicativity of Prop is not a problem from the point of view of the
+logical consistency, but there is a price to be paid for this: we are not
+allowed to eliminate Prop vs. Type[i]. In concrete terms this means that while
+we are allowed to build terms, types or even propositions by structural
+induction on terms, the only think we can do by structural induction/case
+analysis on proofs is to build other proofs.
+
+For instance, we know that a proof of p:A∨B is either a proof of A or a proof B,
+and one could be tempted to define a function that returns the boolean true in
+the first case and false otherwise, by performing a simple case analysis on p:
+
+definition discriminate_to_bool ≝ λA,B:Prop.λp:A∨B.
+ match p with
+ [ or_introl a ⇒ tt
+ | or_intror b ⇒ ff
+ ].
+
+If you type the previous definition, Matita will complain with the following
+error message: ``TypeChecker failure: Sort elimination not allowed: Prop towards
+Type[0]''.
+Even returning the two propositions True and False intead of two booleans would
+not work:
+
+definition discriminate_to_Prop ≝ λA,B:Prop.λp:A∨B.
+ match p with
+ [ or_introl a ⇒ True
+ | or_intror b ⇒ False
+ ].
-example exhint1: ∀b:bool. (b == false) = true → b = false.
-#b #H @(\P H)
-qed.
-
-(* The cartesian product of two DeqSets is still a DeqSet. To prove
-this, we must as usual define the boolen equality function, and prove
-it correctly reflects propositional equality. *)
-
-definition eq_pairs ≝
- λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
-
-lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
- eq_pairs A B p1 p2 = true ↔ p1 = p2.
-#A #B * #a1 #b1 * #a2 #b2 %
- [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
- |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
- ]
-qed.
-
-definition DeqProd ≝ λA,B:DeqSet.
- mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-
-(* Having an unification problem of the kind T1×T2 = carr X, what kind
-of hint can we give to the system? We expect T1 to be the carrier of a
-DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
-This is expressed by the following hint: *)
-
-unification hint 0 ≔ C1,C2;
- T1 ≟ carr C1,
- T2 ≟ carr C2,
- X ≟ DeqProd C1 C2
-(* ---------------------------------------- *) ⊢
- T1×T2 ≡ carr X.
-
-unification hint 0 ≔ T1,T2,p1,p2;
- X ≟ DeqProd T1 T2
-(* ---------------------------------------- *) ⊢
- eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
-
-example hint2: ∀b1,b2.
- 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
-#b1 #b2 #H @(\P H).
-qed-.
\ No newline at end of file
+The error message is the same as before: in both cases the sort of the branches
+is Type[0]. The only think we can do is to return other proof, like in the
+following example: *)
+
+definition or_elim ≝ λA,B,C:Prop.λp:A∨B.λf:A→C.λg:B→C.
+ match p with
+ [ or_introl a ⇒ f a
+ | or_intror b ⇒ g b
+ ].
+
+(* Exercise: repeat the previous examples in interactive mode, eliminating the
+hypothesis p:A∨B. *)
+
+
projects / helm.git / blobdiff