coq

0열

2답변

보조 증명 COQ를 사용하고 있습니다. 내 첫 번째 질문은 Induction.v 파일에 관한 것이고 Require Import basics 대신 Require Export Basics을 사용해야하는 이유는 무엇입니까? 또한 기본 이름을 Mybasics.v으로 변경하더라도 Export basics.v을 만들면 왜 작동합니까? Require Export Bas

4열

1답변

, 명령`가져 오기 BigN` 8.6 COQ 사용했다하지만 COQ에

8.7 내가 COQ 8.6 COQ 8.7 I와 라이브러리하지만 수입 코드 Require Import BigN.으로의 bignum에게 $ opam upgrade bignum Already up-to-date. 를 설치하는 OPAM을 사용 필요 오류가 발생합니다. 그래서이 코드 줄을 bignum_problem.v 파일에서 분리했습니다. 그런 다음 coqc

2열

1답변

COQ 항목 1.2.10 유형 캐스트

확실하지 무엇 COQ 매뉴얼 v8.7.0 item 1.2.10에서 다음과 같은 방법 : 표현 "용어 : 유형"는 형 캐스트 표현이다. 유형이 유형이되도록합니다. "용어 < : 유형는"로컬 용어이 유형 입력이 있는지 확인하기 위해 가상 머신을 설정합니다. 제 생각에는 첫 번째 유형 검사는 Coq (기본값)로 수행되는 반면, 두 번째 검사는 선택된 Coq의

3열

1답변

왜 coqide에서 _CoqProject를 사용하여`make '가 명령 행에서`coqc`와 다른가요?

나는이 개 짧은 파일이 : cc_test이 Lemma cc: 4 = 4. Proof. auto. Qed. 에 의해 주어지고 libtest은 내가 실행 Require Import cc_test. Check cc. 에 의해 주어진다 디렉토리에 coqc -R . ClosureLib -top ClosureLib cc_test "/ 홈/베리/SVN/COQ/Closu

0열

1답변

부울

을 포함하는이 간단한 증거를 완료하는 방법이 운동에 내 진행 여기에서이다 : https://github.com/userhr/MIT-6.826-2017 (** **** Exercise: 2 stars (andb_true_elim2) *) (** Prove the following claim, marking cases (and subcases) with

2열

3답변

전술 자동화 : 간단한 결정 절차

ASCII 문자가 공백인지 아닌지에 대한 결정 절차를 자동화하려고합니다. 여기 제가 현재 가지고있는 것이 있습니다. Require Import Ascii String. Scheme Equality for ascii. Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char)

2열

1답변

`remember (f x)와 같음 : y eqn : H; H를 맑게하십시오; 명확한 x`?

때로는 다른 공간으로 투영하여 가장 좋은 증거가 있습니다. remember (f x) as y eqn:H; clear H; clear x. 내가 Ltac 이것을 자동화하려고 : 순간 나는 다음을 수행 Ltac project x y := let z := fresh in remember x as y eqn:z; clear z; clear

6열

1답변

'nat'에 주사에서 유형에 대한 결정적인 총 주문을 얻습니다.

자연수가 결정 가능한 전체 순서를 지원하기 때문에 ascii 유형의 결정적인 총 주문이 유도됩니다. nat_of_ascii (a : ascii) : nat Coq에서 이것을 표현하는 간결하고 관용적 인 방법은 무엇일까요? (유형 클래스, 모듈 등의 유무에 관계없이)

7열

1답변

Coq에서 계산 된 형식의 암시 적 인수

명시 적으로 인덱스를 스레드 할 필요없이 인덱싱 된 형식을 쓰는 라이브러리가 있습니다. 이것은 관련없는 배관을 숨겨서 더 깨끗한 최상위 유형으로 이어집니다. 에 의해 입증 된 바와 같이 Section Indexed. Local Open Scope type. Context {I : Type} (T : Type) (A B : I -> Type). De

3열

1답변

Streicher_K_ Axiom을 사용하는 방법

누군가가 간단한 예제를 보여줄 수 있습니다 Streicher_K_ 공리를 Coq.Logic.EqdepFacts에서 사용하는 방법? 은 어쩌면 단순한 사실을 보여주는 : 나는 또한 인 Streicher_K_으로 그것을 증명하는 방법을 찾아 시행 착오 Variable A:Type. Variable x:A. Axiom SK:Streicher_K_on_ A x