Coq의 Coinductive Type 스트림에 대한 '머리'정의 (패턴 매칭없이)

Question

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. 

Answer 1

, 이것은 표면적으로 사실이다 : 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 

또한 제거기로 패턴 일치를 바꾸면 다른 계산 동작을하는 용어가 나오는 경우가 많습니다. 그것은

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

이 nat_rec를 사용하여이 기능을 다시 작성 가능하지만, n - 2에 재귀 호출이 조금 복잡하게 두하여 nat 분할 다음 함수를 고려 (그것을 시도!).

이제 주 질문으로 돌아 가면 Coq는 이 아니며은 자동으로 유사한 유형의 유도 성 제거 원리를 생성합니다. Paco 라이브러리는 유도 데이터에 대해 추론에 대한 더 유용한 원칙을 유도하는 데 도움이됩니다. 그러나 내가 아는 한, 평범한 기능을 쓰는 것과 비슷한 것은 없습니다.

제안 된 접근 방식은 유도 데이터 형식에 대해 Coq가 수행하는 방식과 다르다는 점을 지적 할 가치가 있습니다. nat_rect 및 친구들이 유도로 재귀 함수 및 교정을 작성할 수 있다는 점에서 다릅니다. 이러한 연결자를 제공하는 이유 중 하나는 induction 전술로 사용된다는 것입니다. 어떤 종류의 유형 nat -> unit + nat, 어느 정도는 당신이 제안한 것과 일치, 충분하지 않을 것입니다.