The Coq mailing list

[Greg Morrisett <morrisett AT gmail.com>]

Personally, I prefer to write a step function (as opposed to inductive definition) precisely because I can use it for testing.  Even if you have a non-deterministic language, you can usually model this as a function from terms to finite sets of terms.  

There are other advantages:  For instance, pattern matching in a function tells you if you've forgotten a case for a term, whereas it's all too easy to leave out a case in an inductive definition.  That is, you get input coverage this way.  Also, when you truly have a (partial) function, you have to re-establish this fact when you use an inductive definition, but it falls out for free when you define the function.    

Of course, if it's too painful to use the step function for reasoning directly, you can relate it to an inductive definition.  But I rarely find that I need to do that, once I've defined the right set of tactics.  

-Greg

On Fri, Sep 30, 2016 at 5:51 AM, Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de> wrote:

Never mind. I just found out that the "Software Foundations" contains
a section on just this problem. Sorry for the noise on the mailing list.


Am 30/09/16 um 09:39 schrieb Klaus Ostermann:

> I have formalized a small programming language in the style proposed by
> the "Software Foundations" book.
>
> I have defined an inductive type "tm" of Terms and
> an inductive type
>
> Inductive step : tm -> tm -> Prop
>
> to formalize the small-step reduction semantics of the language:
>
> I'd like to test the definitions with some examples. Let's say I have an
> example term t1. I want to find the term t2 such that "step t1 t2" holds.
>
> What is the best way to formalize such tests? Should one use an
> existential type, like
>
> exists t2, step t1 t2
>
> If so, how can one extract the witness t2 from such a theorem for
> inspection?
>
> Is there a way to automate the proof search such that the derivation does
> not have to be built by hand for every example?
>
> Klaus
>