Логика: лексма auxilliry для tr_rev_correct

Question

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

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]

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

Answer 1

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

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

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

Как предполагает Bubbler, вспомогательная лемма 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 тактика (см. главу " Тактика" в Основах логики).

Answer 2

Вы можете видеть, что гипотеза индукции 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.

Answer 3

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

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.