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

きくらげ観察日記

好きなことを、適当に。

Coqで定理の証明中に補題を示す

Coq

assertタクティックを使うと、証明の途中で他の補題を証明できます。

Goal forall P Q R : Prop,
       P -> (P \/ Q -> R) -> R.
Proof.
  intros P Q R H1 H2.
  (* H1 : P *)
  (* H2 : P \/ Q -> R *)
  (* 先にP -> Rを示す *)
  assert (P -> R).
  {
    (* P -> R の証明 *)
    (* この部分は本質的な話ではないので、よくわからなかったら読み飛ばしてOK *)
    intros P1.
    apply or_introl with (B := Q) in P1. (* P1: P \/ Q *)
    apply H2 in P1. (* P1: R *)
    assumption.
  }
  (* ここからは元のゴールの証明 *)
  (* H: P -> R という名前で上の補題が定義された *)
  apply H in H1.
  assumption.
Qed.

また、assert (H: P x).という形にすることによって、今から示す定理の名前をHに指定することもできます。