From: matitaweb Date: Fri, 19 Apr 2013 18:38:02 +0000 (+0000) Subject: commit by user lroversi X-Git-Tag: make_still_working~1186 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c841fac6721efd9ec54ba1ce8479c43ff2389b91;p=helm.git commit by user lroversi --- diff --git a/weblib/lroversi/2009-Andrea-tutorial.ma b/weblib/lroversi/2009-Andrea-tutorial.ma new file mode 100644 index 000000000..fe066116e --- /dev/null +++ b/weblib/lroversi/2009-Andrea-tutorial.ma @@ -0,0 +1,682 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) +(**** +After some experience in the use of Matita I could realize how +useful Andrea's tutorial: +http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.7928 +can be, since it is compact, and allows to focus on the esssential +aspects for a fruitful approach to Matita. +So, I decided to start converting it for the current (23rd +of February 2013) version of Matita. The reason I like to have it +available via web browser is that, quite often, I access +Matita by my tablet. + +For the moment I am very interested to the more 'advanced' parts, +i.e. those ones that start after double induction. +Initially, I will introduce the least amount of code which is +essential to have the advanced part working. Gradually, I plan to +include the whole text as comments to the code. + +DISCLAIMER: +Until not explicitly otherwise written, every part of the content +is due to Andrea.*) + +include "basics/relations.ma". + +(*****************************************************************) +(**************** Chapter 1. Getting started *********************) +(*****************************************************************) +(* Natural numbers are the smallest set generated by a constant O +and a successor function S. Sets of this kind, freely generated by +a finite number of constructors, are known as inductive types. +The definition of natural numbers in Matita reads as follows: *) + +inductive nat : Type[0] ≝ + | O : nat + | S : nat → nat. +interpretation "Natural numbers" 'N = nat. +alias num (instance 0) = "natural number". + +(* By this syntax, we declare we are defining an inductive type of +name nat (which is a Type[0]), built up from the two constructors O +of type nat and S of type nat → nat. +Let us now define a simple function over natural numbers. +The sum of two natural numbers n and m may be defined as follows: +if n is O then the sum is m, otherwise, if n is the successor of +some natural number p, then the sum of n and m is equal to the +successor of the sum of p and m. In this way, we have reduced the +computation of the sum of two natural numbers to a similar problem, +but on smaller input values. This is an example of a recursive +definition, that is a definition of a function in terms of the +function itself. In Matita, the previous definition of the sum +over natural numbers would be written in the following way: *) + +let rec plus n m ≝ + match n with [ O ⇒ m | S p ⇒ S (plus p m) ]. +interpretation "natural plus" 'plus x y = (plus x y). + +(* Equalities ***************************************************************) + +theorem plus_O_n: ∀n:nat. n = O + n. +#n normalize @refl qed. + +theorem plus_n_O: ∀n:nat. n = n + O. +#n (elim n) normalize +[ @refl | #n #H Smp @eq_f @refl] qed. + +theorem plus_sym: ∀ n,m:nat. n+m = m+n. +#n #m elim n normalize +[ @plus_n_O +| #p #H >H @(plus_n_Sm m p)] qed. + +(* Exercise: +lemma not_eq_plus_S_m_O: ∀ n,m:nat. Not ((S n)+m = O). +#n #m @nmk >(plus_sym (S n) m) <(plus_n_Sm m n) #abs destruct qed .*) + +(**************** Section 1.2 Double induction ***************) +theorem nat_elim2 : + ∀R:nat → nat → Prop. + (∀n:nat. R O n) + → (∀n:nat. R (S n) O) + → (∀n,m:nat. R n m → R (S n) (S m)) + → ∀n,m:nat. R n m. +#R #ROn #RSO #RSS #n (elim n) +[ @ROn +| #Pred_n #RPred_nm + #m cases m + [@(RSO Pred_n) + |#m' @(RSS Pred_n m') @(RPred_nm m')] +] qed. + +(**************** Section 1.3 Negation and Discrimination ***) +(* Two major axioms of Peano axiomatization of naturals are: +1) the inequality between O and S x, for any x, and +2) the injectivity of S. +More generally, given any inductive type, we expect to be +able to prove that all constructors are injective and +distinguishable each from the other. + +The statement ∀x. Not (O = (Sx)) is our first example +involving negation. + +In the logical framework of Matita, negation is not +considered as a primitive connective, but is instead defined +in terms of the absurdity proposition False. Explicitly, we +may conclude Not P, if and only if assuming P leads +to an asburdity, that is P → False. + +What about False? The only logical principle related to +False is the ancient property expressed by the latin motto +'ex falso quodlibet', that is, everything may be deduced +under a false assumption. + +Formally, this is expressed by the following property that, +for the moment, we may assume to be a primitive constant +of the system: + +False_ind : ∀P:Prop. False → P + +[Ndr: In fact, False_ind *is* a primitive in Matita as it +is used in many points when building libraries! ] + +Concerning injectivity (or separability) of constructors, +Matita provides the tactic destruct. The tactic expects in +input a term of type e1 = e2. It recursively compares e1 +and e2, skipping common constructors (injectivity) and halts +on subexpressions differing on their leftmost outermost +symbols. If any of these correponding symbols are two +different constructors the tactics automatically closes the +goal [Ndr: that depends on them] having obtained a +contradiction. Otherwise, destruct adds to the context all +new equalities between the different subformulae in +corresponding positions. Luckily, the tactic is much simpler +to use than to explain. Let us see a couple of examples. *) + +theorem not_eq_O_S: ∀ n:nat. Not (O = S n). +#n (* apply the definition of Not *) @nmk #Habs destruct qed. + +(* Exercise: +lemma not_eq_S_O: ∀ n:nat. Not (S n = O). +#n (* apply the definition of Not *) @nmk #Habs destruct qed. *) + +theorem S_inj: ∀ n,m:nat. S n = S m → n = m. +#n #m #Hinj destruct @refl qed . + +(*****************************************************************) +(**************** Chapter 2. Defining properties *****************) +(*****************************************************************) +(* So far, the only property we have been dealing with has +been equality that we have essentially assumed as a +primitive notion of Matita, governed via rewriting and +reflexivity. As an exercise one can prove simmetry and +transitivity of the equality, as follows: *) + +lemma eq_sym: ∀A:Type[0]. ∀x,y:A. x=y → y=x. +#A #x #y #eqxy eqxy @eqyz qed . + +(* The next step is to define a binary predicate +le n m +asserting that n is less or equal to m. As we shall see, +we have some alternatives. + +We start with a natural mathematical definition: +n is less or equal to m + if and only if it exists p such n + p = m. + +We have essentially two different, almost equivalent, ways +to encode such a predicate in Matita: +1) as a definition, or +2) as an inductive type. + +As a definition it is: *) + +definition le1: nat → nat → Prop ≝ + λn,m.∃p:nat.n+p = m. + +(* However, an experienced Matita user would probably prefer +to transform the previous definition of le into the smallest +property induced by *an integer p and a proof of n+p=m * +as follows:*) + +inductive le2 (n,m:nat) : Prop ≝ +le_witness : ∀p:nat.n+p = m → le2 n m. + +(* The constructor le_witness is a user-defined name that +can bw chosen arbitrarily and which idetifies a proof of: + + ∀n,m,p:nat.n + p = m → le2 n m + +Namely, the two parameters n and m are also parameters +for the constructor whose fully blown type is exactly: + + le_witness: ∀n,m,p:nat.n + p = m → le2 n m + +We formally prove the equivalence between the two +previous definitions. + +We start proving that the first definition implies the +second one: *) + +lemma le1_to_le2: ∀n,m:nat.le1 n m → le2 n m. +(* This is the proof pattern we shall follow: +--------------------------------------------------- @npeqm +n:nat,m:nat,∃p:nat.n+p=m, +p:nat,npeqm:n+p=m ⊢ n+p=m +----------------------------------------------- @(le_witness n m p) +n:nat,m:nat,∃p:nat.n+p=m, +p:nat,npeqm:n+p=m ⊢ n+p=m→le2 n m +----------------------------------------------- #p #npeqm +n:nat,m:nat,∃p:nat.n+p=m + ⊢ ∀x:ℕ.n+x=m→le2 n m +----------------------------------------------- elim le1 +n:nat,m:nat,∃p:nat.n+p=m + ⊢ le2 n m +----------------------------------- normalize in le1; +n:nat,m:nat,le1 n m ⊢ le2 n m +------------------------------- #n #m #le1 +∀n,m:nat.le1 n m → le2 n m *) +#n #m #le1 +normalize in le1; elim le1 (* (0) *) +#p #npeqm @(le_witness n m p) @npeqm qed . + +(* Then, the second definition implies the first one: *) +lemma le2_to_le1: ∀n,m:nat.le2 n m → le1 n m. +(* This is the proof pattern we shall follow: +---------- (ex_intro nat (λp:ℕ.n+p=m)) --------- +n:ℕ,m:ℕ,le2:le2 n m ⊢ ∀p:ℕ.n+p=m → ∃p0:ℕ.n+p0=m +------------------------------------------------ normalize +n:ℕ,m:ℕ,le2:le2 n m ⊢ ∀p:ℕ.n+p=m → le1 n m +------------------------------------------- elim le2 +n:ℕ,m:ℕ,le2:le2 n m ⊢ le1 n m +-------------------------------- #n #m #le2 +∀n:ℕ.∀m:ℕ.le2 n m→le1 n m *) +#n #m #le2 elim le2 normalize (* (1) *) +(* (* One may *) check (ex_intro nat (λp:ℕ.n+p=m)) *) +@(ex_intro nat (λp:ℕ.n+p=m)) (* (2) *) +qed . + +(* In the previous proof we do not follow original Asperti's +proof pattern. We directly exploit ex_intro, defined in +lib/basics/logic.ma whose type is: + + eq_intro: ∀A:Type.∀P:A→Prop.∀x:A.Px→∃x:A.Px + +I have do guess the two arguments of ex_intro. In fact, +I have experimented with the original Asperti's proof pattern +which, keep going from (1) above, must develop as follows: + + #p #npeqm @(ex_intro ? ? p npeqm)) + +Specifically, + check (ex_intro ? ? p npeqm)) +lets Matita to automatically build: + (ex_intro ℕ (λ_:ℕ.n+__1=m) p npeqm:∃_:ℕ.n+__1=m) +from which one can synthesize (2). + +We remark that the proof of le2_to_le1 is slightly more +compact than the proof of le1_to_le2. The reason is that +le2_to_le1 does not require the normalization of the +definition of le2 before eliminating it as in (0) above. +This is one of the practical reason for preferring le2 over +le1. More generally, the existential quantifier is just a +particular case of inductive type, and the direct definition +of a property as an inductive types usually allows a simpler +and more direct destructuration of the corresponding +definition. *) + +(**************** Section 2.1 Recursive properties ***) +(* The previous definition of le relies on the definition of +the sum, that is not very elegant. An alternative way to look +at the less or equal relation is as the smallest relation R +being reflexive and such that R n m implies R n (S m). This +notion is precisely captured by the following inductive type: *) +inductive le (n:nat) : nat → Prop ≝ +| le_n : le n n +| le_S : ∀ m:nat. le n m → le n (S m). + +(* Again, let us prove the equivalence between this definition +and the definition of le2. As suggested by the original +tutorial, we start showing why the tactics we learned so far +are not enough. To experiment it, just uncomment in the +right way. *) +(* <-- Erase this.... +lemma le2_to_le_not_general_enough: ∀ n,m:nat. le2 n m → le n m. +(* As suggested, one can start as follows: *) +#n #m #le2 elim le2 #p +(* We get to: + n:ℕ,m:ℕ,le2:le2 n m,p:ℕ ⊢ n+p=m→le n m +At this point, we can try to proceed by induction on p: *) +elim p +[ (* We can prove the base case *) + normalize <(plus_n_O n) #nm *) + +(* In fact, in the course of the proof of le_to_le2 +instead of getting to the point where the goal is + n+p=m→le n m +we need to arrive to the stronger goal: + ∀m:ℕ.n+p=m→le n m +The tactic we need is + generalize in match m; +The working proof follows. *) + +lemma le2_to_le: ∀ n,m:nat. le2 n m → le n m . +(* +The following proof can be seen as split into two +phases. The first one aims at getting to the goal + n:nat,p:ℕ ⊢ ∀m:nat.n+p=m → le n m (1) +which we shall prove by inducton on + +The goal (1) here above needs the introduction to +the right of ∀m, after m has been moved among the +assumptions to discharge all the other assumptions +as required: + +n:nat,p:ℕ ⊢ ∀m:nat.n+p=m → le n m +------------------------------------ generalize in match m; +n:nat,m:nat,p:ℕ ⊢ n+p=m → le n m +------------------------------------ #p +n:nat,m:nat ⊢ ∀p:ℕ.n+p=m→le n m +------------------------------------ elim le2 -le2 +n:nat,m:nat,le2 n m ⊢ le n m +------------------------------------ #n #m #le2 +∀n,m:nat.le2 n m → le n m *) +#n #m #le2 elim le2 -le2 +#p generalize in match m; +(* The second part proves (1) by induction on p: *) +elim p +[ <(plus_n_O n) #n' #neqn' le2 n (S x) + eq ---------------------------------------- ------------------------- + n+p=x ⊢ n+Sp=Sx ⊢ n+Sp=Sx → le2 n (S x) + →E----------------------------------------------------- + n+p=x ⊢ le2 n (S x) + →I----------------------- + ⊢ n+p=x → le2 n (S x) *) + #npeqx + (* check (plus_monotone (n+p) x npeqx) *) + lapply (plus_monotone (n+p) x npeqx) -npeqx + >(plus_n_Sm) + (* check (le_witness n (S x) (S p)) *) + @(le_witness n (S x) (S p)) + ] qed . + +(**************** Section 2.2 Prop vs. Bool ***) +(* The definition of le of the previous section does not give an +effective way to decide if n is less or equal to m. What we are looking +for is a binary boolean function returning true if n ≤ m, and f alse +otherwise. Such a computable function is usually called a decision +procedure. A property admitting a decision procedure is called recursive, +or decidable. We start defining the type of booleans as the smallest type +containing the two elements true and false: *) +inductive bool : Type[0] ≝ +| true : bool +| false : bool. + +(* Then, we define a decision procedure for the less or equal relation: *) +let rec leb n m ≝ + match n with + [ O ⇒ true | (S p) ⇒ match m with + [ O ⇒ false | (S q) ⇒ leb p q]]. + +(* Once given a decision procedure, it is convenient to define a +corresponding elimination principle, which relates in a very general +way the boolean function to its propositional counterpart (le). In our +case the boolean function is leb, and its propositional counterpart +is le. The elimination principle says that: +for all natural numbers n and m, and any proposition P over booleans, +provided we may prove (P true) under the assumption (le n m), and +(P false) under the assumption ¬(le n m), then we can conclude +(P (leb n m)). Namely: + + (n ≤ m → (P true)) → (n ≰ m → (P false)) → P (leb n m) + +The proof requires preliminary steps: +1) the proof of lemmas le_O_n, not_le_Sn_O, le_S_S, +2) the definition of pred +3) the proof the pred is monotonic +4) the proof of le_S_S_to_le. +5) the proof of contraposition, called not_to_not in +lib/basics/logic.ma. Tuttavia, si potrebbe immaginare +di spostare contraposition nella sezione relativa alle +dimostrazioni per assurdo, visto il modo di dimostrarla. *) + +lemma le_O_n : ∀n:nat. le O n. +#n (elim n) [@le_n | #x @le_S ] qed. + +lemma not_le_Sn_O: ∀ n:nat. Not (le (S n) O). +#n @nmk #abs +lapply ((le_to_le2 (S n) O) abs) -abs #le2 elim le2 -le2 #p +>(plus_sym (S n) p) <(plus_n_Sm p n) #abs destruct qed . + +lemma le_S_S: ∀n,m:nat. (le n m) → (le (S n) (S m)). +#n #m #lenm elim lenm -lenm +[ @le_n | #x #H -H @(le_S) ] qed . + +definition pred ≝ + λn. match n with [ O ⇒ O | S p ⇒ p]. + +theorem pred_monotonic: + ∀n,m:nat. le n m → le (pred n) (pred m). +#n #m #lenm (elim lenm) +[ @le_n +| #x normalize in match (pred (S x)); + cases x normalize in match (pred O); + [ #dummy #H @H + | #y normalize in match (pred (S y)); + #dummy @le_S ] qed. + +lemma le_S_S_to_le: ∀n,m:nat. (le (S n) (S m)) → (le n m). +#n #m #leSnSn +(* check ((pred_monotonic (S n) (S m)) leSnSn) *) +lapply ((pred_monotonic (S n) (S m)) leSnSn) +normalize in match (pred (S n)); +normalize in match (pred (S m)); #H @H qed . + +theorem contraposition : ∀A,B:Prop. (A → B) → ¬B →¬A. +#A #B #AB #nB @nmk #A lapply nB lapply (AB A) @absurd qed . + +theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. +(le n m → P true) → (Not (le n m) → P false) → P (leb n m). +@nat_elim2 + [normalize #n #P #Pt #Pf @Pt @(le_O_n) + |normalize #n #P #Pt #Pf @Pf @(not_le_Sn_O) + |normalize #n #m #Hind #P #Pt #Pf @Hind + [#lenm @Pt @le_S_S @lenm + |#nlenm @Pf lapply nlenm @contraposition @le_S_S_to_le ] +qed. + +(* Le seguenti prorietà che si trovano anche in +lib/arithmetics/nat.ma ma sinora non mi paiono necessarie +per questo tutorial, quindi le commento. + + +lemma le_n_Sn : ∀n:nat. le n (S n). +#n @le_S @le_n qed. + +lemma le_tran : ∀n,m,o:nat. le n m → le m o → le n o. +#n #m #o #lenm #lemo (elim lemo) +[@lenm | #x #dummy @le_S ] qed. + +lemma le_pred_n : ∀n:nat. le (pred n) n. +#n (elim n) +[ normalize @le_n +| #m #H normalize @(le_S) @le_n] qed . *) + + +(* Le seguenti proprietà sfruttano pesantemente leb_elim e sono +un esempio fondamentale.*) +theorem leb_true_to_le:∀n,m.leb n m = true → (le n m). +#n #m +(* check (λb:bool. b=true→le n m)) *) +check (∀b:bool. b=true→le n m) +(* check ((λb:bool. b=true→le n m) (leb n m)) *) +@(leb_elim n m (λb:bool. b=true→le n m)) + +(* DA QUI !!!!!!!!!!!!!!!!!*) + +@leb_elim // #_ #abs @False_ind /2/ qed. + +theorem leb_false_to_not_le:∀n,m. + leb n m = false → n ≰ m. +#n #m @leb_elim // #_ #abs @False_ind /2/ qed. + +theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true. +#n #m @leb_elim // #H #H1 @False_ind /2/ qed. + +theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false. +#n #m @leb_elim // #H #H1 @False_ind /2/ qed. + +theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false. +/3/ qed. + + +(*****************************************************************) +(**************** Chapter 3. A non trivial example ***************) +(*****************************************************************) +(* In a way similar to plus we may define the product of two natural +numbers: *) + + +let rec times n m ≝ + match n with [ O ⇒ 0 | S p ⇒ m + (times p m) ]. + +interpretation "natural times" 'times x y = (times x y). + +definition divides1: nat \to nat \to Prop \def +\lambda n,m.\exist p:nat.m = times n p. + +(* However, as we have seen, it is preferable to define divides as +the smallest property induced by a 'witness' p and a proof that +m = np, namely: *) + +inductive divides (n,m:nat) : Prop \def +witness : \forall p:nat.m = times n p \to divides n m. + + +(* Let us now address the decidability of divides, i.e. the problem +to define an algorithmic boolean function that taken in input two +integers n and m returns true if n divides m, and f alse otherwise. +A convenient way to proceed is to address the slightly more general +problem to compute the modulus (mod) of two numbers (i.e. the rest +of an integewr division); obviously n divides m if and only if +m mod n = 0. The natural way to define mod as a recursive function +would look something like the following: *) + +let rec mod m n: nat \def +match (leb (S m) n) with +[ true \Rightarrow m +| false \Rightarrow mod (m-n) n +] + +(* The problem with this definition is that the calculus is based on +a particular kind or recursion that must be guaranteed to be +well-founded (never diverge) . This is typically the case when the +recursive parameter 'decreases' in the recursive call. Unfortunately, +there is no trivial way, for the system, to understand that m − n is +'smaller' than m w.r.t. some well founded ordering +(minus is a user defined operation!). What the system is able to +understand is essentially a syntactic ordering, based on the structure +of inductive data: for instance n is 'smaller' of S n. +A simple but effective approach to this problem is that of defining +an auxiliary function accepting in input an extra-parameter t +providing an upper bound to the complexity of the function, and then +recurring on such an argument. For instance, in the case of the +modulus, we may eventually complete the computation of mod m n in +less than m steps. So, we define: *) + +let rec mod_aux t m n: nat \def +match (leb (S m) n) with +[ true \Rightarrow m +| false \Rightarrow +match t with +[O \Rightarrow m +(* if t is large enough this case never happens *) +|(S t1) \Rightarrow mod_aux t1 (m-n) n +] +]. + +definition mod : nat \to nat \to nat \def +\lambda m,n.mod_aux m m n. + +(* When we define a function having several cases as the previous +one, it is good practice to specify the behavour with a distinct +lemma for each possible branch. In the case of the previous function, +we have the following relevant cases, whose proof is more or less +straightforward. The only novelty is the use of the change tactic, +that allows to replace a goal with an equivalent one (up to +convertibility). Sometimes, the heuristic used by the simplify +tactic simplifies too much, and it turns out to be convenient to +give the system the expected transformation in an explicit way. *) + +lemma O_to_mod_aux: \forall m,n. mod_aux O m n = m. +intros. +simplify.elim (leb (S m) n);reflexivity. +qed. + +lemma lt_to_mod_aux: +\forall t,m,n. m < n \to mod_aux (S t) m n = m. +intros. +change with +( match (leb (S m) n) with +[ true \Rightarrow m +| false \Rightarrow mod_aux t (m-n) n] = m). +rewrite > (le_to_leb_true ? ? H). +reflexivity. +qed. + +lemma le_to_mod_aux: +\forall t,m,n. +n \le m \to mod_aux (S t) m n = mod_aux t (m-n) n. +intros. +change with +(match (leb (S m) n) with +[ true \Rightarrow m +| false \Rightarrow mod_aux t (m-n) n] = mod_aux t (m-n) n). +apply (leb_elim (S m) n);intro +[apply False_ind.apply (le_to_not_lt ? ? H).apply H1 +|reflexivity +] +qed. + +(* In order to understand the use of the previous lemmas, let us +try to prove a simple property of the modulus operation, namely that +for any positive n, m mod n < n. The proof has the following +structure: *) + +theorem lt_mod_aux_m_m: +\forall n. O < n \to +\forall t,m. m \leq t \to (mod_aux t m n) < n. +intros 3. +elim t +[rewrite > O_to_mod_aux. +apply (le_n_O_elim ? H1). +assumption +|elim (decidable_lt m n) +[rewrite > lt_to_mod_aux[assumption|assumption] +|rewrite > le_to_mod_aux +[apply H1. +... +|apply not_lt_to_le. +assumption +] +] +] +qed. + +(* Mimicking the definition of mod_aux, the proof proceeds by +induction on the recursive parameter t. The case t = 0 is closed +by O_to_mod_aux; in case t = Sn1, we distinguish two more cases +according the situations m < n or m ≥ n. In the former case, we use +lt_to_mod_aux while in the latter we use le_to_mod_aux +and the inductive hypothesis H1. The dots correspond to a trivial +but formally cumbersome fragment of the proof. Indeed, after +applying the inductive hypothesis H1 we are left with the following +goal: *) + + +(* Very likely here it will benecessary to expand what +Andrea writes .... *) + +(* The proof requires several elementary arithmetical results, +but is not particualry informative, so we shall skip it here. +Having defined the modulus, we define: *) + +definition divides_b : nat \to nat \to bool \def +\lambda n,m :nat. (eqb (m \mod n) O). + diff --git a/weblib/lroversi/nat.ma b/weblib/lroversi/nat.ma new file mode 100644 index 000000000..aad1828cf --- /dev/null +++ b/weblib/lroversi/nat.ma @@ -0,0 +1,70 @@ +include "hints_declaration.ma". +include "basics/eq.ma". + +ninductive nat : Type ≝ + | O : nat + | S : nat → nat. + +interpretation "Natural numbers" 'N = nat. + +alias num (instance 0) = "nnatural number". + +(* +nrecord pos : Type ≝ + {n:>nat; is_pos: n ≠ 0}. + +ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on +*) + +(* default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind. +*) + +ndefinition pred ≝ + λn. match n with [ O ⇒ O | S p ⇒ p]. + +ntheorem pred_Sn : ∀n. n = pred (S n). +//; nqed. + +ntheorem injective_S : injective nat nat S. +//; nqed. + +(* +ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. +//. nqed. *) + +ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. +/3/; nqed. + +ndefinition not_zero: nat → Prop ≝ + λn: nat. match n with + [ O ⇒ False | (S p) ⇒ True ]. + +ntheorem not_eq_O_S : ∀n:nat. O ≠ S n. +#n; napply nmk; #eqOS; nchange with (not_zero O); +nrewrite > eqOS; //. +nqed. + +ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n. +#n; nelim n;/2/; nqed. + +ntheorem nat_case: + ∀n:nat.∀P:nat → Prop. + (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n. +#n; #P; nelim n; /2/; nqed. + +ntheorem nat_elim2 : + ∀R:nat → nat → Prop. + (∀n:nat. R O n) + → (∀n:nat. R (S n) O) + → (∀n,m:nat. R n m → R (S n) (S m)) + → ∀n,m:nat. R n m. +#R; #ROn; #RSO; #RSS; #n; nelim n;//; +#n0; #Rn0m; #m; ncases m;/2/; nqed. + +ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m). +napply nat_elim2; #n; + ##[ ncases n; /2/; + ##| /3/; + ##| #m; #Hind; ncases Hind;/3/; + ##] +nqed.