4
Coq에서 레코드의 평등성을 증명하려고 시도 할 때 해당 필드를 모두 평등하게 분해하는 전술이 있습니까? 예 :기록적인 평등을위한 전술 계수?
Record R := {x:nat;y:nat}.
Variables a b c d : nat.
Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.
a = c /\ b = d으로 줄일 수있는 방법이 있습니까? 일반적으로 a b c d 중 하나는 큰 복잡한 증명 용어 일 수 있습니다 (나는 증명할 수있는 무의미한 공리로 해방 할 수 있음).
@ Zimm i48 'coq-tactic'에 대한 설명은 다음과 같습니다. "전술은 목표와 용어를 변형시키기 위해 Coq 증명 보조자에서 사용되는 형식이 지정되지 않은 언어 인 Ltac으로 작성된 프로그램입니다." 내 이해에서 이것은 Ltac을 사용하여 * 전술을 쓰는 방법에 대한 질문 또는 일반적으로 증명 자동화에 관한 질문을 의미합니다. 그러나 나는 그 설명이 약간 모호하다는 것을 인정한다. –
좋아요, 롤백하기가 자유 롭습니다. 설명을 향상 시키시겠습니까? 태그 이름을 ltac로 변경하는 것일까 요? 그것은 훨씬 더 명확해질 것입니다! –
@ Zimm i48 전체 설명을 살펴본 결과, "이 태그는 Coq 증명 보조자를 사용하여 증명을 유도하기 위해 coq 전술을 사용하는 데 관련된 문제와 관련된 질문에 사용해야합니다." 이 경우 편집 내용이 완벽하게 맞다고 생각합니다. 나는 (1) 태그 정보를 편집하여 사용법을 명확하게 할 것이다; (2) 새로운 태그'coq-ltac'를 생성하십시오; (3) 일부 게시물에 coq-ltac을 추가하여 의도 된 사용법을 보여줍니다. (4) 어쩌면 우리는 모든 coq-tactic 질문 (현재 56 개가있다)을 거쳐야하며, 실제로 전술 관련 문제인지 확인해야한다. –