2001.12.17 小テストの解答例

問題

任意のリスト xs と ys について、
   rev (xs ++ ys) = (rev ys) ++ (rev xs)
が成立することを帰納法を用いて証明せよ。ここで、
   [] ++ xs = xs                  (1)
   (y:ys) ++ xs = y:(ys ++ xs)    (2)
   rev [] = []                    (3)
   rev (x:xs) = (rev xs) ++ [x]   (4)

解答例

まず、次の二つの補題を証明する。
   補題A    ∀xs:[a], Q(xs)
      ここで Q(xs)は、xs ++ [] = xs
   補題B    ∀xs:[a], R(xs)
      ここで R(xs)は、∀ys,zs :[a] (xs ++ ys) ++ zs = xs ++ (ys ++ zs)

補題Aの証明
   Base) Q([])を示す。
         左辺 = [] ++ []
              = []              by (1)
              = 右辺
   Ind)  Q(x:xs)を示す。
         左辺 = (x:xs) ++ []
              = x:(xs ++ [])    by (2)
              = x:xs            by I.H. Q(xs)
              = 右辺
補題Bの証明
   Base) R([])を示す。
         左辺 = ([] ++ ys) ++ zs
              = ys ++ zs         by (1)
              = [] ++ (ys ++ zs) by (1)
              = 右辺
   Ind)  R(x:xs)を示す。
         左辺 = ((x:xs) ++ ys) ++ zs
              = (x:(xs ++ ys)) ++ zs  by (2)
              = x:((xs ++ ys) ++ zs)  by (2)
              = x:(xs ++ (ys ++ zs))  by I.H. R(xs)
              = (x:xs) ++ (ys ++ zs)  by (2)
              = 右辺
問題の証明
   Base) P([])を示す。
         左辺 = rev([] ++ ys)
              = rev ys                by (1)
              = (rev ys) ++ []        by 補題A
              = (rev ys) ++ (rev [])  by (3)
              = 右辺
   Ind)  P(x:xs)を示す。
         左辺 = rev ((x:xs) ++ ys)
              = rev (x:(xs ++ ys))             by (2)
              = (rev (xs ++ ys)) ++ [x]        by (4)
              = ((rev ys) ++ (rev xs)) ++ [x]  by I.H. P(xs)
              = (rev ys) ++ ((rev xs) ++ [x])  by 補題B
              = (rev ys) ++ (rev (x:xs))       by (4)
              = 右辺