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
| S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (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).
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. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a b).
(* 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.
definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 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.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6m. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m).
#n elim n normalize
(* 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.
*)
[@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) %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
|#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
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.
*)
- [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /2/ | @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) normalize /2/
+ [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
| por: pitem S → pitem S → pitem S
| pstar: pitem S → pitem S.
-definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
-
-definition test ≝ λS:Alpha.λe: pre S. match e with [mk_pair i b ⇒ e].
+definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
interpretation "pstar" 'kstar a = (pstar ? a).
interpretation "por" 'plus a b = (por ? a b).
definition item_concat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
λS,i,e.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pcat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 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:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.∀bcast:(∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S →\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S).\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S
+ ≝ λS,bcast,e1,e2.
+ match e1 with [ pair i1 b1 ⇒ if_then_else b1 (i1 \ 5a title="item concat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2) (i1 ·(bcast S e2)) ]
].
notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
| #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
projects / helm.git / commitdiff