coq

1열

1답변

에 식을 해결, 나는 하나의 표현이 여러 인스턴스를 해결하려면 : Inductive SR: Prop := Sen | Inf. Parameter CA S: Prop. Parameter X: SR -> CA -> Prop -> Prop. Parameter X': SR -> CA -> Prop -> Set. Parameter XP: SR -> CA ->

0열

1답변

Coq에서 HoTT 경로 유도를 사용하는 방법? COQ에서

나는 Definition f (s:Unit) : tt=tt := match s with tt => idpath end. Definition g (p:tt=tt) : Unit := match p with idpath => tt end. 을하고 난 forall (p:tt=tt), (f o g) p = p을 증명하고 싶습니다. HoTT의 책에서 1.12.1

1열

1답변

Coq HoTT - 정리를 올바르게 정리하는 방법은 무엇입니까?

HoTT의 책에서 정리 2.8.1에 대한 증명을 완료했습니다 (아래 참조). 그것은 그러나 나는이 경고 Toplevel input, characters 0-4: <warning> Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-n

2열

1답변

유도의 재귀 적 단계에서 Fixpoint를 '펼치기'사용하기

나는 coq에서 뭔가를 증명하려고 노력하고 있으며 같은 문제가 계속 발생합니다. 유도의 재귀 적 (nil이 아닌) 단계에서 Fixpoint의 정의를 펼치고 싶습니다. 목록 역 (REV)을 전개하기 전에 정의 : n : nat l' : natlist IHl' : rev (rev l') = l' =====================

1열

1답변

not_iff_compat가 현재 환경에서 발견되지 않았습니다.

저는 Coq을 처음 사용 했으므로 증명에서 not_iff_compat theorem을 사용할 때 오류가 있습니다. Require Import Coq.Init.Logic. Lemma dummy: forall A B, (A <-> B) -> (~A <-> ~B). Proof. apply not_iff_compat. Qed. COQ는 저에게 말

2열

1답변

`PartialMap` typeclass에`Map` typeclass를 특화하십시오

Map 및 PartialMap이라는 두 가지 유형의 안경을 정의했으며 이러한 데이터 구조에 대한 명확한 규칙이 있습니다. 특히, 이들은 단지 V 또는 option V을 초과하는지 여부에서만 차이가납니다. PartialMap은 본질적으로 Map의 특별한 경우입니다. 그러나, 나는 그것을 인코딩하는 방법을 잘 모르겠습니다. Class Map M K V: Typ

1열

1답변

쌍

내가 형 TR 두 쌍의에서 다음 정리를 증명하려는 의 평등을 확인하는 방법 : 지금은 Definition s:= nat. Definition d:= nat. Definition c:= nat. Definition p:= nat. Inductive rt: Set := |al : rt |bl : rt. Definition

0열

2답변

Coq true = false 차별 실패, 원시 동등하지 않음

다음을 증명하기 위해 노력하고 있으며 b 및 모든 단일 인수 부울 함수에 대한 모든 사례를 열거하여 해결할 수있는 올바른 접근 방법이 있다고 생각합니다. f 4 개의 함수가 2 개의 부울 값보다 많음) 모든 것을 철저히 파괴함으로써 그 점을 증명합니다. 그러나 Theorem example : forall (f : bool -> bool) (b :

1열

1답변

MSets에서 유도 교정본

Coq 개발에서 MSet 라이브러리를 사용하려고하는데 라이브러리에없는 map 함수가 필요하지만 일반적으로 fold을 사용하여 구현할 수 있습니다. 다음은 gist입니다. 필자가 직면 한 것의 단순화를 풀었습니다. Definition map (f : Exp -> Exp) s := MSet.fold (fun a ac => MSet.add (f a) a

2열

1답변

단순한 형식의 람다 계산식에서 닫힌 용어의 자유 변수에 대한 유도 가설

나는 Coq에서 간단히 형식화 된 람다 미적분을 형식화하려고하고 있는데, 다음과 같은 문제를 가지고있다. 빈 컨텍스트가 비어 있습니다. 다음은 공식화의 관련 부분입니다. Require Import Coq.Arith.Arith. Require Import Coq.MSets.MSets. Require Import Coq.FSets.FMaps. Induc