Mercurial > cpdt > repo

comparison src/Equality.v @ 298:123f466faedc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Small tweak to keep things working in 8.2
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:55:32 -0500
parents b441010125d4
children 7b38729be069
comparison
equal deleted inserted replaced
297:b441010125d4 298:123f466faedc
154 154
155 Variable elm : A. 155 Variable elm : A.
156 156
157 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls), 157 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
158 fhget (fhmap hls) mem = f (fhget hls mem). 158 fhget (fhmap hls) mem = f (fhget hls mem).
159 (* begin thide *) 159 (* begin hide *)
160 induction ls; crush; case a0; reflexivity.
161 (* end hide *)
162 (** [[
160 induction ls; crush. 163 induction ls; crush.
161 164
162 (** In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2 165 ]]
166
167 In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2.
163 168
164 Part of our single remaining subgoal is: 169 Part of our single remaining subgoal is:
165 170
166 [[ 171 [[
167 a0 : a = elm 172 a0 : a = elm
211 216
212 [[ 217 [[
213 reflexivity. 218 reflexivity.
214 219
215 ]] *) 220 ]] *)
221
216 Qed. 222 Qed.
217 (* end thide *) 223 (* end thide *)
218 224
219 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *) 225 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
220 226