--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 <H @eq_f @refl ] qed.
+
+theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
+#n (elim n) normalize
+[#m @eq_f @refl
+|#m #H #p @eq_f <(H p) @eq_f @eq_f2
+ [@refl|@refl]] qed.
+
+(* The monotonicity of plus is not in the original
+Apserti's tutorial but, as far as I could understand
+the way the current version of Matita works, requires
+it to prove the equivalence of the two equivalence
+relations le2 and le we shall see later. *)
+theorem plus_monotone:∀n,m:nat. n=m → (S n) = (S m).
+#n elim n
+[#m #Om <Om @eq_f @refl
+|#m #H #p #Smp >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 @refl qed .
+
+lemma eq_tran: ∀A:Type[0]. ∀x,y,z:A. x=y → y=z → x=z.
+#A #x #y #z #eqxy #eqyz >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 <nm @le_n
+| (* However the assumptions are too weak
+ and we get stuck. *)
+ #x #ind #H
+] .... and erase this --> *)
+
+(* 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' <neqn' @le_n
+| #x #Hind #y #nSxeqy <nSxeqy <(plus_n_Sm) @(le_S)
+ @(Hind (n+x))
+ (* eq_f2 is in lib/basics/logic.ma *)
+ @eq_f2 @refl @refl
+] qed .
+
+(* The converse holds as well: *)
+lemma le_to_le2: ∀ n,m:nat. le n m → le2 n m .
+#n #m #le elim le -le
+[ @(le_witness n n O) <(plus_n_O n) @refl
+| (*
+ *)
+ #x #H -H
+ #le2 elim le2 -le2
+ #p
+ (* The coming steps have n,m,x,p as global assumptions and essentially
+ build the following proof:
+
+ plus_monotone
+ ----------------- -------------
+ ⊢ n+p=x→S(n+p)=Sx n+p=x ⊢ n+p=x plus_n_Sm
+ →E-------------------------------- -------------
+ n+p=x ⊢ S(n+p)=Sx ⊢ S(n+p)=n+Sp ∀n,m,p.n+p=m->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).
+
projects / helm.git / commitdiff