CODEWITHSUNDEEP
haskellequivalentproof
Tom
Tom

Reputation: 135

Prove that reverse=rev

I have some task to do, but don't know how to do it:

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

"Prove that : reverse=rev"

Your help would be appreciated. Thank you.

PS. I can do it using some example but i think thats not professional

Upvotes: 0

Views: 1537

Answers (4)

augustss
augustss

Reputation: 23014

You can make a sloppy proof by structural induction, but if you want to a proof that handles bottom correctly it is less trivial.

Upvotes: 3

Robin Green
Robin Green

Reputation: 33033

Since any list reversing function can only produce any output if given finite lists, we can translate this code into Coq (in which lists are always finite) and prove the desired statement there (ignoring bottom).

This proof is not my own - it is a slightly modified version of a proof from the standard library.

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.

Upvotes: 1

hugomg
hugomg

Reputation: 69934

Instead of trying to prove equivalence directly, I would for each function prove (using induction) that it actually reverses the list. If both of them reverse lists, then they are equivalent.

Proof sketch:

We want to prove that rev works for all lists:

base case lists of length 0: prove that rev [] computes correctly

inductive case: prove that for any n, rev can reverses any list of length n, assuming rev can reverse any list of length up to n-1

Upvotes: 1

Joel Burget
Joel Burget

Reputation: 1438

Induction. The base case is trivial. The inductive step shouldn't be too hard.

Upvotes: 2

Related Questions