The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Hello,

This is can't be done without heavy boilerplate at the time, as far as 
I'm aware. The only thing I can come up with is changing the Program 
Obligation Tactic so that it tries your oracle as well when you need it.

However, you are not the first (and probably not the last) to come up 
with such an idea. Future evolutions of the system might include this 
possibility (it is not clear to me whether it is possible to do in a 
reasonable amount of code in the current architecture, it could create 
some dependency mayhem, but on the architecture I'm trying to get done 
currently it should be doable. I think. I hope.).

I suggest you submit a formal feature wish to the bug tracking system.




Arnaud

Guillaume Melquiond a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>