Ltacの単項データコンストラクタのマッチング

Question

Coqの単純型ラムダ計算を正式化するための演習をいくつか行い、Ltacを使って私の証明を自動化したいと思います。進捗定理を証明しながら：

Theorem progress : forall t T, 
    empty |-- t \in T -> value t \/ exists t', t ==> t'. 

私はLTACコードのこの部分を思い付いた：

Ltac progress_when_stepping := 
    (* right, because progress statement places stepping on the right of \/ *) 
    right; 
    (* use induction hypotheses *) 
    repeat 
    match goal with 
    | [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 _ ==> _ ] => 
     induction H; auto 
    | [ H : _ -> value _ \/ exists _, ?t2 ==> _, H0 : value ?t1 |- 
     exists _, ?C ?t1 ?t2 ==> _ ] => 
     induction H; auto 
    | [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] => 
     induction H; auto 
    end. 

==>は（小ステップセマンティクスを経由して）評価の一つのステップです。マッチ例それぞれの意図は次のとおりです。私たちが言う仮説を持って

1. マッチ任意のバイナリコンストラクタそのコンストラクタステップの最初の項。
2. マッチ任意のバイナリコンストラクタ我々が言う仮説を持っているとき、我々はコンストラクタで、コンストラクタステップと、第1項の第2項は、すでに値
3. マッチだという仮説任意の単項コンストラクタを持っていますそれはコンストラクタの段階での用語です。

しかし、このコードの動作を見ると、3番目のケースもバイナリのコンストラクタと一致しているように見えます。どのように私は実際に単体のコンストラクタと一致するように制限するのですか？

Answer 1

問題は?Cフォーム?C0 ?t0の期間と一致していることです。あなたはこのケースを除外するためにいくつかの二次マッチングを行うことができます。

match goal with 
    … 
| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] => 
    match C with 
    | ?C0 ?t0 => fail 
    | _ => induction H; auto 
    end 
end. 

Answer 2

context ident [ term ]建設がうまくいくように思える：

パターンに対する部分項と一致するパターンの特殊な形式があります： context ident [cpattern]が。 どの用語もcpatternと一致するサブタイトルと一致します。一致が存在する場合、任意のidentには「一致したコンテキスト」、すなわち一致するサブ用語が穴で置き換えられた最初の用語が割り当てられる。 ...歴史的な理由

、例えば全体としてではなく、単項アプリケーション((f 1) 2)のシーケンスとして(f 1 2)としてn進アプリケーションを検討するために使用さcontext。したがって、context [f ?x]は、(f 1 2)で一致するサブタームを見つけることができませんでした。パターンが部分的なアプリケーションであった場合、一致したサブタームは、必ず同じ数の引数を持つアプリケーションでしたでしょう。

だから、私は（少なくとも、それは私がでっち上げてきた最低限の人工的な例で動作します）、これはうまくいくと思います：

... 
    | [ H : _ -> value _ \/ exists _, ?t1 ==> _ 
    |- context [exists _, ?C ?t1 ==> _ ]] => induction H; auto 
...