>

증명 코드를 고려하십시오 :

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

    그래서 이야기는 흥미롭고 직관적이지 않습니다.

    용법 : tac; cycle   ; cycle 때문에작동   cycle 를 실행  모든목표에서 올바르게 순환합니다.

    그러나 pyzwyz  하지 않습니다. 왜요?

    그 이유는 tac. cycle  "현재 목표 선택기를 호출 한 다음 tac. 를 실행합니다. ". 기본 목표 선택기는 tac 입니다. .

    이로 인해 Focus 1 가 발생합니다  아무것도하지 않는 1 개의 목표 (가짜 진 목표) 목록을 순환하려고 시도합니다.

    그러나이 모델에서는 cycle   swap 1 2 를 바꾸려고 시도하기 때문에 오류가 발생합니다.  그리고 1  하나의 목표 목록에서. 2 에서 이것에 관한 문제를 제기했습니다.  버그 추적기

    해결책은 coq 를 사용하는 것입니다.  또는 all: swap . 이것은 all:cycle 를 허용하는 모든 목표에 먼저 중점을 둡니다.  그리고 swap  예상대로 작동합니다.

    전체 코드 목록 :

    cycle
    
    

    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

  • 이전 json - django가 d3에 데이터를 전달 - d3 eachfor는 함수가 아닙니다
  • 다음 php - NGINX 이미지가 표시되지 않습니다