commit by user lroversi

[helm.git] / weblib / lroversi / 2009-Andrea-tutorial.ma

(**************************************************************************)
(*       ___                                                              *)
(*      ||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).