Лемма о списке и rev(list)
Пытаясь доказать следующую лемму, я застрял. Обычно теоремы о списках доказываются по индукции, но я не знаю, куда двигаться дальше.
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
Лемма неверна, как сказано. Прежде чем что-то доказывать, нужно убедиться, что это имеет смысл. Гипотеза, по сути, говорит, что h::t = rev (h::t). Но почему это должно означать, что t = rev t? Если вы удалите элемент из начала палиндромного списка, вероятно, не будет больше не будет палиндромом. Например, «обожествленный» — это палиндром («обожествленный» = rev «обожествленный»), но «обожествленное» не является палиндромом.
Например, в этой конкретной ситуации 1::[2; 1] = (rev [2; 1]) ++ [1], поскольку оба являются [1; 2; 1]. Но [2; 1] не равно rev [2; 1] = [1; 2].
Основной ответ
Прежде чем вы начнете доказывать свою теорему, вы должны попытаться тщательно понять, что говорит ваша теорема. Ваша теорема просто неверна.
Контрпример: 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. Просто эстетический момент, но, вероятно, вам следует лучше познакомиться с написанием в стиле функционального программирования.
Usually theorems about lists are proven using induction
Это довольно наивное утверждение, хотя технически правильное. Существует так много способов провести индукцию по значению, и выбор наведения, который работает лучше всего, является важным навыком. Назвать несколько:
- Введение в список
- Индукция по длина списка
- возникает довольно часто при работе с
revи другими функциями, сохраняющими длину - Пример
- возникает довольно часто при работе с
- Если простая индукция не работает, рассмотрите собственную схему индукции.