В coq, как вы объявляете/подтверждаете элементы перечисления, различны?

Question

Мне весело, представившись Coq. Прямо сейчас я застрял делать доказательств о перечислении:

Inductive Comparison : Type := 
    | EQUAL 
    | GREATER 
    | LESSER. 

ли это неявно верно, что EQUAL и GREATER и LESSER отличаются (это, кажется, что эти документы означают), или в том, что не определено только с выше код? Я не могу понять, как это доказать.

Proposition comp_sanity: forall x : Comparison, 
    x = EQUAL /\ x = GREATER -> False. 
Proof. 
intros x H_eqgr. 

дает мне:

H_eqgr : x = EQUAL /\ x = GREATER 
-------------------------------------------------- 
False 

но я застрял:

Coq> contradiction H_eqgr. 
Error: Not a contradiction. 

Что я должен делать здесь, чтобы иметь полностью (отчетливо) перечисленное типа?

Answer 1

В вашем случае я бы пошел на тактику discriminate вместо contradiction. Короткая версия будет:

Proposition comp_sanity: forall x : Comparison, 
    x = EQUAL /\ x = GREATER -> False. 
Proof. 
now intros x [h1 h2]; subst; discriminate. 
Qed. 

которые переводят на

Proposition comp_sanity: forall x : Comparison, 
    x = EQUAL /\ x = GREATER -> False. 
Proof. 
intros x hx. 
destruct hx as [h1 h2]. 
rewrite h1 in h2. 
now discriminate h2. 
Qed. 

без магии intros картины.

Бест, В.

Answer 2

Тактика contradiction не работает намного лучше, чем пытаться найти что-то в своем контексте, которое имеет тип False. К сожалению, хотя ваш контекст имеет противоречие, до contradiction еще не ясно.

Тактика congruence выполняет больше работы и понимает, что, действительно, два разных конструктора не равны (мы говорим, что конструкторы не пересекаются).

В этом контексте, это более или менее такие же, как вызов subst для распространения равенств о x, что приводит к одной из гипотез EQUAL = GREATER, а затем вызвать discriminate, тактику, которая находит абсурдность в равенстве различных конструкторов.