Как мне доказать следующую лемму в Coq? - PullRequest
Новая
       13

Как мне доказать следующую лемму в Coq?

2 голосов
/ 04 апреля 2019 
Lemma rev_firstn : forall (x : list bool) (n : nat),
rev (firstn n x) = firstn n (rev x).

Я потратил немало времени на это.Я начинаю с разумной цели, но всегда заканчиваю целью, которую невозможно доказать.

Вот мой нынешний подход: 

Proof.
  intros. generalize dependent x. induction n. 
  + easy. 
  + induction x.
    - easy. 
    -

В моем контексте у меня теперь есть: 

IHn : forall x : list bool, rev (firstn n x) = firstn n (rev x)
IHx : rev (firstn (S n) x) = firstn (S n) (rev x)

и моя цель: 

rev (firstn (S n) (a :: x)) = firstn (S n) (rev (a :: x))

Есть ли способ обобщить x в IHx, чтобы я мог специализировать его на (a :: x)?Поскольку я не знаю правильной тактики для этого, я пробую следующее и в конечном итоге получаю ранее упомянутую невозможную цель. 

Proof.
  intros. generalize dependent x. induction n. 
  + easy. 
  + induction x.
    - easy. 
    - assert (rev_cons : forall (b : bool) (l : list bool), 
              rev (b :: l) = rev l ++ [b]).
      { easy. } rewrite firstn_cons. 
      rewrite rev_cons. rewrite rev_cons. specialize (@IHn x).
      rewrite IHn.
Goal: firstn n (rev x) ++ [a] = firstn (S n) (rev x ++ [a])

Эта цель невозможна, потому что для n = 0 и rev x =h :: t, цель уменьшается до [a] = List.hd (rev (h :: t)) ++ [a].

Эта лемма на самом деле несостоятельна или я просто упускаю какую-то тактику?

1 Ответ

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

Предполагая, что firstn и rev - это то, что я думаю, лемма не верна.

rev (firstn 2 [true, false, false])
= rev [true, false]
= [false, true]

, но 

firstn 2 (rev [true, false, false])
= firstn 2 [false, false, true]
= [false, false]

По существу, rev (firstn n x) - это первые n элементы x (в обратном порядке), но firstn n (rev x) - это последние n элементы x (также в обратном порядке).Чтобы эта лемма была верной в любой общности, вам нужно, чтобы x имел не более n элементов.Как отмечает Артур Азеведо Де Аморим в комментариях, вы также можете получить правильную версию этой леммы, если вставите skipn n, чтобы просто посмотреть на последние n (максимум) элементов x.

rev (firstn n (skipn (length x - n)) x) = firstn n (rev x)

...