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

我可以通过重写、展开和/或简化的多种方式来解决这个问题，但我真正想做的是应用一次greaterThan的迭代，将(suc (suc t) > suc t) = true转化为(suc t > t) = true，然后我可以用exact IHt完成证明。

有没有办法实现这个？

附注：我知道我可以使用simpl in IHt然后使用exact，但它会展开匹配表达式，比在这里需要的更冗长。

编辑：感谢Théo Winterhalter的回答，我意识到我也可以单独使用exact，因为这些术语是可转换的，但这不会很好地向学生展示过程。（顺便说一句：归纳的两种情况也可以用trivial解决，但我认为他们从中学到的东西不多。:D）

- Isti115

Answer 1

另一种可能性是使用“Arguments”措辞，告诉“simpl”不要将“greaterThan”简化为匹配表达式。在“greaterThan”的定义之后的某个地方放置“Arguments greaterThan: simpl nomatch.”。然后当您在环境中使用“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

如您所愿。

- SCappella

Answer 2

我不确定一开始就有一种方法可以做到这一点。

通常的方法是通过自反证明对应于计算规则的引理：

Lemma greaterThan_suc_suc :
  forall n m,
    suc n > suc m = n > m.
Proof.
  intros. reflexivity.
Defined.

我使用defined，这样它就会真正展开为eq_refl，如果需要，它就会消失。

还有一种可能是手动进行替换，可以使用change命令。

change (suc (suc t) > suc t) with (suc t > t).

它将检查可转换性并在目标中用另一个表达式替换一个表达式。

您可以通过编写策略来自动化此过程，该策略将执行简化操作。

Ltac red_greaterThan :=
  match goal with
  | |- context [ suc ?n > suc ?m ] =>
    change (suc n > suc m) with (n > m)
  | |- context [ suc ?n > zero ] =>
    change (suc n > zero) with true
  | |- context [ zero > ?n ] =>
    change (zero > n) with false
  end.

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

  (* zero *)
  - red_greaterThan. reflexivity.

  (* suc t *)
  - red_greaterThan. assumption.
Qed.

- Théo Winterhalter

---

虽然这不完全是我想要的（因为它们是可转换的，我也可以仅使用 exact，这不会向学生展示过程），但改变似乎仍然是我最好的选择，所以非常感谢您提到了这种可能性！如果没有更好的答案出现，我将标记您的答案为被接受的。 - Isti115

希望有人能够做到。我也会很高兴。我会更新我的答案并提供更多内容。 - Théo Winterhalter

感谢您更新的内容，我非常感激！最终我已将SCappella的答案标记为被接受的，因为它似乎更适合我所寻找的（需要较少的解释），但其他提出的想法也很棒，值得记住！ - Isti115