Доказательство того, что обратимый список является палиндромом в Coq

Вот мое индуктивное определение палиндромов:

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

И теорема, которую я хочу доказать, из Software Foundations:

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> pal l.

Мои неофициальные наброски доказательства следующие:

Предположим, что l0 - произвольный список, такой что l0 = rev l0. Тогда должен иметь место один из следующих трех случаев. l0 имеет:

(а) нулевые элементы, в этом случае это палиндром по определению.

(б) один элемент, в этом случае он также является палиндромом по определению.

(c) два или более элемента, и в этом случае l0 = x :: l1 ++ [x] для некоторого элемента x и некоторого списка l1, такого что l1 = rev l1.

Теперь, начиная с l1 = rev l1, должен выполняться один из следующих трех случаев ...

Рекурсивный анализ случаев будет прекращен для любого конечного списка l0, потому что длина анализируемого списка уменьшается на 2 на каждой итерации. Если он завершается для любого списка ln, все его внешние списки до l0 также являются палиндромами, поскольку список, построенный путем добавления двух идентичных элементов на обоих концах палиндрома, также является палиндромом.

Я думаю, что это разумная аргументация, но я не знаю, как ее формализовать. Можно ли превратить это в доказательство в Coq? Некоторые объяснения того, как работает использованная тактика, были бы особенно полезны.


theorem-proving coq palindrome logical-foundations
person user287393    schedule 23.06.2014    source источник

Ответы (2)


arrow_upward
15
arrow_downward

Это хороший пример, когда «прямая» индукция вообще не работает, потому что вы напрямую выполняете рекурсивный вызов не в хвосте, а в его части. В таких случаях я обычно советую формулировать вашу лемму с длиной списка, а не с самим списком. Затем вы можете специализировать это. Это будет примерно так:

Lemma rev_eq_pal_length: forall (X: Type) (n: nat) (l: list X), length l <= n -> l = rev l -> pal l.
Proof.
(* by induction on [n], not [l] *)
Qed.

Theorem rev_eq_pal: forall (X: Type) (l: list X), l = rev l -> pal l.
Proof.
(* apply the previous lemma with n = length l *)
Qed.

При необходимости могу помочь более подробно, просто оставьте комментарий.

Удачи !

V.

РЕДАКТИРОВАТЬ: чтобы помочь вам, мне потребовались следующие леммы, чтобы сделать это доказательство, они вам тоже могут понадобиться.

Lemma tool : forall (X:Type) (l l': list X) (a b: X),                                                                                                         
            a :: l = l' ++ b :: nil -> (a = b /\ l = nil) \/ exists k, l = k ++ b :: nil.

Lemma tool2 : forall (X:Type) (l1 l2 : list X) (a b: X),                                                                                                         
     l1 ++ a :: nil = l2 ++ b :: nil -> a = b /\ l1 = l2.
person Vinz    schedule 23.06.2014

arrow_upward
3
arrow_downward

Вы также можете вывести свой принцип индукции из одной из форм хорошо обоснованной индукции.

Notation " [ ] " := nil : list_scope.
Notation " [ x1 ; .. ; x2 ] " := (cons x1 .. (cons x2 nil) ..) : list_scope.
Open Scope list_scope.

Conjecture C1 : forall t1 f1 p1, (forall x1, (forall x2, f1 x2 < f1 x1 -> p1 x2) -> p1 x1) -> forall x1 : t1, p1 x1.
Conjecture C2 : forall t1 p1, p1 [] -> (forall x1 l1, p1 ([x1] ++ l1)) -> forall l1 : list t1, p1 l1.
Conjecture C3 : forall t1 p1, p1 [] -> (forall x1 l1, p1 (l1 ++ [x1])) -> forall l1 : list t1, p1 l1.
Conjecture C4 : forall t1 (x1 x2 : t1) l1, length l1 < length ([x1] ++ l1 ++ [x2]).

Theorem T1 : forall t1 p1,
  p1 [] ->
  (forall x1, p1 [x1]) ->
  (forall x1 x2 l1, p1 l1 -> p1 ([x1] ++ l1 ++ [x2])) ->
  forall l1 : list t1, p1 l1.
Proof.
intros t1 p1 h1 h2 h3.
induction l1 as [l1 h4] using (C1 (list t1) (@length t1)).
induction l1 as [| x1 l1] using C2.
eapply h1.
induction l1 as [| x2 l1] using C3.
simpl.
eapply h2.
eapply h3.
eapply h4.
eapply C4.
Qed.

Вы можете доказать гипотезу C1, сначала применив гипотезу к заключению, затем применив структурную индукцию по f1 x1, а затем используя некоторые факты о <.

Чтобы доказать C3, который не имеет гипотезы индукции, вы сначала используете анализ случая на is_empty l1, а затем используете факты is_empty l1 = true -> l1 = [] и is_empty l1 = false -> l1 = delete_last l1 ++ [get_last l1] (для get_last потребуется значение по умолчанию).

person Community    schedule 23.06.2014