Require ImportRequire Import
  HoTT.Utf8Minimal
  HoTT.Spaces.List.Core
  HoTT.Basics.Overture Basics.Tactics
  HoTT.Spaces.Nat.Core.

Local Open Scope nat_scope.
Local Open Scope type_scope.

Declare Scope ne_list_scope.

Delimit Scope ne_list_scope with ne_list.

Open Scope ne_list_scope.

(** Nonempty list implementation [ne_list.ne_list]. *)

Module ne_list.

Section with_type.
  Context {T: Type}.

(** A nonempty list. Below there is an implicit coercion
    [ne_list >-> list]. *)

  Inductive ne_list : Type
    := one: T → ne_list | cons: T → ne_list → ne_list.

  Fixpoint app (a b: ne_list): ne_list :=
    match a with
    | one x => cons x b
    | cons x y => cons x (app y b)
    end.

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

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

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

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

  Fixpoint from_list (x: T) (xs: list T): ne_list :=
    match xs with
    | nil => one x
    | List.Core.cons h t => cons x (from_list h t)
    end.

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

  Lemma decomp_eq (l: ne_list): l = from_list (head l) (tail l).
T: Type
l: ne_list
l = from_list (head l) (tail l)
  Proof with auto.
T: Type
l: ne_list
l = from_list (head l) (tail l)
    induction l...
T: Type
t: T
l: ne_list
IHl: l = from_list (head l) (tail l)
cons t l = from_list (head (cons t l)) (tail (cons t l))
    destruct l...
T: Type
t, t0: T
l: ne_list
IHl: cons t0 l = from_list (head (cons t0 l)) (tail (cons t0 l))
cons t (cons t0 l) =
from_list (head (cons t (cons t0 l))) (tail (cons t (cons t0 l)))
    cbn in *.
T: Type
t, t0: T
l: ne_list
IHl: cons t0 l = from_list t0 (to_list l)
cons t (cons t0 l) = cons t (from_list t0 (to_list l))
    rewrite IHl...
  Qed. 

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

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

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

  Fixpoint front (l: ne_list) : list T :=
    match l with
    | one _ => nil
    | cons x xs => x :: front xs
    end.

  Lemma two_level_rect (P: ne_list → 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.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
forall l : ne_list, P l
  Proof with auto.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
forall l : ne_list, P l
   cut (∀ l, P l * ∀ x, P (cons x l)).
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
(forall l : ne_list, P l * (forall x : T, P (cons x l))) ->
forall l : ne_list, P l
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
forall l : ne_list, P l * (forall x : T, P (cons x l))
   -
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
(forall l : ne_list, P l * (forall x : T, P (cons x l))) ->
forall l : ne_list, P l intros.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
X: forall l0 : ne_list, P l0 * (forall x : T, P (cons x l0))
l: ne_list
P l apply X.
   -
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
forall l : ne_list, P l * (forall x : T, P (cons x l)) destruct l...
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
P (cons t l) * (forall x : T, P (cons x (cons t l)))
     revert t.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
l: ne_list
forall t : T, P (cons t l) * (forall x : T, P (cons x (cons t l)))
     induction l...
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t0 : T, P (cons t0 l) * (forall x : T, P (cons x (cons t0 l)))
forall t0 : T,
P (cons t0 (cons t l)) * (forall x : T, P (cons x (cons t0 (cons t l))))
     intros.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x : T, P (cons x (cons t1 l)))
t0: T
P (cons t0 (cons t l)) * (forall x : T, P (cons x (cons t0 (cons t l))))
     split.
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x : T, P (cons x (cons t1 l)))
t0: T
P (cons t0 (cons t l))
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x : T, P (cons x (cons t1 l)))
t0: T
forall x : T, P (cons x (cons t0 (cons t l)))
     +
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x : T, P (cons x (cons t1 l)))
t0: T
P (cons t0 (cons t l)) apply IHl.
     +
T: Type
P: ne_list -> Type
Pone: forall x : T, P (one x)
Ptwo: forall x y : T, P (cons x (one y))
Pmore: forall (x y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x : T, P (cons x (cons t1 l)))
t0: T
forall x : T, P (cons x (cons t0 (cons t l))) intro.
T: Type
P: ne_list -> Type
Pone: forall x0 : T, P (one x0)
Ptwo: forall x0 y : T, P (cons x0 (one y))
Pmore: forall (x0 y : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x0 (cons y z))
t: T
l: ne_list
IHl: forall t1 : T, P (cons t1 l) * (forall x0 : T, P (cons x0 (cons t1 l)))
t0, x: T
P (cons x (cons t0 (cons t l))) apply Pmore; intros; apply IHl.
  Qed.

  Lemma tail_length (l: ne_list)
    : S (length (List.Core.tail (to_list l))) = length (to_list l).
