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

さらに、パターン マッチングをエリミネータに置き換えると、計算上の動作が異なる項になる場合が多くあります。nataを 2で除算する次の関数を考えてみましょう。

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帰納法によって再帰関数と証明を書くことができます。これらのコンビネータを提供する理由の 1 つは、それらがinductionタクティックによって使用されることです。nat -> unit + natあなたが提案したものに多かれ少なかれ対応するtype の何かは、十分ではありません。

于 2016-11-25T16:10:09.150 に答える