Haskell 中的结构归纳和归纳假设

Question

我正在尝试使用结构归纳来证明 'ns'。所有列表 'ns' 的类型均为 [Int]，所有 'm' 的类型均为 Int。

foldl (+) m ns = m + (sum ns)

定义：

sum :: [Int] -> Int         -- summation of an Int list
sum []     = 0              -- s.1
sum (x:xs) = x + (sum xs)   -- s.2

foldl :: (a -> b -> a) -> a -> [b] -> a    -- fold left
foldl _ s []     = s                       -- fl.1
foldl f s (x:xs) = foldl f (f s x) xs      -- fl.2

如果有人能帮助我解决这个问题，我们将不胜感激。

Answer 1

我们想证明对于所有ns 和m、foldl (+) m ns = m + sum ns。我们将在ns 上进行归纳。换句话说，我们证明该属性适用于空列表，并且适用于n:ns，只要它适用于ns。

首先，让我们看看空列表，让m 是一个任意数字。我们的目标是证明foldl (+) m [] = m + sum []。有很多方法可以做到这一点，但我们将通过等式推理将等式的左侧转换为右侧。

foldl (+) m []  -- by definition of foldl
m               -- by right identity of addition
m + 0           -- by the definition of sum
m + sum []      -- QED

现在是(:) 案例。让我们的列表为n:ns。假设对于任何m，该属性对于ns 成立（这是归纳假设）。我们的目标是证明foldl (+) m (n:ns) = m + sum (n:ns)。同样，我们使用等式推理。

foldl (+) m (n:ns)    -- by the definition of foldl
foldl (+) (m + n) ns  -- by the induction hypothesis, applied to (m + n)
(m + n) + sum ns      -- by associativity of addition
m + (n + sum ns)      -- by the definition of sum
m + sum (n:ns)        -- QED

我们完成了。

---

新的证明写作学生的一个常见问题是，他们不确定自己所做的事情是否真的有意义，这让他们感到紧张。我建议看一下证明助手，例如 Agda 或 Coq。它们非常适合建立证明写作技巧。作为 Agda 的一个小例子，上面的证明可以在那里写得非常相似，但有一些语法差异：

-- imports omitted

prop : forall m ns → foldl (_+_) m ns ≡ m + sum ns

prop m [] = begin
  foldl (_+_) m []     ≡⟨⟩ 
  m                    ≡⟨ sym $ +-right-identity m ⟩
  m + 0                ≡⟨⟩
  m + sum []           ∎

prop m (x ∷ ns) = begin 
  foldl _+_ m (x ∷ ns)     ≡⟨⟩
  foldl _+_ (m + x) ns     ≡⟨ prop (m + x) ns ⟩  
  (m + x) + sum ns         ≡⟨ +-assoc m x (sum ns) ⟩ 
  m + (x + sum ns)         ≡⟨⟩
  m + sum (x ∷ ns)         ∎