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.
T: Type
l: ne_list
l = from_list (head l) (tail l)
    induction l as [x|x l IHl].
T: Type
x: T
one x = from_list (head (one x)) (tail (one x))
T: Type
x: T
l: ne_list
IHl: l = from_list (head l) (tail l)
cons x l = from_list (head (cons x l)) (tail (cons x l))
    -
T: Type
x: T
one x = from_list (head (one x)) (tail (one x)) reflexivity.
    -
T: Type
x: T
l: ne_list
IHl: l = from_list (head l) (tail l)
cons x l = from_list (head (cons x l)) (tail (cons x l)) destruct l as [y|y l].
T: Type
x, y: T
IHl: one y = from_list (head (one y)) (tail (one y))
cons x (one y) = from_list (head (cons x (one y))) (tail (cons x (one y)))
T: Type
x, y: T
l: ne_list
IHl: cons y l = from_list (head (cons y l)) (tail (cons y l))
cons x (cons y l) =
from_list (head (cons x (cons y l))) (tail (cons x (cons y l)))
      +
T: Type
x, y: T
IHl: one y = from_list (head (one y)) (tail (one y))
cons x (one y) = from_list (head (cons x (one y))) (tail (cons x (one y))) reflexivity.
      +
T: Type
x, y: T
l: ne_list
IHl: cons y l = from_list (head (cons y l)) (tail (cons y l))
cons x (cons y l) =
from_list (head (cons x (cons y l))) (tail (cons x (cons y l))) exact (ap (cons x) 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.
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 rect 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))
rect: forall l0 : ne_list, P l0 * forall x : T, P (cons x l0)
l: ne_list
P l
      exact (fst (rect 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) intro 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))
l: ne_list
P l * forall x : T, P (cons x l)
      induction l as [x|x l IHl].
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))
x: T
P (one x) * forall x0 : T, P (cons x0 (one x))
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))
x: T
l: ne_list
IHl: P l * forall x0 : T, P (cons x0 l)
P (cons x l) * forall x0 : T, P (cons x0 (cons x l))
      +
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))
x: T
P (one x) * forall x0 : T, P (cons x0 (one x)) split.
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))
x: T
P (one x)
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))
x: T
forall x0 : T, P (cons x0 (one x))
        *
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))
x: T
P (one x) exact (Pone x).
        *
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))
x: T
forall x0 : T, P (cons x0 (one x)) intro y.
T: Type
P: ne_list -> Type
Pone: forall x0 : T, P (one x0)
Ptwo: forall x0 y0 : T, P (cons x0 (one y0))
Pmore: forall (x0 y0 : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x0 (cons y0 z))
x, y: T
P (cons y (one x)) exact (Ptwo y x).
      +
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))
x: T
l: ne_list
IHl: P l * forall x0 : T, P (cons x0 l)
P (cons x l) * forall x0 : T, P (cons x0 (cons x l)) destruct IHl as [Pl Pcons].
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))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
P (cons x l) * forall x0 : T, P (cons x0 (cons x l))
        split.
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))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
P (cons x l)
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))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
forall x0 : T, P (cons x0 (cons x l))
        *
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))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
P (cons x l) exact (Pcons x).
        *
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))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
forall x0 : T, P (cons x0 (cons x l)) intro y.
T: Type
P: ne_list -> Type
Pone: forall x0 : T, P (one x0)
Ptwo: forall x0 y0 : T, P (cons x0 (one y0))
Pmore: forall (x0 y0 : T) (z : ne_list),
P z -> (forall y' : T, P (cons y' z)) -> P (cons x0 (cons y0 z))
x: T
l: ne_list
Pl: P l
Pcons: forall x0 : T, P (cons x0 l)
y: T
P (cons y (cons x l))
          exact (Pmore y x l Pl Pcons).
  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 Abbreviation 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.