Named induction hypotheses

[jwaldmann]

I made this example https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/tree/master/test-data/pos/bintree

and I was surprised that I could write two IHs:

    Case Branch l k r
       To show: (inorder . mirror) (Branch l k r) .=. (reverse . inorder) (Branch l k r)
       IH: (inorder . mirror) l .=. (reverse . inorder) l
       IH: (inorder . mirror) r .=. (reverse . inorder) r

and that I could refer to them just by IH (and cyp picks the right one)

[larsrh]

What would you expect here?

[jwaldmann]

Not sure. An optional name after the "IH"? (So it rhymes with lemma and axiom).

• We want the user (the student) to be specific (no "by auto", but always "by this lemma, by that axiom").
• in this case, "IH" is one name for two different things (it could be "IH.1", "IH.2")
• but the same already happens at "by def ": there can be several defs (equations) for one name, and cyp picks the one that matches.

Anyway, does cyp have nested induction proofs? Then "IH" would be overloaded as well.

[larsrh]

Good idea; sounds reasonably easy to implement.

Anyway, does cyp have nested induction proofs? Then "IH" would be overloaded as well.

This should work (with the outer "IH" being shadowed), but I'm sure it's not tested anywhere.

[larsrh]

Would you mind if I included your tree example in this repository?

[jwaldmann]

Feel free to pull/cherry-pick/whatever.

I will certainly make more examples, but I might want to hide their full proofs from my students ...