-(* 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.
+(************************ 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.
+
+As a consequence, the expression
+
+ M:A
+
+really has a double possible reading:
+
+- M is a term of type A
+- M is a proof of the proposition A
+
+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:
+
+ Γ,A ⊢ B Γ ⊢ A → B Γ ⊢ A
+ ---------- -------------------
+ Γ ⊢ A → B Γ ⊢ B
+
+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
+
+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]