Coq: Как переписать внутри лямбды? - PullRequest
Новая
       23

Coq: Как переписать внутри лямбды?

0 голосов
/ 12 апреля 2019

По сути, я хочу доказать следующую лемму, но у меня возникли проблемы, так как я не могу переписать напрямую в лямбдах.

Однако я чувствую, что это должно быть возможно, потому что, если бы я был «внутри» лямбды, я мог бы легко доказать это для любого данного x. 

Lemma lemma :
  forall {A B : Type} (f : A -> B) (g : A -> B), 
    (forall (x : A), f x = g x) -> (fun x => f x) = (fun x => g x).

1 Ответ

3 голосов
/ 12 апреля 2019

Утверждение, которое вы пытаетесь доказать, - это (по сути) функциональная расширяемость, которая, как известно, не известна как , которую невозможно доказать в Coq без дополнительных аксиом.По сути, идея заключается в том, что f и g могут преднамеренно сильно отличаться (их определения могут выглядеть по-разному), но при этом принимать одинаковые значения.Равенство функций (fun x => f x) = (fun x => g x) будет (без каких-либо дополнительных аксиом) означать, что две функции синтаксически одинаковы.

Например, взять f(n) = 0 и g(n) = 1 if x^(3 + n) + y^(3 + n) = z^(3 + n) has a non-trivial solution in integers, otherwise 0 (обе функции от натуральных чисел до натуральных чисел),Тогда f и g намеренно различаются - одно синтаксически не сводится к другому.Однако, благодаря Эндрю Уайлсу, мы знаем, что f и g в значительной степени одинаковы, так как g(n) = 0 для всех n.

Вы можете свободно добавлять свою лемму (или различные усиления) в видеАксиома к Coq, не беспокоясь о несостоятельности.

...