coqの目標に存在するものを破壊する方法

Question

これは少し一般的なので詳細を聞いてみてください。問題を簡単に伝えるために簡略化しました。

は、私の目標はf xが{u | P u}型を持つ

let (r,_) := f x in Q r 

であると言います。

私はQ r を目標としてP rを仮説として「破壊」したいと思います。これを達成する最良の方法は何ですか？過去に は、私が

pose (f x). 

、その後、簡素化することによって何を望むか達成しています。

リクエストごとにここにいくつかの簡単なコードがあります。

Parameter T:Type. 
Parameter P:T -> Prop. 

Axiom A : {t:T|P t}. 

Definition myvar:T. 
    destruct A. 
    exact x. 
Defined. 
Theorem B : P myvar. 

Answer 1

unfold myvar; destruct A. 

この特定のケースではあなたの目標を解決します。

一般に、destruct戦術は任意の用語で使用することができ、用語を抽象化して破壊しようとします。ただし、特に従属型を使用している場合は、この処理が失敗することがあります。

destructの下にgallina matchが使用されています。Coqでは、パターンマッチングで入力情報が失われる可能性があります。詳細については、「Convoy Pattern」を検索してください。

Answer 2

したい場合は、destruct戦術の「出力」を名前を付けることができます。

(* Stupid definitions to create a minimal example *) 
Parameter A: Set. 
Parameter P Q: A -> Prop. 
Definition f (x: A) : {r | P r }. 
Admitted. 

Goal (forall x, let (r, _) := f x in Q r). 
intro x. 
destruct f as [r hr]. (* you goal has now r: A and hr : P r as premises *) 
Abort. 

編集：コメントの後の詳細情報を。 名前を付けないと、xi変数（x0, x1, ...）に基づくスキームを使用してCoqが自動的に行います。 destruct f as [r].