나는 수학 구성 요소 라이브러리를 사용하고 있는데이 증명하려고에 의존의 형태 오류 : 마지막 재 작성 오류 메시지와 함께 실패 Lemma card_sub_ord (k : nat) (P : nat -> bool) :
#|[set i : 'I_k | P i]| <= k.
Proof.
set S := [set i : 'I_k | P i].
우분투 17.04에 Coq 8.6을 새로 설치했습니다. make를 사용하여 프로젝트를 컴파일하려고하면 첫 번째 오류 메시지가 나타날 때까지 제대로 작동합니다. 그럼, 찾아 오류를 수정 CoqIDE을 사용하려고하지만 같은 새로운 오류 메시지를 얻을 : 내 생각 엔 "파일 foo.vo 라이브러리 Top.foo하지 라이브러리 foo는 포함을" 뭔가 CoqIDE
에 대한 인스턴스를 찾을 수없는 전술을 적용 H1 : a
H2 : a -> forall e : nat, b -> g e
============================
...
내가 apply H2 in H1.을 시도, 그것은 나 건물의 한 부분으로 forall e : nat, b -> g e을 가지고 할 Error: Una
목표 상태는 다음과 같은 경우 : 지금 a : Prop
b : Prop
H1 : a
H2 : b -> c
============================
b
I을 : a : Prop
b : Prop
H1 : a
H2 : b -> c
=====================
저는 Coq을 처음 접했고 좀 더 익숙해지기 위해 연습을하고 있습니다. 내 이해는 Coq의 명제를 "실제로"증명하는 것은 Gallina의 유형을 적어 놓은 다음 용어를 결정적인 방식으로 결합하는 전술을 사용하여 거주하고 있음을 보여주는 것입니다. 모든 전술을 제거한 상태에서 실제 용어를 예쁘게 인쇄 한 표현을 얻는 방법이 있는지 궁금합니다. 아래 예에서는
저는 Coq를 배우기 시작했고 매우 간단하게 보이는 것을 증명하려고합니다. 목록에 x가 포함되어 있으면 해당 목록의 x 인스턴스 수가 0이됩니다. 내가 정의한 포함하고 있으며 다음과 같은 기능을 수 : Fixpoint contains (n: nat) (l: list nat) : Prop :=
match l with
| nil => Fals
함수를 정의하려면 함수의 인수가 (적어도) n 위치 함수인지 여부에 따라 달라집니다. 초보 (실패) 시도 rT는 False에 모든 매핑, Definition rT {y:Type}(x:y) := ltac: (match y with
| _ -> _ -> _ => exact True
| _ => exact False end).
Check prod: Typ
에 붙어 있습니다. 아래에 표시된 접미어과 같은 유도 관계가 있습니다. 나는 관련 theorem suffix_app을 증명하려고 노력하고 있습니다. 내 일반적인 생각은 xs가 ys와 같거나 몇 가지 일련의 요소임을 나타내는 접미사 xs ys이라는 사실을 사용하는 것입니다. cons ' Require Import Coq.Lists.List.
Import L
나는 일반적인 설정을 가지고 있습니다. 먼저 몇 가지 유형을 정의한 다음 해당 유형의 일부 기능을 정의합니다. 그러나, 내가하는 일을 형식화하는 많은 방법이 있으므로, 나는 3 가지 버전으로 그것을 할 것입니다. 단순화 (그리고 개요를 유지하기 위해), 나는 하나의 파일에 내 코드를 원한다. 또한 반복 코드을 최소화하고 싶습니다. 기능 f: A -> B의
내가 타이핑 및 하위 유형의 관계에 대한 예를 들어, 판단의 여러 종류의 표기법을 만들 싶습니다 표기법 : 내가 알고있는 것처럼 Reserved Notation "Г '⊢' t '∈' T" (at level 40).
Reserved Notation "Г '⊢' T '<:' U" (at level 40).
Inductive typing_relation