Доказательство по случаям с использованием Coq

Question

У меня есть простая теорема, которую я хочу доказать с помощью доказательств по случаям. Ниже приведен пример.

 
Goal forall a b : Set, a = b \/ a <> b. 
Proof 
    intros a b. 
    ... 

Как бы я решил это решить. И точно, как бы я определил доказательство делами, используя два возможных значения равенства (True или False)?

Любая помощь будет оценена по достоинству. Спасибо,

Answer 1

Я уверен, что равенство Set s не разрешимо в 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

Answer 2

Ваш вопрос затрагивает интересный аспект Coq: разница между высказываниями (т.е. члены Prop) и булевы (т.е. члены bool). Объяснение этого различия в деталях было бы слишком техническим, поэтому я просто попытаюсь сосредоточиться на вашем конкретном примере.

Грубо говоря, Prop в Coq - это не то, что оценивает либо True, либо False, как обычный булев. Вместо этого Prop s имеют правила вывода, которые могут быть объединены, чтобы вывести факты. Используя их, мы можем показать, что предложение имеет место, или показать, что оно противоречиво. То, что делает вещи утонченными, заключается в том, что существует третья возможность, а именно то, что мы не можем ни доказать, ни опровергнуть предложение. Это происходит потому, что 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. Однако, поскольку между обоими типами существует биекция, мы не можем сказать, что противоречить предположить, что nat = nat * nat, но поскольку типы не являются синтаксически равными, также можно предположить, что они разные.Технически говоря, справедливость предложения nat = nat * nat независимая логики Coq.

Если вам действительно нужно то, что вы упомянули, то вам нужно утверждать без середины, как аксиому (Axiom classical : forall P, P \/ ~ P.), что позволит вам производить доказательства \/ без явного доказательства с обеих сторон и рассуждать по случаев. Тогда вы сможете доказать свою примерную теорему чем-то вроде

intros a b. destruct (classical (a = b)). 
    left. assumption. 
    right. assumption.

Надеюсь, это поможет.