===== Maurice Lanselle =====
===== M1-ILC =====

====== mult sur nat ======

===== Définition par cas =====

  * mult(0, m) = 0
  * mult(1, m) = m
  * mult(n0, m) = add(mult(n,m),mult(n,m))
  * mult(n1, m) = add(add(mult(n,m),mult(n,m)), m)

Montrons par induction structurelle sur ''nat'' que <jsm>\forall n \;m : nat, \left[\!| mult\left(n,m\right) |\!\right] = \left[\!| n |\!\right] \times \left[\!| m |\!\right]</jsm>

  * Premier cas : <jsm>\left[\!| mult\left(0,m\right) |\!\right] = 0 = 0 \times \left[\!| m |\!\right] = \left[\!| 0 |\!\right] \times \left[\!| m |\!\right]</jsm>
  * Second cas : <jsm>\left[\!| mult\left(1,m\right) |\!\right] = m = 1 \times \left[\!| m |\!\right] = \left[\!| 1 |\!\right] \times \left[\!| m |\!\right]</jsm>

Hypothèse d'induction : <jsm>\forall x:nat, n:nat \;\text{fixe}, \left[\!| mult\left(n,x\right) |\!\right] = \left[\!| n |\!\right] \times \left[\!| x |\!\right]</jsm>.

Alors, cas 3 et 4 : 
  * <jsm>\left[\!|mult(n0, x)|\!\right] = \left[\!|add(mult(n,x),mult(n,x))|\!\right]</jsm>
    * <jsm> = \left[\!|mult(n,x)|\!\right]+\left[\!|mult(n,x) |\!\right]</jsm> par les propriétés de ''add''
    * <jsm> =  \left[\!| n |\!\right] \times \left[\!| x |\!\right] +  \left[\!| n |\!\right] \times \left[\!| x |\!\right]</jsm> //  par l'hypothèse d'induction (2 fois)//
    * <jsm> = n\times x + n\times x = 2\times n \times x </jsm>
    * <jsm> =  \left[\!| n0 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}</jsm>
  * <jsm>\left[\!| mult(n1, x) |\!\right] = \left[\!|add(add(mult(n,x),mult(n,x)), x)|\!\right]</jsm>
    * <jsm>= \left[\!|add(mult(n,x),mult(n,x))|\!\right] + \left[\!|x)|\!\right]</jsm> : prop. de ''add''
    * <jsm>= \left[\!|mult(n,x)|\!\right] +\left[\!|mult(n,x)|\!\right]+ \left[\!|x)|\!\right]</jsm> : prop. de ''add''
    * <jsm> = \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!|x)|\!\right]</jsm> : hyp. d'induction (2 fois)
    * <jsm> = n \times x + n \times x + 1 \times x </jsm> : sémantique de ''nat''
    * <jsm> = (2\times n + 1) \times x </jsm>
    * <jsm> = \left[\!| n1 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}</jsm>