Coq 只简化/展开一次。 (用函数的一次迭代结果替换目标的一部分。)

Question

我是大学的讲师，参加了一个名为 Type Systems of Languages 的类(class)，教授最后在黑板上的 Type Theory 中使用了以下示例进行归纳证明
演讲:

Suppose, that there are natural numbers defined inductively (for some reason he insists on calling them terms) and we have a greater than function defined recursively on them. We can proove that for every n it holds that (suc n > n).

我准备了以下 Coq 代码来在类中实现它:

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = true.
Proof.
  induction t.

  (* zero *)
  - simpl.
    reflexivity.

  (* suc t *)
  - 

这将我带到以下目标:

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

在它变成自反性之前，我可以通过重写、展开和/或简化以多种方式解决这个问题，但我真正想做的让它更清晰的是应用一个大于的迭代，这只会变成 (suc (suc t) > suc t) = true进入 (suc t > t) = true ，我可以用 exact IHt 完成证明.

有没有办法实现这一点？

ps.:我知道我可以 simpl in IHt然后使用 exact ，但它扩展到匹配表达式，这比这里需要的要冗长得多。

编辑:感谢 Théo Winterhalter的回答我意识到我也可以使用 exact本身，因为条款是可以转换的，但这不会向学生很好地展示这个过程。 (旁注:归纳的两种情况也可以用 trivial 解决，但我认为他们也不会从中学到太多。:D)

Answer 1

另一种可能性是使用 Arguments白话告诉simpl不减少 greaterThan到匹配表达式。把 Arguments greaterThan: simpl nomatch.在 greaterThan 的定义之后的某处.那么当你使用 simpl在环境中

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc (suc t) > suc t) = true

你得到

1 subgoal
t : term
IHt : (suc t > t) = true
______________________________________(1/1)
(suc t > t) = true

如你所愿。