The Coq mailing list

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

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 “nomeata” Breitner
  
mail AT joachim-breitner.de
  https://www.joachim-breitner.de/

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