4
Как можно доказать следующее ?:Как доказать равные функции, зная, что их тела равны?
Lemma forfun: forall (A B : nat->nat), (forall x:nat, A x = B x) ->
(fun x => A x) = (fun x => B x).
Proof.
A
ответ
3
Принцип вы хотите известен как функциональной объемности; в самом общем виде, это говорит
Axiom fun_ext : forall (A B : Type) (f g : A -> B),
(forall x : A, f x = g x) -> f = g.
К сожалению, несмотря на то полезным, этот принцип является независимой базовой логики Coq, что означает, что это не возможно, чтобы доказать или опровергнуть. Однако логика Кока была спроектирована так, что было бы безопасно считать этот принцип аксиомой теории, а Coq's standard library уже определил этот принцип, чтобы вы могли его использовать.
@HoboSapiens Это законный вопрос о программировании в помощнике Coq proof, ср. другие связанные вопросы о теге Coq. –
@HoboSapiens: coq - это автоматизированный теоретический прорыв, который также является языком программирования. (Наведите указатель на тег 'coq': 186 последователей и 410 вопросов здесь на SO.) Этот вопрос касается того, как использовать язык coq, а не как доказать общий математический факт. Тем не менее, я не думаю, что это было бы неуместно на Math.SE. –