DL.v

Require Import Coq.Lists.List.
Require Import FunctionalExtensionality.
Import ListNotations.

Inductive DList (a : Set) :=
| DL : (list a -> list a) -> DList a.

Definition fromList {a : Set} (l : list a) : DList a :=
  DL a (app l).

Definition toList {a : Set} (dl : DList a) : list a :=
  match dl with
  | DL _ f => f []
  end.

Theorem from_to_id :
  forall (a : Set) (xs : list a),
    toList (fromList xs) = xs.
Proof.
  intros.
  induction xs.
  - simpl. trivial.
  - simpl. rewrite app_nil_r. trivial.
Qed.

Theorem to_from_id :
  forall (a : Set) (xs : DList a),
    fromList (toList xs) = xs.
Proof.
  intros.
  induction xs.
  simpl.
  unfold fromList.
  apply f_equal.
  extensionality x.
  induction x.
  rewrite app_nil_r.
  reflexivity.
  (* ??? *)

  
  admit.
Admitted.

Your theorem is false:

Corollary bad : False.
Proof.
  pose proof to_from_id _ (DL _ (fun l => l ++ [0])) as H.
  unfold toList, fromList in H.
  simpl in H.
  inversion H as [Hf].
  clear H.
  assert ([0;1] = [1; 0]).
  { change [0; 1] with ((fun m : list nat => 0 :: m) [1]).
    change [1; 0] with ((fun l : list nat => l ++ [0]) [1]).
    rewrite Hf.
    reflexivity. }
  inversion H.
Qed.