Library hilbert.PartialFun

Require Import ClassicalEpsilon.

Require Import Epsilon.

Require Import Ensembles.

Set Implicit Arguments.
Implicit Arguments In [U].

Inductive optionT (A:Type) : Type :=
  NoneT : optionT A
| SomeT : A -> optionT A.

Section f_fixed.

  Variables A B : Type.
domain
  Variable DA : Ensemble A.
codomain
  Variable DB : Ensemble B.

  Variable f : A -> B.

relational representation
  Variable Rf : A -> B -> Prop.

representation using option types
  Variable f_o : A -> optionT B.

equivalence between a function and a relation
  Definition fun_rel_same :=
    forall a b, In DA a -> (Rf a b <-> f a = b).

  Definition opt_rel_same :=
     forall a b, In DA a -> (Rf a b <-> f_o a = SomeT b).


  Definition rel_domain := forall a, In DA a -> exists b, Rf a b.
  Definition rel_codomain := forall a b, In DA a -> Rf a b -> In DB b.
  Definition rel_functional := forall a b b', In DA a ->
                              Rf a b -> Rf a b' -> b = b'.
  Definition rel_onto := forall b, In DB b -> exists a, In DA a /\ Rf a b.
  Definition rel_inj := forall a a' b, In DA a ->
                                       In DA a' ->
                                       Rf a b ->
                                       Rf a' b ->
                                       a = a'.

  Inductive rel_injection : Prop :=
   rel_inj_i : rel_domain ->
        rel_codomain ->
        rel_functional ->
        rel_inj ->
        rel_injection.

  Inductive rel_bijection : Prop :=
   rel_bij_i : rel_domain ->
        rel_codomain ->
        rel_functional ->
        rel_onto ->
        rel_inj ->
        rel_bijection.

Abstract properties of a function (using option types)
  Definition opt_domain := forall a, In DA a -> exists b, f_o a = SomeT b.

  Definition opt_codomain := forall a b, In DA a ->
                                         f_o a =
                                         SomeT b -> In DB b.

  Definition opt_onto := forall b, In DB b ->
                                   exists a, In DA a /\ f_o a = SomeT b.

  Definition opt_inj := forall a a' b, In DA a ->
                                       In DA a' ->
                                       f_o a = SomeT b ->
                                       f_o a' = SomeT b ->
                                       a = a'.

  Inductive opt_injection : Prop :=
   opt_inj_i : opt_domain -> opt_codomain ->
                            opt_inj -> opt_injection.

  Inductive opt_bijection : Prop :=
   opt_bij_i : opt_domain -> opt_codomain -> opt_onto ->
                            opt_inj -> opt_bijection.

