comparison src/Equality.v @ 118:ee676bf3d681

Up to Streicher
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 12:04:28 -0400
parents
children 8df59f0b3dc0
comparison
equal deleted inserted replaced
117:d176595cf46e 118:ee676bf3d681
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import Eqdep List.
12
13 Require Import Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Reasoning About Equality Proofs}% *)
20
21 (** In traditional mathematics, the concept of equality is usually taken as a given. On the other hand, in type theory, equality is a very contentious subject. There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal. Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly. In this chapter, we will focus on design patterns for circumventing these tricky issues, and we will introduce the different notions of equality as they are germane. *)
22
23
24 (** * Heterogeneous Lists Revisited *)
25
26 (** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)
27
28 Section fhlist.
29 Variable A : Type.
30 Variable B : A -> Type.
31
32 Fixpoint fhlist (ls : list A) : Type :=
33 match ls with
34 | nil => unit
35 | x :: ls' => B x * fhlist ls'
36 end%type.
37
38 Variable elm : A.
39
40 Fixpoint fmember (ls : list A) : Type :=
41 match ls with
42 | nil => Empty_set
43 | x :: ls' => (x = elm) + fmember ls'
44 end%type.
45
46 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
47 match ls return fhlist ls -> fmember ls -> B elm with
48 | nil => fun _ idx => match idx with end
49 | _ :: ls' => fun mls idx =>
50 match idx with
51 | inl pf => match pf with
52 | refl_equal => fst mls
53 end
54 | inr idx' => fhget ls' (snd mls) idx'
55 end
56 end.
57 End fhlist.
58
59 Implicit Arguments fhget [A B elm ls].
60
61 (** We can define a [map]-like function for [fhlist]s. *)
62
63 Section fhlist_map.
64 Variables A : Type.
65 Variables B C : A -> Type.
66 Variable f : forall x, B x -> C x.
67
68 Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=
69 match ls return fhlist B ls -> fhlist C ls with
70 | nil => fun _ => tt
71 | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
72 end.
73
74 Implicit Arguments fhmap [ls].
75
76 (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap]. It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *)
77
78 Variable elm : A.
79
80 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
81 fhget (fhmap hls) mem = f (fhget hls mem).
82 induction ls; crush.
83
84 (** Part of our single remaining subgoal is:
85
86 [[
87
88 a0 : a = elm
89 ============================
90 match a0 in (_ = a2) return (C a2) with
91 | refl_equal => f a1
92 end = f match a0 in (_ = a2) return (B a2) with
93 | refl_equal => a1
94 end
95 ]]
96
97 This seems like a trivial enough obligation. The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq]. Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
98
99 [[
100
101 destruct a0.
102
103 [[
104 User error: Cannot solve a second-order unification problem
105 ]]
106
107 This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed. We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
108
109 [[
110
111 assert (a0 = refl_equal _).
112
113 [[
114 The term "refl_equal ?98" has type "?98 = ?98"
115 while it is expected to have type "a = elm"
116 ]]
117
118 In retrospect, the problem is not so hard to see. Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically. Thus, the essential lemma we need does not even type-check!
119
120 Is it time to throw in the towel? Luckily, the answer is "no." In this chapter, we will see several useful patterns for proving obligations like this.
121
122 For this particular example, the solution is surprisingly straightforward. [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments. *)
123
124 case a0.
125 (** [[
126
127 ============================
128 f a1 = f a1
129 ]]
130
131 It seems that [destruct] was trying to be too smart for its own good. *)
132
133 reflexivity.
134 Qed.
135
136 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
137
138 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
139 simple destruct pf; reflexivity.
140 Qed.
141
142 (** [simple destruct pf] is a convenient form for applying [case]. It runs [intro] to bring into scope all quantified variables up to its argument. *)
143
144 Print lemma1.
145
146 (** [[
147
148 lemma1 =
149 fun (x : A) (pf : x = elm) =>
150 match pf as e in (_ = y) return (0 = match e with
151 | refl_equal => 0
152 end) with
153 | refl_equal => refl_equal 0
154 end
155 : forall (x : A) (pf : x = elm), 0 = match pf with
156 | refl_equal => 0
157 end
158 ]]
159
160 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
161
162 Definition lemma1' :=
163 fun (x : A) (pf : x = elm) =>
164 match pf return (0 = match pf with
165 | refl_equal => 0
166 end) with
167 | refl_equal => refl_equal 0
168 end.
169
170 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
171
172 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
173 (** [[
174
175 simple destruct pf.
176
177 [[
178
179 User error: Cannot solve a second-order unification problem
180 ]] *)
181 Abort.
182
183 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
184
185 Definition lemma2' :=
186 fun (x : A) (pf : x = x) =>
187 match pf return (0 = match pf with
188 | refl_equal => 0
189 end) with
190 | refl_equal => refl_equal 0
191 end.
192
193 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
194
195 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
196 (** [[
197
198 simple destruct pf.
199
200 [[
201
202 User error: Cannot solve a second-order unification problem
203 ]] *)
204 Abort.
205
206 (** This time, even our manual attempt fails.
207
208 [[
209
210 Definition lemma3' :=
211 fun (x : A) (pf : x = x) =>
212 match pf as pf' in (_ = x') return (pf' = refl_equal x') with
213 | refl_equal => refl_equal _
214 end.
215
216 [[
217
218 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
219 "x = x'"
220 ]]
221
222 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering to the [in]-bound variable [x']. To do a dependent [match], we %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq]. We are just as constrained to use the "real" value [x] for the first argument. Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
223
224 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *)
225
226 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
227 intros; apply UIP_refl.
228 Qed.
229
230 Check UIP_refl.
231 (** [[
232
233 UIP_refl
234 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
235 ]]
236
237 [UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an %\textit{%#<i>#axiom#</i>#%}%. *)
238
239 Print eq_rect_eq.
240 (** [[
241
242 eq_rect_eq =
243 fun U : Type => Eq_rect_eq.eq_rect_eq U
244 : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
245 x = eq_rect p Q x p h
246 ]]
247
248 [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. [eq_rect] is the automatically-generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.
249
250 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via "informal" metatheory.
251
252 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
253
254 Print Streicher_K.
255 (** [[
256
257 Streicher_K =
258 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
259 : forall (U : Type) (x : U) (P : x = x -> Prop),
260 P (refl_equal x) -> forall p : x = x, P p
261 ]]
262
263 This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *)
264
265 End fhlist_map.
266