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

きくらげ観察日記

好きなことを、適当に。

Coqで既存の定理、定義に従って計算する。

Coq

定義に従って計算する

定義に従って計算するには、simpl, compute, unfoldが使えます。
simpl.はゴールの式をいい感じに簡単にしてくれるのに対し、compute.はとりあえず式展開します。また、unfoldは定義の左辺から右辺に書き換えます。

Fixpoint fact (n : nat) : nat :=
  match n with
    | O => 1
    | S n' => n * fact n'
  end.

Example fact_example1:
  forall n : nat, fact (S n) = S n * fact n.
Proof.
  intros n.
  simpl.
  (* ここでのゴール:
   * fact n + n * fact n = fact n + n * fact n
   *)
  reflexivity.
Qed.

Definition mult n m := n * m.

Goal forall n m : nat, mult n m = n * m.
Proof.
  intros n m.
  (* Goal: mult n m = n * m *)
  unfold mult.
  (* Goal: n * m = n * m *)
  reflexivity.
Qed.

定理を用いて書き換える

前提や既に定義された定理として等式がある場合、rewriteを使うことで書き換えることができます。

Goal forall (T : Type) (x : T) (f g : T -> T),
       g (f x) = x -> g (f (g (f x))) = x.
Proof.
  intros T x f g H. (* H : g (f x) = x *)
  (* この時点でのゴール: g (f (g (f x))) = x *)
  rewrite -> H. (* Hを用いて、ゴールの左辺を右辺に書き換える *)
  (* この時点でのゴール: g (f x) = x *)
  rewrite -> H. (* もう一度適用 *)
  (* この時点でのゴール: x = x *)
  reflexivity.
Qed.

等式Hを用いて左辺を右辺に置き換える場合は->, 右辺を左辺に書き換える場合は<-を使います。

また、simpl in H, rewrite -> ... in Hを使うことで、ゴールではなく前提にある式の項を書き換えることができます。

Goal forall P : Prop, 1 + 1 = 0 -> P.
Proof.
  intros P H. (* H : 1 + 1 = 0 *)
  simpl in H. (* H : 2 = 0 *)
  discriminate.
Qed.