coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Trying examples in formalized programming languages

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Trying examples in formalized programming languages
Date: Fri, 30 Sep 2016 09:39:24 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx03.uni-tuebingen.de
Ironport-phdr: 9a23:X1okCBXnCUHlX77dmc4sdvBhlUvV8LGtZVwlr6E/grcLSJyIuqrYZhCAt8tkgFKBZ4jH8fUM07OQ6PG6HzZYqs/Z6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLHovceLKFwQ3nKUWvBbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4/VmwLiVJvGBTI9hTzWJG55ij+v/dmni6BIcDsSLkyXxy/6aYuVALlgiYBODM/tm3a3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

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

[Coq-Club] Trying examples in formalized programming languages, Klaus Ostermann, 09/30/2016
- Re: [Coq-Club] Trying examples in formalized programming languages, Klaus Ostermann, 09/30/2016
  - Re: [Coq-Club] Trying examples in formalized programming languages, Greg Morrisett, 09/30/2016