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

きくらげ観察日記

好きなことを、適当に。

Coqで等式の左右を入れ替える

Coq

タイトルの通りです。

eq_reflをdestructしていい感じにやるような方法でも解けることは解けます。

Goal forall (T : Type) (x y : T), x = y -> y = x.
Proof.
  intros T x y H. (* H : x = y *)
  destruct H.
  (* Goal: x = x *)
  reflexivity.
Qed.

しかし、等式の左右入れ替えを行うためのタクティック、symmetryが用意されているので、これを使ったほうが賢いでしょう。

Goal forall (T : Type) (x y : T), x = y -> y = x.
Proof.
  intros T x y H. (* H : x = y *)
  (* Goal: y = x *)
  symmetry.
  (* Goal: x = y *)
  apply H.
Qed.