#coq #proof
Вопрос:
Если у меня есть теорема вида:
Theorem my_thm (n: nat -gt; nat): exists t: nat, n t = 0. Admitted. Если я хочу доказать это для функции , которая такова my_func 0 = 0 , как я могу сказать coq, что действительно существует такое t, потому что my_func 0 = 0 ?
У этого нет глубокой цели, но вы понимаете, как работает экзистенциальное доказательство в coq.
Комментарии:
1. Ваша теорема касается всех функций типа nat-gt;nat. Существует множество таких функций, которые никогда не имеют значения 0.
2. Что делать, если я хочу использовать эту теорему для определенной функции ?
3. Вы принимаете
Theorems заDefinitions. То, что вы сделали, — это утверждение истинности логического предложения∀ (n : nat → nat), ∃ (t : nat), n t = 0. Что вы действительно хотите сделать , так это определить логический предикат над значениямиn : nat → nat, т. Е. Функцию, которая сопоставляет свой аргументn : nat → natс предложением (независимо от того, доказано это или нет).Definition my_pred (n : nat → nat) := ∃ (t : nat), n t = 0.Тогдаmy_predэто функция типа(nat → nat) → Propиmy_pred my_funявляется предложением. Вы можете объявить и доказать теорему, подтверждающую истинность этой опоры.
Ответ №1:
Вы можете добавить здесь аргумент P , который утверждал бы , что это свойство выполняется, и использовать его позже в своей теореме, используя эту exists тактику. Например (я использую ssreflect, но, думаю, вы поймете идею):
Theorem my_thm (n: nat -gt; nat) (P : n 0 = 0) : exists u, n u = 0. Proof. exists 0. exact: P. Qed. Конечно, вы также можете изменить тело теоремы, чтобы оно лучше соответствовало вашим потребностям.