非依赖列表类型 Coq

Question

我试图在 Coq 中定义一个非依赖的 list 类型，但我想不出一个方法来做到这一点。我设法公理化地定义了 ndList，修改了 Coq 的 list 定义。这是我目前的工作：

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.

有没有办法将 ndList 定义为 Inductive 类型？

感谢您的帮助。

Answer 1

您的 "non-dependent" 列表类型可证明与 Coq 的 list 类型同构：

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.

您还可以轻松地自动获得 el 大约 list 秒，甚至：

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

这是否满足您的目的，还是您想要更多？

非依赖列表类型 Coq

Non-dependent list type Coq

coq