나는 다음과 평등을 증명하기 위해 노력하고 COQ

평등 FORALL :나는 다음과 평등을 증명하기 위해 노력하고 COQ

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.을 이 질문은 더 나은 제목을 사용할 수 있습니다. 제발 제안 해주세요.

출처

2017-10-11 krokodil

나는 Coq 라이브러리가 어딘가에 'nm nm'의 단일성을 증명할 수 있다고 생각한다. 그렇지 않다면 나는 coq-club에서 두 번 뜬 것으로 보았다. 따라서 메일 링리스트 아카이브를 검색해 볼 수도있다. . 그런 다음 재 작성을 허용해야하는'ic0'과'ic1'을 일반화 할 수 있습니다. –

여기에서 유니티를 사용하는 방법을 모릅니다. 그런데 도움이된다면 부적합이라는 증거를 사용하는 것이 좋습니다 ... – krokodil

remember이 버그이기 때문에 subst 전술이 실패합니다. 이 버그는 here으로보고되었습니다. (abstract admit, admit이 Coq.Compat.AdmitAxiom에서 오는 목표를 확인하고 완료하면 유형 오류로 실패하지 않아야합니다. 그렇다면 Coq (또는 사용중인 플러그인)에 버그가 있음을 의미합니다.

당신이 n - n 및 0 mod S n이 judgmentally 동일한 것으로, 어떤 의미에서, 운이있어

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.

참고 : 여기에

는 작업 증거 (8.6.1 및 8.7 + 베타 테스트)입니다. simpl을 사용하면이 사실을 알 수 있으며 rewrite을 사용할 수 있습니다.

출처

2017-10-11 05:30:34

나는 다음과 평등을 증명하기 위해 노력하고 COQ

답변

관련 문제