The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Hi,

I am looking for a way to express oracles; in other words, information
that come from outside a lambda-term. See the toy example below:

        Definition cbrt_aux x y :=
          let y' := Zsucc y in
          if andb (Zle_bool (y * y * y) x) (Zlt_bool x (y' * y' * y'))
          then Some y else None.
        
        Notation cbrt := (fun x => cbrt_aux x _).
        
        Definition test := cbrt 20%Z.

This defines a function cbrt that returns the integer cube root of its
argument, if prepended by "Some". Its proof of correctness (not shown
here) is trivial, since it is by definition.

Obviously and unfortunately, Coq will complain that it is not able to
infer the placeholder (the actual cube root) in the definition of
"test". The placeholder can be filled manually though:

        Definition test : option Z.
        refine (cbrt 20%Z).
        exact 2%Z. (* <-- here *)
        Defined.

What I would like is for Coq to fill the placeholder automatically, for
instance by calling a tactic. To clarify, the following would be fine to
me:

        fun x => cbrt_aux x ltac:(magic_cbrt x).

Coq would consider the second parameter as "_", but if it needs its
value, it would call the tactic (which could possible call an external
program with the XML mechanism) and then stores the result in the
lambda-term.

Is it possible to achieve this trick with the existing system or do I
need to modify Coq?

Best regards,

Guillaume