From: Andrea Asperti Date: Mon, 11 Mar 2013 10:32:22 +0000 (+0000) Subject: Chpater 4 and 5 X-Git-Tag: make_still_working~1223 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65c5a379db69f0df0c803f4b24bb3219c9da752a;p=helm.git Chpater 4 and 5 --- diff --git a/matita/matita/lib/tutorial/chapter4.ma b/matita/matita/lib/tutorial/chapter4.ma index aa2f5b08a..d11b920f8 100644 --- a/matita/matita/lib/tutorial/chapter4.ma +++ b/matita/matita/lib/tutorial/chapter4.ma @@ -1,340 +1,482 @@ -(* -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 - (\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. *) + + diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma index b90433657..925776785 100644 --- a/matita/matita/lib/tutorial/chapter5.ma +++ b/matita/matita/lib/tutorial/chapter5.ma @@ -1,253 +1,523 @@ -(* -Effective searching - -The fact of being able to decide, via a computable boolean function, the -equality between elements of a given set is an essential prerequisite for -effectively searching an element of that set inside a data structure. In this -section we shall define several boolean functions acting on lists of elements in -a DeqSet, and prove some of their properties.*) - -include "basics/lists/list.ma". -include "tutorial/chapter4.ma". - -(* The first function we define is an effective version of the membership relation, -between an element x and a list l. Its definition is a straightforward recursion on -l.*) - -let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝ - match l with - [ nil ⇒ false - | cons a tl ⇒ (x == a) ∨ memb S x tl - ]. - -notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}. -interpretation "boolean membership" 'memb a l = (memb ? a l). - -(* We can now prove several interesing properties for memb: -- memb_hd: x is a member of x::l -- memb_cons: if x is a member of l than x is a member of a::l -- memb_single: if x is a member of [a] then x=a -- memb_append: if x is a member of l1@l2 then either x is a member of l1 - or x is a member of l2 -- memb_append_l1: if x is a member of l1 then x is a member of l1@l2 -- memb_append_l2: if x is a member of l2 then x is a member of l1@l2 -- memb_exists: if x is a member of l, than l can decomposed as l1@(x::l2) -- not_memb_to_not_eq: if x is not a member of l and y is, then x≠y -- memb_map: if a is a member of l, then (f a) is a member of (map f l) -- memb_compose: if a is a member of l1 and b is a meber of l2 than - (op a b) is a member of (compose op l1 l2) +(* + More Data Types *) -lemma memb_hd: ∀S,a,l. memb S a (a::l) = true. -#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) // -qed. +include "basics/logic.ma". -lemma memb_cons: ∀S,a,b,l. - memb S a l = true → memb S a (b::l) = true. -#S #a #b #l normalize cases (a==b) normalize // -qed. +(******************************** Option Type *********************************) -lemma memb_single: ∀S,a,x. memb S a (x::[]) = true → a = x. -#S #a #x normalize cases (true_or_false … (a==x)) #H - [#_ >(\P H) // |>H normalize #abs @False_ind /2/] -qed. +(* Matita may only define total functions. However, not always we may return a +meaningful value: for instance, working on natural numbers, the predecessor of +0 is undefined. In these situations, we may either return a default value +(usually, pred 0 = 0), or decide to return an "option type" as a result. An +Option type is a polymorphic type that represents encapsulation of an optional +value. It consists of either an empty constructor (traditionally called None), +or a constructor encapsulating the original data type A (written Some A): *) -lemma memb_append: ∀S,a,l1,l2. -memb S a (l1@l2) = true → memb S a l1= true ∨ memb S a l2 = true. -#S #a #l1 elim l1 normalize [#l2 #H %2 //] -#b #tl #Hind #l2 cases (a==b) normalize /2/ -qed. - -lemma memb_append_l1: ∀S,a,l1,l2. - memb S a l1= true → memb S a (l1@l2) = true. -#S #a #l1 elim l1 normalize - [normalize #le #abs @False_ind /2/ - |#b #tl #Hind #l2 cases (a==b) normalize /2/ - ] -qed. - -lemma memb_append_l2: ∀S,a,l1,l2. - memb S a l2= true → memb S a (l1@l2) = true. -#S #a #l1 elim l1 normalize // -#b #tl #Hind #l2 cases (a==b) normalize /2/ -qed. - -lemma memb_exists: ∀S,a,l.memb S a l = true → ∃l1,l2.l=l1@(a::l2). -#S #a #l elim l [normalize #abs @False_ind /2/] -#b #tl #Hind #H cases (orb_true_l … H) - [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) // - |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl - @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl // - ] -qed. - -lemma not_memb_to_not_eq: ∀S,a,b,l. - memb S a l = false → memb S b l = true → a==b = false. -#S #a #b #l cases (true_or_false (a==b)) // -#eqab >(\P eqab) #H >H #abs @False_ind /2/ -qed. +inductive option (A:Type[0]) : Type[0] ≝ + None : option A + | Some : A → option A. -lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → - memb S2 (f a) (map … f l) = true. -#S1 #S2 #f #a #l elim l normalize [//] -#x #tl #memba cases (true_or_false (a==x)) - [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize // - |#eqx >eqx cases (f a==f x) normalize /2/ - ] -qed. - -lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. - memb S1 a1 l1 = true → memb S2 a2 l2 = true → - memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true. -#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //] -#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1) - [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // - |#membtl @memb_append_l2 @Hind // - ] -qed. - -(* -Unicity - -If we are interested in representing finite sets as lists, is is convenient -to avoid duplications of elements. The following uniqueb check this property. -*) - -let rec uniqueb (S:DeqSet) l on l : bool ≝ - match l with - [ nil ⇒ true - | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl - ]. - -(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *) - -let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝ +(* The type option A is isomorphic to the disjoint sum between A and unit. The +two bijections are simply defined as +follows: +\begin{lstlisting}[language=grafite] +definition option_to_sum ≝ λA.λx:option A. + match x with + [ None ⇒ inl ?? it + | Some a ⇒ inr ?? a ]. +\end{lstlisting} + +\begin{lstlisting}[language=grafite] +definition sum_to_option ≝ λA.λx:unit+A. + match x with + [ inl a ⇒ None A + | inr a ⇒ Some A a ]. +\end{lstlisting} +The fact that going from the option type to the sum and back again we get the +original element follows from a straightforward case analysis: +\begin{lstlisting}[language=grafite] +lemma option_bij1: ∀A,x. sum_to_option A (option_to_sum A x) = x. +#A * // qed. +\end{lstlisting} +The other direction is just slightly more complex, since we need to exploit +the fact that the unit type contains a single element: we could use lemma ... or +proceed by cases on the unit element. +\begin{lstlisting}[language=grafite] +lemma option_bij2: ∀A,x. option_to_sum A (sum_to_option A x) = x. +#A * // * // qed. +\end{lstlisting} +We shall see more examples of functions involving the otion type in the +next section. + +\subsection{Lists} +The option type, as well as the cartesian product or the sum are simple +examples of polymorphic types, that is types that depend in a uniform +and effective way on other types. This form of polymorphism (sometimes +called {\em parametric} polymporphism to distinguish it from the +{\em ad hoc} polymorphism +typical of object oriented languages) is a major feature of modern +functional programming languages: in many intersting cases, +it allows to write {\em generic} functions operating on inputs without +depending on their type. Typical examples can be found on lists. +For instance, appending two lists is an operation that is essentially +independent from the type $A$ of the elements in the list, and we would like +to write a {\em single} append function working parametrically on $A$. + +The first step is to define a type for lists polimorphic over the +type $A$ of its elements: +\begin{lstlisting}[language=grafite] +inductive list (A:Type[0]) : Type[0] := + | nil: list A + | cons: A -> list A -> list A. +\end{lstlisting} +The deinition should be clear: a list is either empty (\verb+nil+) or +is is obtained by concatenating (\verb+cons+) an element of type $A$ +to a given list. In other word, the type of lists is the smallest inductive +type generated by the two constructors \verb+nil+ and \verb+cons+. + +The first element of a list is called its {\em head}. If the list +is empty the head is undefined: as discussed in the previous section, +we should either return a ``default'' +element, or decide to return an option type. +We have an additional complication in this +case, since the ``default'' element should have type $A$ (as the head), +and we know nothing about $A$ (it could even be an empty type!). We +have no way to guess a canonical element, and the only +possibility (along this approach) is to take it in input. These +are the two options: +\begin{lstlisting}[language=grafite] +definition hd ≝ λA.λl: list A.λd:A. + match l with [ nil ⇒ d | cons a _ ⇒ a]. + +definition option_hd ≝ + λA.λl:list A. match l with + [ nil ⇒ None ? + | cons a _ ⇒ Some ? a ]. +\end{lstlisting} +What remains of a list after removing its head is called the {\em tail} +of the list. Again, the tail of an empty list is undefined, but in +this case the result must be a list, and we have a canonical inhabitant +of lists, that is the empty list. So, it is natural to extend the +definition of tail saying that the tail of nil is nil (that is +very similar to say that the predecessor of $0$ is $0$): +\begin{lstlisting}[language=grafite] +definition tail ≝ λA.λl: list A. + match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. +\end{lstlisting} + +Using destruct, it is easy to prove that \verb+cons+ is injective +in both arguments. +\begin{lstlisting}[language=grafite] +lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2. +#A #a1 #a2 #l1 #l2 #Heq destruct // qed. + +lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2. +#A #a1 #a2 #l1 #l2 #Heq destruct // qed. +\end{lstlisting} +The append function is defined by recursion over the first list: +\begin{lstlisting}[language=grafite] +let rec append A (l1: list A) l2 on l1 ≝ match l1 with + [ nil ⇒ l2 + | cons hd tl ⇒ hd :: append A tl l2 ]. +\end{lstlisting} +We leave to the reader to prove that \verb+append+ is associative, and +that \verb+nil+ is a neutral element for it. + +\input{list_notation.tex} + +We conclude this section discussing another important operation +over lists, namely the reverse funtion, retrurning +a list with the same elements of the original list but in reverse order. + +One could define the revert operation as follows: +\begin{lstlisting}[language=grafite] +let rec rev S l1 on l1 ≝ + match l1 with + [ nil ⇒ nil + | cons a tl ⇒ rev A tl @ [a] + ]. +\end{lstlisting} +However, this implementation is sligtly inefficient, since it has a +quadratic complexity. +A better solution consists in exploiting an accumulator, passing through +the following auxilary function: +\begin{lstlisting}[language=grafite] +let rec rev_append S (l1,l2:list S) on l1 ≝ + match l1 with [ nil ⇒ l2 - | cons a tl ⇒ - let r ≝ unique_append S tl l2 in - if memb S a r then r else a::r + | cons a tl ⇒ rev_append S tl (a::l2) ]. -lemma memb_unique_append: ∀S,a,l1,l2. - memb S a (unique_append S l1 l2) = true → memb S a l1= true ∨ memb S a l2 = true. -#S #a #l1 elim l1 normalize [#l2 #H %2 //] -#b #tl #Hind #l2 cases (true_or_false … (a==b)) #Hab >Hab normalize /2/ -cases (memb S b (unique_append S tl l2)) normalize - [@Hind | >Hab normalize @Hind] -qed. - -lemma unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. - (∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) → - ∀x. memb S x (unique_append S l1 l2) = true → P x. -#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/ -qed. - -lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true → - uniqueb S (unique_append S l1 l2) = true. -#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2 -cases (true_or_false … (memb S a (unique_append S tl l2))) -#H >H normalize [@Hind //] >H normalize @Hind // -qed. - -(* -Sublists - -*) -definition sublist ≝ - λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true. - -lemma sublist_length: ∀S,l1,l2. - uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|. -#S #l1 elim l1 // -#a #tl #Hind #l2 #unique #sub -cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //] -* #l3 * #l4 #eql2 >eql2 >length_append normalize -applyS le_S_S eql2 in sub; #sub #x #membx -cases (memb_append … (sub x (orb_true_r2 … membx))) - [#membxl3 @memb_append_l1 // - |#membxal4 cases (orb_true_l … membxal4) - [#eqxa @False_ind lapply (andb_true_l … unique) - <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 // - ] - ] -qed. - -lemma sublist_unique_append_l1: - ∀S,l1,l2. sublist S l1 (unique_append S l1 l2). -#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/] -#x #tl #Hind #l2 #a -normalize cases (true_or_false … (a==x)) #eqax >eqax -[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2))) - [#H >H normalize // | #H >H normalize >(\b (refl … a)) //] -|cases (memb S x (unique_append S tl l2)) normalize - [/2/ |>eqax normalize /2/] -] -qed. - -lemma sublist_unique_append_l2: - ∀S,l1,l2. sublist S l2 (unique_append S l1 l2). -#S #l1 elim l1 [normalize //] #x #tl #Hind normalize -#l2 #a cases (memb S x (unique_append S tl l2)) normalize -[@Hind | cases (a==x) normalize // @Hind] -qed. - -lemma decidable_sublist:∀S,l1,l2. - (sublist S l1 l2) ∨ ¬(sublist S l1 l2). -#S #l1 #l2 elim l1 - [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/ - |#a #tl * #subtl - [cases (true_or_false (memb S a l2)) #memba - [%1 whd #x #membx cases (orb_true_l … membx) - [#eqax >(\P eqax) // |@subtl] - |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd - ] - |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons // - ] - ] -qed. - -(* -Filtering -*) - -lemma memb_filter_true: ∀S,f,a,l. - memb S a (filter S f l) = true → f a = true. -#S #f #a #l elim l [normalize #H @False_ind /2/] -#b #tl #Hind cases (true_or_false (f b)) #H -normalize >H normalize [2:@Hind] -cases (true_or_false (a==b)) #eqab - [#_ >(\P eqab) // | >eqab normalize @Hind] -qed. - -lemma memb_filter_memb: ∀S,f,a,l. - memb S a (filter S f l) = true → memb S a l = true. -#S #f #a #l elim l [normalize //] -#b #tl #Hind normalize (cases (f b)) normalize -cases (a==b) normalize // @Hind +definition reverse ≝λS.λl.rev_append S l []. +\end{lstlisting} + +{\bf Exercise} Prove the following results: +\begin{lstlisting}[language=grafite] +lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a]. + +lemma reverse_append: ∀S,l1,l2. + reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1). + +lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l. +\end{lstlisting} + + +\subsection{List iterators} +In general, an iterator for some data type is an object that enables to +traverse its structure performing a given computation. +There is a canonical set of iterators over lists deriving from +the programming experience. In this section we shall review a few of +them, proving some of their properties. + +A first, famous iterator is the map function, that +applies a function $f$ to each element of a list $[a_1,\dots , a_n]$, +building the list $[f\,a_1; \dots ; f\,a_n]$. +\begin{lstlisting}[language=grafite] +let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ + match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. +\end{lstlisting} +The \verb+map+ function distributes over \verb+append+, as can be simply +proved by induction over the first list: +\begin{lstlisting}[language=grafite] +lemma map_append : ∀A,B,f,l1,l2. + (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). +#A #B #f #l1 elim l1 + [ #l2 @refl | #h #t #IH #l2 normalize // ] qed. +\end{lstlisting} +The most important itarator is traditionally called {\em fold}; we +shall only consider the so called fold-right variant, +that takes in input a function $f:A\to B \to B$, a list $[a_1; \dots; a_n]$ +of elements of type $A$, a base element $b:B$ and returns +the value $f\,a_1\,(f\,a_2\,(\dots (f\,a_n\,b) \dots))$. +\begin{lstlisting}[language=grafite] +let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ + match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)]. +\end{lstlisting} +Many other interesting functions can be defined in terms of \verb+foldr+. +A first interesting example is the filter function, taking in input +a boolean test \verb+p+ and a list $l$ and returning the sublist of all +elements of $l$ satisfying the test. +\begin{lstlisting}[language=grafite] +definition filter ≝ + λT.λp:T → bool. + foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T). +\end{lstlisting} +As another example, we can generalize the map function to an operation +taking in input a binary function $f:A\to B \to C$, two lists +$[a_1;\dots ;a_n]$ and $[b_1;\dots ;b_m]$ and returning the list +$[f\,a_1\,b_1; \dots ;f\,a_n\,b_1;\dots ;f\,a_1\,b_m; f\,a_n\,b_m]$ +\begin{lstlisting}[language=grafite] +definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2. + foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1. +\end{lstlisting} +The folded function $\lambda$\verb+i,acc.(map ?? (f i) l2)@acc+ +takes in input an element $i$ and an accumulator, +and add to the accumulator the values obtained by mapping the +partial instantiation $f\,i$ on the elements of $l_2$. This function +is iterated over +all elements of the first list $l_1$, starting with an empty accumulator. + +\subsection{Naive Set Theory} +Given a ``universe'' $U$ (an arbitrary type $U:Type$), a naive but +practical way to deal with ``sets'' in $U$ is simply to identify +them with their characteristic property, that is to as functions +of type $U\to \mbox{Prop}$. + +For instance, the empty set is defined by the False predicate; +a singleton set $\{x\}$ is defined by the property that its elements are +equal to $x$. + +\begin{lstlisting}[language=grafite] +definition empty_set ≝ λU:Type[0].λu:U.False. +definition singleton ≝ λU.λx,u:U.x=u. +\end{lstlisting} + +The membership relation is trivial: an element $x$ is in the set +(defined by the property) $P$ if and only if it enjoyes the property: + +\begin{lstlisting}[language=grafite] +definition member ≝ λU:Type[0].λu:U.P→Prop:U.P u. +\end{lstlisting} +The operations of union, intersection, complementation and substraction +are defined in a straightforward way, in terms of logical operations: + +\begin{lstlisting}[language=grafite] +definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a. + +definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa..P a ∧ Q a. + +definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w. + +definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w. +\end{lstlisting} +More interesting are the notions of subset and equality. Given +two sets $P$ and $Q$, $P$ is a subset of $Q$ when any element $u$ in +$P$ is also in $Q$, that is when $P\,u$ implies $Q\,u$. +\begin{lstlisting}[language=grafite] +definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a). +\end{lstlisting} +Then, two sets $P$ and $Q$ are equal when $P \subseteq Q$ and +$Q \subseteq P$, or equivalently when for any element $u$, +$P\,u \iff Q\,u$. +\begin{lstlisting}[language=grafite] +definition eqP ≝ λA:Type.λP,Q:A → Prop.∀a:A.P a ↔ Q a. +\end{lstlisting} +We shall use the infix notation $\approx$ for the previous notion of +equality. +It is important to observe that the \verb+eqP+ is +different from Leibniz equality of section \ref{}. As we already +observed, Leibniz equality is a pretty syntactical (or intensional) +notion, that is a notion concerning the {\em connotation} of an object +and not its {\em denotation} (the shape assumed by the object, and +not the information it is supposed to convey). Intensionality stands +in contrast with {\em extensionality}, referring to principles that +judge objects to be equal if they enjoy {\em a given subset} of external, +observable properties (e.g. the property of having the same +elements). For instance given two sets $A$ and $B$ we can prove that +$A\cup B \approx B\cup A$, since they have the same elements, but +there is no way to prove $A\cup B = B\cup A$. + +The main practical consequence is that, while we can always exploit +a Leibniz equality between two terms $t_1$ and $t_2$ for rewriting +one into the other (in fact, this is the {\em essence} of Leibniz +equality), we cannot do the same for an extensional equality (we +could only rewrite inside propositions ``compatible'' with our +external observation of the objects). + +\subsection{Sets with decidable equality} +We say that a property $P:A\to Prop$ over a datatype $A$ +is {\em decidable} when we have an +effective way to assess the validity of $P\,a$ for any +$a:A$. As a consequence +of G\"odel incompleteness theorem, not every predicate +is decidable: for instance, extensional equality on sets is not decidable, +in general. + +Decidability can be expressed in several possible ways. A convenient +one is to state it in terms of the computability of the characterisitc +function of the predicate $P$, that is in terms of the existence of a +function $Pb: A \to \mbox{bool}$ such that + \[P\,a \iff Pb\,a = \mbox{true}\] +Decidability is an important issue, and since equality is an essential +predicate, it is always interesting to try to understand when a given +notion of equality is decidable or not. + +In particular, Leibniz equality on inductively generated datastructures +is often decidable, since we can simply write a decision algorithm by +structural induction on the terms. For instance we can define +characteristic functions for booleans and natural numbers in the following +way: +\begin{lstlisting}[language=grafite] +definition beqb ≝ λb1,b2. + match b1 with [ true ⇒ b2 | false ⇒ notb b2]. + +let rec neqb n m ≝ +match n with + [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] + | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] + ]. +\end{lstlisting} +It is so important to know if Leibniz equality for a given type is decidable +that turns out to be convenient to pack this information into a single +algebraic datastructure, called \verb+DeqSet+: +\begin{lstlisting}[language=grafite] +record DeqSet : Type[1] ≝ + { carr :> Type[0]; + eqb: carr → carr → bool; + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}. + +notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. +interpretation "eqb" 'eqb a b = (eqb ? a b). +\end{lstlisting} +A \verb+DeqSet+ is simply a record composed by a carrier type \verb+carr+, +a boolean function \verb+eqb: carr+$\to$\verb+carr+$\to$\verb+carr+ representing +the decision algorithm, and a {\em proof} \verb+eqb_true+ that the decision algorithm +is correct. The \verb+:>+ symbol declares \verb+carr+ as a {\em coercion} from a DeqSet to its +carrier type. We use the infix notation ``=='' for the decidable +equality \verb+eqb+ of the carrier. + +Suppose we proved the following facts (do it as an exercise) +\begin{lstlisting}[language=grafite] +lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2. +lemma neqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m. +\end{lstlisting} +Then, we can build the following records: +\begin{lstlisting}[language=grafite] +definition DeqBool ≝ mk_DeqSet bool beqb beqb_true_to_eq. +definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true. +\end{lstlisting} +Note that, since we declare a coercion from the \verb+DeqSet+ to its +carrier, the expression \verb+0:DeqNat+ is well typed, and it is understood +by the system as \verb+0:carr DeqNat+ (that is, coercions are automatically +insterted by the system, if required). + +%It is convenient to have a simple way to {\em reflect} \cite{ssreflect} +%a proof of +%$(eqb\;x\;y = true)$ into a proof of $(x = y)$; we use the two operators +%$\mathit{\\P}$ and $\mathit{\\b}$ to this aim. + +\subsection{Unification hints} +Suppose now to write an expression of the following kind: +\[b == \mbox{false}\] +that, after removing the notation, is equivalent to +\[eqb\;?\;b\;\mbox{false}\] +The system knows that $\mbox{false}$ is a boolean, so in order to +accept the expression, he should {\em figure out} some \verb+DeqSet+ +having \verb+bool+ +as carrier. This is not a trivial operation: Matita should either try +to synthetize it (that is a complex operation known as {\em narrowing}) +or look into its database of results for a possible solution. + +In this situations, we may suggest the intended solution to Matita using +the mechanism of unification hints \cite{hints}. The concrete syntax +of unification hints is a bit involved: we strongly recommend the user +to include the file \verb+hints_declaration.ma+ that allows you +to write thing in a more convenient and readable way. +\begin{lstlisting}[language=grafite] +include ``hints_declaration.ma''. +\end{lstlisting} +For instance, the following declaration tells Matita that a solution +of the equation \verb+bool = carr X+ is $X = DeqBool$. +\begin{lstlisting}[language=grafite] +unification hint 0 ≔ ; + X ≟ DeqBool +(* ---------------------------------------- *) ⊢ + bool ≡ carr X. +\end{lstlisting} +Using the previous notation (we suggest the reader to cut and paste it +from previous hints) the hint is expressed as an inference rule. +The conclusion of the rule is the unification problem that we intend to solve, +containing one or more variables $X_1,\dots X_b$. The premises of +the rule are the solutions we are suggesting to Matita. In general, +unification hints should only be used when there exists just one +``intended'' (canonical) solution for the given equation. +When you declare a unification hint, Matita verifies it correctness by +instantiating the unification problem with the hinted solution, +and checking the convertibility between the two sides of the equation. +\begin{lstlisting}[language=grafite] +example exhint: ∀b:bool. (b == false) = true → b = false. +#b #H @(\P H). qed. +\end{lstlisting} +In a similar way, + +\begin{lstlisting}[language=grafite] +unification hint 0 ≔ b1,b2:bool; + X ≟ mk_DeqSet bool beqb beqb_true +(* ---------------------------------------- *) ⊢ + beqb b1 b2 ≡ eqb X b1 b2. +\end{lstlisting} + + +\subsection{Prop vs. bool} +It is probably time to make a discussion about \verb+Prop+ and \verb+bool+, and +their different roles in a the Calculus of Inductive Constructions. + +Inhabitants of the sort \verb+Prop+ are logical propositions. In turn, logical +propositions \verb+P:Prop+ can be inhabitated by their proofs $H:P$. Since, in +general, the validity of a property $P$is not decidable, the role of the +proof is to provide a witness of the correctness of $P$ that the system can +automatically check. + +On the other hand, bool is just an inductive datatype with two constructors true +and false: these are terms, not types, and cannot be inhabited. +Logical connectives on bool are computable functions, defined by their +truth tables, using case analysis. -lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → -memb S x l = true ∧ (f x = true). -/3/ qed. - -lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true → -memb S x (filter ? f l) = true. -#S #f #x #l #fx elim l normalize // -#b #tl #Hind cases (true_or_false (x==b)) #eqxb - [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize // - |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind] - ] -qed. - -(* -Exists - -*) - -let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ -match l with -[ nil ⇒ false -| cons h t ⇒ orb (p h) (exists A p t) -]. \ No newline at end of file + Prop and bool are, in a sense, complementary: the former is more suited for +abstract logical reasoning, +while the latter allows, in some situations, for brute-force evaluation. +Suppose for instance that we wish to prove that the $2 \le 3!$. Starting +from the definition of the factorial function and properties of the less +or equal relation, the previous proof could take several steps. Suppose +however we proved the decidability of $\le$, that is the existence of +a boolean function $\mbox{leb}$ reflecting $\le$ in the sense that +\[n \le m \iff \mbox{leb}\,n,m = \mbox{true}\] +Then, we could reduce the verification of $2 \le 3!$ to that of +of $\mbox{leb}\,2,3! = \mbox{true}$ that just requires a mere computation! + +\subsection{Finite Sets} +A finite set is a record consisting of a DeqSet $A$, +a list of elements of type A enumerating all the elements of the set, +and the proofs that the enumeration does not contain repetitions +and is complete (\verb+memb+ is the membership operation on +lists, defined in the obvious way, and the question mark is an {\em +implicit parameter} automatically filled in by the system). +\begin{lstlisting}[language=grafite] +record FinSet : ≝ +{ FinSetcarr:> DeqSet; + enum: list FinSetcarr; + enum_unique: uniqueb FinSetcarr enum = true; + enum_complete : ∀x:FinSetcarr. memb ? x enum = true}. +\end{lstlisting} +The library provides many operations for building new \verb+FinSet+s by +composing +existing ones: for example, +if \verb+A+ and \verb+B+ have type \verb+FinSet+, then +also \verb+option A+, \verb+A+$\times$\verb+B+, +\verb+A+$\oplus$\verb+B+ are finite sets. In all these cases, unification +hints are used to suggest the {\em intended} finite set structure +associated with them, that makes their use quite transparent to the user. + +A particularly intersting case is that of the arrow type \verb+A+$\to$\verb+B+. +We may define the graph of \verb+f:A+$\to$\verb+B+, as the +set (sigma type) of all pairs $\langle a,b \rangle$ such that +$f (a) = b$. +\begin{lstlisting}[language=grafite] +definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (\fst p) = \snd p. +\end{lstlisting} +In case the equality is decidable, we may effectively +enumerate all elements of the graph by simply filtering from +pairs in \verb+A+$\times$\verb+B+ those satisfying the +test $\lambda$\verb+p.f (\fst p) == \snd p)+: + +\begin{lstlisting}[language=grafite] +definition graph_enum ≝ λA,B:FinSet.λf:A→B. + filter ? (λp.f (\fst p) == \snd p) (enum (FinProd A B)). +\end{lstlisting} +The proofs that this enumeration does not contain repetitions and +is complete are straightforward. + +\subsection{Vectors} +A vector of length $n$ of elements of type $A$ +is simply defined in Matita as a record composed +by a list of elements of type $A$, plus a proof that the +list has the expected length. Vectors are a paradigmatic example +of {\em dependent} type, that is of a type whose definition depends on +a term. +\begin{lstlisting}[language=grafite] +record Vector (A:Type) (n:nat): Type ≝ +{ vec :> list A; + len: length ? vec = n }. +\end{lstlisting} +Given a list $l$ we may trivially turn it into a vector of length $|l|$; +we just need to prove that $|l|=|l|$ that follows from the reflexivity +of equality. +\begin{lstlisting}[language=grafite] +lemma Vector_of_list ≝ λA,l.mk_Vector A (|l|) l (refl ??). +\end{lstlisting} + +Most functions operating on lists can be naturally extended to +vectors: interesting cases are \verb+vec_append+, concatenating vectors, +and \verb+vec_map+, mapping a function $f$ on all elements of the input +vector and returning a vector of the same dimension of the input one. + +Since a vector is automatically coerced, if needed, to the list of +its elements, we may simply use typical functions over lists (such as +\verb+nth+) to extract/filter specific components. + +The function \verb+change_vec A n v a i+ replaces the content of +the vector $v$ at position $i$ with the value $a$. + +The most frequent operation on vectors for the purposes or our work +is their comparison. In this case, we have essentially two possible +approaches: we may proceed component-wise, using the following lemma +\begin{lstlisting}[language=grafite] +lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d. + (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2. +\end{lstlisting} +or alternatively we may manipulate vectors exploiting the commutation +or idempotency of \verb+change_vec+ and its interplay with +other operations.