Proofs of the difference list invariant for various operations

DList.v

Require Import Lists.List.
Import ListNotations.
Open Scope list_scope.
Require Import Logic.FunctionalExtensionality.
Require Import Lists.Streams.

Inductive DList (a : Type) : Type :=
| MkDList : (list a -> list a) -> DList a.
Arguments MkDList {a} f.

Definition apply {a} (dl : DList a) : list a -> list a :=
  let 'MkDList f := dl in f.

Definition valid_DList {a} (d : DList a) : Prop :=
  exists p, forall (l : list a), apply d l = p ++ l.

Definition fromList {a} (l : list a) : DList a :=
  MkDList (fun l2 => l ++ l2).

Theorem valid_fromList :
  forall {a} (l : list a),
  valid_DList (fromList l).
Proof.
intros a l. unfold valid_DList. simpl. exists l. auto.
Qed.

Definition toList {a} (dl : DList a) : list a :=
  apply dl [].

Definition invariant_DList {a} (xs : DList a) : Prop :=
  fromList (toList xs) = xs.

Theorem invariantImpliesValid :
  forall {a} (d : DList a),
  invariant_DList d -> valid_DList d.
Proof.
unfold valid_DList, invariant_DList, fromList, toList.
intros a d invariant.
exists (toList d).
intros z. destruct d. simpl.
injection invariant as invariant.
change (l [] ++ z) with ((fun l2 => l [] ++ l2) z).
rewrite -> invariant.
auto.
Qed.

Theorem toFromList :
  forall {a} (l : list a),
  toList (fromList l) = l.
Proof. intros. simpl. apply app_nil_r. Qed.

Theorem fromToList :
  forall {a} (dl : DList a),
  valid_DList dl ->
  invariant_DList dl.
Proof.
unfold invariant_DList.
intros a [l] valid_dl.
unfold valid_DList in valid_dl. simpl in valid_dl.
simpl. unfold fromList. f_equal. extensionality l2.
destruct valid_dl as [p P].
rewrite -> (P []). rewrite -> (P l2).
rewrite -> app_nil_r. auto.
Qed.

Theorem applyToList :
  forall {a} (xs : DList a) (ys : list a),
  valid_DList xs ->
  apply xs ys = toList xs ++ ys.
Proof.
intros a [l] ys valid_dl.
unfold valid_DList in valid_dl. simpl in valid_dl. simpl.
destruct valid_dl as [p P].
rewrite -> (P ys). rewrite -> (P []).
rewrite -> app_nil_r. auto.
Qed.

Definition empty {a} : DList a :=
  MkDList id.

Theorem valid_empty :
  forall {a},
  valid_DList (@empty a).
Proof.
intros a. unfold valid_DList. simpl. exists []. auto.
Qed.

Theorem toListEmpty :
  forall {a},
  toList (@empty a) = [].
Proof. auto. Qed.

Definition singleton {a} (x : a) : DList a :=
  MkDList (fun l => x :: l).

Theorem valid_singleton :
  forall {a} (x : a),
  valid_DList (singleton x).
Proof.
intros a x. unfold valid_DList. simpl. exists [x]. auto.
Qed.

Theorem toListSingleton :
  forall {a} (x : a),
  toList (singleton x) = [x].
Proof. auto. Qed.

Definition cons {a} (x : a) (xs : DList a) : DList a :=
  MkDList (fun l => x :: apply xs l).

Theorem valid_cons :
  forall {a} (x : a) (xs : DList a),
  valid_DList xs ->
  valid_DList (cons x xs).
Proof.
intros a x [xs] valid_xs.
unfold valid_DList. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
destruct valid_xs as [p P].
exists (x :: p). simpl.
intros l. rewrite <- (P l). auto.
Qed.

Theorem toListCons :
  forall {a} (x : a) (xs : DList a),
  toList (cons x xs) = x :: toList xs.
Proof. auto. Qed.

Definition snoc {a} (xs : DList a) (x : a) : DList a :=
  MkDList (fun l => apply xs (x :: l)).

