コック：破壊（コ）誘導仮説情報

Question

を失うことなく、次の展開を考えてみましょう：

Require Import Relation RelationClasses. 

Set Implicit Arguments. 

CoInductive stream (A : Type) : Type := 
| scons : A -> stream A -> stream A. 

CoInductive stream_le (A : Type) {eqA R : relation A} 
         `{PO : PartialOrder A eqA R} : 
         stream A -> stream A -> Prop := 
| le_step : forall h1 h2 t1 t2, R h1 h2 -> 
      (eqA h1 h2 -> stream_le t1 t2) -> 
      stream_le (scons h1 t1) (scons h2 t2). 

私は仮説stream_le (scons h1 t1) (scons h2 t2)を持っている場合destruct戦術は、仮説のペアにそれを回すためには、それが合理的であるR h1 h2およびeqA h1 h2 -> stream_le t1 t2。しかし、それは何も起こりません。destructは何か重要でないことを行うたびに情報を失います。代わりに、新しい用語h0、h3、t0、t3は、それらがそれぞれh1に等しいことがないリコール、h2、t1、t2で、文脈に導入されています。

この種の「スマートdestruct」をすばやく簡単に行う方法があるかどうかを知りたいと思います。ここで私が今持っているものです：destructを呼び出す

Theorem stream_le_destruct : forall (A : Type) eqA R 
    `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A), 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    destruct H eqn:Heq. 
    remember (scons h1 t1) as s1 eqn:Heqs1; 
    remember (scons h2 t2) as s2 eqn:Heqs2; 
    destruct H; 
    inversion Heqs1; subst; clear Heqs1; 
    inversion Heqs2; subst; clear Heqs2. 
    split; assumption. 
Qed. 

Answer 1

確かに、inversionはあなたが望むものを基本的に行いますが、Arthurが指摘したように、主に異なる合同ステップのために少し不安定です。

inversionは、destructのバージョンを呼び出していますが、最初にいくつかの等価性を覚えておいてください。あなたがよく知っているように、Coqのパターンマッチングはコンストラクタの引数を "忘れる"でしょう。ただし、これらが変数である場合を除き、破壊のスコープの下のすべての変数がインスタンス化されます。

これはどういう意味ですか？これは、誘導型のI : Idx -> Propを適切に破壊するには、I x -> Q xという形式の目標を達成したいので、I xを破壊すると、Qのxも修正されます。したがって、誘導I termと目標Q (f term)の標準的な変換は、それをI x -> x = term -> Q (f x)に書き換えることです。次に、I xを破棄すると、xが適切なインデックスにインスタンス化されます。

これを念頭に置いて、case:のCoq 8.7の手法を使用して手動で反転を実装するとよいでしょう。

From Coq Require Import ssreflect. 
Theorem stream_le_destruct A eqA R `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A) : 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2). 
Proof. 
move E1: (scons h1 t1) => sc1; move E2: (scons h2 t2) => sc2 H. 
by case: sc1 sc2/H E1 E2 => h1' h2' t1' t2' hr ih [? ?] [? ?]; subst. 
Qed. 

あなたはより多くの詳細については、マニュアルを読むことができますが、基本的に最初の行で、私たちは、私たちに必要な等式を作成します。次に、我々はその用語を破壊し、目標を解決する適切なインスタンス化を得ることができます。戦術の良い効果は、破壊に反して、まずその依存関係をスコープに入れずに、用語を破壊しないようにしようとすることです。

Answer 2

は直接何をしたいあなたを与えることはありません。代わりにinversionを使用する必要があります。それはそれは難しい一貫それらに名前を付けるために作り、スプリアス平等の仮説の多くを生成する傾向があるよう

Theorem stream_le_destruct : forall h1 h2 t1 t2, 
    stream_le (scons h1 t1) (scons h2 t2) -> 
    h1 <= h2 /\ (h1 = h2 -> stream_le t1 t2). 
Proof. 
    intros. 
    inversion H; subst; clear H. 
    split; assumption. 
Qed. 

残念ながら、inversion戦術は非常に悪い、行儀ています。 1つ（幾分重量がある、確かに）の代替方法はinversionを呼び出す代わりに、inversionを使用して、あなたがしたような補題を証明し、この補題を証明に適用することです。