lean - 为什么在这个嵌套归纳证明中不需要第二个归纳假设？

Question

我正在玩自然数游戏，我已经完成了mul_add. 证明如下所示：

lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=

begin

  induction b with B hB,

  -- b base case
  rw add_zero a,
  rw mul_zero t,
  rw add_zero (t*a),
  refl,

  induction a with A hA,

  -- a base case
  rw zero_add (succ B),
  rw mul_zero t,
  rw zero_add (t * succ B),
  refl,

  -- joint inductive step
  rw add_succ (succ A) B,
  rw mul_succ t (succ A + B),
  rw hB,
  rw add_assoc (t*succ A) (t*B) t,
  rw <- mul_succ t B,
  refl,

end

为什么我不需要hA在这个证明中使用归纳假设？直觉上，我似乎应该“用尽”证明过程中产生的一切。作为参考，产生的两个归纳假设是

hA : t * (A + B) = t * A + t * B → t * (A + succ B) = t * A + t * succ B,
hB : t * (succ A + B) = t * succ A + t * B

Answer 1

在这个证明中实际上不需要第二次归纳。您为该succ案例编写的证明有效，无需先进行归纳A，只需将每次提及的内容替换succ A为a

这个证明应该有效。

lemma mul_add (t a b : nat) : t * (a + b) = t * a + t * b :=

begin

  induction b with B hB,

  -- b base case
  rw add_zero a,
  rw mul_zero t,
  rw add_zero (t*a),
  refl,

  rw add_succ a B,
  rw mul_succ t (a + B),
  rw hB,
  rw add_assoc (t*a) (t*B) t,
  rw <- mul_succ t B,
  refl,

end

有时，您可能需要对自然数是否为零进行大小写拆分，但不使用归纳假设，但这不是其中一种情况。