Theorem valid_snoc :
  forall {a} (xs : DList a) (x : a),
  valid_DList xs ->
  valid_DList (snoc xs x).
Proof.
intros a [xs] x valid_xs.
unfold valid_DList. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
destruct valid_xs as [p P].
exists (p ++ [x]). intros l. rewrite <- app_assoc.
simpl. rewrite -> (P (x :: l)). auto.
Qed.

Theorem toListSnoc :
  forall {a} (xs : DList a) (x : a),
  valid_DList xs ->
  toList (snoc xs x) = toList xs ++ [x].
Proof.
intros a [xs] x valid_xs. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
destruct valid_xs as [p P].
rewrite -> (P [x]). rewrite -> (P []).
rewrite -> app_nil_r. auto.
Qed.

Definition append {a} (xs : DList a) (ys : DList a) : DList a :=
  MkDList (fun l => apply xs (apply ys l)).

Theorem valid_append :
  forall {a} (xs ys : DList a),
  valid_DList xs ->
  valid_DList ys ->
  valid_DList (append xs ys).
Proof.
intros a [xs] [ys] valid_xs valid_ys.
unfold valid_DList. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
unfold valid_DList in valid_ys. simpl in valid_ys.
destruct valid_xs as [p P].
destruct valid_ys as [q Q].
exists (p ++ q). intros l.
rewrite -> (Q l). rewrite -> (P (q ++ l)).
apply app_assoc.
Qed.

Theorem toListAppend :
  forall {a} (xs ys : DList a),
  valid_DList xs ->
  valid_DList ys ->
  toList (append xs ys) = toList xs ++ toList ys.
Proof.
intros a [xs] [ys] valid_xs valid_ys. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
unfold valid_DList in valid_ys. simpl in valid_ys.
destruct valid_xs as [p P].
destruct valid_ys as [q Q].
rewrite -> (P []). rewrite -> (Q []).
rewrite -> 2 app_nil_r. rewrite -> (P q).
auto.
Qed.

Fixpoint foldrList {a b} (k : a -> b -> b) (z : b) (l : list a) : b :=
  match l with
  | []      => z
  | x :: xs => k x (foldrList k z xs)
  end.

Definition concat {a} : list (DList a) -> DList a :=
  foldrList append empty.

Theorem valid_concat :
  forall {a} (l : list (DList a)),
  Forall valid_DList l ->
  valid_DList (concat l).
Proof.
intros a l valid_l. unfold valid_DList.
induction l as [|d ds IHds].
- exists []. auto.
- change (concat (d :: ds))
    with (append d (concat ds)).
  simpl.
  inversion valid_l as [|A B valid_d valid_ds]. subst.
  destruct valid_d as [p P].
  destruct (IHds valid_ds) as [q Q].
  exists (p ++ q).
  intros l.
  rewrite -> (Q l).
  rewrite -> (P (q ++ l)).
  apply app_assoc.
Qed.

Theorem toListConcat :
  forall {a} (xss : list (DList a)),
  Forall valid_DList xss ->
  toList (concat xss) = List.concat (List.map toList xss).
Proof.
intros a xss valid_xss. induction xss as [|x xs IHxs].
- auto.
- change (toList (concat (x :: xs)))
    with (apply x (toList (concat xs))).
  inversion valid_xss as [|A B valid_x valid_xs]. subst.
  simpl.
  rewrite <- (IHxs valid_xs).
  unfold toList.
  destruct valid_x as [p P].
  destruct (valid_concat xs valid_xs) as [q Q].
  rewrite -> (Q []).
  rewrite -> (P []).
  rewrite -> (P (q ++ [])).
  rewrite -> 2 app_nil_r.
  auto.
Qed.

CoFixpoint repeat {a} (x : a) : Stream a :=
  Cons x (repeat x).

Fixpoint take {a} (n : nat) (s : Stream a) : list a :=
  let 'Cons x xs := s in
  match n with
  | 0   => []
  | S m => x :: take m xs
  end.

Definition replicateList {a} (n : nat) (x : a) : list a :=
  take n (repeat x).

