The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Right, epsilon had that specification thing about it.
It's still equivalent, see (kinda dirty but still works) proof in 
attached file.

Gaëtan Gilbert

On 08/12/2017 16:50, Joachim Breitner wrote:
> Dear Gaëtan,
>
> please allow me to get back to this.
>
> Am Mittwoch, den 06.12.2017, 21:56 +0100 schrieb Gaëtan Gilbert:
> > It's equivalent to epsilon.
> >
> > Let A : Type. Consider the function
> >
> >     λ x : A + bool => match x with inl a => inl a | inr b => inr (not b)
> >
> > It has a fixed point if and only if A is inhabited, but A + bool is
> > always inhabited (eg by inl true).
> >
> > In the attached file I use this to prove epsilon from your axioms.
>
> in your file you define
>
>      Lemma epsilon A (H : inhabited A) : A.
>
> but that is not (as I first thought) the epsilon from
> Coq.Logic.ClassicalEpsilon or Coq.Logic.Epsilon, which is
>
>       Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
>
>
> I see that your [epsilon] allows me to get a value out of an
> [inhabited A], which is usually not allowed, but what are the
> consequences of that? How does it related to the full Hilbert’s axiom?
>
>
> Thanks,
> Joachim
Require Import ChoiceFacts.
Require Import ClassicalFacts.

Axiom deferredFix : forall {a}, a -> (a -> a) -> a.

Axiom deferredFix_eq : forall {a} d (f : a -> a),
    (exists x, f x = x) ->
    deferredFix d f = f (deferredFix d f).

Definition pseudoFix A (x : sum A bool) : sum A bool
  := match x with
     | inl a => inl a
     | inr true => inr false
     | inr false => inr true
     end.

Lemma pseudoFix_pr A :
  match deferredFix (inr true) (pseudoFix A) with
  | inl _ => A
  | inr _ => A -> False
  end.
Proof.
  pose proof (deferredFix_eq (inr true) (pseudoFix A)) as E.
  destruct (deferredFix _ _) as [a|na].
  - exact a.
  - intros a.
    pose proof (E (ex_intro _ (inl a) eq_refl)) as E'.
    clear E;destruct na;discriminate.
Qed.

Lemma classic A : A + (A->False).
Proof.
  pose proof (pseudoFix_pr A). destruct (deferredFix _ _);auto.
Qed.

Lemma drink : SmallDrinker'sParadox.
Proof.
  hnf. intros A P [x];revert x.
  apply excluded_middle_independence_general_premises.
  red. clear A P.
  intros A B.
  destruct (classic A) as [a|na];auto.
  right;intros x;destruct (na x).
Qed.

Lemma epsilon : EpsilonStatement.
Proof.
  apply constructive_indefinite_description_and_small_drinker_imp_epsilon.
  - exact drink.
  - intros A P x.
    set (T := _).
    destruct (classic T) as [t|nt];[exact t|unfold T in *;clear T].
    apply False_rect;destruct x as [x px];apply nt;auto;exists x;trivial.
Qed.
Print Assumptions epsilon.
(* Fetching opaque proofs from disk for Coq.Logic.ChoiceFacts
Fetching opaque proofs from disk for Coq.Logic.ClassicalFacts

Axioms:
deferredFix_eq : forall (a : Type) (d : a) (f : a -> a),
                 (exists x : a, f x = x) -> deferredFix d f = f (deferredFix d f)
deferredFix : forall a : Type, a -> (a -> a) -> a
*)