Логика: лексма auxilliry для tr_rev_correct - PullRequest
Новая
       71

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

0 голосов
/ 05 мая 2019

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

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]

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

1 Ответ

1 голос
/ 06 мая 2019

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