Fixpoint replicate_helper {a} (n : nat) (x : a) (xs : list a) : list a :=
  match n with
  | 0   => xs
  | S m => x :: replicate_helper m x xs
  end.

Definition replicate {a} (n : nat) (x : a) : DList a :=
  MkDList (replicate_helper n x).

Theorem valid_replicate :
  forall {a} (n : nat) (x : a),
  valid_DList (replicate n x).
Proof.
intros a n x. unfold valid_DList.
induction n as [|m IHm]; simpl.
- exists []. auto.
- simpl in IHm. destruct IHm as [p P].
  exists (x :: p). intros l.
  rewrite -> (P l). auto.
Qed.

Theorem toListReplicate :
  forall {a} (n : nat) (x : a),
  toList (replicate n x) = replicateList n x.
Proof.
intros a n x. unfold replicateList.
induction n as [|m IHm]; simpl.
- auto.
- simpl in IHm. rewrite -> IHm. auto.
Qed.

Definition headList {a} (xs : list a) : option a :=
  match xs with
  | x :: _ => Some x
  | [] => None
  end.

Definition head {a} (xs : DList a) : option a :=
  match toList xs with
  | x :: _ => Some x
  | [] => None
  end.

Theorem headToList :
  forall {a} (xs : DList a),
  head xs = headList (toList xs).
Proof. auto. Qed.

Definition tailList {a} (xs : list a) : option (list a) :=
  match xs with
  | _ :: ys => Some ys
  | [] => None
  end.

Definition tail {a} (xs : DList a) : option (list a) :=
  match toList xs with
  | _ :: ys => Some ys
  | [] => None
  end.

Theorem tailToList :
  forall {a} (xs : DList a),
  tail xs = tailList (toList xs).
Proof. auto. Qed.

Definition foldr {a b} (f : a -> b -> b) (z : b) (xs : DList a) : b :=
  foldrList f z (toList xs).

Theorem foldrToList :
  forall {a b} (f : a -> b -> b) (z : b) (xs : DList a),
  foldr f z xs = foldrList f z (toList xs).
Proof. auto. Qed.

Definition map {a b} (f : a -> b) : DList a -> DList b :=
  foldr (fun x => cons (f x)) empty.

Lemma foldrConsFromList :
  forall {a b} (f : a -> b) (l : list a),
  foldrList (fun x : a => cons (f x)) empty l = fromList (List.map f l).
Proof.
intros a b f l. induction l as [|x xs IHxs]; simpl.
- auto.
- rewrite -> IHxs. auto.
Qed.

Theorem valid_map :
  forall {a b} (f : a -> b) (xs : DList a),
  valid_DList xs ->
  valid_DList (map f xs).
Proof.
intros a b f [xs] valid_xs.
unfold valid_DList, map, foldr. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
destruct valid_xs as [p P].
rewrite -> (P []). rewrite -> app_nil_r.
rewrite -> foldrConsFromList.
destruct (valid_fromList (List.map f p)) as [q Q].
exists q. intros l.
rewrite -> Q.
auto.
Qed.

Theorem toListMap :
  forall {a b} (f : a -> b) (xs : DList a),
  valid_DList xs ->
  toList (map f xs) = List.map f (toList xs).
Proof.
intros a b f [xs] valid_xs.
unfold map, foldr. simpl.
unfold valid_DList in valid_xs. simpl in valid_xs.
destruct valid_xs as [p P].
rewrite -> (P []). rewrite -> app_nil_r.
rewrite -> foldrConsFromList.
rewrite -> toFromList.
auto.
Qed.

Fixpoint prependToAll {a} (sep : a) (l : list a) : list a :=
  match l with
  | []      => []
  | x :: xs => sep :: x :: prependToAll sep xs
  end.

Definition intersperse {a} (sep : a) (l : list a) : list a :=
  match l with
  | []      => []
  | x :: xs => x :: prependToAll sep xs
  end.

Definition intercalateList {a} (sep : list a) (xss : list (list a)) : list a :=
  List.concat (intersperse sep xss).

Definition intercalate {a} (sep : DList a) (xss : list (DList a)) : DList a :=
  concat (intersperse sep xss).

