読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqで代数的データ型の各要素についての等式を得る

Coq

前提 C x y z = C x' y' z から x = x', y = y', z = z' を導くためのタクティックが用意されています。

injection

等式 H : C x y z = C x' y' z' についてinjection Hをすると、ゴールをx = x' -> y = y' -> z = z' -> (元のゴール)という形に書き換えてくれます。

Goal forall n m : nat, S n = S m -> n = m.
Proof.
  intros n m H. (* H : S n = S m *)
  injection H.
  (* Goal: n = m -> n = m *)
  intros. assumption.
Qed.

inversion

injectionの進化版です。injectionをした後introsをし、さらに得られた等式を使ってゴールを書き換えてくれます。

Goal forall n m : nat, S n = S m -> n = m.
Proof.
  intros n m H. (* H : S n = S m *)
  inversion H. (* H1 : n = m *)
  (* Goal: m = m *)
  reflexivity.
Qed.

ちなみに、明らかに異なる等式に対してinversionをすると、そこで矛盾が導けて即座に証明終了になります。

Goal forall (P : Prop) (n : nat), 0 = S n -> P.
Proof.
  intros P n H. (* H : 0 = S n *)
  inversion H.
Qed.