求解Software Foundations中leb_plus_exists与plus_leb_exists证明问题

定理1：leb_plus_exists #

Theorem leb_plus_exists : forall n m, n <=? m = true -> exists x, m = n+x.

证明思路： #

对自然数n进行归纳：

• 基例（n=O）：
  此时O <=? m = true恒成立，取x=m即可满足m = O + m（依赖plus_O_n定理），用exists m后调用reflexivity完成。
• 归纳步（n=S n'）：
  归纳假设为：forall m, n' <=? m = true -> exists x, m = n' + x。
  假设(S n') <=? m = true，根据leb定义，m不可能是O（否则假设不成立），对m做destruct：
  • 若m=O：直接用contradiction推翻假设。
  • 若m=S m'：假设化简为n' <=? m' = true，应用归纳假设得到exists x, m' = n' + x，对该存在量词destruct得具体x和等式。
    推导m = S m' = S (n' + x) = (S n') + x = n + x（依赖plus_n_Sm定理），用exists x后通过rewrite等式完成证明。

定理2：plus_exists_leb #

Theorem plus_exists_leb : forall n m, (exists x, m = n+x) -> n <=? m = true.

证明思路： #

先对假设中的存在量词destruct，得到具体x和等式H: m = n + x，再对x进行归纳：

• 基例（x=O）：
  此时m = n + O = n（依赖plus_O_n定理），需证n <=? n = true，直接调用leb_refl或展开leb定义验证即可。
• 归纳步（x=S x'）：
  归纳假设为：forall n m, m = n + x' -> n <=? m = true。
  此时m = n + S x' = S (n + x')（依赖plus_n_Sm定理），对n分情况讨论：
  • 若n=O：O <=? S (O + x')恒为true（符合leb定义）。
  • 若n=S n'：根据leb定义，(S n') <=? S (n + x')等价于n' <=? (n + x')，而n + x' = S n' + x' = S (n' + x')，只需证n' <=? S (n' + x') = true——这可通过leb的递归性质推导：任意自然数k，n' <=? S k恒为true，递归到n'=O时直接成立，否则继续缩小自然数规模直至基例。

内容的提问来源于stack exchange，提问作者VikramG