Lemma valid_prependToAll :
  forall {a} (sep : DList a) (xss : list (DList a)),
  valid_DList sep ->
  Forall valid_DList xss ->
  Forall valid_DList (prependToAll sep xss).
Proof.
intros a sep xss valid_sep valid_xss.
induction xss as [|x xs IHxs]; simpl.
- constructor.
- constructor.
  + auto.
  + constructor; inversion valid_xss; auto.
Qed.

Lemma valid_intersperse :
  forall {a} (sep : DList a) (xss : list (DList a)),
  valid_DList sep ->
  Forall valid_DList xss ->
  Forall valid_DList (intersperse sep xss).
Proof.
intros a sep xss valid_sep valid_xss.
destruct xss as [|x xs]; simpl.
- constructor.
- constructor; inversion valid_xss; subst.
  + auto.
  + apply valid_prependToAll; auto.
Qed.

Theorem valid_intercalate :
  forall {a} (sep : DList a) (xss : list (DList a)),
  valid_DList sep ->
  Forall valid_DList xss ->
  valid_DList (intercalate sep xss).
Proof.
intros a sep xss valid_sep valid_xss.
unfold valid_DList, intercalate.
destruct (valid_concat (intersperse sep xss)
                       (valid_intersperse sep xss valid_sep valid_xss))
         as [p P].
exists p. intros l. rewrite -> (P l).
auto.
Qed.

Lemma mapPrependToAll :
  forall {a b} (f : a -> b) (sep : a) (xs : list a),
  List.map f (prependToAll sep xs) =
  prependToAll (f sep) (List.map f xs).
Proof.
intros a b f sep xs. induction xs as [|x xs IHxs].
- auto.
- simpl. rewrite -> IHxs. auto.
Qed.

Lemma mapIntersperse :
  forall {a b} (f : a -> b) (sep : a) (xs : list a),
  List.map f (intersperse sep xs) =
  intersperse (f sep) (List.map f xs).
Proof.
intros a b f sep xs. destruct xs as [|x xs].
- auto.
- simpl. rewrite -> mapPrependToAll. auto.
Qed.

Theorem toListIntercalate :
  forall {a} (sep : DList a) (xss : list (DList a)),
  valid_DList sep ->
  Forall valid_DList xss ->
  toList (intercalate sep xss) = intercalateList (toList sep) (List.map toList xss).
Proof.
intros a sep xss valid_sep valid_xss.
unfold intercalateList, intercalate.
rewrite -> (toListConcat (intersperse sep xss)
                         (valid_intersperse sep xss valid_sep valid_xss)).
rewrite -> mapIntersperse.
auto.
Qed.

Definition bind {a b} (m : DList a) (k : a -> DList b) : DList b :=
  foldr (fun x => append (k x)) empty m.

Lemma foldrAppendConcat :
  forall {a b} (f : a -> DList b) (l : list a),
  foldrList (fun x : a => append (f x)) empty l = concat (List.map f l).
Proof.
intros a b f l. induction l as [|x xs IHxs]; simpl.
- auto.
- rewrite -> IHxs. auto.
Qed.

Lemma valid_list_map :
  forall {a b} (k : a -> DList b) (l : list a),
  (forall (x : a), valid_DList (k x)) ->
  Forall valid_DList (List.map k l).
Proof.
intros a b k l valid_k. induction l as [|x xs IHxs]; simpl.
- constructor.
- constructor.
  + apply (valid_k x).
  + auto.
Qed.

Theorem valid_bind :
  forall {a b} (m : DList a) (k : a -> DList b),
  valid_DList m ->
  (forall (x : a), valid_DList (k x)) ->
  valid_DList (bind m k).
Proof.
intros a b [m] k valid_m valid_k.
unfold valid_DList, bind, foldr. simpl.
destruct valid_m as [p P]. simpl in P.
rewrite -> (P []). rewrite -> app_nil_r.
rewrite -> foldrAppendConcat.
destruct (valid_concat (List.map k p)
                       (valid_list_map k p valid_k))
         as [q Q].
exists q. intros l.
rewrite -> (Q l). auto.
Qed.