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 \forall n \;m : nat, \left[\!| mult\left(n,m\right) |\!\right] = \left[\!| n |\!\right] \times \left[\!| m |\!\right]

  • Premier cas : \left[\!| mult\left(0,m\right) |\!\right] = 0 = 0 \times \left[\!| m |\!\right] = \left[\!| 0 |\!\right] \times \left[\!| m |\!\right]
  • Second cas : \left[\!| mult\left(1,m\right) |\!\right] = m = 1 \times \left[\!| m |\!\right] = \left[\!| 1 |\!\right] \times \left[\!| m |\!\right]

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

Alors, cas 3 et 4 :

  • \left[\!|mult(n0, x)|\!\right] = \left[\!|add(mult(n,x),mult(n,x))|\!\right]
    • = \left[\!|mult(n,x)|\!\right]+\left[\!|mult(n,x) |\!\right] par les propriétés de add
    • = \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!| n |\!\right] \times \left[\!| x |\!\right] par l'hypothèse d'induction (2 fois)
    • = n\times x + n\times x = 2\times n \times x
    • = \left[\!| n0 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}
  • \left[\!| mult(n1, x) |\!\right] = \left[\!|add(add(mult(n,x),mult(n,x)), x)|\!\right]
    • = \left[\!|add(mult(n,x),mult(n,x))|\!\right] + \left[\!|x)|\!\right] : prop. de add
    • = \left[\!|mult(n,x)|\!\right] +\left[\!|mult(n,x)|\!\right]+ \left[\!|x)|\!\right] : prop. de add
    • = \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!|x)|\!\right] : hyp. d'induction (2 fois)
    • = n \times x + n \times x + 1 \times x : sémantique de nat
    • = (2\times n + 1) \times x
    • = \left[\!| n1 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}
 
m1ilc/semantics_td_2a.txt · Dernière modification: 2010/03/04 18:25 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki