定義一個「頭」用於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類型的流（沒有模式匹配）

回答

相關問題