7

私は、match構築の助けを借りて定式化された仮説のルールを書こうとしています:

Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat.
intros.

x : nat
H : match x with
    | 0%nat => 10%nat
    | 1%nat => 5%nat
    | S (S _) => 10%nat
    end = 5%nat
============================
 x = 1%nat

どうすればそのような仮説を一致させることができますか? 次の簡単な方法は失敗します。

match goal with
  |[H:match ?e with | ?a => ?x | ?b => ?y | ?c => ?z end = ?b] => idtac
end.

> Syntax error: 'end' expected after [branches] (in [match_constr]).
4

1 に答える 1

9

ステートメントのパターン マッチングmatchはやや奇妙です。

最初に知っておくべきことは、Coq の内部には、match複数の変数に対する a やディープ マッチングのようなものがないということです。すべてがより単純なmatchステートメントに変換されます。したがって、あなたが書いた用語は、実際には次の用語の構文シュガーです。

match x with
| 0 => 10
| S x' =>
  match x' with
  | 0 => 5
  | S x'' => 10
  end
end

これは、証明状態を出力するときに Coq が示唆していることです。問題は、このシンタックス シュガーが Ltac パターンでは機能しないことです。したがって、 amatchに言及する Ltac パターンを記述するときは、常にそれが 1 レベルの であるかのように一致させるように努める必要がありますmatch。

2 番目の問題は、次のような :のパターン部分をバインドできないことです。match

match goal with
| H : match ?x => _ | ?y => _ end = 5 |- _ => (* ... *)
end

Ltac では意味がありません。

問題を解決するには、次の 2 つの選択肢があります。

  1. matchパターン部分のタイプのコンストラクターの正確なリストを使用して、期待するものを書き留めます。

    match goal with
| H : match x with 0 => _ | S _  => _ end = 5 |- _ => (* ... *)
end

  2. どんなものにもマッチする特別なmatch (* ... *) with _ => _ end構文を使用してください: match

    match goal with
| H : match x with _ => _ end = 5 |- _ => (* ... *)
end

多くの場合、あなたの場合のように、深いものを含むのすべてのブランチを検討したい場合があります。matchこのイディオムは、その場合に役立ちます。

repeat match goal with
| H : match ?x with _ => _ end = _ |- _ =>
  destruct x; try solve [inversion H]
end.
于 2015-02-11T15:44:21.520 に答える