Abstract properties of f: A->B (wrt. domain DA and codomain DB

  Definition fun_codomain := forall a, In DA a -> In DB (f a).
  Definition fun_onto := forall b, In DB b -> exists a, In DA a /\ f a = b.
  Definition fun_inj := forall a a' , In DA a -> In DA a' -> f a = f a' ->
                 a = a'.

  Definition image := fun b => exists a, In DA a /\ f a = b.

  Inductive fun_injection : Prop :=
   fun_inj_i : fun_codomain ->
                            fun_inj -> fun_injection.

  Inductive fun_bijection : Prop :=
   fun_bij_i : fun_codomain -> fun_onto ->
                            fun_inj -> fun_bijection.
Hint Unfold In.

  Lemma bijection_fun_rel : fun_rel_same -> fun_bijection -> rel_bijection.
  Proof.
   clear f_o.
    intro Sa; red in Sa.
  destruct 1;split.

    red.
  intros; exists (f a).
   case (Sa a (f a) H2).
  auto.
  red.
  intros.
 case (Sa a b H2).
 red in H.
 intros H4 _;generalize (H4 H3).
 intro; subst b;auto.
 red;intros.
 case (Sa a b H2);intros.
 case (Sa a b' H2);intros.
 intuition.
 subst b;auto.
 red;intros.
 red in H0.
 case (H0 _ H2).
 intros a (Ha,Ea).
 case (Sa a b Ha).
 intros.
 exists a;auto.
 red;intros.
 red in H1.
 generalize (H1 _ _ H2 H3).
 intro.
 apply H6.
 case (Sa a b H2);case (Sa a' b H3).
 intuition.
 subst b;auto.
Qed.

  Definition rel_inv := fun b a => In DA a /\ In DB b /\ Rf a b.

  Lemma bijection_rel_fun : fun_rel_same -> rel_bijection -> fun_bijection.
  Proof.
    intro Sa; red in Sa.
  clear f_o.
  destruct 1;split.

    red.
  red in H0.
 intros ;apply H0 with a; auto.
   case (Sa a (f a) H4).
  auto.
  red.
  intros.
  red in H2.
 case (H2 _ H4).
 intros a (Ha,Ra).
 exists a.
 case (Sa a b Ha).
 auto.
 red.
 red in H3.
 intros.
 apply H3 with (f a);auto.
 case (Sa a (f a) H4);auto.
 rewrite H6; case (Sa a' (f a') H5);auto.
Qed.


End f_fixed.

Lemma rel_inv_bij : forall (A B : Type)(DA : Ensemble A)
                                       (DB : Ensemble B)
                   (Rf : A -> B -> Prop),
                   (rel_bijection DA DB Rf) ->
                   (rel_bijection DB DA (rel_inv DA DB Rf)).
 destruct 1; split.
 red.
 intros b Hb. case (H2 b Hb).
 intros x (Inx,Rxb). exists x;red;auto.
 red.
 intros b a Inb Rba.
 case (H2 b Inb).
 intros x (Hx,Rx).
 replace a with x.
 auto.
 case Rba.
 intros Ha (Hb,Hab).

 apply ( H3 _ _ b Hx Ha Rx Hab).
 red;intros b a a';intros.
 red in H5; decompose [and] H5.
 red in H6; decompose [and] H6.
 clear H5 H6.
 apply (H3 a a' b);auto.
 red; intros a; intros.
 case (H a);auto.
 intros b Rab; exists b.
 split.
 apply H0 with a;auto.
 red;repeat split;auto.
 apply H0 with a.
 auto.
 auto.

 red;intros b b' a.
 intros.
 apply (H1 a); auto.
 case H6;auto.
 case H6;tauto.
 case H7;tauto.
Qed.




Conversion from a relational definition : A->B->Prop into a partial function of type A->B

 Section rel_to_fun.
 Variables ( A B : Type).
 Variable b : B.
 Variables (DA : Ensemble A)
           (Rf : A -> B -> Prop).

 Definition r2i := iota_fun b DA Rf.

 Hypothesis ff : (rel_functional DA Rf).
 Hypothesis fd : (rel_domain DA Rf).

 Lemma r2i_ok : fun_rel_same DA r2i Rf.
 Proof.
 unfold fun_rel_same.
 intros; pattern (r2i a).
 unfold r2i.
  split.
 intro;
 rewrite (iota_fun_rw b DA Rf a b0).
 auto.
 exists b0;split;auto.
 intros;eapply ff;eauto.
 auto.
 auto.

 intro.
 generalize H0.
 clear H0.

 pattern a, (iota_fun b DA Rf a).
eapply iota_fun_ind;auto.

 case (fd H);intros.
 exists x;split;auto.
 intros;eapply ff;eauto.
  destruct 3;auto.
Qed.

 Definition r2f : A -> B.
 refine (the_fun b DA Rf _).
 intros a Ha; case (fd Ha);intros x Hx.
 exists x;split;auto.
 intros;eapply ff;eauto.
 auto.
 Defined.

Lemma r2f_ok : fun_rel_same DA r2f Rf.
 Proof.
 unfold fun_rel_same.
 intros; pattern (r2f a).
 split.
 intros.
  unfold r2f.
 symmetry;eapply the_fun_rw.
 auto.
 auto.
 pattern a, (r2f a).
 pfun_e.
 destruct 3;auto.
Qed.

End rel_to_fun.

Ltac r2i_e :=
 (pfun_e ||
   (match goal with
   [ |- (?Q ?a (?f ?t)) ] =>
   (let g := eval cbv zeta beta delta [f r2i] in f in
       
     change (Q a (g t))) ; apply iota_fun_ind ; auto

| [ |- (?Q ?a (?f ?t1 ?t2)) ] =>
   (let g := eval cbv zeta beta delta [f r2i] in f in
       
     change (Q a (g t1 t2))) ; apply iota_fun_ind ;auto

end)).

A tactic for generating calls to r2f
Ltac fun_def D R :=
  match goal with [ |- ?A -> ?B] =>
          let Iota := fresh in
             let HF := fresh in
           let HD := fresh in
            (assert (b : B);[auto |
             (assert (Iota : iota b);[auto|
             (assert(HF:rel_functional D R);
               [idtac| assert(HD:rel_domain D R);[idtac|exact (r2f Iota HF HD)]])])])
  end.

Definition exist_1_R_a (A B:Type)(X:Ensemble A)(R: A-> B -> Prop)
                (H: rel_domain X R)
                (H': rel_functional X R) :
                forall a, In X a -> ex (unique (R a)).
Proof.
 intros.
 case (H a H0).
 intros x Hx;exists x;split;auto.
 intros;eapply H';eauto.
Qed.

Ltac r2f_e_aux :=
 match goal with
  | [|- (?P ?u (r2f (DA:=?X) (Rf:=?Y) ?I ?IFu ?ID ?t)) ]=>
   change (P u (the_fun I X Y (exist_1_R_a ID IFu) t)) ;
   apply the_fun_ind; auto
 end.

Ltac r2f_e :=
  r2f_e_aux ||
  (match goal with
  | [ |- (?P ?u (?f ?t)) ] =>
    (let g := eval cbv zeta beta delta [f] in f in
       r2f_e_aux)
  end).


Section inversion_of_bijection.
 Variables (A B : Type)
           (a : A)
           (DA : Ensemble A)
           (DB : Ensemble B)
           (f : A -> B).

 Let inv_spec := fun y x => In DA x /\ In DB y /\ f x = y.

 Definition inv_fun := r2i a DB inv_spec.

 Hypothesis f_b : fun_bijection DA DB f.

 Lemma inv_spec_ex : forall b, In DB b -> exists a, inv_spec b a.
 Proof.
   intros.
   case f_b.
   intros.
   case (H1 b H).
 intros x (Hx, fxb).
 unfold inv_spec.
 exists x;auto.
 Qed.

Lemma inv_spec_func : forall b, In DB b ->
                 forall a a', inv_spec b a -> inv_spec b a' -> a=a'.
Proof.
  intros.
  case f_b;intros.
  red in H4.
  apply H4.
  case H0;auto.
  case H1;auto.
  case H0;case H1;intros.
  transitivity b;intuition.
Qed.

Lemma inv_compose : fun_bijection DA DB f ->
                    forall x, DA x -> inv_fun (f x) = x.
Proof.
 intros.
 unfold inv_fun, r2i.
 pattern (f x), (iota_fun a DB inv_spec (f x)).
 apply iota_fun_ind;auto.
 case H.
 intros.
 unfold inv_spec.
 exists x.
 repeat split;auto.
 intros y (H4,(H5,H6)).
 apply H3;auto.
  case H;intros.
 apply H1;auto.
 unfold inv_spec.
 case H;intros.
 decompose [and] H5.
 apply H3;auto.
Qed.

Lemma inv_composeR : fun_bijection DA DB f ->
                    forall b, DB b -> f (inv_fun b) = b.
Proof.
 intros.
 case H;intros.
 unfold inv_fun,r2i.
 pattern b, (iota_fun a DB inv_spec b).
 apply iota_fun_ind;auto.
 case (H2 b H0);intros x (H',H5).
 exists x ; repeat split;auto.
 destruct 1.
 decompose [and] H6;subst b;auto.
 destruct 2.
 tauto.
Qed.

Lemma inv_fun_bij : fun_bijection DA DB f -> fun_bijection DB DA inv_fun.
 destruct 1; split.
 red.
 intros.
 case (H0 a0 H2); intros x (Hx,Hx').
 subst a0.
 rewrite inv_compose;auto.
 red.
 intros x Hx.
 exists (f x).
 split.
 apply H;auto.
 rewrite inv_compose;auto.
 red.
 intros b b' Hb Hb' Eq.
 rewrite <- (inv_composeR f_b Hb).
rewrite <- (inv_composeR f_b Hb').
 rewrite Eq;auto.
Qed.

End inversion_of_bijection.

Check inv_fun.