Coq简单/展开一次。（用功能的一次迭代的结果替换目标的一部分。）

Question

我是一所大学的讲师，参加一门名为“ 类型系统的语言 ” 的课程，在最后一次讲解中，该教授将以下示例用于类型理论的归纳证明：

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

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

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

ps .：我知道我可以simpl in IHt再使用exact，但它会扩展为match表达式，比这里需要的更为冗长。

编辑：感谢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

如你所愿。