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. |