coq - Coq简单/展开一次。 (将目标的一部分替换为函数的一次迭代的结果。)

我是大学的讲师，课程名为“语言类型系统”，最后教授在董事会上使用以下示例对类型理论进行归纳证明
演讲:

假设存在归纳定义的自然数(由于某种原因，他坚持称其为术语)，而我们在它们上递归定义了一个大于函数。我们可以证明，对于每一个n，它都拥有(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

我可以通过重写，展开和/或简化来以多种方式解决这个问题，直到它变成反射性，但是我真正想做得更干净的方法是应用GreaterThan的一个迭代，这只会将(suc (suc t) > suc t) = true变成(suc t > t) = true ，然后我可以使用exact IHt完成证明。

有没有办法解决这个问题？

ps .:我知道我可以先simpl in IHt然后使用exact，但是它扩展为match表达式，比这里需要的更加冗长。

编辑:感谢Théo Winterhalter的回答，我意识到我也可以单独使用exact，因为这些术语是可转换的，但是对学生来说并不能很好地说明这一过程。 (附带说明:两种归纳情况也可以用trivial解决，但是我认为它们都不会对它们有太多了解。:D)

最佳答案

另一种可能性是使用本地的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

如你所愿。