Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Require Import List.
Import ListNotations.
Set Implicit Arguments.
Fixpoint reverse (X: Type) (xs: list X): list X :=
match xs with
| [] => []
| x :: xs' => reverse xs' ++ [x]
end.
Lemma app_eq_nil: forall (X: Type) (xs ys: list X), xs ++ ys = xs -> ys = [].
induction xs; simpl; inversion 1; auto.
Qed.
Theorem rev_spec_complete:
forall (X: Type) (rev: list X -> list X),
(forall x, rev [x] = [x]) ->
(forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs) ->
(forall xs, rev xs = reverse xs).
Proof.
intros X rev S A; induction xs as [|x' xs']; simpl.
assert (rev ([] ++ []) = rev [] ++ rev []) as H; auto.
apply (@app_eq_nil X (rev [])); symmetry; apply H.
assert (x' :: xs' = [x'] ++ xs') as H; auto.
rewrite H; rewrite <- IHxs'; rewrite A; rewrite S; reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.