Невозможно найти экземпляр для переменной - PullRequest
Новая
       4

Невозможно найти экземпляр для переменной

10 голосов
/ 16 января 2012

Контекст: я работаю над упражнениями в Основы программного обеспечения . 

Theorem neg_move : forall x y : bool,
  x = negb y -> negb x = y.
Proof. Admitted.

Theorem evenb_n__oddb_Sn : forall n : nat,
  evenb n = negb (evenb (S n)).
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    simpl. reflexivity.
  Case "n = S n'".
    rewrite -> neg_move.

Перед последней строкой моя подцель выглядит так: 

evenb (S n') = negb (evenb (S (S n')))

И я хочу преобразовать это в это: 

negb (evenb (S n')) = evenb (S (S n'))

Однако, когда я пытаюсь пройти через rewrite -> neg_move, выдается эта ошибка:

Ошибка: невозможно найти экземпляр для переменной y.

Я уверен, что это действительно просто, но что я делаю не так? (Пожалуйста, не отдавайте ничего для решения evenb_n__oddb_Sn, если я не делаю это совершенно неправильно).

1 Ответ

10 голосов
/ 16 января 2012

Как упоминал данпортин, Coq говорит вам, что не знает, как создать экземпляр y. Действительно, когда вы делаете rewrite -> neg_move, вы просите его заменить negb x на y. Теперь, что y должен использовать Coq здесь? Он не может понять это.

Один из вариантов - создать экземпляр y явно при переписывании:

rewrite -> neg_move with (y:=some_term)

Это выполнит переписывание и попросит вас подтвердить помещение, здесь добавится подцель вида x = negb some_term.

Другим вариантом является специализация neg_move при переписывании:

rewrite -> (neg_move _ _ H)

Здесь H должен быть термином типа some_x = negb some_y. Я поставил две подстановочные знаки для параметров x и y для neg_move, поскольку Coq может выводить их из H как some_x и some_y соответственно. Затем Coq попытается переписать в вашей цели вхождение negb some_x с помощью some_y. Но сначала вам нужно включить в свои гипотезы этот термин H, что может быть дополнительным бременем ...

(обратите внимание, что первый вариант, который я вам дал, должен быть эквивалентен rewrite -> (neg_move _ some_term))

Другой вариант - erewrite -> negb_move, который добавит необработанные переменные, которые будут выглядеть как ?x и ?y, и попытается выполнить перезапись. Затем вам нужно будет доказать предпосылку, которая будет выглядеть как (evenb (S (S n'))) = negb ?y, и, надеюсь, в процессе решения этой подцели, Coq выяснит, что ?y должно было быть с самого начала (хотя есть некоторые ограничения, а некоторые проблемы могут возникнуть, если Coq решает цель, не выясняя, что ?y должно быть).

Однако для вашей конкретной проблемы это гораздо проще: 

==========
evenb (S n') = negb (evenb (S (S n')))

symmetry.

==========
negb (evenb (S (S n'))) = evenb (S n')

apply neg_move.

==========
evenb (S (S n')) = negb (evenb (S n'))

И это то, что вы хотели (в обратном порядке, сделайте еще symmetry., если вам все равно).

...