Coq를 통해 함수 입증
이번에 Coq의 함수에 대해 몇 가지 증명을 진행하였다.편리한 전략으로 노동력과 재료를 줄이는 것을 증명하다.
3
Require Import Utf8.
Set Implicit Arguments.
함수의 상등역함수, 합성, 항등함수, 단사, 전사를 정의한다.3
Definition feq A B(f g:A->B):=
forall a,f a=g a.
Definition cancel A B(f:A->B)(g:B->A):=
forall a,g(f(a))=a.
Definition injection A B(f:A->B):=
forall a1 a2,f a1=f a2->a1=a2.
Definition surjection A B(f:A->B):=
forall b,exists a,f a=b.
Definition comp A B C(f:A->B)(g:B->C)(a:A):=g(f a).
Definition id {A}(a:A):=a.
증명 본문.
Goal forall A B(f:A->B),
feq f f.
Proof.
split.
Qed.
Goal forall A B(f g:A->B),
feq f g->feq g f.
Proof.
easy.
Qed.
Goal forall A B(f g h:A->B),
feq f g->feq g h->feq f h.
Proof.
congruence.
Qed.
Goal forall A B(f:A->B),
feq(fun a=>f a)f.
Proof.
split.
Qed.
Goal forall A B C D(f:A->B)(g:B->C)(h:C->D),
comp(comp f g)h=comp f(comp g h).
Proof.
split.
Qed.
Goal forall A B(f:A->B),
feq(comp f id)f.
Proof.
split.
Qed.
Goal forall A B(f:A->B),
feq(comp id f)f.
Proof.
split.
Qed.
Goal forall A,injection(id:A->A).
Proof.
easy.
Qed.
Goal forall A,surjection(id:A->A).
Proof.
intros.
intro.
exists b.
split.
Qed.
Goal forall A B(f:A->B)(g:B->A),
cancel f g<->forall a b,f a=b->g b=a.
Proof.
firstorder.
congruence.
Qed.
Goal forall A B(f:A->B)(g:B->A),
cancel f g<->feq(comp f g)id.
Proof.
easy.
Qed.
Goal forall A(a:A),id a=a.
Proof.
split.
Qed.
Goal forall A B(f h:A->B)(g:B->A),
cancel f g->
cancel g h->
feq f h.
Proof.
congruence.
Qed.
Goal forall A B C(f:A->B)(g:B->C),
injection f->
injection g->
injection(comp f g).
Proof.
firstorder.
Qed.
Goal forall A B C(f:A->B)(g:B->C),
surjection f->
surjection g->
surjection(comp f g).
Proof.
intros.
intro.
destruct(H0 b).
destruct(H x).
exists x0.
unfold comp.
congruence.
Qed.
Goal forall A B C(f:A->B)(g:B->C),
injection(comp f g)->injection f.
Proof.
unfold injection,comp.
intros.
apply H.
congruence.
Qed.
Goal forall A B C(f:A->B)(g:B->C),
surjection(comp f g)->surjection g.
Proof.
firstorder.
Qed.
Goal forall A B(f:A->B)(g:B->A),
cancel f g->
injection f.
Proof.
congruence.
Qed.
Goal forall A B(f:A->B)(g:B->A),
cancel f g->
surjection g.
Proof.
firstorder.
Qed.
Reference
이 문제에 관하여(Coq를 통해 함수 입증), 우리는 이곳에서 더 많은 자료를 발견하고 링크를 클릭하여 보았다 https://zenn.dev/sabataro/articles/3b1859bf87d62760c350텍스트를 자유롭게 공유하거나 복사할 수 있습니다.하지만 이 문서의 URL은 참조 URL로 남겨 두십시오.
우수한 개발자 콘텐츠 발견에 전념 (Collection and Share based on the CC Protocol.)