theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

noConfusion and unreachable patterns

Open rambip opened this issue 2 years ago • 1 comments

In the chapter induction and recursion, part "dependant pattern matching", I find the explanations quite hard to follow.

First, the goal of the auxiliairy functions is not described explicitely Worse, it uses "noConfusion". I was not able to find any documentation about this function, and no definition either.

I think it would be more clear to have a dedicated chapter about unreachable patterns explaining:

  • what are the strategies to deal with unreachable patterns
  • how does the equation compiler can understand some patterns are not accessible in a pattern matching
  • how you ca use "False.elim" to fill impossible cases
  • how to create a pattern matching with zero cases (or why it is impossible)
  • what is the function "Nat.noConfusion"

An example to prove that 0 != 1 would be a nice illustation I think I hope my feedback will help improve the documentation !

rambip avatar Feb 13 '23 11:02 rambip

I found this explanation very helpfull: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

rambip avatar Feb 14 '23 12:02 rambip