Существует тактика под названием fix.Я попытаюсь объяснить, что происходит на высоком уровне, потому что я думаю, что это крутой взлом, но учтите, что fix - это палка о двух концах, которую обычно не рекомендуется использовать: она зависит от действительно низкоуровневых деталейCoq, которые делают доказательства довольно хрупкими, и когда они ломаются, сообщения об ошибках трудно понять.
fix foo i, где foo - свежая переменная, а i - целое число,тактика, которая применяется к цели с не менее i аргументами (например, forall n, evenb n = true -> ... имеет два: n и доказательство evenb n = true), а предполагает цель, которую вы пытаетесь доказать , назвав эту новую гипотезу foo.(Да, вы правильно прочитали.)
Theorem evenb_double_k : forall n,
evenb n = true -> exists k, n = double k.
Proof.
fix self 1.
(*
1 subgoal (ID 17)
self : forall n : nat,
evenb n = true -> exists k : nat, n = double k
============================
forall n : nat, evenb n = true -> exists k : nat, n = double k
*)
Конечно, есть загвоздка: в том, что гипотеза должна быть применена к правильному подтерию n (который является первый аргумент цели, вот что означает числовой параметр fix self 1, мы говорим, что первый аргумент - это убывающий аргумент ).Что такое правильная подтерма n?Это значение, которое вы можете получить только путем уничтожения n, хотя бы один раз.
Обратите внимание, что Coq не будет сразу жаловаться, если вы все же решите применить гипотезу self напрямую (nне правильная субтерма сама по себе).Coq проверяет только требование "subterm" на Qed. РЕДАКТИРОВАТЬ : Вы также можете использовать команду Guarded в любое время, чтобы проверить это.
apply self. (* seems fine, all goals done. *)
Qed. (* ERROR! *)
Вы можете приблизительно представить fix как форму сильной индукции, где индукцияГипотеза (self) дана для всех членов, меньших текущего, а не только для непосредственных предшественников.Однако это «подтериальное» отношение на самом деле не фигурирует в утверждении self.(Эта особенность делает fix опасной тактикой низкого уровня.)
После fix вы обычно хотите destruct уменьшающий аргумент.Именно здесь fix позволяет вашему доказательству следовать структуре evenb.Ниже мы немедленно уничтожаем снова в случае S.Таким образом, мы получаем три случая: n = O, n = S O, n = S (S n') для некоторых n' : nat.
Первый случай прост, второй пустует, а третий - где вам нужно«гипотеза об индукции» self при n'.
Proof.
fix self 1.
intros n.
destruct n as [| [| n']].
- exists 0; reflexivity.
- discriminate.
- simpl. intro H.
apply self in H.
destruct H as [k Hk].
exists (S k).
rewrite Hk; reflexivity.
Qed.
Некоторые рассуждения здесь довольно общие, и их можно вывести в пользовательский принцип индукции даже на nat с, что конкретно является Theorem.
Theorem even_ind :
forall (P : nat -> Prop),
P O ->
(forall n, evenb n = true -> P n -> P (S (S n))) ->
forall n, evenb n = true -> P n.
Сравните его со стандартным принципом индукции для nat, который на самом деле также является теоремой, названной nat_ind.Это то, что используется в тактике induction под капотом.
About nat_ind.
(* nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n
*)
Шаг индукции в nat_ind изменяется от n до S n, тогда как шаг индукции для even_ind идет от n до S (S n), и имеет дополнительную гипотезу о том, что наши числа четные.
Доказательство even_ind следует структуре, аналогичной evenb_double_k, хотя оно более абстрактно, поскольку оно обобщает по всемпредикаты P для nat.
Proof.
intros P HO HSS.
fix self 1.
intros n.
destruct n as [| [| n']].
- intro; apply HO.
- discriminate.
- intros H. apply HSS.
+ apply H.
+ apply self.
apply H.
Qed.
Другой подход здесь заключается в том, чтобы вообще не использовать fix (поскольку этого следует избегать), но оставить induction в качестве примитива, чтобы доказать альтернативуeven_ind принцип.Это нормально для nat, но для некоторых сложных индуктивных типов принцип индукции по умолчанию слишком слаб, и рукописный fix является единственным способом.
Наконец, возвращаясь к evenb_double_k, мы можемиспользуйте новый принцип индукции с apply even_ind, вместо fix или induction.Теперь мы получаем только два значимых случая, O и S (S n'), где n' четное.
Theorem evenb_double_k' : forall n,
evenb n = true -> exists k, n = double k.
Proof.
apply even_ind.
- exists 0. reflexivity.
- intros n H [k Hk].
exists (S k).
rewrite Hk.
reflexivity.
Qed.
Определения, использованные в этом ответе:
Fixpoint evenb n :=
match n with
| S (S n') => evenb n'
| S O => false
| O => true
end.
Fixpoint double k :=
match k with
| O => O
| S k' => S (S (double k'))
end.