coq-tactic

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

-1열

2답변

Coq : 문자열과 관련된 명령문을 증명하는 방법은 무엇입니까?

나는 string a을 가지고 있으며, string b과 비교할 때 같음이 string c 인 경우는 string x입니다. 나는 가설에서 fun x <= fun c이라는 것을 안다. 아래 진술서를 어떻게 증명합니까? fun은 string을 사용하는 함수이며 nat을 반환합니다. fun (if a == b then c else x) <= S (fun c)

1열

1답변

바인더에서 일반화 표현

바인더에서 표현식을 일반화해야합니다. 예를 들어, 나는 내 목표에 두 표현식이 있습니다 (fun a b => g a b c) 및 (fun a b => f (g a b c)) 을 그리고 g _ _ c 부분을 일반화 할 : 할 한 가지 방법으로 먼저 재 작성하는 것입니다 (fun a b => (fun x y => g x y c) a b) 두 번째로

2열

1답변

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

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

0열

2답변

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

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

1열

1답변

뺄셈에 대한 Coq 증명은 통근하지 않습니다.

뺄셈이 Coq에서 출퇴근하지 않는다는 것을 증명하고 싶지만 막혀 있습니다. 나는 내가 Coq에서 증명하고 싶은 성명이 쓰여질 것이라고 믿는다. forall a b : nat, a <> b -> a - b <> b - a 내가 지금까지 가지고있는 증거가있다. Theorem subtraction_does_not_commute : forall a b :

0열

2답변

Coq의 XML 프로토콜 문서에서 "editId"는 무엇입니까?

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

1열

1답변

COQ Ssreflect

나는 수학 구성 요소 라이브러리를 사용하여 다음을 증명하려고에 bigops을 포함하는 엄격한 불평등 증명 : 처음 Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R): (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) -> \sum_(i < q)

1열

1답변

CoqIde의 "Ring"전술이 허용되지 않습니다.

Coq를 배우고 있으며, 처음으로 ring 전술을 사용해야합니다. Require Ring. 또는 Require ArithRing. 뒤에 목표를 가지고있는 방정식의 오른쪽을 단순화하기 위해 사용했지만 Coq는 존재하지 않는 참조를 취합니다. 나는 (내가 ring과 ring_simplify 여러 번 시도) 여기에 코드 내 조각을 복사 Lemma sum_n_p