사례별로 증명을 사용하여 증명하고자하는 간단한 정리가 있습니다. 예가 아래에 나와 있습니다.Coq을 사용한 사례 별 증명
Goal forall a b : Set, a = b \/ a <> b.
Proof
intros a b.
...
어떻게 해결할 수 있습니까? 정확히 어떻게 평등 (True 또는 False)의 가능한 두 가지 값을 사용하여 사례별로 증명을 정의 할 수 있습니까?
도움을 주시면 감사하겠습니다. 고마워,
나는 Set의 평등이 Coq에서 결정할 수 없다고 확신한다. 이유는 (필자가 제한적으로 이해하는 한) 유도 식으로 정의 된 집합이 아니기 때문입니다 (따라서, 당신을위한 사례 분석은 없습니다 ...). 또한 닫힌 집합이 아닙니다. 새 데이터 형식을 정의 할 때마다 Set의 새 가족을 만드십시오. 따라서 귀하가 보여주는 목표를 입증 한 용어는 새로운 주민을 반영하여 업데이트해야합니다.
@hardmath가 자신의 의견에 언급 한대로 Classical 가정 (Axiom classic : forall P:Prop, P \/ ~ P.)을 사용하여 목표를 증명할 수 있습니다.
@Robin Green이 여기에서 언급 한 바와 같이, 당신은 결정적으로 동등한 유형에 대해 이러한 종류의 목표를 증명할 수 있습니다. 이를 위해 decide equality 전술에 대한 도움을 얻을 수 있습니다. 참조 : http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic121
이 답변에 대해 좀 더 자세히 설명하기 위해 일부 유형 T (여기서 T는'Set')에 대해이 결과를 증명하는 두 가지 주요 방법이 있습니다. T가 평등을 결정할 수있는 알려진 절차를 가지고 있다면 절차가 결정할 수 있다는 증거를 사용하십시오. 그렇지 않으면 고전 논리에 의지해야합니다. Coq의 기본 논리는 직관 주의적이다. –
귀하의 질문은 명제 (예 : Prop의 회원)와 부울 (즉, bool의 회원) 간의 차이점에 대해 언급합니다. 이 차이점을 자세히 설명하는 것은 다소 전문적 일 수 있으므로 특정 예제에만 집중하려고 노력할 것입니다.
대략적으로 Coq의 Prop은 보통 부울처럼 True 또는 False으로 평가되는 것이 아닙니다. 대신 Prop에는 사실을 추론하기 위해 조합 할 수있는 추론 규칙이 있습니다. 그것들을 사용하여 우리는 명제가 유지되고 있다는 것을 보여줄 수 있습니다. 사물을 미묘하게 만드는 것은 세 번째 가능성, 즉 우리가 명제를 증명하거나 논박 할 수 없다는 것입니다. 이것은 Coq가 건설 논리이기 때문에 발생합니다. 이것의 가장 잘 알려진 결과 중 하나는 으로 알려진 익숙한 추론 원칙이 (forall P : Prop, P \/ ~ P)임을 Coq에서 증명할 수 없다는 것입니다. 즉, P \/ ~ P이라고 주장하면 이는 P을 증명할 수 있음을 의미합니다. 또는 ~ P을 증명할 수 있습니다. 어느 것을 보유하고 있는지 알지 못하면이를 주장 할 수 없습니다.
어떤 명제에서는 P \/ ~ P이 성립한다는 것을 알 수 있습니다. 예를 들어, forall n m : nat, n = m \/ n <> m을 표시하는 것은 어렵지 않습니다. 위의 발언에 이어, 이는 자연수의 모든 쌍에 대해, 우리는 그들이 동일하다는 증거 또는 그렇지 않은 증명을 산출 할 수 있음을 의미합니다.
반면에 nat을 Set으로 변경하면 예제 에서처럼 우리는 결코 이론을 증명할 수 없습니다. 이유를 확인하려면 Setnat * nat 쌍의 자연수를 고려하십시오. 우리가 당신의 정리를 증명할 수 있다면, 그것은 nat = nat * nat \/ nat <> nat * nat을 따를 것입니다. 다시 말하면 위의 발언에 따르면 이는 즉 nat = nat * nat 또는 nat <> nat * nat을 증명할 수 있음을 의미합니다. 그러나 두 유형간에 bijection이 있기 때문에 nat = nat * nat이라고 가정하는 것은 모순이라고 말할 수는 없지만 형식이 구문 적으로 동일하지 않기 때문에 서로 다르다고 가정하는 것이 좋습니다.기술적으로 말하면, 명제 nat = nat * nat의 유효성은 이고 Coq의 논리는입니다.
당신은 정말 당신이, 당신은 당신이 어느 한쪽의 명시적인 증거없이 \/의 증거를 생성 할 수 있습니다 공리 (Axiom classical : forall P, P \/ ~ P.)로 제외 된 중간 주장에 의해 추론 할 필요가 언급 한 사실을해야하는 경우 사례. 그런 다음 예제 정리를 증명할 수 있습니다.
intros a b. destruct (classical (a = b)).
left. assumption.
right. assumption. 희망이 있습니다.
어떤 Coq 버전을 사용하고 있습니까? 항고술'A \/~ A '에 근거한 증거를 요구하고 있습니까, 아니면 특정한 분쟁'a = b \/a <> b'를 가정 한 예를 생각해 보시겠습니까? – hardmath