Coq: работа с неравенствами (<>)

Question

Я пытаюсь понять логику работы с неравенствами в Coq.

• Когда в цели присутствует <>, выполнение intros contra. меняет цель на False и перемещает цель к гипотезе, но с <> переключенным на =.Я думаю, я понимаю, как это звучит.Если в качестве цели я поставлю цель a <> b, то гипотеза a = b вызовет противоречие.

  Однако я не могу сделать обратное в Coq.Если у меня есть цель a = b, я не могу intros contra., чтобы иметь False в качестве цели и a <> b в качестве гипотезы. Будет ли это intros логически обоснованным?Разве это не поддерживается только потому, что никогда не требуется заполнять доказательство?

• Когда <> находится в гипотезе H, выполнение destruct H. удалит гипотезу(Я не могу сделать destruct (H) eqn:H.), и это переключит любую цель на ту же, что и H, но с <>, переключенным на =. Я не понимаю логику здесь .Если у меня есть гипотеза, которая является неравенством, я не вижу, как отсутствие ее равнозначно равенству как цели.

  Как неравенство индуктивно для использования destruct?

  Если у меня есть противоречивая гипотеза G 0 <> 0, чтобы завершить доказательство и сказать, что это противоречие, мне нужно сделать destruct G. (* now the goal is 0 = 0 *). reflexivity. Почему невозможнопросто сделайте что-то вроде inversion G., как вы сделали бы с гипотезой S n = 0?.

Итак, на самом деле у меня есть 4 связанных вопроса, помеченных вполужирный .

Answer 1

Будет ли это intros [по цели a = b] логически обоснованным?

Если я понимаю ваш вопрос, вы хотите знать, возможно ли иметьцель a = b, позвоните intros contra и превратите ее в цель H : a <> b |- False.Это было бы правильно, но не выводимо в базовой конструктивной логике Кока для произвольных типов a и b: оно утверждает, что предложение a = b поддерживает исключение двойного отрицания (~ (~ a = b) -> a = b).Coq не поддерживает это, потому что это будет означать работу в другом логическом формализме.

Как неравенство индуктивно для использования destruct?

Как отмечали yeputonsa <> b определяется как a = b -> False, а ложность индуктивно определяется как предложение без конструкторов;таким образом, уничтожение чего-то типа False просто завершает доказательство.Кроме того, вызов destruct для чего-то типа A -> B примерно приводит к генерации цели типа A, вводит это доказательство в подтекст для получения доказательства B, а затем вызывает destruct для этогодоказательство B.В вашем случае это означает делать в точности то, что вы описали.

Почему невозможно просто сделать что-то вроде inversion G., как вы сделали бы с гипотезой S n = 0?

Я предполагаю, что inversion не так снисходителен, как destruct, и не распространяется на последствия, как я объяснил выше.