Как доказать, что при равенстве, что строка обратная, ее хвост также обратный? - PullRequest
Новая
       12

Как доказать, что при равенстве, что строка обратная, ее хвост также обратный?

0 голосов
/ 10 мая 2019 
Theorem rev_cons :
  forall X x (l : list X),
  x :: l = rev (x :: l) -> l = rev l.

Это настолько интуитивно для меня, что поражает воображение, что я ничего не могу поделать.Я начинаю с индукции на l, решаю базовый случай, используя рефлексивность, и сразу зацикливаюсь на другом.

Что именно мне здесь не хватает?

1 Ответ

2 голосов
/ 10 мая 2019

Я не думаю, что это правда. Показательный пример: 

Require Import List.

Axiom rev_cons :
  forall X x (l : list X),
  x :: l = rev (x :: l) -> l = rev l.

Theorem argh : False.
assert (H := rev_cons _ 1 (2 :: 1 :: nil) eq_refl).
inversion H.
Qed.
...