홈>
증명 코드를 고려하십시오 :
Definition f (a: nat): nat.
Proof.
Admitted.
Lemma rew: forall (a p : nat) (A: a + 1 = p),
f a = f p.
Proof.
Admitted.
Lemma userew: forall (a b: nat), f a = f b.
Proof.
intros.
erewrite rew.
cycle 1.
(* Goal does not cycle *)
swap 1 2.
(* Goal does not swap *)
Abort.
안타깝게도,
cycle
그리고
swap
작동하지 않습니다. 왜, 어떻게 올바르게 사용합니까?
- 답변 # 1
관련 자료
- unreal 4 - Pitch, Roll 및 Yaw 대신 X, Y 및 Z를 사용하는 방법
- javascript - Vue 3 사용 및 플러그인 Boostrap-vue 추가 방법?
- node.js - FFMPEG 및 노드에서 스트림을 사용하는 방법
- c# - ASPNET에서 ConcurrentDictionary 및 Task를 사용하는 방법
- next.js - NextJS에서 Linaria를 어떻게 사용할 수 있습니까?
- C에서 realloc을 사용하는 방법
- postgresql - 조인 SQL 쿼리에서 Case를 사용하는 방법
- mysql - LEFT JOIN으로 WHERE 조건을 사용하는 방법은 무엇입니까?
- c# - 내 코드에서이 Crc32 클래스를 사용하는 방법
- python - pip로 설치할 때 git repo에서 py 스크립트를 사용하는 방법
- html - 슬라이더 틱과 함께 span 태그를 사용하는 방법은 무엇입니까?
- compression - ZLIB deflate 방법을 사용하는 방법?
- python - 입력을 사용하여 함수를 호출하는 방법은 무엇입니까?
- oop - PHP에서 MVC 패턴을 올바르게 사용하는 방법
- swift - NSStoryboardSegue와 함께 tableViewrow를 사용하는 방법
- typescript - fp-ts에서 파이프를 사용하여 if 문을 제거하는 방법
- vue.js - 계산 된 속성에서 소품을 사용하는 방법은 무엇입니까?
- string - Ruby 변수 인수에서 "# {…}를 사용하는 방법?
- keras - 텍스트 분류에 GPT 3를 어떻게 사용할 수 있습니까?
- db2 - CONCAT에서 문자열을 사용하는 방법
관련 질문
- Coq: 평등 전술의 대칭성과 전이성은 어떻게 정의됩니까?
- coq - 목표를 모순하여 증명하는 방법?
- coq - 일부의 평등을 증명하는 방법
- coq tactic - 이중 의미로 Coq 사용 개선
- coq tactic - Coq에서 True-> P 형식의 가설을 어떻게 단순화합니까?
- SSReflect 산술 문과 함께 Coq 산술 솔버 전술을 사용하는 방법
- equality - coq에서 유도 원리를 명시 적으로 사용하는 방법은 무엇입니까?
- theorem proving - Coq에는 Rabs, Rineq와 함께 작업하기위한 전술이 있습니까?
- coq - Fixpoint 정의를 기반으로하는 증명 Lemma
- proof - coq - eqb_list_true_iff의 가설에 귀납 가설 적용
그래서 이야기는 흥미롭고 직관적이지 않습니다.
용법 :
그러나 pyzwyz 하지 않습니다. 왜요?tac; cycle
; cycle
때문에작동cycle
를 실행 모든목표에서 올바르게 순환합니다.그 이유는
tac. cycle
"현재 목표 선택기를 호출 한 다음tac.
를 실행합니다. ". 기본 목표 선택기는tac
입니다. .이로 인해
그러나이 모델에서는Focus 1
가 발생합니다 아무것도하지 않는 1 개의 목표 (가짜 진 목표) 목록을 순환하려고 시도합니다.cycle
swap 1 2
를 바꾸려고 시도하기 때문에 오류가 발생합니다. 그리고1
하나의 목표 목록에서.2
에서 이것에 관한 문제를 제기했습니다. 버그 추적기 해결책은coq
를 사용하는 것입니다. 또는all: swap
. 이것은all:cycle
를 허용하는 모든 목표에 먼저 중점을 둡니다. 그리고swap
예상대로 작동합니다.전체 코드 목록 :
TL;DR사용
Definition f (a: nat): nat. Proof. Admitted. Lemma rew: forall (a p : nat) (A: a + 1 = p), f a = f p. Proof. Admitted. Lemma userew: forall (a b: nat), f a = f b. Proof. intros. erewrite rew. (* NOTICE all: *) all: cycle 1. (* NOTICE all: *) all: swap 1 2. Abort.
또는tactic; swap
all:swap