定义一个“头”用于Coq的coinductive类型的流（没有模式匹配）

1）I相信这是可以使用感应类型没有模式匹配。（仅使用_rec，_rect，_ind）。这是不透明的，复杂的，但可能的。 2）是否有可能使用带模式匹配的共诱导类型？定义一个“头”用于Coq的coinductive类型的流（没有模式匹配）

有存在的函数从coinductive类型构造函数coinductive类型的结构域的结合。 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.

来源

2016-11-25 First Last

虽然可以使用感应类型，而无需直接诉诸模式匹配，这只是表面上真实的：由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

此外，也有许多情况下，通过消除替换模式匹配会导致不同的计算行为的术语。考虑下面的函数，它由两部分一nat：

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策略所使用。某种类型的nat -> unit + nat，或多或少与您所提议的内容相对应，是不够的。

来源

2016-11-25 16:10:09

定义一个“头”用于Coq的coinductive类型的流（没有模式匹配）

回答

相关问题