Coq 中的归纳之谜

编程问答 2022-05-25

问题描述

对于下面的定义和定理

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat)                : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

Theorem Sn_le_Sm__n_le_m2 : forall n m,S n <= S m -> n <= m.
Proof.
intros. remember (S n). remember (S m). induction H.
- subst. apply S_injective in Heqn1. subst. constructor.
- PROBELEM STATE

当我们进入问题状态时，CoqIDE中显示的本地上下文是

n,m,n0 : nat
Heqn0 : n0 = S n
m0 : nat
Heqn1 : S m0 = S m
H : n0 <= m0
IHle : m0 = S m -> n <= m

我不明白为什么我们会得到 IHle : m0 = S m -> n <= m。根据我的理解，由于最初的目标是 forall n m,S n <= S m -> n <= m，所以归纳假设应该是 S n <= S m0 -> n <= m0。

如果你能告诉我为什么归纳假设不是我的想法，我将不胜感激。

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

coqcoq-tacticcoqide