Coqで証明　順序を保つ写像

今回は順序関係に関する証明をしました。証明は自明な部分もあまり省略せずに書いてみました。今までより長めの証明になったので修正に対応しやすいようにバレットやイントロパターンによる命名などを使って書いてみました。初めて使ってみたので書き方は変かもしれないです。何か気になる点などあれば細かいことでもかまいませんのでコメントいただけるとありがたいです。

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.

全順序集合A、Bにおいて、ｆ:A->Bが順序を保てば、ｆ^-1:B->Aも順序を保つ

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.