きくらげ観察日記

好きなことを、適当に。

Coqで定理の特定の項だけを書き換える

rewriteやsimplを使って定理を書き換えようとすると、どうしても思ったとおりに書き換えがいかないことがあります。

(* 結合法則と交換法則を使って、3つの項を入れ替える *)
Goal forall (T : Type) (op : T -> T -> T),
       (forall x y z : T, op (op x y) z = (op x (op y z))) ->
       (forall x y : T, op x y = op y x) ->
       (forall x y z : T, op (op x y) z = op (op z y) x).
Proof.
  intros T op assoc comm.
  intros x y z.
  (* Goal: op (op x y) z = op (op z y) x *)
  rewrite -> assoc. (* op (op z y) x -> op z (op y x) したい *)
  (* Goal: op x (op y z) = op (op z y) x になってしまった……。 *)
Abort. (* 本当はこの状態からでも証明はできるが、思ったとおりにいかなかったのでとりあえずAbort *)

こういった場合は、replaceタクティックを使うとうまく行きます。

rewrite hoge with fuga.

このタクティックはゴール中の項hogeを、すべてfugaで置き換えてくれます。
そうして書き換わったゴールを証明したあと、今度はhoge = fugaであることの証明を行います。

Goal forall (T : Type) (op : T -> T -> T),
       (forall x y z : T, op (op x y) z = (op x (op y z))) ->
       (forall x y : T, op x y = op y x) ->
       (forall x y z : T, op (op x y) z = op (op z y) x).
Proof.
  intros T op assoc comm.
  intros x y z.
  (* Goal: op (op x y) z = op (op z y) x *)
  replace (op (op z y) x) with (op z (op y x)).
  (* Goal: op (op x y) z = op z (op y x) *)
  replace (op y x) with (op x y).
  (* Goal: op (op x y) z = op z (op x y) *)
  replace (op z (op x y)) with (op (op x y) z).
  reflexivity.
  - (* op (op x y) z = op z (op x y) の証明 *)
    apply comm.
  - (* op x y = op y x の証明 *)
    apply comm.
  - (* op z (op y x) = op (op z y) x の証明 *)
    rewrite -> assoc.
    reflexivity.
Qed.

また、replace hoge with fuga in Hを使うことによって、ゴールではなく前提H内の項を書き換えることもできます。

Goal forall (T : Type) (x y : T) (P : T -> T -> Prop),
       x = y -> P x y -> P y y.
Proof.
  intros T x y P xisy Pxy. (* xisy : x = y, Pxy : P x y *)
  replace x with y in Pxy. (* Pxy: P y y に書き換わる *)
  apply Pxy.
Qed