定理からの情報を使ったパターンマッチング

Question

私は以下の質問をしています。

(* Suppose we have type A *) 
    Variable A: Type. 

    (* Also we have a function that returns the type (option A) *) 
    Definition f_opt x: option A := ... 

    (* Then, I can prove that this function always returns something: *) 
    Theorem always_some: forall x, exists y, f_opt x = Some y. 
    Admitted. 

    (* Or, equivalently: *) 
    Theorem always_not_none: forall x, f_opt x <> None. 
    Admitted. 

今、私はいつもタイプAの値を返すf_optのバージョンを取得したいと思います。このような何か：

Definition f x: A := 
    match f_opt x with 
     | Some y => y 
    end. 

しかし、私は次のエラーを取得：

Non exhaustive pattern-matching: no clause found for pattern None .

私はタイプの作品のいくつかの種類を行う必要があることを理解し、私はまさに私が何をすべきか理解していないが。

Answer 1

でCoqの根底にある理論では、すべてのパターンマッチングは網羅的でなければならない。すなわち、問題の帰納的型のすべてのコンストラクタを明示的に考慮する必要がある。このため、あなたが見たエラーメッセージが表示されます。私たちはこの制限を回避するにはどうすればよい

？いくつかの解決策があります。まず、CoqにNoneブランチが発生しないことを納得させる方法を見てみましょう。このために、私たちはあなたのalways_not_none定理を使用します。

Definition f x : A := 
    match f_opt x as res return res <> None -> A with 
    | Some y => fun _ => y 
    | None => fun H => match H eq_refl with end 
    end (always_not_none x). 

このコードは、一見奇妙に見えるかもしれませんが、それはほとんどあなたがしたいパターンマッチを行います。 CoqにNoneケースが発生しないことを説明するために、always_not_noneとその枝にf_opt x = Noneという矛盾を導くという事実を組み合わせています。このブランチにはH eq_reflという語があります。そして、矛盾しているmatchは、ブランチが偽であることをCoqに確信させるには十分です。ビットは、より正式に、False、矛盾する命題ので、我々はタイプFalseの用語に一致したときに、に対処するための何の枝が存在しない、任意のコンストラクタなしで定義され、式全体が私たちが望む任意の型を返すことができます - にこの場合、A。このコードについて奇妙です何

は試合の型注釈であり、それは機能の代わりに、直接タイプAの何かを返すこと。我々は（f_opt xがそのブランチにNoneに等しいことを、ここで）私たちは試合の特定のブランチであることから得られる情報を利用したいとき、我々は明示的に行う必要があります。これは、理由はCoqの中でどのように機能するかに依存するパターンマッチで行われますその一致をAdam Chlipalaがconvoy patternと呼ぶ関数に戻します。これは、Coqがその余分な情報を使用する予定の場所を知り、正しく行われていることを確認するために行われます。ここでは、f_opt xがが必要とする仮説に矛盾を導くためにNoneであることを使用する。

これはあなたの問題を解決しますが、私は一般的に、このようにそれをやってから身を助言します。あなたはAタイプは、いくつかの要素a : Aが生息していることがわかっている場合たとえば、あなたは、単にその枝のfリターンaを作ることができます。これは、関数内での校正の言及を避ける利点があります。これは、用語を単純化して書き換えるときにしばしば邪魔になります。

Answer 2

あなたがそうすることをSetかTypeであなたの実存証明always_not_noneを配置する必要があります：

Theorem always_some: forall x, { y: A & f_opt x = Some y}. 
... 
Qed. 

その後、次の操作を実行（またはrefineまたはProgramを使用）することができます

Definition f (x: B) : A := 
    let s := always_some x in let (x0, _) := s in x0. 

Answer 3

コックのProgramモジュールを使用して、あなたは徹底的パターンマッチを書きますが、いくつかの枝が到達し、後でこれが事実であるという証拠を提供することは不可能であることを注釈を付けることができます。

Require Import Program. 
Program Definition f x : A := 
match f_opt x with 
| Some a => a 
| None => ! 
end. 
Next Obligation. 
destruct (always_some x). congruence. 
Qed. 

（Programモジュールしかし、完全な明示的な定義では、 "護送パターン"を使って書く必要がある場面の背後にある多くの作業を行いますが、Programは、JMeqと多くの依存関係を生成することがあります。タイプが関係していても、必要でない場合もあります。）