T: Type
l: ne_list
(length (Core.tail (to_list l))).+1 = length (to_list l)
  Proof.
T: Type
l: ne_list
(length (Core.tail (to_list l))).+1 = length (to_list l) destruct l; reflexivity. Qed.
End with_type.

Arguments ne_list : clear implicits.

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

Lemma tails_are_shorter {T} (y x: ne_list T):
  InList x (to_list (tails y)) →
  leq (length (to_list x)) (length (to_list y)).
T: Type
y, x: ne_list T
InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
Proof.
T: Type
y, x: ne_list T
InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
  induction y; cbn.
T: Type
t: T
x: ne_list T
(one t = x) + Empty -> length (to_list x) <= 1
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
(cons t y = x) + InList x (to_list (tails y)) ->
length (to_list x) <= (length (to_list y)).+1
  -
T: Type
t: T
x: ne_list T
(one t = x) + Empty -> length (to_list x) <= 1 intros [[] | C].
T: Type
t: T
x: ne_list T
length (to_list (one t)) <= 1
T: Type
t: T
x: ne_list T
C: Empty
length (to_list x) <= 1
    +
T: Type
t: T
x: ne_list T
length (to_list (one t)) <= 1 constructor.
    +
T: Type
t: T
x: ne_list T
C: Empty
length (to_list x) <= 1 elim C.
  -
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
(cons t y = x) + InList x (to_list (tails y)) ->
length (to_list x) <= (length (to_list y)).+1 intros [[] | C].
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
length (to_list (cons t y)) <= (length (to_list y)).+1
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
C: InList x (to_list (tails y))
length (to_list x) <= (length (to_list y)).+1
    +
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
length (to_list (cons t y)) <= (length (to_list y)).+1 exact _.
    +
T: Type
t: T
y, x: ne_list T
IHy: InList x (to_list (tails y)) -> length (to_list x) <= length (to_list y)
C: InList x (to_list (tails y))
length (to_list x) <= (length (to_list y)).+1 by apply leq_succ_r, IHy.
Qed.

Fixpoint map {A B} (f: A → B) (l: ne_list A): ne_list 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: ne_list A)
  : to_list (map f l) = List.Core.list_map f (to_list l).
A, B: Type
f: A -> B
l: ne_list A
to_list (map f l) = list_map f (to_list l)
Proof.
A, B: Type
f: A -> B
l: ne_list A
to_list (map f l) = list_map f (to_list l)
  induction l.
A, B: Type
f: A -> B
t: A
to_list (map f (one t)) = list_map f (to_list (one t))
A, B: Type
f: A -> B
t: A
l: ne_list A
IHl: to_list (map f l) = list_map f (to_list l)
to_list (map f (cons t l)) = list_map f (to_list (cons t l))
  -
A, B: Type
f: A -> B
t: A
to_list (map f (one t)) = list_map f (to_list (one t)) reflexivity.
  -
A, B: Type
f: A -> B
t: A
l: ne_list A
IHl: to_list (map f l) = list_map f (to_list l)
to_list (map f (cons t l)) = list_map f (to_list (cons t l)) cbn.
A, B: Type
f: A -> B
t: A
l: ne_list A
IHl: to_list (map f l) = list_map f (to_list l)
(f t :: to_list (map f l))%list = (f t :: list_map f (to_list l))%list rewrite <- IHl.
A, B: Type
f: A -> B
t: A
l: ne_list A
IHl: to_list (map f l) = list_map f (to_list l)
(f t :: to_list (map f l))%list = (f t :: to_list (map f l))%list reflexivity.
Qed.

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

Fixpoint zip {A B: Type} (l: ne_list A) (m: ne_list B)
  : ne_list (A * B) :=
  match l with
  | one a => one (a, head m)
  | cons a l =>
      match m with
      | one b => one (a, b)
      | cons b m => cons (a, b) (zip l m)
      end
  end.

  Module notations.

    Global Notation ne_list := ne_list.

    Global Notation "[: x :]" := (one x) : ne_list_scope.

    Global Notation "[: x ; .. ; y ; z :]"
        := (cons x .. (cons y (one z)) ..) : ne_list_scope.

    Global Infix ":::" := cons : ne_list_scope.

  End notations.

End ne_list.

Global Coercion ne_list.to_list : ne_list.ne_list >-> list.