Library zoo.common.listne

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.options.

Definition listne A :=
  { x : list A | x ≠ [] }.

Section listne.
  Context {A : Type}.

  Implicit Type x y : A.
  Implicit Type l : listne A.

  Program Definition listne۰app l1 l2 : listne A :=
    `l1 ++ `l2.

  #[global] Instance listne۰elem_of : ElemOf A (listne A) :=
    λ x l,
      x ∈ `l.

  Definition listne۰Forall P l :=
    Forall P (`l).

  Lemma listneｰnon_empty l :
    ∃ x,
    x ∈ l.

  Lemma listneｰelem_ofｰsingleton x y H :
    x ∈ [y]↾H ↔
    x = y.
  Lemma listneｰelem_ofｰapp l1 l2 x :
    x ∈ listne۰app l1 l2 ↔
    x ∈ l1 ∨ x ∈ l2.

  Lemma listne۰Forallｰ∀ P l :
    listne۰Forall P l ↔
    ∀ x, x ∈ l → P x.
  Lemma listne۰Forallｰsingleton {P} x H :
    listne۰Forall P ([x]↾H) ↔
    P x.
  Lemma listne۰Forallｰapp P l1 l2 :
    listne۰Forall P (listne۰app l1 l2) ↔
      listne۰Forall P l1 ∧
      listne۰Forall P l2.
  Lemma listne۰Forallｰelem_of P l x :
    listne۰Forall P l →
    x ∈ l →
    P x.
End listne.