list.v

Require Import Coq.Unicode.Utf8.

Section lists.
  Variable A:Set.

  Inductive list:Set :=
  | nil: list
  | cons: A → list → list.

  Definition empty (l:list):Prop := l = nil.


  Definition empty_dec (l:list): {empty l} + {¬empty l}.
  refine (
    match l with
    | nil => left _ _
    | _ => right _ _
    end
  ); unfold empty; trivial.
  unfold not; intro H; discriminate H.
  Defined.

  Definition empty_b (l:list):bool :=
    if empty_dec l then true else false.

  Definition pop (l:list)(h:¬empty l): {l' | exists a, l = cons a l'}.
  induction l.
  + unfold not, empty in h; intuition.
  + refine ( exist _ l _ ).
    exists a.
    trivial.
  Defined.

  Definition push (l:list) (a:A): {l' | l' = cons a l}.
  refine (
    exist _ (cons a l) _
  ); reflexivity.
  Defined.

  Definition head (l:list)(h:¬empty l): { a | ∃ r, l = cons a r }.
  induction l.
  + unfold not, empty in h; intuition.
  + refine ( exist _ a _ ).
    exists l.
    trivial.
  Defined.

  Theorem push_head_equal: ∀ l a,
    match push l a with
    | exist l' h => ∀ h',
        match head l' h' with
        | exist a' h'' => a = a'
        end
    end.
  Proof.
    intros.
    unfold push.
    reflexivity.
  Qed.

  Theorem push_pop_equal: ∀ l a,
    match push l a with
    | exist l' h => ∀ h',
        (match pop l' h' with
        | exist l'' h'' => l = l''
        end)
    end.
  Proof.
    intros.
    unfold push.
    reflexivity.
  Qed.
End lists.