Alex Weisberger (Sep 04 2022 at 03:41): Alex Weisberger (Sep 04 2022 at 03:41):I'm also working through Types and Programming Languages, and came across something that I don't understand. I'm trying to prove the determinism of a simple small step semantics of boolean expressions:
datatype tapl_bool =
TTrue |
FFalse |
IfElse tapl_bool tapl_bool tapl_bool
inductive beval1 :: "tapl_bool ⇒ tapl_bool ⇒ bool" where
beval1_if_true: "beval1 (IfElse TTrue t2 t3) t2" |
beval1_if_false: "beval1 (IfElse FFalse t2 t3) t3" |
beval1_if: "beval1 t1 t1' ⟹ beval1 (IfElse t1 t2 t3) (IfElse t1' t2 t3)"
The book puts determinism in words as:
"If t -→ t′ and t -→ t′′, then t′ = t′′.
I expressed this as a theorem with:
theorem "beval1 t1 t2 ∧ beval1 t1 t3 ⟶ t2 = t3"
But when I begin the proof by induction, I get a failure to apply the proof method:
apply(induction t1 t2 arbitrary: t3 rule: beval1.induct)
The phrasing of the theorem seems simple, an intuitive expression of the wording in the book to me. Can someone provide any info on why the induction tactic fails to be applied in this case?
Mathias Fleury (Sep 04 2022 at 05:06):You need to write it as
theorem "beval1 t1 t2 ⟹ beval1 t1 t3 ⟹ t2 = t3"
(for technical reasons, the thing you do induction on has to be on top level of the ⟹)
Alex Weisberger (Sep 04 2022 at 14:43):Interesting. I still find the difference between ==> and --> a little confusing, but it's easy enough to remember to use ==> when using induction. Thanks.
Last updated: Dec 21 2024 at 16:20 UTC