이 질문은 Software Foundations,에서 영감을 얻었지만 운동에 관한 것은 아닙니다. 내가 아는 바로는, 지금까지. Imp 장 ("간단한 명령 프로그램")은 단순한 환경에 대한 기능 맵 ("총계 및 부분 맵"에서)을 사용합니다. [1] 프로그래밍 언어. 임프의 장에서 프로그램에 대한 Inductive id : Type :=
| Id :
Coq's XML Protocol document (for the Add operation)에서 줄은 <int>${editId}</int>입니다. 편집 ID는 무엇입니까? ideslave 모드에서 coqtop과 상호 작용하지 못했기 때문에이 질문을했습니다. 예를 들어 coq-8.6.1/theories/FSets/FSetCompat.v를 사용하여, I는 <c
clear_multiple H1, H2, H3.과 같은 일을하기 위해 여러 가설을 정리하는 전술을 갖고 싶다고 말합니다. 나는 다음과 같은 쌍을 사용하여 그렇게하려고 :이 Variable A: Prop.
Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).
내 질문은, 어떻게해야하는 것입니
나는 나를 놀라게하는 것을 이해하려고 노력하고있다. 다음 두 가지 정의를 고려하십시오. Require Import List.
Variable A:Type.
Inductive NoDup : list A -> Prop :=
NoDup_nil : NoDup nil
| NoDup_cons : forall x l, ~ In x l -> NoDup l
조건 분기에 대한 간단한 구조가 w COQ의 평등 테스트 /있다 : Check ltac:(tryif unify 1 (S 0) then idtac "success" else idtac "fail"). (*success...*)
< 및/또는 <=을 테스트하기 위해 비슷한 방법이 있나요?
저는 지난 몇 주 동안 Coq 증명 보조원과 함께 일해 왔지만 오늘은 특별한 무엇인가를 겪었습니다. 벤자민 피어스 (Benjamin Pierce)의 "Types and programming languages"책의 연습을 통해 작업하고 있습니다. 이 실습 중 하나에서 특정 hoare 셋이 유효하다는 자체 제작 프로그래밍 언어 (Pier in의 연습 문제)에
목록 고유성 및 해당 결정 성 함수에 대한 조건부를 Coq에 정의하고 싶습니다. 내 첫 번째 시도했다 : 여기 Section UNIQUE.
Variable A : Type.
Variable P : A -> Prop.
Variable PDec : forall (x : A), {P x} + {~ P x}.
Definiti
Coq 8.7은 대중적인 Ssreflect 라이브러리를 통합합니다. 나는 그것이 Unable to locate library ssrnat with prefix Coq의 불평 ssrnat 가져올 때, 그러나 From Coq Require Import ssreflect ssrfun ssrbool.
, 그리고 나도 디스크에 COQ 분포 ssrnat을 찾을 수
f : x -> y -> z이라는 정의가 있다고 가정하면 x을 쉽게 추론 할 수 있습니다. 을 사용하여 x에 암시 적 인수를 사용하도록 선택했습니다. Definition id : forall (S : Set), S -> S :=
fun S s => s.
Arguments id {_} s.
Check (id 1).
은 분명히 S = nat 될 수