From: Andrea Asperti Date: Sun, 10 Mar 2013 14:08:14 +0000 (+0000) Subject: chapters 2 e 3 X-Git-Tag: make_still_working~1225 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9245402674a791dfdb943902f8288d742088c854;p=helm.git chapters 2 e 3 --- diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma index 7dda6e6f2..14ae1b679 100644 --- a/matita/matita/lib/tutorial/chapter2.ma +++ b/matita/matita/lib/tutorial/chapter2.ma @@ -26,12 +26,14 @@ ones you received in input. Most mathematical functions can be naturally defined in this way. For instance, the sum of two natural numbers can be defined as follows: *) -let rec add n m ≝ +let rec add n (m:nat) ≝ match n with [ O ⇒ m -| S a ⇒ S (add a m) +| S a ⇒ add (S a) m ]. +check + (* Observe that the definition of a recursive function requires the keyword "let rec" instead of "definition". The specification of formal parameters is different too. In this case, they come before the body, and do not require a λ. diff --git a/matita/matita/lib/tutorial/chapter3.ma b/matita/matita/lib/tutorial/chapter3.ma index a6a05a7b6..e427482a4 100644 --- a/matita/matita/lib/tutorial/chapter3.ma +++ b/matita/matita/lib/tutorial/chapter3.ma @@ -1,338 +1,584 @@ (* -Polymorphism and Higher Order + EVERYTHING IS AN INDUCTIVE TYPE +*) + +include "basics/pts.ma". + +(* As we mentioned several times, very few notions are really primitive in +Matita: one of them is the notion of universal quantification (or dependent +product type) and the other one is the notion of inductive type. Even the arrow +type A → B is not really primitive: it can be seen as a particular case of the +dependent product ∀x:A.B in the degenerate case when B does not depends on x. +All the other familiar logical connectives - conjunction, disjunction, negation, +existential quantification, even equality - can be defined as particular +inductive types. + We shall look at these definitions in this section, since it can be useful to +acquire confidence with inductive types, and to get a better theoretical grasp +over them. +*) +(******************************* Conjunction **********************************) + +(* In natural deduction, logical rules for connectives are divided in two +groups: there are introduction rules, allowing us to introduce a logical +connective in the conclusion, and there are elimination rules, describing how to +de-construct information about a compound proposition into information about its +constituents (that,is, how to use an hypothesis having a given connective as its +principal operator). + +Consider conjunction. In order to understand the introduction rule for +conjunction, you should answer the question: how can we prove A∧B? The answer is +simple: we must prove both A and B. Hence the introduction rule for conjunction +is A → B → A∧B. + +The general idea for defining a logical connective as an inductive type is +simply to define it as the smallest proposition generated by its introduction +rule(s). + +For instance, in the case of conjunction, we have the following definition: *) + +inductive And (A,B:Prop) : Prop ≝ + conj : A → B → And A B. + +(* The corresponding elimination rule is induced by minimality: if we have a +proof of A∧B it may only derive from the conjunction of a proof of A and a proof +of B. A possible way to formally express the elimination rule is the following: + + And_elim: ∀A,B,P:Prop. (A → B → P) → A∧B → P + +that is, for all A and B, and for any proposition P if we need to prove P under +the assumption A∧B, we can reduce it to prove P under the pair of assumptions A +and B. + +It is interesting to observe that the elimination rule can be easily derived +from the introduction rule in a completely syntactical way. +Basically, the general structure of the (non recursive, non dependent) +elimination rule for an inductive type T is the following + + ∀A1,… An.∀P:Prop. C1 → … → Cn → T → P + +where A1, … An are the parameters of the inductive type, and every Ci is derived +from the type Ti of a constructor ci of T by just replacing T with P in it. For +instance, in the case of the conjunction we only have one constructor of type +A → B → A∧B and replacing A∧B with P we get C = A \to B \to P. + +Every time we declare a new inductive proposition or type T, Matita +automatically generates an axiom called T\_ind that embodies the elimination +principle for this type. The actual shape of the elimination axiom is sensibly +more complex of the one described above, since it also takes into account the +possibility that the predicate P depends over the term of the given inductive +type (and possible arguments of the inductive type). +We shall discuss the general case in Section ??. + +Actually, the elimination tactic elim for an element of type T is a +straightforward wrapper that applies the suitable elimination axiom. +Let us see this in action on a simple lemma. Suppose we want to prove the +following trivial result: *) -include "tutorial/chapter2.ma". -include "basics/bool.ma". - -(* Matita supports polymorphic data types. The most typical case are polymorphic -lists, parametric in the type of their elements: *) - -inductive list (A:Type[0]) : Type[0] ≝ - | nil: list A - | cons: A -> list A -> list A. - -(* The type notation list A is the type of all lists with elements of type A: -it is defined by two constructors: a polymorphic empty list (nil A) and a cons -operation, adding a new head element of type A to a previous list. For instance, -(list nat) and and (list bool) are lists of natural numbers and booleans, -respectively. But we can also form more complex data types, like -(list (list (nat → nat))), that is a list whose elements are lists of functions -from natural numbers to natural numbers. - -Typical elements in (list bool) are for instance, - nil nat - the empty list of type nat - cons nat true (nil nat) - the list containing true - cons nat false (cons nat (true (nil nat))) - the list containing false and true -and so on. - -Note that both constructos nil and cons are expecting in input the type parameter: -in this case, bool. +lemma And_left: ∀A,B:Prop. And A B →A. +(* After introducing A and B we could decompose with * the hypothesis A∧B to +get the two premises A and B and use the former to close the goal, as expressed +by the following commands + #A #B * // qed. +However, a viable alternative is to explicitly apply the elimination principle: *) +#A #B @And_ind // qed. -(* -Defining your own notation -We now add a bit of notation, in order to make the syntax more readable. In -particular, we would like to write [] instead of (nil A) and a::l instead of -(cons A a l), leaving the system the burden to infer A, whenever possible. -*) +(********************************* Disjunction ********************************) + +(* Let us apply the previous methodology to other connectives, starting with +disjunction. The first point is to derive the introduction rule(s). When can we +conclude A∨B? Clearly, we must either have a proof of A, or a proof of B. So, we +have two introduction rules, in this case: + A → A∨B and + B → A∨B +that leads us to the following inductive definition of disjunction: *) -notation "hvbox(hd break :: tl)" - right associative with precedence 47 - for @{'cons $hd $tl}. +inductive Or (A,B:Prop) : Prop ≝ + or_introl : A → Or A B + | or_intror : B → Or A B. + +(* The elimination principle, automatically generated by the system is -notation "[ list0 x sep ; ]" - non associative with precedence 90 - for ${fold right @'nil rec acc @{'cons $x $acc}}. + or_ind: ∀A,B,P:Prop. (A → P) → (B → P) → A∨B → P + +that is a traditional formulation of the elimination rule for the logical +disjunction in natural deduction: if P follows from both A and B, then it also +follows from their disjunction. *) -notation "hvbox(l1 break @ l2)" - right associative with precedence 47 - for @{'append $l1 $l2 }. +(************************************ False ***********************************) -interpretation "nil" 'nil = (nil ?). -interpretation "cons" 'cons hd tl = (cons ? hd tl). +(* More surprisingly, we can apply the same methodology to define the constant +False. The point is that, obviously, there is no (canonical) way to conclude +False: so we have no introduction rule, and we must define an inductive type +without constructors, that is accepted by the system. *) -(* -Basic operations on lists +inductive False: Prop ≝ . -Let us define a few basic functions over lists. Our first example is the -append function, concatenating two lists l1 and l2. The natural way is to proceed -by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl -then we recursively append tl and l2 , and then add hd as first element. Note that -the append function itself is polymorphic, and the first argument it takes in input -is the type A of the elements of two lists l1 and l2. -Moreover, since the append function takes in input several parameters, we must also -specify in the its defintion on which one of them we are recurring: in this case l1. -If not othewise specified, recursion is supposed to act on the first argument of the -function.*) +(* The elimination principle is in this case -let rec append A (l1: list A) l2 on l1 ≝ - match l1 with - [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. + False_ind: ∀P:Prop.False → P + +that is the well known principle of explosion: ``ex falso quodlibet''. *) -interpretation "append" 'append l1 l2 = (append ? l1 l2). +(************************************ True ************************************) -(* As usual, the function is executable. For instance, (append A nil l) reduces to -l, as shown by the following example: *) - -example nil_append: ∀A.∀l:list A. [] @ l = l. -#A #l normalize // qed. - -(* Proving that l @ [] = l is just a bit more complex. The situation is exactly -the same as for the addition operation of the previous chapter: since append is -defined by recutsion over the first argument, the computation of l @ [] is stuck, -and we must proceed by induction on l *) - -lemma append_nil: ∀A.∀l:list A.l @ [] = l. -#A #l (elim l) normalize // qed. +(* What about True? You may always conclude True, hence the corresponding +inductive definition just has one trivial constructor, traditionally named I: *) -(* similarly, we can define the two functions head and tail. Since we can only define -total functions, we should decide what to do in case the input list is empty. -For tl, it is natural to return the empty list; for hd, we take in input a default -element d of type A to return in this case. *) - -definition head ≝ λA.λl: list A.λd:A. - match l with [ nil ⇒ d | cons a _ ⇒ a]. +inductive True: Prop ≝ I : True. -definition tail ≝ λA.λl: list A. - match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. - -example ex_head: ∀A.∀a,d,l. head A (a::l) d = a. -#A #a #d #l normalize // qed. - -example ex_tail: tail ? (cons ? true []) = []. -normalize // qed. - -theorem associative_append: -∀A.∀l1,l2,l3: list A. (l1 @ l2) @ l3 = l1 @ (l2 @ l3). -#A #l1 #l2 #l3 (elim l1) normalize // qed. - -(* Problemi con la notazione *) -lemma a_append: ∀A.∀a.∀l:list A. (a::[]) @ l = a::l. -// qed. - -theorem append_cons: -∀A.∀a:A.∀l,l1: list A.l@(a::l1)= (l @ (cons ? a [])) @ l1. -// qed. - -(* Other typical functions over lists are those computing the length -of a list, and the function returning the nth element *) - -let rec length (A:Type[0]) (l:list A) on l ≝ -match l with - [ nil ⇒ O - | cons a tl ⇒ S (length A tl)]. - -let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ - match n with - [O ⇒ head A l d - |S m ⇒ nth m A (tail A l) d]. - -example ex_length: length ? (cons ? O []) = S O. -normalize // qed. - -example ex_nth: nth (S O) ? (cons ? (S O) (cons ? O [])) O = O. -normalize // qed. - -(* Proving that the length of l1@l2 is the sum of the lengths of l1 -and l2 just requires a trivial induction on the first list. *) - - lemma length_add: ∀A.∀l1,l2:list A. - length ? (l1@l2) = add (length ? l1) (length ? l2). -#A #l1 elim l1 normalize // qed. - -(* -Comparing Costructors - -Let us come to a more interesting question. How can we prove that the empty -list is different from any list with at least one element, that is from any list -of the kind (a::l)? We start defining a simple predicate stating if a list is -empty or not. The predicate is computed by inspection over the list *) - -definition is_nil: ∀A:Type[0].list A → Prop ≝ -λA.λl.match l with [ nil ⇒ l = [] | cons hd tl ⇒ (l ≠ [])]. - -(* Next we need a simple result about negation: if you wish to prove ¬P you are -authorized to add P to your hypothesis: *) - -lemma neg_aux : ∀P:Prop. (P → ¬P) → ¬P. -#P #PtonegP % /3/ qed. - -theorem diff_cons_nil: -∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. -#A #l #a @neg_aux #Heq -(* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux. -Next we use the change tactic to pass from the current goal a::l≠ [] to the -expression is_nil a::l, convertible with it. *) -(change with (is_nil ? (a::l))) -(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial -goal [] = [] *) ->Heq // qed. +(* As expected, the elimination rule is not informative in this case: the only +way to conclude P from True is to prove P: -(* As an application of the previous result let us prove that l1@l2 is empty if -and only if both l1 and l2 are empty. -The idea is to proceed by cases on l1: if l1=[] the statement is trivial; on the -other side, if l1 = a::tl, then the hypothesis (a::tl)@l2 = [] is absurd, hence we -can prove anything from it. -When we know we can prove both A and ¬A, a sensible way to proceed is to apply -False_ind: ∀P.False → P to the current goal, that breaks down to prove False, and -then absurd: ∀A:Prop. A → ¬A → False to reduce to the contradictory cases. -Usually, you may invoke automation to take care to solve the absurd case. *) - -lemma nil_to_nil: ∀A.∀l1,l2:list A. - l1@l2 = [] → l1 = [] ∧ l2 = []. -#A #l1 cases l1 normalize /2/ #a #tl #l2 #H @False_ind /2/ qed. - -(* -Higher Order Functionals - -Let us come to some important, higher order, polymorphic functionals -acting over lists. A typical example is the map function, taking a function -f:A → B, a list l = [a1; a2; ... ; an] and returning the list -[f a1; f a2; ... ; f an]. *) - -let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ - match l with [ nil ⇒ [] | cons x tl ⇒ f x :: (map A B f tl)]. - -(* Another major example is the fold function, that taken a list -l = [a1; a2; ... ;an], a base value b:B, and a function f: A → B → B returns -(f a1 (f a2 (... (f an b)...))). *) - -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)]. - -(* As an example of application of foldr, let us use it to define a filter -function that given a list l: list A and a boolean test p:A → bool returns the -sublist of elements satisfying the test. In this case, the result type B of -foldr should be (list A), the base value is [], and f: A → list A →list A is -the function that taken x and l returns x::l, if x satisfies the test, and l -otherwise. We use an if_then_else function included from bool.ma to this purpose. *) - -definition filter ≝ - λT.λp:T → bool. - foldr T (list T) (λx,l0. if p x then x::l0 else l0) []. - -(* Here are a couple of simple lemmas on the behaviour of the filter function. -It is often convenient to state such lemmas, in order to be able to use rewriting -as an alternative to reduction in proofs: reduction is a bit difficult to control. + True_ind: ∀P:Prop.P → True → P *) -lemma filter_true : ∀A,l,a,p. p a = true → - filter A p (a::l) = a :: filter A p l. -#A #l #a #p #pa (elim l) normalize >pa // qed. +(******************************** Existential *********************************) + +(* Finally, let us consider the case of existential quantification. In order to +conclude ∃x:A.Q x we need to prove Q a for some term a:A. Hence, the +introduction rule for the existential looks like the following: + + ∀a:A. Q a → ∃x.Q x + +from which we get the following inductive definition, parametric in A and Q: *) + +inductive ex (A:Type[0]) (Q:A → Prop) : Prop ≝ + ex_intro: ∀x:A. Q x → ex A Q. + +(* The elimination principle automatically generated by Matita is + + ex_ind: ∀A.∀Q:A→Prop.∀P:Prop. (∀x:A. Q x → P) → ∃x:A.Q → P + +That is, if we know that P is a consequence of Q x for any x:A, then it is +enough to know ∃x:A.Q x to conclude P. It is also worth to spell out the +backward reading of the previous principle. +Suppose we need to prove P under the assumption ∃x:A.Q. Then, eliminating the +latter amounts to assume the existence of x:A such that Q\; x and proceed +proving P under these new assumptions. *) + +(****************************** A bit of notation *****************************) + +(* Since we make a frequent use of logical connectives and quantifiers, it would +be nice to have the possibility to use a more familiar-looking notation for +them. As a matter of fact, Matita offers you the possibility to associate your +own notation to any notion you define. + +To exploit the natural overloading of notation typical of scientific literature, +its management is splitted in two steps, in Matita: one from presentation level +to content level, where we associate a notation to a fragment of abstract +syntax, and one from content level to term level, where we provide (possibly +multiple) interpretations for the abstract syntax. + +The mapping between the presentation level (i.e. what is typed on the keyboard +and what is displayed in the sequent window) and the content level is defined +with the "notation" command. When followed by >, it defines an input (only) +notation (that is, used in parsing but not in pretty printing). *) + +notation "hvbox(a break \land b)" + left associative with precedence 35 for @{ 'and $a $b }. + +(* This declaration associates the infix notation "a \lanb b" - rendered a ∧ b +by the UTF-8 graphical facilities - with an abstract syntax tree composed by the +new symbol 'and applied to the result of the parsing of input argument a and b. + +The presentation pattern is always enclosed in double quotes. The special +keyword "break" indicates the breaking point and the box schema hvbox indicates +a horizontal or vertical layout, according to the available space for the +rendering (they can be safely ignored for the scope of this tutorial). + +The content pattern begins right after the for keyword and extends to the end of +the declaration. Parts of the pattern surrounded by @{… } denote verbatim +content fragments, those surrounded by ${… }$ denote meta-operators and +meta-variables (for example $a) referring to the meta-variables occurring in +the presentation pattern. + +The declaration also instructs the system that the notation is supposed to be +left associative and provides information about the syntactical precedence of +the operator, that governs the way an expression with different operators is +interpreted by the system. +For instance, suppose we declare the logical disjunction at a lower precedence: +*) + +notation "hvbox(a break \lor b)" + left associative with precedence 30 for @{ 'or $a $b }. + +(* Then, an expression like A ∧ B ∨ C will be understood as (A ∧ B) ∨ C and not +A ∧ (B ∨ C). +An annoying aspect of notation is that it will eventually interfere with the +system parser, so introducing operators with the suitable precedence is an +important and delicate issue. The best thing to do is to consult the file +``basics/core\_notation.ma'' and, unless you cannot reuse an already existing +notation overloading it (that is the recommended solution), try to figure out by +analogy the most suited precedence for your operator. + +We cannot use the notation yet. Suppose we type: + + lemma And_comm: ∀A,B. A∧B → B∧A. + +Matita will complain saying that there is no interpretation for the symbol +'and. In order to associate an interpretation with content +elements, we use the following commands: *) + +interpretation "logical and" 'and x y = (And x y). +interpretation "logical or" 'or x y = (Or x y). + +(* With these commands we are saying that a possible interpretation of the +symbol 'and+ is the inductive type And, and a possible interpretation of the +symbol 'or is the inductive type Or. +Now, the previous lemma is accepted: *) + +lemma And_comm: ∀A,B. A∧B → B∧A. +#A #B * /2/ qed. + +(* We can give as many interpretations for a same symbol as we wish: Matita will +automatically try to guess the correct one according to the context inside which +the expression occurs. +To make an example, let us define booleans and two boolean functions andb and +orb. *) + +inductive bool : Type[0] ≝ tt : bool | ff : bool. + +definition andb ≝ λb1,b2. + match b1 with [tt ⇒ b2 | ff ⇒ ff ]. + +definition orb ≝ λb1,b2. + match b1 with [tt ⇒ tt | ff ⇒ b2 ]. + +(* Then, we could then provide alternative interpretations of 'and and 'or+ over +them: *) + +interpretation "boolean and" 'and x y = (andb x y). +interpretation "boolena or" 'or x y = (orb x y). + +(* In the following lemma, the disjunction would be intrerpreted as +propositional disjunnction, since A and B must be propositions *) + +lemma Or_comm: ∀A,B. A∨B → B∨A. +#A #B * /2/ qed. + +(* On the other side, in the following lemma the disjunction is interpreted as +boolean disjunction, since a and b are boolean expressions *) + +lemma andb_comm: ∀a,b.∀P:bool→Prop. P (a∨b) → P (b∨a). +* * // qed. + +(* Let us conclude this section with a discussion of the notation for the +existential quantifier. *) + +notation "hvbox(\exists ident i : ty break . p)" + right associative with precedence 20 for + @{'exists (\lambda ${ident i} : $ty. $p) }. + +(* The main novelty is the special keyword "ident" that instructs the system +that the variable i is expected to be an identifier. Matita abstract syntax +trees include lambda terms as primitive data types, and the previous declaration +simply maps the notation ∃x.P into a content term of the form ('exists (λx.p)) +where p is the content term obtained from P. + +The corresponding interpretation is then straightforward: *) + +interpretation "exists" 'exists x = (ex ? x). + +(* The notational language of Matita has an additional list operator for dealing +with variable-size terms having a regular structure. Such operator has a +corresponding fold operator, to build up trees at the content level. + +For example, in the case of quantifiers, it is customary to group multiple +variable declarations under a same quantifier, writing e.g. ∃x,y,z.P instead of +∃x.∃y.∃z.P. + +This can be achieved by the following notation: *) + +notation > "\exists list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 + for ${ default + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } } + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } } + }. + +(* The presentational pattern matches terms starting with the existential +symbol, followed by a list of identifiers separated by commas, optionally +terminated by a type declaration, followed by a fullstop and finally by the body +term. We use list1 instead of list0 since we expect to have at least one +identifier: conversely, you should use list0 when the list can possibly be +empty. + +The "default" meta operator at content level matches the presentational opt and +has two branches, which are chosen depending on the matching of the optional +subexpression. Let us consider the first, case, where we have +an explicit type. The content term is build by folding the function + + rec acc @{'exists (λ${ident x}:$T.$acc)} + +(where "rec" is the binder, "acc" is the bound variable and the rest is the +body) over the initial content expression @{$Px}. *) + + +(***************************** Leibniz Equality *******************************) + +(* Even equality is a derived notion in Matita, and a particular case of an +inductive type. The idea is to define it as the smallest relation containing +reflexivity (that is, as the smallest reflexive relation over a given type). *) + +inductive eq (A:Type[0]) (x:A) : A → Prop ≝ + refl: eq A x x. -lemma filter_false : ∀A,l,a,p. p a = false → - filter A p (a::l) = filter A p l. -#A #l #a #p #pa (elim l) normalize >pa normalize // qed. +(* We can associate the standard infix notation for equality via the following +declarations: *) -(* As another example, let us redefine the map function using foldr. The -result type B is (list B), the base value b is [], and the fold function -of type A → list B → list B is the function mapping a and l to (f a)::l. +notation "hvbox(a break = b)" + non associative with precedence 45 for @{ 'eq ? $a $b }. + +interpretation "leibnitz's equality" 'eq t x y = (eq t x y). + +(* The induction principle eq_ind automatically generated by the system +(up to dependencies) has the following shape: + + ∀A:Type[0].∀x:A. ∀P:A→Prop. P x → ∀y:A. x = y → P y + +This principle is usually known as ``Leibniz equality'': two objects x and y are +equal if they cannot be told apart, that is for any property P, P x implies P y. + +As a simple exercise, let us also proof the following variant: *) + +lemma eq_ind_r: ∀A:Type[0].∀x:A. ∀P:A→Prop. P x → ∀y:A. y = x → P y. +#A #x #P #Hx #y #eqyx H // qed. -#l (elim l) normalize // qed. +(* Using a similar technique you can always prove that different constructors of +a same inductive type are distinct from each other; actually, this technique is +also at the core of the "destruct" tactics of the previous chapter, in order to +automatically close absurd cases. *) + +(********************************** Inversion *********************************) +include "basics/logic.ma". + +(* The only inductive type that really needs arguments is equality. In all other +cases you could conceptually get rid of them by adding, inside the type of +constructors, the suitable equalities that would allow to turn arguments into +parameters. + +Consider for instance our opp predicate of the introduction: *) + +inductive bank : Type[0] ≝ + | east : bank + | west : bank. + +inductive opp : bank → bank → Prop ≝ + | east_west : opp east west + | west_east : opp west east. + +(* The predicate has two arguments, and since they are mixed up in the type of +constructors we cannot express them as parameters. However, we could state it in +the following alternative way: *) + +inductive opp1 (b1,b2: bank): Prop ≝ + | east_west : b1 = east → b2 = west → opp1 b1 b2 + | west_east : b1 = west → b2 = east → opp1 b1 b2. + +(* Or also, more elegantly, in terms of the opposite function *) + +definition opposite ≝ λb. match b with [east ⇒ west | west ⇒ east]. + +inductive opp2 (b1,b2: bank): Prop ≝ + | opposite_to_opp2 : b1 = opposite b2 → opp2 b1 b2. + +(* Suppose now to know (opp x west), where x:bank. From this hypothesis we +should be able to conclude x = east, but this is slightly less trivial then one +could expect. *) + +lemma trivial_opp : ∀x. opp x west → x = east. +(* After introducing x and H:opp x west, one could be naturally tempted to +proceed by cases on H, but this would lead us nowhere: in fact it would generate +the following two subgoals: + + G1: east=east + G2: west=east + +The first one is trivial, but the second one is false and cannot be proved. +Also working by induction on $x$ (clearly, before introducing H) +does not help, since we would get the goals + + G_1: opp east west → east=east + G_2: opp west west → west=east + +Again, the first goal is trivial, but proving that (opp west west) is absurd has +about the same complexity of the original problem. +In fact, the best approach consists in "generalizing" the statement to something +similar to lemma opp_to_opposite of the introduction, and then prove it as a +corollary of the latter. *) +#x change with (opp x west → x=opposite west); generalize in match west; +#b * // qed. + +(* It is interesting to observe that we would not have the same problem with +opp1 or opp2. For instance: *) + +lemma trivial_opp1 : ∀x. opp1 x west → x = east. +#x #H cases H +(* applying cases analysis on H:opp1 x west, we obtain the two subgoals + + G_1: x=east → west=west → x=east + G_2: x=west → west=east → x=east + +The first one is trivial, and the second one is easily closed using descruct. *) + [//|#H1 #H2 destruct (H2)] qed. + +(* The point is that pattern matching is not powerful enough to discriminate the +structure of arguments of inductive types. To this aim, however, you may exploit +an alternative tactics called "Inversion". *) + +(* Suppose to have in the local context an expression H:T t1 … tn, where T is +some inductive type. Then, inversion applied to H derives for each possible +constructor ci of (T t1 … tn), all the necessary conditions that should hold in +order to have c_i:T t1 … tn. + +For instance, let us consider again our trivial problem trivial_opp: *) + +lemma trivial_opp2: ∀x. opp x west → x = east. +#x #H inversion H + +(* the previous invocation to inversion results in the following subgoals: + + G1: x=east → west=west →x=east + G2: x=west → west=east →x=east + +How can we prove (opp t1 t2)? we have only two possibility: via east_west, that +implies t1=east and t2=west, or via west_east, that implies t1=west and t2=west. +Note also that G1 and G2 are precisely the same goals generated by case analysis +on opp1. So we can vlose the goal in exactly the sane way: *) + [//|#H1 #H2 destruct (H2)] qed. + +(* Let us remark that invoking inversion on inductive types without arguments +does not make any sense, and has no practical effect. *) + +(* A final worning. Inversion generates equalities, and by convention it uses +the standard leibniz quality defined basics/logic.ma. This is the reason why we +included this file at the beinning of this section, instead of working with our +local equality. *) -(* -Big Operators - -Building a library of basic functions, it is important to achieve a -good degree of abstraction and generality, in order to be able to reuse -suitable instances of the same function in different context. This has not -only the obvious benefit of factorizing code, but especially to avoid -repeating proofs of generic properties over and over again. -A really convenient tool is the following combination of fold and filter, -that essentially allow you to iterate on every subset of a given enumerated -(finite) type, represented as a list. *) - - let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l:B ≝ - match l with - [ nil ⇒ b - | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else - (fold A B op b p f l)]. - -(* It is also important to spend a few time to introduce some fancy notation -for these iterators. *) - - notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" - with precedence 80 -for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}. - -notation "\fold [ op , nil ]_{ident i ∈ l } f" - with precedence 80 -for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}. - -interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l). - -theorem fold_true: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → - \fold[op,nil]_{i ∈ a::l| p i} (f i) = - op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). -#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. - -theorem fold_false: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f. -p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = - \fold[op,nil]_{i ∈ l| p i} (f i). -#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. - -theorem fold_filter: -∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B. - \fold[op,nil]_{i ∈ l| p i} (f i) = - \fold[op,nil]_{i ∈ (filter A p l)} (f i). -#A #B #a #l #p #op #nil #f elim l // -#a #tl #Hind cases(true_or_false (p a)) #pa - [ >filter_true // > fold_true // >fold_true // - | >filter_false // >fold_false // ] -qed. - -record Aop (A:Type[0]) (nil:A) : Type[0] ≝ -{op :2> A → A → A; - nill:∀a. op nil a = a; - nilr:∀a. op a nil = a; - assoc: ∀a,b,c.op a (op b c) = op (op a b) c -}. - -theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f:A → B. - op (\fold[op,nil]_{i ∈ I} (f i)) (\fold[op,nil]_{i ∈ J} (f i)) = - \fold[op,nil]_{i ∈ (I@J)} (f i). -#A #B #I #J #nil #op #f (elim I) normalize - [>nill//|#a #tl #Hind