implementations.ne_list

This module should be Required but not Imported (except for the notations submodule).

Require Import
  Unicode.Utf8 Coq.Lists.List Setoid Morphisms Permutation.

Instance: A, Proper (@Permutation A ==> eq) (@length A).


Section contents.

  Context {T: Type}.

  Inductive L: Type := one: T L | cons: T L L.

  Fixpoint app (a b: L) {struct a}: L :=
    match a with
    | one x => cons x b
    | cons x y => cons x (app y b)
    end.

  Fixpoint foldr {R} (o: T R) (f: T R R) (a: L): R :=
    match a with
    | one x => o x
    | cons x y => f x (foldr o f y)
    end.

  Fixpoint foldr1 (f: T T T) (a: L): T :=
    match a with
    | one x => x
    | cons x y => f x (foldr1 f y)
    end.

  Definition head (l: L): T := match l with one x => x | cons x _ => x end.

  Fixpoint to_list (l: L): list T :=
    match l with
    | one x => x :: nil
    | cons x xs => x :: to_list xs
    end.

  Global Coercion to_list: L >-> list.

  Definition tail (l: L): list T := match l with one _ => nil | cons _ x => to_list x end.

  Definition last: L T := foldr1 (fun x y => y).

  Fixpoint replicate_Sn (x: T) (n: nat): L :=
    match n with
    | 0 => one x
    | S n' => cons x (replicate_Sn x n')
    end.

  Fixpoint take (n: nat) (l: L): L :=
    match l, n with
    | cons x xs, S n' => take n' xs
    | _, _ => one (head l)
    end.

  Lemma two_level_rect (P: L Type)
    (Pone: x, P (one x))
    (Ptwo: x y, P (cons x (one y)))
    (Pmore: x y z, P z ( y', P (cons y' z)) P (cons x (cons y z))):
       l, P l.

  Lemma tl_length (l: L): S (length (tl l)) = length l.

  Notation ListPermutation := (@Permutation.Permutation _).

  Definition Permutation (x y: L): Prop := ListPermutation x y.

  Global Instance: Equivalence Permutation.

  Global Instance: Proper (Permutation ==> ListPermutation) to_list.

  Lemma Permutation_ne_tl_length (x y: L):
    Permutation x y length (tl x) = length (tl y).

End contents.

Implicit Arguments L [].

Fixpoint tails {A} (l: L A): L (L A) :=
  match l with
  | one x => one (one x)
  | cons x y => cons l (tails y)
  end.

Lemma tails_are_shorter {A} (y x: L A):
  In x (tails y)
  length x <= length y.

Fixpoint map {A B} (f: A B) (l: L A): L B :=
  match l with
  | one x => one (f x)
  | cons h t => cons (f h) (map f t)
  end.

Lemma list_map {A B} (f: A B) (l: L A): to_list (map f l) = List.map f (to_list l).

Global Instance: forall {A B} (f: A B), Proper (Permutation ==> Permutation) (map f).

Module notations.

  Global Notation ne_list := L.
  Global Infix ":::" := cons (at level 60, right associativity).

End notations.