Coq 中的 forall 平等

Question

我试图证明以下等式：

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A)
(ic0 : 0 < S n) (ic1 : 0 mod S n < S n):
  gen (n - n) ic1 = gen 0 ic0.

n-n 是 Nat.sub_diag 的 0，0 mod S n 也是 Nat.mod_0_l 的 0。但是我不能轻易地将这些引理应用于类型。我尝试了 remember/rewrite/subst 的常用技巧，但 subst 部分失败：

   remember (gen (n-n)) as Q.
   remember (n-n) as Q1.
   rewrite Nat.sub_diag in HeqQ1.
   subst.

P.S。这个问题可能使用更好的标题。请提出建议。

Answer 1

subst 策略失败，因为 remember 有问题；我已经报告了这个错误 here。（作为理智，检查一下，用 abstract admit 完成一个目标，其中 admit 来自 Coq.Compat.AdmitAxiom，应该永远不会因类型错误而失败。如果是这样，那就意味着 Coq 中存在错误（或您正在使用的插件。）

这是一个工作证明（在 8.6.1 和 8.7+beta2 中测试）：

Require Import Coq.Arith.Arith.

Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A)
      (ic0 : 0 < S n) (ic1 : 0 mod S n < S n):
  gen (n - n) ic1 = gen 0 ic0.
Proof.
  revert ic0 ic1; simpl; rewrite Nat.sub_diag; intros ic0 ic1.
  apply f_equal, le_unique.
Qed.

请注意，从某种意义上说，您很幸运，n - n 和 0 mod S n 在判断上是相等的。使用 simpl 暴露了这个事实，并允许 rewrite 工作。

Coq 中的 forall 平等

forall equality in Coq

coq