Preuve de code simple

gistfile1.txt

length :: [a] -> Int
length    [] = 0
length (h:t) = 1 + length t

Prouver que la propriété P :
	length [ l1 ++ l2 ] = length l1 + length l2

----------------

Montrons P([], [])
	length [] = 0
	[ [] ++ [] ] = []
	donc on a bien P([], [])

Montrons que P(l1, l2) => P(e:l1, l2)
	length e:l1 + length l2 = 1 + length l1 + length l2
	de plus [ e:l1 ++ l2 ] = e:[ l1 ++ l2 ]
	donc, length [ e:l1 ++ l2 ] = length e:[ l1 ++ l2 ]
	                            = 1 + length [ l1 ++ l2 ]
	Or P(l1, l2) est vrai, donc P(e:l1, l2) est vraie

P(l1, []) => P(e:l1, []) est deja montrée dans le point precedent

Il nous reste a montrer P(l1, l2) <=> P(l2, l1)
       length l1 + length l2 = length l2 + length l1 (par associativité de l'addition)
       length [ l1 ++ l2 ] = length l1 + length l2
       length [ l2 ++ l1 ] = length l2 + length l1
       on a donc associativité de la propriété.