Докажите, что наоборот = rev - PullRequest
Новая
       7

Докажите, что наоборот = rev

0 голосов
/ 08 мая 2011

У меня есть какое-то задание, но я не знаю, как это сделать: 

reverse, rev :: [a] [a]

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

rev = aux [] where
    aux ys [] = ys
    aux ys (x:xs) = aux (x:ys) xs

"Докажите, что: reverse = rev"

Ваша помощь будет принята с благодарностью.Спасибо.

PS.Я могу сделать это на некотором примере, но я думаю, что это не профессионально

Ответы [ 4 ]

3 голосов
/ 08 мая 2011

Вы можете сделать неаккуратное доказательство путем структурной индукции, но если вы хотите получить доказательство, которое правильно обрабатывает дно, оно менее тривиально.

2 голосов
/ 08 мая 2011

Индукционная.Базовый случай тривиален.Индуктивный шаг не должен быть слишком сложным.

1 голос
/ 08 мая 2011

Поскольку любая функция обращения к списку может производить любой вывод только при наличии конечных списков, мы можем перевести этот код в Coq (в котором списки всегда конечны) и доказать желаемое утверждение там (игнорируя дно).

Это доказательство не мое, это слегка измененная версия доказательства из стандартной библиотеки. 

Open Scope list_scope.

Require List.
Require Import FunctionalExtensionality.

Section equivalence.

  Variable A : Type.

  (* The reverse function is already defined in the standard library as List.rev. *)
  Notation reverse := (@List.rev A).

  Fixpoint aux (ys l2 : list A) :=
    match l2 with
      nil => ys
      | x :: xs => aux (x :: ys) xs
    end.

  Definition rev : list A -> list A
    := aux nil.

  Lemma aux_rev : forall l l', aux l' l = reverse l ++ l'.
  Proof.
    induction l; simpl; auto; intros.
    rewrite <- List.app_assoc; firstorder.
  Qed.

  Theorem both_equal : reverse = rev.
    extensionality xs.
    unfold rev.
    rewrite aux_rev.
    now rewrite List.app_nil_r.
  Qed.

End equivalence.
1 голос
/ 08 мая 2011

Вместо того чтобы пытаться доказать эквивалентность напрямую, я бы для каждой функции доказывал (используя индукцию), что она фактически переворачивает список.Если оба они переворачивают списки, то они эквивалентны.

Эскиз доказательства:

Мы хотим доказать, что rev работает для всех списков:

базовый случай списки длиной 0: доказать, что rev [] правильно вычисляет

индуктивный случай : доказать, что для любого n, rev может обратитьлюбой список длины n, предполагая, что rev может перевернуть любой список длины до n-1

...