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.