From 634dd58a077d3380f90e47a5f6a40a648ad9f17b Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 12 Dec 2011 13:45:50 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 109 +++++++++++++++++++----------------- weblib/tutorial/chapter4.ma | 20 ++----- 2 files changed, 64 insertions(+), 65 deletions(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 85815e006..42b3d8e74 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -1,26 +1,27 @@ include "basics/types.ma". -(* Most of the types we have seen so far are enumerated types, composed by a finite set of -alternatives, and records, composed by tuples of heteregoneous elements. -A more interesting case of type definition is when some of the rules defining its elements are -recursive, i.e. they allow the formation of more elements of the type in terms of the already -defined ones. The most typical case is provided by the natural numbers, that can be defined as -the smallest set generated by a constant 0 and a successor function from natural numbers to -natural numbers *) +(* Most of the types we have seen so far are enumerated types, composed by a +finite set of alternatives, and records, composed by tuples of heteregoneous +elements. A more interesting case of type definition is when some of the rules +defining its elements are recursive, i.e. they allow the formation of more +elements of the type in terms of the already defined ones. The most typical case +is provided by the natural numbers, that can be defined as the smallest set +generated by a constant 0 and a successor function from natural numbers to natural +numbers *) inductive nat : Type[0] ≝ | O :nat | S: nat →nat. -(* The two terms O and S are called constructors: they define the signature of the type, whose -objects are the elements freely generated by means of them. So, examples of natural numbers are -O, S O, S (S O), S (S (S O)) and so on. +(* The two terms O and S are called constructors: they define the signature of the +type, whose objects are the elements freely generated by means of them. So, +examples of natural numbers are O, S O, S (S O), S (S (S O)) and so on. -The language of Matita allows the definition of well founded recursive functions over inductive -types; in order to guarantee termination of recursion you are only allowed to make recursive -calls on structurally smaller arguments than the 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 *) +The language of Matita allows the definition of well founded recursive functions +over inductive types; in order to guarantee termination of recursion you are only +allowed to make recursive calls on structurally smaller arguments than the 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 ≝ match n with @@ -28,15 +29,16 @@ match n with | S a ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (add a m) ]. -(* It is worth to observe that the previous algorithm works by recursion over the first -argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O) -is stuck. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it -is called induction. The induction principle states that, given a property P(n) over natural -numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude -P(n) for any n. +(* It is worth to observe that the previous algorithm works by recursion over the +first argument. This means that, for instance, (add O x) will reduce to x, as +expected, but (add x O) is stuck. +How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do +it is called induction. The induction principle states that, given a property P(n) +over natural numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), +than we can conclude P(n) for any n. -The elim tactic, allow you to apply induction in a very simple way. If your goal is P(n), the -invocation of +The elim tactic, allow you to apply induction in a very simple way. If your goal is +P(n), the invocation of elim n will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m). @@ -53,8 +55,8 @@ After normalization, both goals are trivial. normalize // qed. -(* In a similar way, it is convenient to state a lemma about the behaviour of add when the -second argument is not zero. *) +(* In a similar way, it is convenient to state a lemma about the behaviour of +add when the second argument is not zero. *) lemma add_S : ∀a,b. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a a b). @@ -71,8 +73,8 @@ theorem add_comm : ∀a,b. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1) (* We have two sub goals: G1: ∀b. b = add b O G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x). -G1 is just our lemma add_O. For G2, we start introducing x and the induction hypothesis IH; -then, the goal is proved by rewriting using add_S and IH. +G1 is just our lemma add_O. For G2, we start introducing x and the induction +hypothesis IH; then, the goal is proved by rewriting using add_S and IH. For Matita, the task is trivial and we can simply close the goal with // *) // qed. @@ -94,9 +96,10 @@ definition nat_of_bool ≝ λb. match b with definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. -(* We are interested to prove that for any natural number n there exists a natural number m that -is the integer half of n. This will give us the opportunity to introduce new connectives and -quantifiers and, later on, to make some interesting consideration on proofs and computations. *) +(* We are interested to prove that for any natural number n there exists a natural +number m that is the integer half of n. This will give us the opportunity to +introduce new connectives and quantifiers and, later on, to make some interesting +consideration on proofs and computations. *) theorem ex_half: ∀n.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m). #n elim n normalize @@ -104,26 +107,30 @@ theorem ex_half: ∀n.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n  (* We proceed by induction on n, that breaks down to the following goals: G1: ∃m.O = add O O ∨ O = S (add m m) G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m) -The only way we have to prove an existential goal is by exhibiting the witness, that in the case -of first goal is O. We do it by apply the term called ex_intro instantiated by the witness. -Then, it is clear that we must follow the left branch of the disjunction. One way to do it is by -applying the term or_introl, that is the first constructor of the disjunction. However, -remembering the names of constructors can be annyoing: we can invoke the application of the n-th -constructor of an inductive type (inferred by the current goal) by typing %n. At this point -we are left with the subgoal O = add O O, that is closed by computation. -It is worth to observe that invoking automation at depth /3/ would also automatically close G1. +The only way we have to prove an existential goal is by exhibiting the witness, +that in the case of first goal is O. We do it by apply the term called ex_intro +instantiated by the witness. Then, it is clear that we must follow the left branch +of the disjunction. One way to do it is by applying the term or_introl, that is +the first constructor of the disjunction. However, remembering the names of +constructors can be annyoing: we can invoke the application of the n-th +constructor of an inductive type (inferred by the current goal) by typing %n. At +this point we are left with the subgoal O = add O O, that is closed by +computation. It is worth to observe that invoking automation at depth /3/ would +also automatically close G1. *) [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) %1 // -(* The case of G2 is more complex. We should start introducing x and the inductive hypothesis +(* The case of G2 is more complex. We should start introducing x and the +inductive hypothesis IH: ∃m. x = add m m ∨ x = S (add m m) -At this point we should assume the existence of m enjoying the inductive hypothesis. To -eliminate the existential from the context we can just use the case tactic. This situation where -we introduce something into the context and immediately eliminate it by case analysis is so -frequent that Matita provides a convenient shorthand: you can just type a single "*". -The star symbol should be reminiscent of an explosion: the idea is that you have a structured -hypothesis, and you ask to explode it into its constituents. In the case of the existential, -it allows to pass from a goal of the shape +At this point we should assume the existence of m enjoying the inductive +hypothesis. To eliminate the existential from the context we can just use the case +tactic. This situation where we introduce something into the context and immediately +eliminate it by case analysis is so frequent that Matita provides a convenient +shorthand: you can just type a single "*". +The star symbol should be reminiscent of an explosion: the idea is that you have a +structured hypothesis, and you ask to explode it into its constituents. In the case +of the existential, it allows to pass from a goal of the shape (∃x.P x) → Q to a goal of the shape ∀x.P x → Q @@ -131,10 +138,10 @@ to a goal of the shape |#x * (* At this point we are left with a new goal with the following shape G3: ∀m. x = add m m ∨ x = S (add m m) → .... -We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then reason by -cases on this hypothesis. It is the same situation as before: we explode the disjunctive -hypothesis into its possible consituents. In the case of a disjunction, the * tactic allows -to pass from a goal of the form +We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then +reason by cases on this hypothesis. It is the same situation as before: we explode the +disjunctive hypothesis into its possible consituents. In the case of a disjunction, the +* tactic allows to pass from a goal of the form A∨B → Q to two subgoals of the form A → Q and B → Q @@ -145,7 +152,7 @@ is hence m, and we have to prove the right branch of the disjunction. In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x) is hence (S m), and have to follow the left branch of the disjunction. *) - [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /2/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a m)) normalize /2/ + [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a m)) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ ] qed. diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index fd0f71144..8649c4469 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -105,9 +105,7 @@ inductive pitem (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alp | por: pitem S → pitem S → pitem S | pstar: pitem S → pitem S. -definition pre ≝ λS.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S a title="Product" href="cic:/fakeuri.def(1)"×/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a. - -definition test ≝ λS:Alpha.λe: pre S. match e with [mk_pair i b ⇒ e]. +definition pre ≝ λS.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S a title="Product" href="cic:/fakeuri.def(1)"×/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a. interpretation "pstar" 'kstar a = (pstar ? a). interpretation "por" 'plus a b = (por ? a b). @@ -188,17 +186,11 @@ interpretation "oplus" 'oplus a b = (lor ? a b). definition item_concat: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S ≝ λS,i,e.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pcat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e〉. -definition lcat: ∀S:Alpha.∀bcast:(∀S:Alpha.pre S →pre S).pre S → pre S → pre S - ≝ λS:Alpha.λbcast:∀S:Alpha.pre S → pre S.λe1,e2:pre S. - match e1 with [ mk_pair i1 b1 ⇒ e2]. - - match e1 with [ _ => e1]. - - match b1 with - [ false ⇒ e2 | _ => e1 ]]. +interpretation "item concat" 'concat i e = (item_concat ? i e). - | true ⇒ item_concat S i1 (bcast S e2) - ] +definition lcat: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.∀bcast:(∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S →a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S).a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S + ≝ λS,bcast,e1,e2. + match e1 with [ pair i1 b1 ⇒ if_then_else b1 (i1 a title="item concat" href="cic:/fakeuri.def(1)"·/a e2) (i1 ·(bcast S e2)) ] ]. notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. @@ -753,4 +745,4 @@ ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e. | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ | #x; #y; #K; ncases (?:False); /2/ | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] -##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; \ No newline at end of file +##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; \ No newline at end of file -- 2.39.2