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?
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
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 07 2023 at 20:16 UTC