• General
• How can I prove that two constructors are different?
• During an inductive proof, how do I eliminate impossible cases of an inductive definition?
• How can I prove that two terms in an inductive set are equal? Or different?
• Why is the proof of 0 + n = n on natural numbers trivial but the proof of n + 0 = n is not?
• Why is dependent elimination in Prop not available by default?
• Argh! I cannot write expressions like "if n <= p then p else n", as in any programming language.
• I wrote my own decision procedure for ≤, which is much faster than yours, but proving theorems such as max_equiv seems to be quite difficult.
• Recursion
• Why can't I define a non-terminating program?
• Why are only structurally well-founded loops allowed?
• How to define loops based on non structurally smaller recursive calls?
• What is behind the accessibility and well-foundedness proofs?
• How to perform simultaneous double induction?
• How to define a function by simultaneous double recursion?
• How to perform nested and double induction?
• How to define a function by nested recursion?
• Co-Inductive Types
• References