🐓

# Coqで証明　順序を保つ写像

2020/10/04に公開

``````Set Implicit Arguments.
``````

``````Definition antisymmetric U(R:U->U->Prop):=
forall x y,R x y->R y x->x=y.
``````

``````Definition total U(R:U->U->Prop):=
forall x y,R x y\/R y x.
``````

``````Definition isotone A B(Ra:A->A->Prop)(Rb:B->B->Prop)(f:A->B):=
forall a1 a2,Ra a1 a2->Rb(f a1)(f a2).
``````

g o f = id

``````Definition cancel A B(f:A->B)(g:B->A):=
forall a,g(f(a))=a.
``````

``````Definition inv A B(f:A->B)(g:B->A):=
cancel f g/\cancel g f.
``````

``````Definition surjection A B(f:A->B):=
forall b,exists a,f a=b.
``````

g o f = id ならば　ｇは全射

``````Lemma L1 A B(f:A->B)(g:B->A):
cancel f g->surjection g.
Proof.
intro.
unfold surjection.
intro a.
unfold cancel in H.
specialize(H a).
exists(f a).
assumption.
Qed.
``````

``````Goal forall A B(Ra:A->A->Prop)(Rb:B->B->Prop)(f:A->B)(f':B->A),
total Ra->
antisymmetric Rb->
inv f f'->
isotone Ra Rb f->isotone Rb Ra f'.
Proof.
intros.
unfold isotone.
intros b1 b2 H3.
unfold inv in H1.
destruct H1 as [H1 H1'0].
assert(H4:surjection f).
- clear H3 b1 b2 H2 H1 H0 H Rb Ra.
eapply L1.
eassumption.
- clear H1'0.
assert(H4'0:=H4).
unfold surjection in H4,H4'0.
specialize(H4 b1).
specialize(H4'0 b2).
destruct H4 as [a1 H4].
destruct H4'0 as [a2 H4'0].
unfold total in H.
assert(H'0:=H).
specialize(H'0 a1 a2).
destruct H'0 as [H'0|H'0].
+ rewrite<-H4.
rewrite<-H4'0.
unfold cancel in H1.
rewrite H1,H1.
assumption.
+ clear H1.
unfold isotone in H2.
specialize(H2 a2 a1).
specialize(H2 H'0).
clear H'0.
rewrite H4 ,H4'0 in H2.
clear H4 H4'0.
unfold antisymmetric in H0.
specialize(H0 b1 b2).
specialize(H0 H3 H2).
rewrite H0.
specialize(H(f' b2)(f' b2)).
tauto.
Qed.
``````

ログインするとコメントできます