The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

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
>