CODEWITHSUNDEEP
coq
madipi
madipi

Reputation: 355

Non-dependent list type Coq

I'm trying to define a non-dependent list type in Coq, but I cannot figure out a way to do that. I managed to define ndList axiomatically, modifying Coq's list definition. Here's my work so far:

Axiom ndList : forall C: Type, Type.
Axiom nil : forall C, ndList C.
Axiom cons : forall C, forall (c: C) (l: ndList C), ndList C.
Arguments nil {_}.
Arguments cons {_} _ _.
Axiom el : forall (C L: Type), forall (a: L) (s: ndList C)
    (l: forall (x: C) (z: L), L), L.
Axiom c1 : forall (C L: Type), forall (a: L) (l: forall (x: C) (z: L), L), 
  el C L a nil l = a.
Axiom c2 : forall (C L: Type), forall (s: ndList C) (c: C) (a: L) 
  (l: forall (x: C) (z: L), L), 
    el C L a (cons c s) l = l c (el C L a s l).
Axiom c_eta : forall (C L: Type), forall (a: L) (l: forall (x: C) (z: L), L)
  (t: forall y: ndList C, L) (s: ndList C) (eq1: t nil = a) 
  (eq2: forall (x: C) (z: ndList C), t (cons x z) = l x (t z)),
    el C L a s l = t s.

Is there a way to define ndList as an Inductive type?

Thanks for helping.

Upvotes: 0

Views: 128

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

Your "non-dependent" list type is provably isomorphic to Coq's list type:

Axiom ndList : forall C: Type, Type.
Axiom nil : forall C, ndList C.
Axiom cons : forall C, forall (c: C) (l: ndList C), ndList C.
Arguments nil {_}.
Arguments cons {_} _ _.
Axiom el : forall (C L: Type), forall (a: L) (s: ndList C)
                                      (l: forall (x: C) (z: L), L), L.
Axiom c1 : forall (C L: Type), forall (a: L) (l: forall (x: C) (z: L), L),
      el C L a nil l = a.
Axiom c2 : forall (C L: Type), forall (s: ndList C) (c: C) (a: L)
                                      (l: forall (x: C) (z: L), L),
      el C L a (cons c s) l = l c (el C L a s l).
Axiom c_eta : forall (C L: Type), forall (a: L) (l: forall (x: C) (z: L), L)
                 (t: forall y: ndList C, L) (s: ndList C) (eq1: t nil = a)
                 (eq2: forall (x: C) (z: ndList C), t (cons x z) = l x (t z)),
      el C L a s l = t s.

Section iso.
  Context {A : Type}.
  Definition list_to_ndList : list A -> ndList A
    := list_rect (fun _ => ndList A)
                 nil
                 (fun x _ xs => cons x xs).
  Definition ndList_to_list (ls : ndList A) : list A
    := el A (list A)
          Datatypes.nil
          ls
          Datatypes.cons.
  Lemma list_eq (ls : list A) : ndList_to_list (list_to_ndList ls) = ls.
  Proof.
    unfold ndList_to_list, list_to_ndList.
    induction ls as [|x xs IHxs];
      repeat first [ progress simpl
                   | progress rewrite ?c1, ?c2
                   | congruence ].
  Qed.
  Lemma ndList_eq (ls : ndList A) : list_to_ndList (ndList_to_list ls) = ls.
  Proof.
    unfold ndList_to_list, list_to_ndList.
    transitivity (el A (ndList A) nil ls cons); [ symmetry | ]; revert ls;
      match goal with
      | [ |- forall ls, @?LHS ls = @?RHS ls ]
        => intro ls; apply (c_eta _ _ _ _ RHS ls)
      end;
      repeat first [ progress simpl
                   | progress intros
                   | progress rewrite ?c1, ?c2
                   | congruence ].
  Qed.
End iso.

You can also easily get your el about lists, automatically, even:

Scheme el := Minimality for list Sort Type.
Check el. (* forall A P : Type, P -> (A -> list A -> P -> P) -> list A -> P *)

Does this suffice for your purposes, or are you wanting more?

Upvotes: 3

Related Questions