Лемма о списке и рев (список) - PullRequest
Новая
       5

Лемма о списке и рев (список)

0 голосов
/ 03 июля 2019

Пытаясь доказать следующую лемму, я застрял. Обычно теоремы о списках доказываются с помощью индукции, но я не знаю, куда двигаться дальше. 

Lemma reverse_append : forall (T : Type) (h : T) (t : list T), h::t = rev(t) ++ [h] -> t = rev(t).
Proof.
  intros. induction t.
  - simpl. reflexivity.
  - simpl. simpl in H.

Result:

1 subgoal (ID 522)

T : Type
h, x : T
t : list T
H : h :: x :: t = (rev t ++ [x]) ++ [h]
IHt : h :: t = rev t ++ [h] -> t = rev t
============================
x :: t = rev t ++ [x]

Ответы [ 2 ]

2 голосов
/ 03 июля 2019

Основной ответ

Прежде чем начать доказательство своей теоремы, вы должны попытаться тщательно понять, что говорит ваша теорема. Ваша теорема просто неверна.

Контрпример: 2 :: [1;2] = rev [1;2] ++ [2], но [1;2] не является палиндромом.

Полное доказательство: 

Require Import List.
Import ListNotations.

Lemma reverse_append_false :
  ~(forall (T : Type) (h : T) (t : list T), h::t = rev(t) ++ [h] -> t = rev(t)).
Proof. intros H. specialize (H nat 2 [1;2] eq_refl). inversion H. Qed.

Незначительные проблемы

rev(t) должно быть просто rev t. Просто эстетический момент, но, вероятно, вам стоит познакомиться с написанием в стиле функционального программирования.

Обычно теоремы о списках доказываются с помощью индукции

Это довольно наивное утверждение, хотя и технически правильное. Есть так много способов индукции по значению, и выбор индукции, которая работает лучше всего, является критически важным навыком. Чтобы назвать несколько:

  • Индукция в списке
  • Индукция по длине списка
    • возникает довольно часто при работе с rev и другими функциями, сохраняющими длину
  • Если простая индукция не работает, рассмотрите собственную схему индукции
1 голос
/ 03 июля 2019

Лемма не соответствует действительности, как указано. Прежде чем что-то доказывать, вы должны убедиться, что это имеет смысл. Гипотеза по существу говорит, что h::t = rev (h::t). Но почему это означает, что t = rev t? Если вы удалите элемент из начала палиндромного списка, он, вероятно, не будет больше палиндромом. Например, deified - это палиндром («deified» = rev «deified»), но eified не является палиндромом.

Для примера в этой конкретной ситуации, 1::[2; 1] = (rev [2; 1]) ++ [1], так как оба [1; 2; 1]. Но [2; 1] не равно rev [2; 1] = [1; 2].

...