РЕДАКТИРОВАТЬ: После дальнейшего обсуждения в комментариях, фактическая путаница была такая:
Не match a with... = match b with дает мне False сразу же, как S S Z = S Z ?
Вы можете сопоставить с шаблоном nat, а с функциями - нет. Зависимое сопоставление с образцом - это то, как мы можем доказать инъективность и дизъюнктность конструкторов, тогда как единственное, что мы можем сделать с функцией, это применить ее. (См. Также Откуда мы знаем, что все конструкторы Coq инъективны и не пересекаются? )
Тем не менее, я надеюсь, что остальная часть ответа ниже по-прежнему поучительна.
Из комментариев:
AFAIU, = имеет очень точное значение в Coq / CI C - syntacti c равенство нормальных форм.
Это не так правильно. Например, мы можем доказать следующее:
Lemma and_comm : forall a b : bool, (* a && b = b && a *)
match a with
| true => b
| false => false
end = match b with
| true => a
| false => false
end.
Proof.
destruct a, b; reflexivity.
Qed.
Мы можем использовать eq_refl только тогда, когда две стороны синтаксически равны, но есть больше правил рассуждения, которые мы можем применять помимо конструкторов индуктивных суждений, большинство особенно зависимое сопоставление с образцом и, если мы допускаем это, функциональная расширенность.
Но f и g, очевидно, не равны как структуры данных.
Это утверждение кажется путать доказуемость и правду. Важно различать guish эти два мира. (И я не логик, так что возьмите то, что я собираюсь сказать, с долей соли.)
Coq - игра с символами, с четко определенными правилами для построения терминов определенных типов. , Это доказуемость. Когда Coq принимает доказательство, все, что мы знаем, это то, что мы создали термин, следуя правилам.
Конечно, мы также хотим, чтобы эти термины и типы что-то значили. Когда мы докажем предложение, мы ожидаем, что это скажет нам что-то о состоянии мира. Это правда. И в некотором смысле, Coq очень мало говорит по этому вопросу. Когда мы читаем f = g, мы даем значение символу f, значение g, а также значение =. Это полностью зависит от нас (ну, всегда есть правила, которым нужно следовать), и существует более одной интерпретации (или «модели»).
«Наивная модель», которую большинство людей имеет в виду, рассматривает функции как отношения (также называемые графиками) между входами и выходами. В этой модели функциональность расширяется: функция - это не более, чем отображение между входами и выходами, поэтому две функции с одинаковыми отображениями равны. Функциональность расширяется в Coq (мы не можем доказать False), потому что есть хотя бы одна модель, в которой она действительна.
В вашей модели функция характеризуется своим кодом, по модулю уравнения. (Это более или менее «модель syntacti c», где мы интерпретируем каждое выражение как само по себе, с минимально возможным количеством поведения semanti c.) Тогда действительно есть функции, которые экстенсивно равны, но с разными код. Таким образом, функциональная экстенсиональность недопустима в этой модели, но это не означает, что она неверна (то есть, что мы можем доказать ее отрицание) в Coq, как это оправдывалось ранее.
f и g не являются «очевидно, не равен», потому что равенство, как и все остальное, относится к конкретной интерпретации.