coq

2열

1답변

목록에 주어진 nat가 목록에없는 가장 작은 값을 반환하는 Coq 함수를 작성하려면 어떻게해야합니까?

Coq는 인수가 감소하지 않기 때문에 아래 기능을 받아들이지 않습니다. 그러나 fvs의 길이가 유한하므로 함수가 종료됩니다. Fixpoint generate_unique_name (fvs: list nat) (base: nat) : nat := if (isIn fvs base) then (generate_unique_name fvs (S base)) el

2열

1답변

유도로 두 고정 점 함수를 증명합니다.

2 개의 고정 소수점 정의가 포함 된 겉보기에는 간단한 보조 정리로 고민하고 있습니다. From Coq Require Import Vector Program. Import VectorNotations. Program Fixpoint Vnth {A:Type} {n} (v : t A n) : forall i, i < n -> A := match

1열

1답변

Coq에서 선택적으로 재 작성하는 방법은 무엇입니까?

a : nat fvs : list nat H : a = max (maxNum fvs) a + 1 H1 : max (maxNum fvs) a >= a Doing rewrite H in H1.은 a을 모두 대체하는 반면, 나는 RHS에서만 a를 다시 쓰려고합니다. 할 수 있습니까? 나는 위의 두 가지 가설들로부터 거짓을 증명하고 싶다.

3열

1답변

Coq에서 다음 형식의 함수를 작성하려면 어떻게해야합니까?

f x = f (g subtermOfX) 함수에 대한 arg가 전달 된 arg의 직접적인 하위 항목 인 경우에만 재귀가 허용됩니까? Coq가 실제로 종료되는 것을 볼 수 있도록하려면?

1열

1답변

Coq`path` 구현

다음은 최대 Coq equality implementation입니다 (이 질문은 자체 포함되어 있음). 고정 된 수의 자식이있는 고정 된 태그 집합 (arityCode)을 가진 간단한 유도 형 나무 (t)가 있습니다. 트리 형태의 경로 (path)가 있습니다. 일부 조작을 구현하려고합니다. 특히 커서를 여러 방향으로 움직일 수 있기를 원합니다. 이것은 매우

2열

1답변

Coq에서 "if then else"는 부울이 아닌 첫 번째 인수를 허용합니까?

if a then b else c이 match a with true => b | false => c end을 나타내는 자습서를 읽었습니다. 그러나 전자는 a의 형식을 매우 이상하게 검사하지 않지만 후자는 물론 a이 부울임을 확인합니다. 예를 들어, Coq < Check if nil then 1 else 2. if nil then 1 else 2

1열

1답변

종속 유형 인스턴스 간의 평등성 입증

대수적 구조 (예 : 모든 단일체 클래스)에 해당하는 클래스를 형식화하려고 시도하면 자연스러운 설계는 필요한 모든 모델을 모델 유형으로 monoid (a:Type)을 생성하는 것입니다 필드 (요소 e:a, 운영자 app : a -> a -> a, 모노로이드 법칙이 충족됨을 증명 함). 이렇게하면지도 monoid: Type -> Type이 생성됩니다. 이 접

0열

1답변

posets에서 null 요소의 유일성 증명에 매달려

Posets에서 사실을 구현하여 COQ를 배우려고합니다. 내 첫 번째 정리를 증명하는 동안 나는 여기에서 붙어있다. Class Poset {A: Type} (leq : A -> A -> Prop) : Prop := { reflexivity: forall x y : A, x = y -> (leq x y); antisymmetry: foral

0열

2답변

어떻게하면 Coq 가설 'd = d + 1'에서 '거짓'과 확장으로 무엇을 증명할 수 있습니까?

Goal forall (d : nat), d + 1 = d -> False. Proof. intros d H. Abort. False을 H에서 어떻게 증명할 수 있습니까? inversion H이 복제 중입니다.

0열

2답변

Coq에서 무한 표현의 유한 부분 집합으로 계산하기

나는 (Z, Z)에서 whatever까지 일종의지도로 취급하는 함수 Z -> Z -> whatever을 가지고 있는데, 이것을 FF으로 입력합시다. whatever은 nix 또는 inj_whatever에서 구성 가능한 단순한 합계입니다. 내가의 방식으로, 일부 데이터 초기화이지도 : Definition i (x y : Z) (f : FF) : FF :=