Set Implicit
Arguments.
Definition
inhabited (A:Type) := exists a:A, True.
Parameter
epsilon : forall (A:Type), inhabited A -> (A->Prop) -> A.
Definition
iota (A:Type)(inh : inhabited A)(P: A-> Prop) :=
epsilon inh (fun x => P x /\ forall y, P y -> x = y).
Inductive
defined (A:Type)(P:A->Prop) : A -> Prop :=
defined_intro : forall inh , (exists a, P a) ->
(forall a b, P a -> P b -> a = b) ->
defined P (iota inh P).
Section
AFC.
Variables
(A:Type)(R:A->A->Prop).
Hypothesis
H : forall x, exists y, R x y.
Remark
inhab : forall x, inhabited (sigT (R x)).
Proof
.
intro x; case (H x);intros.
exists (existT _ x0 H0).
trivial.
Qed
.
Let
pi1 := fun (x:A) (s:sigT (R x)) => match s with (existT w _) => w end.
Let
phi := (fun x => epsilon (inhab x) (fun (s:(sigT (R x))) => R x (pi1 s))).
Lemma
afc : exists f, forall x, R x (f x).
Proof
.
exists (fun x => match (phi x) with (existT z _) => z end).
intro;case (phi x);auto.
Qed
.
End
AFC.
Definition
epsilonax (A:Type) (inh:inhabited A):=
forall (P : A -> Prop),
(exists a, P a) ->
P (epsilon inh P).
Definition
iotax (A:Type) (inh:inhabited A):=
forall (P : A -> Prop),
(exists a, P a) ->
(forall a b, P a -> P b -> a = b) ->
P (iota inh P).
Theorem
epsilon_ind :
forall (A:Type)(i:inhabited A)(HH:epsilonax i)(P:A->Prop)
(Q:A->Prop), (exists a:A, P a)->
(forall a : A, P a -> Q a) ->
(Q (epsilon i P)).
Proof
.
intros A i H P Q exP P_Q.
apply P_Q.
apply H; assumption.
Qed
.
Theorem
epsilon_iota : forall (A:Type)(inh: inhabited A),
epsilonax inh -> iotax inh.
Proof
.
red; intros A inh eax P exP unicityP.
unfold iota;apply epsilon_ind; auto.
case exP; intros a Ha;exists a;auto.
tauto.
Qed
.
Ltac
iota_elim_aux :=
match goal with [ |- (?P (iota (A:=?X) ?inh ?Q))] =>
let HH := fresh "Iota" in
(assert (HH:iotax inh);[auto|generalize (iota inh Q) (HH Q)])
end.
Ltac
iota_elim := iota_elim_aux ||
match goal with
[ |- (?P (?k ?arg))] =>
(let v := eval cbv zeta beta delta [k] in (k arg) in
(match v with (iota ?inh ?d) => change (P v); iota_elim_aux end))
| [ |- (?P ?k)] =>
(let v := eval cbv zeta beta delta [k] in k in
(match v with (iota ?inh ?d) => change (P v); iota_elim_aux end))
end.
Theorem
iota_ind :
forall (A:Type)(i:inhabited A)(HH:iotax i)(P:A->Prop)
(Q:A->Prop), (exists a:A, P a)->
(forall a a':A, P a -> P a' -> a=a') ->
(forall a : A, P a -> Q a) ->
(Q (iota i P)).
Proof
.
intros.
apply H1.
apply HH;auto.
Qed
.
Ltac
epsilon_elim_aux :=
match goal with [ |- (?P (epsilon (A:=?X) ?inh ?Q))] =>
let HH := fresh "Epsilon" in
(assert (HH:epsilonax inh);[auto|generalize (epsilon inh Q) (HH Q)])
end.
Ltac
epsilon_elim := epsilon_elim_aux ||
match goal with [ |- (?P (?k ?d))] =>
(let v := eval cbv zeta beta delta [k] in (k d) in
(match v with (epsilon ?inh ?d) => change (P v); epsilon_elim_aux end))
| [ |- (?P ?k)] =>
(let v := eval cbv zeta beta delta [k] in k in
(match v with (epsilon ?inh ?d) => change (P v); epsilon_elim_aux end))
end.
Section
A_fixed.
Variable
A : Type.
Hypothesis
inh : inhabited A.
Hint
Unfold iotax epsilonax.
Record
def (pred: A -> Prop): Type := {
def_iotax : iotax inh;
def_ex : exists d, pred d;
def_unic : forall d d', pred d ->
pred d' ->
d = d'
}.
Record
choice(pred : A-> Prop) : Type := {
choice_ax : epsilonax inh;
choice_ex : exists d, pred d
}.
Definition
the (pred : A->Prop)(d:def pred) :=
iota inh pred.
Definition
some (pred : A->Prop)(c : choice pred) :=
epsilon inh pred.
Theorem
the_ok : forall (pred:A->Prop)(d:def pred), pred (the d).
Proof
.
destruct d;simpl.
unfold the;simpl.
auto.
apply def_iotax0; auto.
Qed
.
Theorem
the_rw : forall (pred:A->Prop)(d:def pred) a, pred a -> a = the d.
Proof
.
intros p d;case d.
simpl;intros.
unfold the;simpl.
apply def_unic0.
auto.
apply def_iotax0.
auto.
auto.
Qed
.
Theorem
some_ok : forall (pred:A->Prop)(c:choice pred), pred (some c).
Proof
.
destruct c as [ax exP];simpl.
unfold some;simpl; auto.
apply ax;auto.
Qed
.
End
A_fixed.
tactics for using definitions |
Ltac
the_elim_aux :=
match goal with [ |- (?P (the ?d))] =>
generalize (the d) (the_ok d); simpl
end.
Ltac
the_elim := the_elim_aux ||
match goal with [ |- (?P ?k)] =>
(let v := eval cbv beta zeta delta [k] in k in
(match v with (the ?d) => change (P v); the_elim_aux end))
end.
Ltac
def_tac := apply Build_def .
Ltac
define inh P :=
assert (d : def inh P);[ def_tac | exact (the d)];auto.
Ltac
some_elim_aux :=
match goal with [ |- (?P (some ?d))] =>
generalize (some d) (some_ok d); simpl
end.
Ltac
some_elim := some_elim_aux ||
match goal with [ |- (?P ?k)] =>
(let v := eval cbv beta zeta delta [k] in k in
(match v with (some ?d) => change (P v); some_elim_aux end))
end.
Ltac
choice_tac := apply Build_choice .
Ltac
choose inh P :=
assert (d : choice inh P);[ choice_tac| exact (some d)];auto.
Section
AB_fixed.
Variables
A B: Type.
Hint
Unfold iotax.
Record
choice_defun (DA: A -> Prop)(R : A -> B -> Prop) : Type := {
choice_defun_inh : inhabited B;
choice_defun_epsax : epsilonax choice_defun_inh;
choice_defun_ex : forall d, DA d -> exists d', R d d'}.
Record
defun (DA: A -> Prop)(R : A -> B -> Prop) : Type := {
fun_inh : inhabited B;
fun_iotax : iotax fun_inh;
fun_ex : forall d, DA d -> exists d', R d d';
fun_u : forall d d' d'', DA d -> R d d' -> R d d'' -> d' = d''}.
Definition
iota_fun (inhB : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
(iota inhB (fun (b:B) => DA a /\ R a b)).
Definition
choice_fun (inhB : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
(epsilon inhB (fun (b:B) => DA a /\ R a b)).
Lemma
choice_fun_ok : forall inhB : inhabited B,
epsilonax inhB ->
forall (DA : A->Prop)(R:A->B->Prop)(a:A),
(exists d : B, R a d) ->
DA a -> R a (choice_fun inhB DA R a).
Proof
.
intros.
unfold choice_fun.
pattern (epsilon inhB (fun b : B => DA a /\ R a b)).
epsilon_elim.
intros.
case H2;intuition.
case H0;intros.
exists x;auto.
Qed
.
Lemma
iota_fun_ok : forall inhB : inhabited B,
iotax inhB ->
forall (DA : A->Prop)(R:A->B->Prop)(a:A),
(exists d : B, R a d) ->
(forall d d', R a d -> R a d' -> d = d') ->
DA a -> R a (iota_fun inhB DA R a).
Proof
.
intros.
unfold iota_fun.
pattern (iota inhB (fun b : B => DA a /\ R a b)).
iota_elim.
intros.
case H3;intuition.
case H0;intros.
exists x;auto.
Qed
.
Definition
make_defun (inhB : inhabited B)(iotaB : iotax inhB)
(P:A->Prop)
(R:A -> B -> Prop)
(e : forall d, P d -> exists d',
R d d')
(u: forall d d' d'',
P d -> R d d' -> R d d'' -> d' = d'') : defun P R.
intros.
exact (Build_defun P R iotaB e u).
Defined
.
Definition
make_choice_defun (inhB : inhabited B)(eB : epsilonax inhB)
(P:A->Prop)
(R:A -> B -> Prop)
(e : forall d, P d -> exists d',
R d d')
: choice_defun P R.
intros.
exact (Build_choice_defun P R eB e).
Defined
.
Definition
some_fun (P: A-> Prop)(R:A->B->Prop)
(d:choice_defun P R) := choice_fun (choice_defun_inh d) P R.
Definition
the_fun (P: A-> Prop)(R:A->B->Prop)
(d:defun P R) := iota_fun (fun_inh d) P R.
Theorem
choice_defun_ok : forall (P: A-> Prop)(R:A->B->Prop)
(d:choice_defun P R) (x:A), P x -> R x (some_fun d x).
Proof
.
intros P R d; case d.
intros.
unfold some_fun.
unfold choice_fun.
simpl.
pattern (epsilon choice_defun_inh0 (fun b : B => P x /\ R x b)).
epsilon_elim.
intros.
auto.
case H0.
case (choice_defun_ex0 x);intros.
auto.
exists x0;auto.
auto.
Qed
.
Theorem
defun_ok : forall (P: A-> Prop)(R:A->B->Prop)
(d:defun P R) (x:A), P x -> R x (the_fun d x).
Proof
.
intros P R d; case d.
intros.
unfold the_fun.
unfold iota_fun.
simpl.
pattern (iota fun_inh0 (fun b : B => P x /\ R x b)).
iota_elim.
intros.
auto.
case H0.
case (fun_ex0 x);intros.
auto.
exists x0;auto.
intuition.
eauto.
auto.
Qed
.
End
AB_fixed.
Ltac
choice_defun_elim_aux :=
match goal with [ |- (?P (some_fun ?d ?t)) ] =>
(generalize (some_fun d t) (choice_defun_ok d t);
simpl ;
let H := fresh "H'" in
let P := fresh in
let U := fresh "y" in
( intro U ;
match goal with [ |- (?A -> ?B) -> ?C ] =>
(assert (H : A);[try auto | intro P; generalize (P H)]) end)
)
end.
Ltac
defun_elim_aux :=
match goal with [ |- (?P (the_fun ?d ?t)) ] =>
(generalize (the_fun d t) (defun_ok d t);
simpl ;
let H := fresh "H'" in
let P := fresh in
let U := fresh "y" in
( intro U ;
match goal with [ |- (?A -> ?B) -> ?C ] =>
(assert (H : A);[try auto | intro P; generalize (P H)]) end)
)
end.
Ltac
defun_elim :=
defun_elim_aux ||
(match goal with [ |- (?P (?f ?t)) ] =>
(let g := eval cbv beta zeta delta [f ] in f in
(match g with (the_fun ?d) =>
change (P (g t)) ; defun_elim_aux end)) end).
Ltac
choice_defun_elim :=
choice_defun_elim_aux ||
(match goal with [ |- (?P (?f ?t)) ] =>
(let g := eval cbv beta zeta delta [f ] in f in
(match g with (some_fun ?d) =>
change (P (g t)) ; choice_defun_elim_aux end)) end).
Ltac
iota_fun_elim_aux :=
let IO := fresh "Iota" in
match goal with
[ |- (?Q (iota_fun (B:= ?Y) ?I ?P ?R ?t)) ] =>
(assert (IO: iotax I);[auto
| generalize (iota_fun I P R t) (iota_fun_ok IO P R t);
simpl ;
let H := fresh "H'" in
let P := fresh in
let U := fresh "y" in
let H0 := fresh "H" in
let H1 := fresh "H" in
let H2 := fresh "H" in
let H3 := fresh "H" in
(intro U; match goal with [ |- (?A -> ?B -> ?C -> ?D) -> ?G]
=> intro H0; assert (H:C);[auto |
assert (H1:A);[auto |
assert (H2 : B);[auto |
assert (H3:D);[auto|idtac]]]] end)]) end.
Ltac
iota_fun_elim :=
iota_fun_elim_aux ||
(match goal with [ |- (?Q (?f ?t)) ] =>
(let g := eval cbv beta zeta delta [f ] in f in
(match g with (iota_fun ?I ?P ?R ) =>
change (Q (g t)) ; iota_fun_elim_aux end)) end).
Ltac
iota_e := the_elim || defun_elim || iota_elim || iota_fun_elim.
Ltac
epsilon_e := some_elim || epsilon_elim || choice_defun_elim.
Ltac
fun_define inh P R :=
assert (d : defun P R);[(apply make_defun with inh
;auto)|
exact (the_fun d)].
Hint
Resolve epsilon_iota.