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.