Inductively Defined Propositions

Inductively Defined Propositions

Using Evidence in Proofs

Inversion on Evidence

Induction on Evidence

Inductive Relations

Case Study: Regular Expressions

The remember Tactic

Case Study: Improving Reflection

Additional Exercises

Extended Exercise: A Verified Regular-Expression Matcher