The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi,

thanks! That settles it quite conclusively :-)


JFTR, switching from

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

to 

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

does not make a difference.

Thanks,
Joachim


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.
> 
> Gaëtan Gilbert
> 
> On 06/12/2017 19:21, Joachim Breitner wrote:
> > Hi list,
> > 
> > I would like to be able to define recursive function and defer the
> > termination proof to later; this is especially interesting in the
> > context of generated Coq code with hs-to-coq[1].
> > 
> > 
> > What I currently use is
> >    
> >      Axiom unsafeFix : forall {a}, (a -> a) -> a.
> > 
> > to define the recursive function, and then
> > 
> >      Axiom unsafeFix_eq : forall {a} (f : a -> a),
> >         unsafeFix f = f (unsafeFix f).
> > 
> > and to some extent and pragmatically speaking, this is not too bad if I
> > am disciplined in the use of these axioms[2].
> > 
> > 
> > But it is still unsatisfying, and if possible I’d like to avoid such
> > dangerous axioms. So I am wondering about these:
> > 
> >      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).
> > 
> > 
> > I believe these are consistent with basic Coq, because I can implement
> > them using the Hilbert Choice operator provided in the Coq standard
> > library:
> > 
> >      Require Import Coq.Logic.ClassicalEpsilon.
> > 
> >      Definition deferredFix : forall {a}, a -> (a -> a) -> a :=
> >        fun {a} def f => epsilon (inhabits def) (fun x => f x = x).
> > 
> >      Definition deferredFix_eq : forall {a} d (f : a -> a),
> >        (exists x, f x = x) ->
> >        deferredFix d f = f (deferredFix d f) :=
> >        fun a d f H =>
> >              eq_sym (epsilon_spec (inhabits d) (fun x => f x = x) H).
> > 
> > 
> > But are they as strong as Hilbert’s epsilon, or are they weaker? How
> > weak are they?
> > 
> > 
> > Regards,
> > Joachim
> > 
> > 
> > [1] https://arxiv.org/abs/1711.09286
> > [2] https://www.joachim-breitner.de/blog/733-Existence_and_Termination
> > 
> > 
-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part