gistfile1.v

Require Import List.

Definition list1 (A : Type) := { lst1 : list A | lst1 <> nil }.

Definition of_h_t (A : Type) (h : A) (t : list A) : list1 A.
refine (exist _ (h :: t) _).
discriminate.
Defined.

Extraction of_h_t.

Lemma nil_neq_nil : forall A:Type, (nil <> (nil : list A)) -> False.
intros A H.
case H.
reflexivity.
Qed.

Definition list1_destruct (A : Type) (lst1 : list1 A)
  : (A * list A)
  :=
    match lst1 with
    | exist nil proof => False_rect _ (nil_neq_nil A proof)
    | exist (cons h t) _proof => (h, t)
    end
.

Extraction list1_destruct.

Definition map' (A B : Type) (f : A -> B) (a : list1 A) : list1 B :=
  let (ahd, atl) := list1_destruct A a in
  let bhd := f ahd in
  let btl := List.map f atl in
  of_h_t B bhd btl
.

Extraction map'.

Definition map (A B : Type) (f : A -> B) (a : list1 A) : list1 B.
refine (
  match a with
  | exist alst _ => exist _ (List.map f alst) _
  end
).
destruct alst; unfold map; try discriminate; auto.
Defined.

Extraction map.

$ coqc List1.v
type 'a list1 = 'a list
(** val of_h_t : 'a1 -> 'a1 list -> 'a1 list1 **)

let of_h_t h t =
  h :: t
(** val list1_destruct : 'a1 list1 -> 'a1 * 'a1 list **)

let list1_destruct = function
| [] -> assert false (* absurd case *)
| h :: t -> (h, t)
(** val map' : ('a1 -> 'a2) -> 'a1 list1 -> 'a2 list1 **)

let map' f a =
  let (ahd, atl) = list1_destruct a in
  let bhd = f ahd in let btl = map f atl in of_h_t bhd btl
(** val map0 : ('a1 -> 'a2) -> 'a1 list1 -> 'a2 list1 **)

let map0 f a =
  map f a