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值爲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. 

附：這個問題可能會使用更好的標題。請建議。

Answer 1

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工作。