Одна вещь, которую Coq использует повсеместно, - это понятие «предложения как типы».Интуитивно, типы являются коллекциями объектов.Так каковы элементы этих коллекций?Это доказательства.Утверждаемое суждение - это тип, который содержит элемент, а не доказуемое суждение - это тип, который не содержит доказательства.
Итак, a = b - это тип, тип доказательств и b = a это также тип доказательств, но они не доказывают одно и то же утверждение.Цель логики в Coq - быть очень точным в утверждениях.Можно ли сказать, что a = b и b = a одинаковы?Ну, в некотором смысле это не так.Если у меня есть цель вида C(a, b), и я переписываю с доказательством a = b, тогда я получаю C(a, a), и если я переписываю с доказательством b = a, тогда я получаю C(b, b), и эти два невыглядит также.Одни утверждают, что они одинаковы (потому что a и b одинаковы по предположению), но можно также утверждать, что они не одинаковы (потому что вы не используете их одинаково).
При разработке логической системы, такой как Coq, оказывается, что вы можете делать много логики, даже если вы не пытаетесь говорить о равенстве между предложениями, а концентрируетесь только на использовании эквивалентности между предложениями.Поэтому люди пытались добавить наименьшее количество свойств к понятию равенство .В частности, равенство между типами было оставлено голым.Вы увидите, что равенство практично использовать, когда речь идет о равенстве между данными первого порядка, оно менее удобно, когда речь идет о данных более высокого порядка (например, равенство между функциями), и неудобно, когда речь идет о равенстве между типами.
С другой стороны, если они хотят изучить связь между двумя суждениями, они только пытаются проверить, подразумевает ли одно суждение другое, и если они хотят быть более точными, они пытаются увидеть, подразумевают ли они друг другавзаимно.Для большинства практических целей этого будет достаточно, и я предлагаю вам придерживаться этой дисциплины, если вы считаете себя новичком.
Здесь мы можем захотеть доказать a = b -> b = a.Если мы сделаем это в качестве доказательства, используя тактику, то intro поможет нам дать имя a = b (скажем, H), а rewrite H поможет нам преобразовать b = a в a = a.Теперь последнее доказательство можно сделать с помощью рефлексивности.Но когда я говорю, преобразуйте b = a в a = a.Я имею в виду только то, что a = a -> b = a имеет доказательство, другими словами «есть функция, когда на входе дается доказательство a = a, она выдает на выходе доказательство b = a. При выполнении доказательства мы имеемСоздается впечатление, что доказательство a = a превращается в доказательство b = a, оставаясь неизменным, но это не так: здесь наблюдаются два разных доказательства.
В конце концов, (a = b) <-> (b = a) - это простосоединение (a = b) -> (b = a) и (b = a) -> (a = b). Тактика rewrite также была расширена, так что вы также можете переписать с помощью теоремы эквивалентность, а не равенство.