Coq 仅简化/展开一次。（用函数一次迭代的结果替换目标的一部分。）

Question

我是大学 class 的讲师，教授的题目是 语言的类型系统 ，教授最后在黑板上使用了以下类型理论中的归纳证明示例讲座：

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 代码以在 class 中实现它：

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，但它扩展到匹配表达式，这比这里需要的要冗长得多。

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

Answer 1

我不确定有什么方法可以立即做到这一点。一种常用的方法是通过自反性证明对应于计算规则的引理：

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.

Answer 2

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

如你所愿。

Coq 仅简化/展开一次。（用函数一次迭代的结果替换目标的一部分。）

Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)

coq

proof

coq-tactic

induction

Coq 仅简化/展开一次。 （用函数一次迭代的结果替换目标的一部分。）

Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)

coq

proof

coq-tactic

induction

Coq 仅简化/展开一次。（用函数一次迭代的结果替换目标的一部分。）