非依赖列表类型 Coq答案

【问题标题】：Non-dependent list type Coq非依赖列表类型 Coq
【发布时间】：2017-09-12 23:05:54
【问题描述】：

我试图在 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 类型？

感谢您的帮助。

【问题讨论】：

有什么特别的理由想要公理地定义这个吗？列表作为归纳类型的定义可在线获取：coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html。
不，实际上没有。我知道这个定义，但list_rec 使用了依赖类型P : list A -> Set。相反，我想定义一个稍微不同的列表类型，其中P 不依赖于list A。无论如何，我设法以公理的方式定义了它（请参阅更新的问题文本），但我想知道是否存在归纳等价物。
您的e1 只是list_rect 的特例，其中P := fun _ : list C => L。（另见Coq.Lists.List.fold_right。）
你也可以用 Definition ndList (C:Type) : Type := forall T:Type, T -> (C->T) -> T. 做类似的事情（这显然是你曾经在更老的 Coq 版本中必须做的事情。）不过，最重要的事情是由于 Universe 层次结构，您将无法直接将递归运算符应用于涉及 list 本身的类型（例如，您必须手动定义 append）。
您可以使用Scheme list_ind_non_dep := Minimality for list Sort Type 来定义非依赖原则（参见doc）。

标签： coq

【解决方案1】：

您的“非依赖”列表类型可证明与 Coq 的 list 类型同构：

Axiom ndList：forall C：类型，类型。 Axiom nil : forall C, ndList C. 公理缺点：forall C、forall (c: C) (l: ndList C)、ndList C。参数无 {_}。论据缺点 {_} _ _。公理 el : forall (C L: Type), forall (a: L) (s: ndList C) (l: forall (x: C) (z: L), L), L. 公理 c1 : forall (C L: Type), forall (a: L) (l: forall (x: C) (z: L), L), el C L a 无 l = a。公理 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)。公理 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。 ISO 部分。上下文{A：类型}。定义 list_to_ndList : 列表 A -> ndList A := list_rect (fun _ => ndList A) 零（乐趣 x _ xs => 缺点 x xs）。定义 ndList_to_list (ls : ndList A) : 列表 A := el A (列表 A) 数据类型.nil ls 数据类型.cons。引理 list_eq (ls : list A) : ndList_to_list (list_to_ndList ls) = ls。证明。展开 ndList_to_list、list_to_ndList。归纳 ls as [|x xs IHxs]; 首先重复[进度简单 |进度重写 ?c1, ?c2 |一致 ]。 Qed。引理 ndList_eq (ls : ndList A) : list_to_ndList (ndList_to_list ls) = ls。证明。展开 ndList_to_list、list_to_ndList。传递性（el A (ndList A) nil ls cons）； [对称| ];恢复 ls; 匹配目标 | [ |- forall ls, @?LHS ls = @?RHS ls ] => 介绍；申请（c_eta _ _ _ _ RHS ls）结尾; 首先重复[进度简单 |进度介绍 |进度重写 ?c1, ?c2 |一致 ]。 Qed。结束iso。

您还可以轻松地自动获取您的el 关于lists，甚至：

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

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

【讨论】：

这正是我想要的。谢谢！