3

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. コンストラクターのステップの 2 番目の項とコンストラクターの最初の項が既に値であるという仮説がある場合、任意のバイナリコンストラクターに一致します。
  3. コンストラクターの項がステップするという仮説がある場合、任意の単項コンストラクターに一致します。

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

4

2 に答える 2

2

問題は、それ?Cがフォームの用語に一致すること?C0 ?t0です。このケースを除外するために、いくつかの二次照合を行うことができます。

match goal with
  …
| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] =>
  match C with
    | ?C0 ?t0 => fail
    | _ => induction H; auto
  end
end.
于 2016-05-06T10:13:52.830 に答える
0

context ident [ term ]構築がうまくいくようです：

サブタームをパターンと照合する特殊な形式のパターンがあります: context ident [cpattern]. cpattern に一致するサブタームを持つ任意のタームに一致します。一致する場合、オプションの ident に「一致したコンテキスト」が割り当てられます。つまり、一致したサブタームが穴に置き換えられた最初のタームです。 ...

歴史的な理由から、単項アプリケーションのシーケンスとしてではなく、全体contextとして n 項アプリケーションを考慮するために使用されます。したがって、 で一致するサブタームを見つけることができません。パターンが部分的なアプリケーションである場合、一致したサブタームは、まったく同じ数の引数を持つアプリケーションである必要があります。(f 1 2)((f 1) 2)context [f ?x](f 1 2)

だから、これはうまくいくと思います（少なくとも、私が作成した最小限の人為的な例ではうまくいきます）：

...
  | [ H : _ -> value _ \/ exists _, ?t1 ==> _
    |- context [exists _, ?C ?t1 ==> _ ]] => induction H; auto
...
于 2016-05-06T10:08:39.323 に答える