Mercurial > cpdt > repo

comparison src/Equality.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents 559ec7328410
children 123f466faedc
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
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 thide *)
160 induction ls; crush. 160 induction ls; crush.
161 161
162 (** Part of our single remaining subgoal is: 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
163
164 Part of our single remaining subgoal is:
163 165
164 [[ 166 [[
165 a0 : a = elm 167 a0 : a = elm
166 ============================ 168 ============================
167 match a0 in (_ = a2) return (C a2) with 169 match a0 in (_ = a2) return (C a2) with
193 195
194 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! 196 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!
195 197
196 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. 198 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.
197 199
198 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. *) 200 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.
199 201
202 [[
200 case a0. 203 case a0.
201 (** [[ 204
202 ============================ 205 ============================
203 f a1 = f a1 206 f a1 = f a1
204 207
205 ]] 208 ]]
206 209
207 It seems that [destruct] was trying to be too smart for its own good. *) 210 It seems that [destruct] was trying to be too smart for its own good.
208 211
212 [[
209 reflexivity. 213 reflexivity.
214
215 ]] *)
210 Qed. 216 Qed.
211 (* end thide *) 217 (* end thide *)
212 218
213 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *) 219 (** It will be helpful to examine the proof terms generated by this sort of strategy. A simpler example illustrates what is going on. *)
214 220
603 (** This time, the naive theorem statement type-checks. *) 609 (** This time, the naive theorem statement type-checks. *)
604 610
605 (* EX: Prove [fhapp] associativity using [JMeq]. *) 611 (* EX: Prove [fhapp] associativity using [JMeq]. *)
606 612
607 (* begin thide *) 613 (* begin thide *)
608 Theorem fhapp_ass' : forall ls1 ls2 ls3 614 Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
609 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
610 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3. 615 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
611 induction ls1; crush. 616 induction ls1; crush.
612 617
613 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is: 618 (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is:
614 619
615 [[ 620 [[
616 ============================ 621 ============================
617 (a0, 622 (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
618 fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
619 (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
620 (a0,
621 fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
622 (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
623 623
624 ]] 624 ]]
625 625
626 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. 626 It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. Here is what happens when we try that in Coq 8.2:
627 627
628 [[ 628 [[
629 rewrite IHls1. 629 rewrite IHls1.
630 630
631 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with 631 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
632 "fhlist B (ls1 ++ ?1572 ++ ?1573)" 632 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
633 633
634 ]] 634 ]]
635
636 Coq 8.3 currently gives an error message about an uncaught exception. Perhaps that will be fixed soon. In any case, it is educational to consider a more explicit approach.
635 637
636 We see that [JMeq] is not a silver bullet. We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts. Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type. That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument. 638 We see that [JMeq] is not a silver bullet. We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts. Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type. That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
637 639
638 We can get around this problem by another multiple use of [generalize]. We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *) 640 We can get around this problem by another multiple use of [generalize]. We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *)
639 641