Mercurial > cpdt > repo

comparison src/Equality.v @ 365:990151eac6af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Discuss reduction of [fix]
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Nov 2011 16:52:15 -0500
parents 2fbb47fb02bd
children b809d3a8a5b1
comparison
equal deleted inserted replaced
364:2fbb47fb02bd 365:990151eac6af
87 87
88 reflexivity. 88 reflexivity.
89 Qed. 89 Qed.
90 (* end thide *) 90 (* end thide *)
91 91
92 (** The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a %\index{propositional equality}\textit{%#<i>#propositional equality#</i>#%}%, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use. 92 (** The [beta] reduction rule applies to recursive functions as well, and its behavior may be surprising in some instances. For instance, we can run some simple tests using the reduction strategy [compute], which applies all applicable rules of the definitional equality. *)
93
94 Definition id (n : nat) := n.
95
96 Eval compute in fun x => id x.
97 (** %\vspace{-.15in}%[[
98 = fun x : nat => x
99 ]]
100 *)
101
102 Fixpoint id' (n : nat) := n.
103
104 Eval compute in fun x => id' x.
105 (** %\vspace{-.15in}%[[
106 = fun x : nat => (fix id' (n : nat) : nat := n) x
107 ]]
108
109 By running [compute], we ask Coq to run reduction steps until no more apply, so why do we see an application of a known function, where clearly no beta reduction has been performed? The answer has to do with ensuring termination of all Gallina programs. One candidate rule would say that we apply recursive definitions wherever possible. However, this would clearly lead to nonterminating reduction sequences, since the function may appear fully applied within its own definition, and we would naively %``%#"#simplify#"#%''% such applications immediately. Instead, Coq only applies the beta rule for a recursive function when %\emph{%#<i>#the top-level structure of the recursive argument is known#</i>#%}%. For [id'] above, we have only one argument [n], so clearly it is the recursive argument, and the top-level structure of [n] is known when the function is applied to [O] or to some [S e] term. The variable [x] is neither, so reduction is blocked.
110
111 What are recursive arguments in general? Every recursive function is compiled by Coq to a %\index{Gallina terms!fix}%[fix] expression, for anonymous definition of recursive functions. Further, every [fix] with multiple arguments has one designated as the recursive argument via a [struct] annotation. The recursive argument is the one that must decrease across recursive calls, to appease Coq's termination checker. Coq will generally infer which argument is recursive, though we may also specify it manually, if we want to tweak reduction behavior. For instance, consider this definition of a function to add two lists of [nat]s elementwise: *)
112
113 Fixpoint addLists (ls1 ls2 : list nat) : list nat :=
114 match ls1, ls2 with
115 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists ls1' ls2'
116 | _, _ => nil
117 end.
118
119 (** By default, Coq chooses [ls1] as the recursive argument. We can see that [ls2] would have been another valid choice. The choice has a critical effect on reduction behavior, as these two examples illustrate: *)
120
121 Eval compute in fun ls => addLists nil ls.
122 (** %\vspace{-.15in}%[[
123 = fun _ : list nat => nil
124 ]]
125 *)
126
127 Eval compute in fun ls => addLists ls nil.
128 (** %\vspace{-.15in}%[[
129 = fun ls : list nat =>
130 (fix addLists (ls1 ls2 : list nat) : list nat :=
131 match ls1 with
132 | nil => nil
133 | n1 :: ls1' =>
134 match ls2 with
135 | nil => nil
136 | n2 :: ls2' =>
137 (fix plus (n m : nat) : nat :=
138 match n with
139 | 0 => m
140 | S p => S (plus p m)
141 end) n1 n2 :: addLists ls1' ls2'
142 end
143 end) ls nil
144 ]]
145
146 The outer application of the [fix] expression for [addList] was only simplified in the first case, because in the second case the recursive argument is [ls], whose top-level structure is not known.
147
148 The opposite behavior pertains to a version of [addList] with [ls2] marked as recursive. *)
149
150 Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
151 match ls1, ls2 with
152 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
153 | _, _ => nil
154 end.
155
156 Eval compute in fun ls => addLists' ls nil.
157 (** %\vspace{-.15in}%[[
158 = fun ls : list nat => match ls with
159 | nil => nil
160 | _ :: _ => nil
161 end
162 ]]
163
164 We see that all use of recursive functions has been eliminated, though the term has not quite simplified to [nil]. We could get it to do so by switching the order of the [match] discriminees in the definition of [addLists'].
165
166 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match]. This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint].
167
168 %\medskip%
169
170 The standard [eq] relation is critically dependent on the definitional equality. The relation [eq] is often called a %\index{propositional equality}\textit{%#<i>#propositional equality#</i>#%}%, because it reifies definitional equality as a proposition that may or may not hold. Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity. In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina. We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
93 171
94 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality %``%#"#as data.#"#%''% *) 172 This all may make it sound like the choice of [eq]'s definition is unimportant. To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs. Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality %``%#"#as data.#"#%''% *)
95 173
96 174
97 (** * Heterogeneous Lists Revisited *) 175 (** * Heterogeneous Lists Revisited *)