Логика: вспомогательная лемма для tr_rev_correct

В главе «Логика» представлена ​​хвостовая рекурсивная версия функции обратного списка. Нам нужно доказать, что он работает правильно:

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

(* Tail recursion rev *)
Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

Но прежде чем это доказать, я хотел доказать лемму:

Lemma rev_append_app: forall (X: Type) (x: X) (l : list X),
    rev_append l [x] = rev_append l [] ++ [x].
Proof.
  intros X x l. induction l as [| h t IH].
  - simpl. reflexivity.
  - simpl.

Вот я застрял:

X : Type
x, h : X
t : list X
IH : rev_append t [x] = rev_append t [ ] ++ [x]
============================
rev_append t [h; x] = rev_append t [h] ++ [x]

Что делать дальше?


coq logical-foundations
person user4035    schedule 05.05.2019    source источник
comment
Короткий ответ: доказать эту лемму не легче, чем исходную.   -  person Li-yao Xia    schedule 05.05.2019
comment
@ Li-yaoXia Пожалуйста, подскажи.   -  person user4035    schedule 05.05.2019

Ответы (3)


arrow_upward
4
arrow_downward

Как вы заметили во время попытки доказательства, при вводе шага индукции от rev_append l [x] до rev_append (h :: t) [x] вы получаете термин rev_append t [h; x] после упрощения. Шаг индукции ведет не к базовому случаю функции rev_append, а к другому рекурсивному вызову, который нельзя упростить.

Обратите внимание, как гипотеза индукции, которую вы хотели бы применить, делает утверждение о rev_append t [x] для некоторого фиксированного x, но в вашей цели дополнительный элемент списка h перед тем, как он встанет на пути, и гипотеза индукции бесполезна.

Это то, на что имел в виду ответ Бабблера, когда утверждал, что ваша гипотеза индукции недостаточно сильна: он делает заявление только о случае, когда второй аргумент является списком с единственным элементом. Но даже после шага индукции (одно рекурсивное приложение) в этом списке уже есть как минимум два элемента!

Как предположил Баблер, вспомогательная лемма rev_append l (l1 ++ l2) = rev_append l l1 ++ l2 сильнее и не имеет этой проблемы: при использовании в качестве гипотезы индукции ее также можно применить к rev_append t [h; x], что позволяет вам доказать равенство с rev_append t [h] ++ [x].

Пытаясь доказать вспомогательную лемму, вы можете застрять (как и я) точно так же, как и при доказательстве самого rev_append_app. Важнейший совет, который помог мне продолжить, заключался в том, чтобы быть осторожным с тем, какие из универсально количественно определяемых переменных вы вводите, прежде чем начинать индукцию. Если вы специализируетесь на каком-либо из них слишком рано, вы можете ослабить свою гипотезу индукции и снова застрять. Возможно, вам придется изменить порядок этих количественных переменных или использовать тактику generalize dependent (см. Тактика главы Основы логики).

person Simon    schedule 07.08.2019

arrow_upward
2
arrow_downward

Вы можете видеть, что гипотеза индукции IH недостаточно сильна, чтобы доказать цель. Здесь вам нужно в первую очередь доказать более общее утверждение. Дополнительные упражнения, посвященные этой теме, можно найти здесь. (На самом деле хвостовая рекурсивная реверсия - одно из упражнений.)

В вашем случае полностью обобщенное утверждение может быть таким:

Lemma rev_append_app': forall (X: Type) (l l1 l2 : list X),
    rev_append l (l1 ++ l2) = rev_append l l1 ++ l2.

Доказать это по индукции тривиально. Затем вы можете доказать свое собственное утверждение как следствие этого:

Corollary rev_append_app: forall (X: Type) (x: X) (l : list X),
    rev_append l [x] = rev_append l [] ++ [x].
Proof. intros. apply (rev_append_app _ _ [] [x]). Qed.
person Bubbler    schedule 05.05.2019

arrow_upward
0
arrow_downward

используйте тактику обобщения зависимостей следующим образом:

Lemma rev_append_app: forall (X: Type) (l l1: list X) (x : X),
    rev_append l (l1 ++ [x]) = rev_append l l1 ++ [x].
  intros.
  generalize dependent l1.
  induction l as [| h t IH].
  - intros.
    easy.
  - intros.
    apply (IH (h::l1)).
Qed.
person user2068018    schedule 22.08.2019