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

きくらげ観察日記

好きなことを、適当に。

Coqで「…かつ…」、「…または…」を扱う

Coq

連言「かつ」、選言「または」を表すandとorは、Coqでは次のようなデータ構造として定義されています。

Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B

where "A /\ B" := (and A B) : type_scope.

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B

where "A \/ B" := (or A B) : type_scope.

AとBからA /\ Bを導く

conjはAとBを引数にとり、A /\ Bを生成するコンストラクタですが、見方を変えれば「A -> B -> A /\ B」という定理になります。

Goal forall P Q : Prop, P -> Q -> P /\ Q.
Proof.
  intros. (* P : Prop, Q : Prop, H : P, H0 : Q *)
  apply conj.
  - (* P の証明 *)
    assumption.
  - (* Q の証明 *)
    assumption.
Qed.

apply conjと同等のことを行うタクティックとして、splitというものが用意されています。

Goal forall P Q : Prop, P -> Q -> P /\ Q.
Proof.
  intros. (* P : Prop, Q : Prop, H : P, H0 : Q *)
  split.
  - assumption.
  - assumption.
Qed.

A /\ B から A, Bを導く

A /\ Bはただのデータ構造なので、destructすればAとBを取り出すことができます。

Goal forall P Q : Prop, P /\ Q -> P.
Proof.
  intros P Q H. (* H : P /\ Q *)
  destruct H. (* H : P, H0 : Q *)
  assumption.
Qed.

Goal forall P Q : Prop, P /\ Q -> Q.
Proof.
  intros P Q H. (* H : P /\ Q *)
  destruct H. (* H : P, H0 : Q *)
  assumption.
Qed.

A, Bから A \/ Bを導く

andと同様に、orもコンストラクタor_introl, or_introrを用いれば導くことができます。

Goal forall P Q : Prop, P -> P \/ Q.
Proof.
  intros P Q H. (* H : P *)
  apply or_introl.
  - (* P の証明 *)
    assumption.
Qed.

Goal forall P Q : Prop, Q -> P \/ Q.
Proof.
  intros P Q H.
  apply or_intror.
  assumption.
Qed.

また、apply or_introl, apply or_introrと同等のことを行うタクティックとして、left, rightが用意されています。

Goal forall P Q : Prop, P -> P \/ Q.
Proof.
  intros.
  left.
  assumption.
Qed.

Goal forall P Q : Prop, Q -> P \/ Q.
Proof.
  intros.
  right.
  assumption.
Qed.

P \/ QからPが成立する場合とQが成立する場合について場合分けを行う

こちらもandと同様に、destructを用いることで場合分けが行えます。

Goal forall P Q R: Prop,
       P \/ Q -> (P -> R) -> (Q -> R) -> R.
Proof.
  intros. (* H : P \/ Q, H0 : P -> R, H1 : Q -> R *)
  destruct H.
  - (* P が成り立つ場合。*)
    (* H : P *)
    apply H0 in H. (* H : R *)
    assumption.
  - (* Q が成り立つ場合 *)
    (* H : Q *)
    apply H1 in H. (* H : R *)
    assumption.
Qed.

ちなみに、and, orどころかCoqの任意の命題はただのデータ型なので、上の定理は次のような「証明」を行うこともできます。

Definition hoge (P Q R : Prop) :
  P \/ Q -> (P -> R) -> (Q -> R) -> R :=
  fun PorQ PthenR QthenR =>
    match PorQ with
      | or_introl p => PthenR p
      | or_intror q => QthenR q
    end.

Check hoge.
(*
 * hoge
 *     : forall P Q R : Prop, P \/ Q -> (P -> R) -> (Q -> R) -> R
 *)