FORALL平等勒柯克

我试图证明以下等式：FORALL平等勒柯克

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值为0 Nat.sub_diag和0 mod S n也为0的Nat.mod_0_l。不过，我无法轻易将这些引理应用于类型。我试过的remember/rewrite/subst惯用的伎俩，但subst部分失败：

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

附：这个问题可能会使用更好的标题。请建议。

来源

2017-10-11 krokodil

我认为Coq库可能在某个地方具有“lt nm”的单一性 - 如果不是这样，我想我已经看到它在coq-club上浮动了几次，因此您可以尝试搜索邮件列表存档。然后，你可以概括'ic0'和'ic1'这应该有希望允许重写。 –

不知道如何在这里使用unicity。顺便说一下，如果有帮助，我可以使用证明不相关的方法。 – krokodil

subst战术失败，因为remember是越野车;我已经报告了这个错误here。（作为一个理智，检查，完成一个目标abstract admit，其中admit来自Coq.Compat.AdmitAxiom，应该永远不会因为类型错误而失败。如果确实如此，这意味着Coq（或您正在使用的插件）中存在错误。）

这里是一个工作证明（在8.6.1和8.7 +β2测试）：

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是judgmentally相等。使用simpl公开此事实，并允许rewrite工作。

来源

2017-10-11 05:30:34

FORALL平等勒柯克

回答

相关问题