Mercurial > cpdt > repo
comparison src/Equality.v @ 296:559ec7328410
Spelling errors found preparing JFR paper
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 09 Dec 2010 14:39:49 -0500 |
parents | 1b6c81e51799 |
children | b441010125d4 |
comparison
equal
deleted
inserted
replaced
295:6833a1b778c0 | 296:559ec7328410 |
---|---|
78 ============================ | 78 ============================ |
79 (let y := 0 in y) = 0 | 79 (let y := 0 in y) = 0 |
80 | 80 |
81 ]] | 81 ]] |
82 | 82 |
83 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *) | 83 The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term substituted. *) |
84 | 84 |
85 cbv zeta. | 85 cbv zeta. |
86 (** [[ | 86 (** [[ |
87 ============================ | 87 ============================ |
88 0 = 0 | 88 0 = 0 |
295 The term "refl_equal x'" has type "x' = x'" while it is expected to have type | 295 The term "refl_equal x'" has type "x' = x'" while it is expected to have type |
296 "x = x'" | 296 "x = x'" |
297 | 297 |
298 ]] | 298 ]] |
299 | 299 |
300 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. | 300 The type error comes from our [return] annotation. In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring 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. |
301 | 301 |
302 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *) | 302 Nonetheless, it turns out that, with one catch, we %\textit{%#<i>#can#</i>#%}% prove this lemma. *) |
303 | 303 |
304 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. | 304 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x. |
305 intros; apply UIP_refl. | 305 intros; apply UIP_refl. |