(A <-> B) → A = B?

이 집합을 정의한다고 가정합니다.(A <-> B) → A = B?

Inductive Set_1 : Set := 
    | Constr_1 : Set_1 
    | Constr_2 : Set_1.

이 문장을 증명할 수 있습니까?

(Constr_1 = Constr_2) = False

그렇다면, 내가 어떤 전술을 사용합니까? 이것은 autorewrite에 유용 할 수 있습니다.

2013-01-14 Anonymous

가능한 복제본 [어떻게 증명할 수 있습니까?] (http://stackoverflow.com/questions/11071165/how-can-this-be-proved-in-coq) –

(A <-> B) -> A = B은 명제 연장 성으로 불리며, classical logic에 의해 암시됩니다.

autorewrite과 동등한 번호를 사용하기 위해 필요하지는 않지만 단지 Require Import Coq.Setoids.Setoid입니다.

2013-01-17 13:44:48

답변