Library hilbert.Epsilon
Require Import Classical.
Require Import ChoiceFacts.
Require Export ClassicalEpsilon.
Set Implicit Arguments.
Lemma ex_unic_introduction :
forall (A:Type)(P:A->Prop),
(ex P ) ->
(forall a b, P a -> P b -> a = b)->
ex (unique P).
Proof.
intros.
case (unique_existence P).
destruct 1.
split;auto.
case H;intros x Hx.
exists x;auto.
case H1.
exists x.
auto.
Qed.
Ltac ex_unic_intro :=
match goal with [ |- ex (unique ?P) ] =>
apply ex_unic_introduction end.
Theorem epsilon_ind :
forall (A:Type)(a: A)(P:A->Prop)
(Q:A->Prop), (ex P)->
(forall a : A, P a -> Q a) ->
Q (epsilon a P).
Proof.
intros A a P Q exP P_Q.
apply P_Q.
apply epsilon_spec.
case exP ;intros x H.
exists x;assumption.
Qed.
Theorem epsilon_equiv : forall (A:Type)(a: A)(P:A->Prop),
(ex P)<-> P (epsilon a P).
Proof.
split.
intros; apply epsilon_ind; auto.
exists (epsilon a P); auto.
Qed.
Definition tau (A:Type)(a:A)(P:A->Prop) :=
epsilon a (fun y => ~ (P y)).
Lemma forall_def : (forall P, P \/ ~ P) ->
forall (A:Type)(a:A)(P:A->Prop),
(forall y, P y) <-> P (tau a P).
Proof.
intros class A a P; split.
auto.
intros H y .
case (class (P y));auto.
intro Hy.
revert H.
pattern (tau a P).
unfold tau;apply epsilon_ind;auto.
exists y;auto.
tauto.
Qed.
Definition iota (A:Type)(a : A)(P: A-> Prop) :=
epsilon a (fun x => P x /\ forall y, P y -> x = y).
Lemma iota_e : forall (A:Type) (a: A) (P : A -> Prop),
(exists x:A, P x /\
forall b, P b -> x = b) ->
P (iota a P).
Proof.
intros A a P H.
unfold iota.
apply epsilon_ind.
auto.
case H.
intros.
case H1;auto.
Qed.
Theorem iota_ind :
forall (A:Type)(a: A)(P:A->Prop)
(Q:A->Prop), (exists b:A, P b /\
(forall c:A, P c -> b = c)) ->
(forall b : A, P b -> Q b) ->
(Q (iota a P)).
Proof.
intros.
apply H0.
apply iota_e;auto.
Qed.
Ltac epsilon_elim_aux :=
match goal with [ |- (?P (epsilon (A:=?X) ?a ?Q))] =>
apply epsilon_ind; auto
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 ?w ?d) => change (P v); epsilon_elim_aux end))
| [ |- (?P (?k ?arg ?arg1))] =>
(let v := eval cbv zeta beta delta [k] in (k arg arg1) in
(match v with (epsilon ?w ?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 ?w ?d) => change (P v); epsilon_elim_aux end))
end.
Ltac iota_elim_aux :=
match goal with [ |- (?P (iota (A:=?X) ?i ?Q))] =>
apply iota_ind; auto
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 ?w ?d) => change (P v); iota_elim_aux end))
| [ |- (?P (?k ?arg ?arg1))] =>
(let v := eval cbv zeta beta delta [k] in (k arg arg1) in
(match v with (iota ?w ?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 ?w ?d) => change (P v); iota_elim_aux end))
end.
Lemma iota_parameter_rw : forall (A:Type)(a b:A)(P:A-> Prop),
(exists x :A, P x /\ (forall y : A, P y -> x = y)) ->
iota a P = iota b P.
Proof.
intros.
pattern (iota a P).
iota_elim.
pattern (iota b P).
iota_elim.
intros b0 H0 b1 H1.
revert H;intros (x,(Hx,H')).
transitivity x;auto.
symmetry;auto.
Qed.
Structures for descriptions and specifications
The operators "some" and "the" correspond to epsilon and iota
applied to the proof they expect
Definition some(A:Type)(a: A)(P:A->Prop)(pi:ex P)
: A
:= epsilon a P.
Implicit Arguments some [A P].
Definition the (A:Type)(a: A)(P:A->Prop)
(pi:ex (unique P))
: A
:= iota a P.
Implicit Arguments the [A P].
Lemma some_e : forall (A:Type)(a: A)(P:A->Prop)(pi:ex P),
P (some a pi).
Proof.
intros.
unfold some.
epsilon_elim.
Qed.
Implicit Arguments some_e [A P].
Theorem some_ind :forall (A:Type)(a: A)(P Q:A->Prop)(pi:ex P),
(forall a, P a -> Q a) -> Q (some a pi).
Proof.
intros.
apply H ;apply some_e.
Qed.
Theorem the_e : forall (A:Type)(a:A)(P:A->Prop)
(pi:ex (unique P)),
P (the a pi).
Proof.
unfold the.
intros.
iota_elim.
Qed.
Implicit Arguments the_e [A P].
Theorem the_ind : forall (A:Type)(a: A)(P Q:A->Prop)
(pi:ex (unique P)),
(forall b, P b -> Q b) -> Q (the a pi).
Proof.
intros A a P Q pi H;apply H;apply the_e.
Qed.
Implicit Arguments the_ind [A P].
Theorem the_rw : forall (A:Type)(a: A)(P:A->Prop)
(pi:ex (unique P)) b,
P b -> b= the a pi.
Proof.
intros A a P pi b Hb.
case pi; intros x (Px,Eqx).
unfold the.
pattern (iota a P).
iota_elim.
intros.
rewrite <- (Eqx b0).
symmetry.
auto.
auto.
Qed.
Implicit Arguments the_rw [A P].
Ltac the_elim_aux :=
match goal with [ |- (?Q (the ?w ?d))] =>
apply the_ind 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 ?w ?d) => change (P v); the_elim_aux end))
end.
Ltac some_elim_aux :=
match goal with [ |- (?P (some ?w ?d))] =>
generalize (some w d) (some_e w 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 ?w ?d) => change (P v); some_elim_aux end))
end.
Ltac hilbert_e := epsilon_elim || iota_elim || some_elim || the_elim.
Ltac he t n := pattern t at n; hilbert_e.
Tactic Notation "h_elim" constr(T) "at" integer(n) :=
pattern T at n; hilbert_e.
Tactic Notation "h_elim" constr(T) :=
pattern T ; hilbert_e.
Ltac some_i P :=
refine (some _ (P:=P) _).
Ltac the_i P :=
refine (the _ (P:=P) _).
Building partial functions
Section AB_fixed.
Variables A B: Type.
description of some partial function by a Domain and a binary relation
Definition choice_fun (b : B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
(epsilon b (fun (b':B) => DA a /\ R a b')).
Definition iota_fun (b : B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
(iota b (fun (b':B) => DA a /\ R a b')).
Lemma choice_fun_e : forall b : B,
forall (DA : A->Prop)(R:A->B->Prop)(a:A),
(exists d : B, R a d) ->
DA a -> R a (choice_fun b DA R a).
Proof.
intros.
unfold choice_fun.
pattern (epsilon b (fun b : B => DA a /\ R a b)).
epsilon_elim.
intros.
case H;intuition.
exists x;auto.
tauto.
Qed.
Lemma choice_fun_ind : forall b : B,
forall (P : A->Prop)(Q R:A->B->Prop)(a x:A),
(exists d : B, R a d) -> a = x ->
P a -> (forall b, P a -> R a b -> Q a b) ->
Q x (choice_fun b P R a).
Proof.
intros.
subst x.
apply H2.
auto. apply choice_fun_e;auto.
Qed.
a partial function equipped with a proof of its partial correctness
Definition the_fun (b : B)(DA : A->Prop)(R:A->B->Prop)
(pi : forall a, DA a -> ex (unique (R a))) (a:A):=
(iota b (fun (b:B) => DA a /\ R a b)).
same stuff but without unicity of the result
Definition some_fun (b : B)(DA : A->Prop)(R:A->B->Prop)
(pi : forall a, DA a -> exists b: B, R a b) (a:A):=
(epsilon b (fun (b:B) => DA a /\ R a b)).
Lemma iota_fun_e : forall b : B,
forall (DA : A->Prop)(R:A->B->Prop)(a:A),
(ex (unique (R a))) ->
DA a -> R a (iota_fun b DA R a).
Proof.
intros.
unfold iota_fun.
pattern (iota b (fun b' : B => DA a /\ R a b')).
iota_elim.
case H;intros.
case H1; exists x;try tauto.
split;auto.
destruct 1;auto.
tauto.
Qed.
Lemma iota_fun_ind : forall b : B,
forall (P : A->Prop)(Q R:A->B->Prop)(a x:A),
a = x -> (ex (unique (R a))) ->
P a -> (forall b, P a -> R a b -> Q a b) ->
Q x (iota_fun b P R a).
Proof.
intros.
subst x.
apply H2.
auto. apply iota_fun_e.
case H0;intros d (Hd,Hd').
exists d;auto.
auto.
red.
auto.
auto.
Qed.
Lemma iota_fun_rw : forall b: B,
forall (P : A->Prop)(R:A->B->Prop)(a:A)(b':B),
(ex (unique ( R a))) ->
P a ->
R a b' -> b'= (iota_fun b P R a).
Proof.
intros.
unfold iota_fun.
pattern (iota b (fun b0 : B => P a /\ R a b0)).
iota_elim.
exists b';repeat split;auto.
case H;intros d (Hd,Hd').
intuition.
transitivity d;auto.
symmetry;auto.
case H;intros d (Hd,Hd').
destruct 1;auto.
transitivity d;auto.
symmetry;auto.
Qed.
Theorem the_fun_e : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> ex (unique (R a))) (a:A),
P a -> R a (the_fun b P R pi a) .
Proof.
intros b P R pi a H.
unfold the_fun.
pattern (iota b (fun b0 : B => P a /\ R a b0)).
iota_elim.
case (pi a H).
intros x (Hx,H'x).
exists x.
split;auto.
destruct 1;auto.
tauto.
Qed.
Theorem some_fun_e : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> exists b0: B, R a b0) (a:A),
P a -> R a (some_fun b P R pi a) .
Proof.
intros b P R pi a H.
unfold some_fun.
pattern (epsilon b (fun b0 : B => P a /\ R a b0)).
epsilon_elim.
case (pi a H).
intros x Hx.
exists x.
split;auto.
destruct 1;auto.
Qed.
Theorem the_fun_rw : forall (b : B)(P: A-> Prop)(R:A->B->Prop)
(pi : forall a, P a -> ex (unique ( R a))) (a:A)(b0:B),
P a -> R a b0 -> b0= (the_fun b P R pi a) .
Proof.
intros b P R pi a b0 H H0.
unfold the_fun.
pattern (iota b (fun b1 : B => P a /\ R a b1)).
iota_elim.
exists b0.
repeat split;auto.
case (pi a H).
intros x (Hx,H'x) a' (Ha',Ha'').
transitivity x.
symmetry;auto.
auto.
destruct 1.
case (pi a H).
intros x (H3,H4).
transitivity x;auto.
symmetry;auto.
Qed.
Theorem the_fun_ind : forall (b : B)(P: A-> Prop)(Q R:A->B->Prop)
(pi : forall a, P a -> ex (unique (R a))) (a x:A),
P a -> a = x ->
(forall b0, P a -> R a b0 -> Q a b0) -> Q x (the_fun b P R pi a) .
intros.
subst x.
apply H1. auto. eapply the_fun_e.
auto.
Qed.
Theorem some_fun_ind : forall (b : B)(P: A-> Prop)(Q R:A->B->Prop)
(pi : forall a, P a -> exists b: B, R a b) (a x:A),
a = x -> P a -> (forall b0, P a -> R a b0 -> Q a b0) ->
Q x (some_fun b P R pi a) .
intros.
subst x.
apply H1. auto. eapply some_fun_e.
auto.
Qed.
End AB_fixed.
tactic for building a partial function
Opaque the_fun some_fun.
Ltac the_fun_i P R:=
refine (the_fun _ P R _).
Ltac some_fun_i P R:=
refine (some_fun _ P R _).
Ltac the_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (the_fun ?i ?P ?R ?d) => change (Q a (v t));
apply the_fun_ind ; auto end)) end.
Ltac some_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (some_fun ?i ?P ?R ?d) => change (Q a (v t));
apply some_fun_ind ; auto end)) end.
Ltac iota_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (iota_fun ?i ?P ?R ) => change (Q a (v t));
apply iota_fun_ind ; auto end)) end.
Ltac choice_fun_elim :=
match goal with [ |- (?Q ?a (?f ?t)) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (choice_fun ?i ?P ?R ) => change (Q a (v t));
apply choice_fun_ind ; auto end)) end.
Ltac pfun_e := choice_fun_elim || iota_fun_elim || some_fun_elim ||
the_fun_elim.
Ltac iota_fun_rewrite :=
match goal with [ |- (?f ?x = ?y) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (iota_fun ?i ?P ?R ) =>
change (v x = y);symmetry; apply iota_fun_rw; auto
end)) end.
Ltac the_fun_rewrite :=
match goal with [ |- (?f ?x = ?y) ] =>
(let v := eval cbv beta zeta delta [f] in f in
(match v with (the_fun ?i ?P ?R ?d ) =>
change (v x = y);symmetry; apply the_fun_rw; auto
end)) end.
Section definite_description.
Lemma dd'' : forall (A:Type)(B:A->Type)
(R:forall x:A, B x -> Prop),
(forall x: A, (B x)) ->
(sigT (fun f : forall x:A, B x =>
(forall x:A, (exists y:B x, R x y) -> R x (f x)))).
Proof.
intros A B R i.
exists (fun (x:A) => (epsilon (i x) (fun y => (R x y)))).
intros x [y ry].
apply (epsilon_spec). exists y; trivial.
Qed.
Lemma dd' : forall (A:Type) (B:A -> Type)
(R:forall x:A, B x -> Prop),
(forall x, (B x)) ->
(forall x:A, exists y : B x, R x y ) ->
sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
Proof.
intros.
case (dd'' B R X).
intros.
exists x.
intros;apply r.
auto.
Qed.
End definite_description.
Definition epsilon_extensionality :=
forall (A:Type)(a: A)(P Q:A->Prop),
(forall a, P a <-> Q a) ->
epsilon a P = epsilon a Q.
Definition restricted_epsilon_extensionality :=
forall (A:Type)(a: A)(P Q:A->Prop),
(forall a0, P a0 <-> Q a0) ->
ex P ->
epsilon a P = epsilon a Q.
Lemma or_to_sum : forall P Q : Prop, P \/ Q -> {P}+{Q}.
Proof.
intros P Q H.
pose (y := epsilon true (fun b => b=true /\ P \/ b=false /\ Q)).
case_eq y.
intro eg.
left.
generalize eg;pattern y; hilbert_e.
case H.
exists true;auto.
exists false;auto.
destruct 1.
tauto.
case H0;intros; subst a; discriminate.
intro eg;right.
generalize eg;pattern y; hilbert_e.
case H.
exists true;auto.
exists false;auto.
destruct 1.
intro; subst a.
case H0. discriminate 1.
tauto.
Qed.
Opaque epsilon.