I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19).
(1) In the rule induction principles for
To show P(a nat) whenever a nat, it is enough to show: (1) P(zero nat). (2) for every a, if (a nat and) P(a nat), then P(succ(a) nat).
why is the bracketed "(a
nat and)" clause necessary (and similarly for
tree)? This seems "natural" - we shouldn't need to prove things about syntactic entities that don't define
nats - but doesn't appear in the definition given of property P "respecting the rules" defining
tree (also on p. 19), which is how the rule induction principle is defined. In the proof of Lemma 2.1, the extra "a nat and" part has become part of the definition of the property P - what's going on here?
(2) I don't understand the induction step of Lemma 2.1 (
succ(a) nat implies
a nat). If I were doing this proof, I'd just invert the rules for
nat right away, or, using Harper's property P, say: If
succ(a) is of form
succ(b), then by injectivity,
b nat as
a nat, but injectivity hasn't been proven yet. It seems instead that Harper applies the induction hypothesis about
a directly to
succ(a) - I must be missing something.
(3) In a more naive framework, Lemma 2.3 would just follow from sufficiency of the
= nat relation rules ("inversion"), but I don't know how to write down a proof in this style. Why is induction even needed?
I'm sorry if these questions seem like nitpicking, but Martin-Löf/LF feels very foreign to me. If I squint and pretend I'm doing everything in a more "traditional" operational semantics, I can read other parts of the book (with slightly different proofs), but I feel I'm missing the point in doing so.
If these questions are too tedious to answer individually, are there other references on doing semantics in this style?