저는 Coq을 처음 접했고 완전히 잘못된 길을 가고있을 수도 있습니다. 인간이 읽을 수있는 형태로 구문을 너무 많이 숨기고 자동 전술이 실패하기 때문에 인간이 읽을 수있는 공리/정리 인 공리/정리 (공리/정리) 중에서 힌트로 유용한 정리를 선택해야합니다. 그들을 사용합니다. 나는 두 세계의 장점을 누릴 수있는 방법이 있는지 알고 싶습니다.Coq : 의미있는 힌트를 추가하는 방법?
나는 조금 더 정교한 예를 제시 할 것이다. 그렇지 않다면 나는 내 뜻을 전달할 수 없을 것이라고 두려워하기 때문이다.
학습 운동으로 나는 그룹 이론을 시도하고 있습니다. 여기 내 정의는 다음과 같습니다.
Variable G: Set.
Variable op: G -> G -> G.
Variable inv: G -> G.
Variable e:G.
Infix "+" := op.
Notation "- x" := (inv x).
Definition identity x := forall a:G, a + x = a /\ x + a = a.
Definition associative_law := forall a b c:G, a + (b + c) = (a + b) + c.
Definition identity_law := identity e.
Definition inverse_law := forall a:G, a + (-a) = e /\ -a + a = e.
Definition group_laws:= associative_law /\ identity_law /\ inverse_law.
Axiom group_laws_hold: group_laws.
나는 모든 것을 사람이 읽을 수 있도록하려고 시도했다. 그래서 전자가 정체성이라고 말하는 공리는 "group_laws"와 "identity"라는 두 추상화 계층 뒤에 숨어 있습니다.
나는이 공리를 작성할 수직접 (물론, 나는 그것의 절반이 필요합니다) :
Axiom identity_law_holds: forall a:G, a + e = a.
을 지금, 힌트로 우리 그룹 - 공리를 보자 :
Hint Resolve group_laws_hold.
을 지금 나는 그룹에 대한 단순한 진술을 증명하려고한다. 정체성은 유일하다 :
지금까지는 그렇게 좋았다. 이제 나의 현재 목표는 "x + e = x"입니다. 내가 지금한다면
apply group_laws_hold.
이 목표는 해결 될 것입니다. 그러나 "auto"를 수행하는 것은 아무 것도하지 않습니다. 아마도 "group_laws_hold"가 "x + e"와 같은 구문이 아니기 때문에 Coq는 "group_laws_hold"가 "x + e = x" = x ". 내가 힌트를 추가하는 경우
그러나
Hint Resolve identity_law_holds.
Axiom identity_law_holds: forall a:G, a + e = a /\ e + a = a.
그런 다음 "자동"다시 실패합니다.
내 질문은 : "자동"작동하지만 내 "일반 공감 identity_law_holds : forall a : G, a + e = a"보다 일반적인 힌트와 같은 코드를 수정하는 방법이 있습니까?