1

1）我相信可以在没有模式匹配的情况下使用归纳类型。（仅使用 _rec、_rect、_ind）。它是不透明的，复杂的，但可能的。2）是否可以在没有模式匹配的情况下使用共归纳类型？

存在从协归纳类型到协归纳类型构造函数域的并集的函数。Coq 是否显式生成它？如果是，如何重写 'hd' ？

Section stream.
  Variable A : Type.

  CoInductive stream : Type :=
  | Cons : A -> stream -> stream.
End stream.

Definition hd A (s : stream A) : A :=
  match s with
    | Cons x _ => x
  end.
4

1 回答 1

3

尽管可以在不直接求助于模式匹配的情况下使用归纳类型，但这只是表面上的正确：Coq 生成的_rec,_rect和_ind组合子都是根据match. 例如：

Print nat_rect.

nat_rect = 
fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 => f
  | S n0 => f0 n0 (F n0)
  end
     : forall P : nat -> Type,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

此外，在许多情况下，用消除器替换模式匹配会导致术语具有不同的计算行为。考虑以下函数，它将 anat除以二：

Fixpoint div2 (n : nat) :=
  match n with
  | 0 | 1 => 0
  | S (S n') => S (div2 n')
  end.

可以使用 重写这个函数，nat_rec但是递归调用n - 2使它有点复杂（试试看！）。

现在，回到您的主要问题，Coq 不会自动为协推类型生成类似的消除原则。Paco库有助于推导出更有用的推理推理数据的原则。但据我所知，编写普通函数没有类似的东西。

值得指出的是，您提出的方法与 Coq 对归纳数据类型所做的不同，因为它nat_rect和朋友允许通过归纳编写递归函数和证明。提供这些组合器的原因之一是它们被induction策略使用。type 的东西，nat -> unit + nat或多或少与您提出的建议相对应，是不够的。

于 2016-11-25T16:10:09.150 回答