Уничтожение по результату применения функции предиката - PullRequest
Новая
       11

Уничтожение по результату применения функции предиката

5 голосов
/ 27 декабря 2011

Я новичок в Coq и быстро задаю вопрос о тактике уничтожения. Предположим, у меня есть функция count, которая подсчитывает количество вхождений данного натурального числа в список натуральных чисел: 

Fixpoint count (v : nat) (xs : natlist) : nat :=
  match xs with
    | nil => 0
    | h :: t =>
      match beq_nat h v with
        | true => 1 + count v xs
        | false => count v xs
      end
  end.

Я бы хотел доказать следующую теорему: 

Theorem count_cons : forall (n y : nat) (xs : natlist),
  count n (y :: xs) = count n xs + count n [y].

Если бы я доказывал аналогичную теорему для n = 0, я мог бы просто разложить y до 0 или S y '. В общем случае я хотел бы уничтожить (beq_nat n y) значение true или false, но я не могу заставить это работать - мне не хватает некоторого фрагмента синтаксиса Coq.

Есть идеи?

1 Ответ

5 голосов
/ 27 декабря 2011

Ваш код не работает 

Fixpoint count (v : nat) (xs : natlist) : nat :=
 match xs with
  | nil => 0
  | h :: t =>
  match beq_nat h v with
    | true => 1 + count v xs (*will not compile since "count v xs" is not simply recursive*)
    | false => count v xs
  end
end.

вы, вероятно, имели в виду 

Fixpoint count (v : nat) (xs : natlist) : nat :=
 match xs with
  | nil => 0
  | h :: t =>
  match beq_nat h v with
    | true => 1 + count v t
    | false => count v t
  end
end.

Использование destruct - это отличный способ получить ваше решение. Но вам нужно помнить несколько вещей

  • destruct является синтаксическим, то есть заменяет термины, выраженные в вашей цели / предположениях. Итак, обычно вам нужно что-то вроде simpl (работает здесь) или unfold сначала.
  • порядок терминов имеет значение. destruct (beq_nat n y) - это не то же самое, что destruct (beq_nat y n). В этом случае вы хотите второй из этих

Обычно проблема в том, что destruct тупой, поэтому вы должны делать смарты самостоятельно.

В любом случае, начните доказательство 

intros n y xs. simpl. destruct (beq_nat y n).

И все будет хорошо.

...