6

多くの場合、Coq では次のことを行っていることに気付きます。たとえば、証明の目標があります。

some_constructor a c d = some_constructor b c d

a = bとにかく、他のすべてが同じであるため、証明する必要があるだけなので、次のようにします。

assert (a = b).

次に、そのサブゴールを証明します。

rewrite H.
reflexivity.

証明を終了します。

しかし、私の証明の一番下にぶら下がっているそれらを持っているのは、不必要な混乱のようです.

Coqには、コンストラクターの等価性を取り、それをコンストラクターパラメーターの等価性に分割するための一般的な戦略がありますsplitか?

4

2 に答える 2

4

Coq の検索機能を使用できます。

  Search (?X _ = ?X _).
  Search (_ _ = _ _).

いくつかのノイズの中で補題を明らかにする

f_equal: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

そして、複数引数の等号の兄弟: f_equal2... f_equal5(Coq バージョン 8.4 以降)。

次に例を示します。

Inductive silly : Set :=
  | some_constructor : nat -> nat -> nat -> silly
  | another_constructor : nat -> nat -> silly.

Goal forall x y,
    x = 42 ->
    y = 6 * 7 ->
    some_constructor x 0 1 = some_constructor y 0 1.
  intros x y Hx Hy.
  apply f_equal3; try reflexivity.

この時点で、証明する必要があるのはx = y.

于 2016-05-27T19:52:36.927 に答える