Mercurial > cpdt > repo

comparison src/ProgLang.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents fd6ec9b2dccb
children dac7a2705b00
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2011-2012, Adam Chlipala 1 (* Copyright (c) 2011-2012, 2015, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import FunctionalExtensionality List. 11 Require Import FunctionalExtensionality List.
12 12
13 Require Import CpdtTactics DepList. 13 Require Import Cpdt.CpdtTactics Cpdt.DepList.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *) 19 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
19 20
20 (** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions. I believe the pragmatic questions in this domain are far from settled and remain as important open research problems. However, in this chapter, I will demonstrate two underused encoding approaches. Note that I am not recommending either approach as a silver bullet! Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques. For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%{{http://www.cis.upenn.edu/~bcpierce/sf/}Software Foundations}%}% by Pierce et al. 21 (** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions. I believe the pragmatic questions in this domain are far from settled and remain as important open research problems. However, in this chapter, I will demonstrate two underused encoding approaches. Note that I am not recommending either approach as a silver bullet! Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques. For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%{{http://www.cis.upenn.edu/~bcpierce/sf/}Software Foundations}%}% by Pierce et al.
21 22
22 This chapter is also meant as a case study, bringing together what we have learned in the previous chapters. We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts. We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts. 23 This chapter is also meant as a case study, bringing together what we have learned in the previous chapters. We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts. We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts.
23 24
24 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip. 25 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
25 26
26 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. *) 27 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. We also use [f_equal] to simplify goals of a particular form that will come up with the term denotation function that we define shortly. *)
27 28
28 Ltac ext := let x := fresh "x" in extensionality x. 29 Ltac ext := let x := fresh "x" in extensionality x.
29 Ltac pl := crush; repeat (ext || f_equal; crush). 30 Ltac pl := crush; repeat (match goal with
31 | [ |- (fun x => _) = (fun y => _) ] => ext
32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal
33 end; crush).
30 34
31 (** At this point in the book source, some auxiliary proofs also appear. *) 35 (** At this point in the book source, some auxiliary proofs also appear. *)
32 36
33 (* begin hide *) 37 (* begin hide *)
34 Section hmap. 38 Section hmap.