Mercurial > cpdt > repo

comparison src/StackMachine.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents 8caa3b3f8fc0
children 3f4576f15130
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
71 match b with 71 match b with
72 | Plus => plus 72 | Plus => plus
73 | Times => mult 73 | Times => mult
74 end. 74 end.
75 75
76 ]]
77
76 In this example, we could also omit all of the type annotations, arriving at: 78 In this example, we could also omit all of the type annotations, arriving at:
77 79
78 [[ 80 [[
79 Definition binopDenote := fun b => 81 Definition binopDenote := fun b =>
80 match b with 82 match b with
81 | Plus => plus 83 | Plus => plus
82 | Times => mult 84 | Times => mult
83 end. 85 end.
84 86
87 ]]
88
85 Languages like Haskell and ML have a convenient %\textit{%#<i>#principal typing#</i>#%}% property, which gives us strong guarantees about how effective type inference will be. Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard heuristically in practice. Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language. 89 Languages like Haskell and ML have a convenient %\textit{%#<i>#principal typing#</i>#%}% property, which gives us strong guarantees about how effective type inference will be. Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard heuristically in practice. Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
86 90
87 This is as good a time as any to mention the preponderance of different languages associated with Coq. The theoretical foundation of Coq is a formal system called the %\textit{%#<i>#Calculus of Inductive Constructions (CIC)#</i>#%}%, which is an extension of the older %\textit{%#<i>#Calculus of Constructions (CoC)#</i>#%}%. CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development. Still, it is nice to know that it has been proved that CIC enjoys properties like %\textit{%#<i>#strong normalization#</i>#%}%, meaning that every program (and, more importantly, every proof term) terminates; and %\textit{%#<i>#relative consistency#</i>#%}% with systems like versions of Zermelo Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory. 91 This is as good a time as any to mention the preponderance of different languages associated with Coq. The theoretical foundation of Coq is a formal system called the %\textit{%#<i>#Calculus of Inductive Constructions (CIC)#</i>#%}%, which is an extension of the older %\textit{%#<i>#Calculus of Constructions (CoC)#</i>#%}%. CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development. Still, it is nice to know that it has been proved that CIC enjoys properties like %\textit{%#<i>#strong normalization#</i>#%}%, meaning that every program (and, more importantly, every proof term) terminates; and %\textit{%#<i>#relative consistency#</i>#%}% with systems like versions of Zermelo Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory.
88 92
89 Coq is actually based on an extension of CIC called %\textit{%#<i>#Gallina#</i>#%}%. The text after the [:=] and before the period in the last code example is a term of Gallina. Gallina adds many useful features that are not compiled internally to more primitive CIC features. The important metatheorems about CIC have not been extended to the full breadth of these features, but most Coq users do not seem to lose much sleep over this omission. 93 Coq is actually based on an extension of CIC called %\textit{%#<i>#Gallina#</i>#%}%. The text after the [:=] and before the period in the last code example is a term of Gallina. Gallina adds many useful features that are not compiled internally to more primitive CIC features. The important metatheorems about CIC have not been extended to the full breadth of these features, but most Coq users do not seem to lose much sleep over this omission.
105 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *) 109 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *)
106 110
107 (** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses. *) 111 (** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses. *)
108 112
109 Eval simpl in expDenote (Const 42). 113 Eval simpl in expDenote (Const 42).
110 (** [[ 114 (** [= 42 : nat] *)
111 = 42 : nat 115
112 ]] *)
113 Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)). 116 Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
114 (** [[ 117 (** [= 4 : nat] *)
115 = 4 : nat 118
116 ]] *)
117 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). 119 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
118 (** [[ 120 (** [= 28 : nat] *)
119 = 28 : nat
120 ]] *)
121 121
122 (** ** Target Language *) 122 (** ** Target Language *)
123 123
124 (** We will compile our source programs onto a simple stack machine, whose syntax is: *) 124 (** We will compile our source programs onto a simple stack machine, whose syntax is: *)
125 125
275 275
276 To progress further, we need to use the definitions of some of the functions appearing in the goal. The [unfold] tactic replaces an identifier with its definition. 276 To progress further, we need to use the definitions of some of the functions appearing in the goal. The [unfold] tactic replaces an identifier with its definition.
277 *) 277 *)
278 278
279 unfold compile. 279 unfold compile.
280 280 (** [[
281 (** [[
282
283 n : nat 281 n : nat
284 s : stack 282 s : stack
285 p : list instr 283 p : list instr
286 ============================ 284 ============================
287 progDenote ((IConst n :: nil) ++ p) s = 285 progDenote ((IConst n :: nil) ++ p) s =
288 progDenote p (expDenote (Const n) :: s) 286 progDenote p (expDenote (Const n) :: s)
289 ]] *) 287 ]] *)
290 288
291 unfold expDenote. 289 unfold expDenote.
292 290 (** [[
293 (** [[
294
295 n : nat 291 n : nat
296 s : stack 292 s : stack
297 p : list instr 293 p : list instr
298 ============================ 294 ============================
299 progDenote ((IConst n :: nil) ++ p) s = progDenote p (n :: s) 295 progDenote ((IConst n :: nil) ++ p) s = progDenote p (n :: s)
461 (** And the proof is completed, as indicated by the message: 457 (** And the proof is completed, as indicated by the message:
462 458
463 [[ 459 [[
464 Proof completed. 460 Proof completed.
465 461
462 ]]
463
466 And there lies our first proof. Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers. If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving. Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma. We abort the old proof attempt and start again. 464 And there lies our first proof. Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers. If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving. Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma. We abort the old proof attempt and start again.
467 *) 465 *)
468 466
469 Abort. 467 Abort.
470 468
706 | TIBinop _ _ _ _ b => 704 | TIBinop _ _ _ _ b =>
707 match s with 705 match s with
708 (arg1, (arg2, s')) => ((tbinopDenote b) arg1 arg2, s') 706 (arg1, (arg2, s')) => ((tbinopDenote b) arg1 arg2, s')
709 end 707 end
710 end. 708 end.
709
710 ]]
711 711
712 The Coq type-checker complains that: 712 The Coq type-checker complains that:
713 713
714 [[ 714 [[
715 The term "(n, s)" has type "(nat * vstack ts)%type" 715 The term "(n, s)" has type "(nat * vstack ts)%type"