coq의 and와 or를 포함한 명제

지금까지의 보도

전번: https://zenn.dev/emma_e_evans/articles/de3c743845c2cf2dd42d
마지막: https://zenn.dev/emma_e_evans/articles/3ac81ac25d3a650618a7

and가 포함된 명제 증명

and는 coq에서/(빗장과 반빗장) 을 쓴다.
and가 포함된다고 가정한 경우와 목표가 and를 포함한다고 가정한 경우를 분리해서 봅시다.

가설에 and가 포함된 경우

명제 "forall(AB:Prop), A/\B->B"를 증명할 때,

Example prop3: forall (A B:Prop), A /\ B -> B.
Proof.
intros.
apply H.
Qed.

끝.간단하네.

하면, 만약, 만약...

명제 "forall(AB:Prop), A->B->A/\B.를 증명하려면,

Example prop4: forall (A B:Prop), A -> B -> A /\ B.
Proof.
intros.
split.
apply H.
apply H0.
Qed.

.여기서 split은 목표 A/\B를 A와 B로 나누어 증명하는 시스템이다.

or를 포함하는 명제 증명

orcoq로 쓰기/.이쪽도 같은 상황에서 분리해서 봅시다.

또는 가정에 포함될 때

명제 "forall(A:Prop), A/B->(~A)->B를 증명할 때,

Example prop5: forall (A B:Prop), A \/ B -> (~ A) -> B.
Proof.
intros. (* A \/ B と ~ A を仮定に追加して，Bを証明する *)
destruct H. (* A \/ B をAが真のときとBが真のときとで場合分け *)
(* Aが真のとき *)
contradiction. (* Aと~Aの2つの仮定が矛盾しているので何でも導ける*)
(* Bが真のとき *)
apply H. (* 自明 *)
Qed.

.이렇게 가설을 분류할 때destruct 정책을 사용합니다.참고로 Inductive에 정의된 것에 대해destruct를 적용하면 구성자의 상황에 따라 분리된다.

골문에 포함될 때

명제 "forall(AB:Prop), A->A/B."를 증명할 때,

Example prop6: forall (A B:Prop), A -> A \/ B.
Proof.
intros. (* 仮定にAを追加して，A\/Bを証明する *)
left. (* A \/ Bを証明する代わりに左側のAだけに絞って証明する *)
apply H. (* 仮定AをゴールAに適用して終わり *)
Qed.

.댓글에도 A/B라는 목표에 대해left,right Takus로 목표를 잠글 수 있다고 적혀 있다.