Pattern matching in let not substituting

Stream: lean4

[Eric Wieser]

Is this intended behavior?

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  let 3 := n | failure
  return i -- fails, pattern match did not substitute in hypothesis

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  let 3 := n | failure
  return i -- fails, pattern match did not substitute in goal

I thought let was suitable as a substitute for all single-arm matches, which work fine:

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  match n with
  | 3 => return i -- ok
  | _ => failure

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  match n with
  | 3 => return i -- ok
  | _ => failure

[Damiano Testa]

Does if let work there?

[Eric Wieser]

Yes!

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  if let 3 := n then
    return i
  else
    failure

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  if let 3 := n then
    return i
  else
    failure

(but this doesn't help with fixing quote4#29, since Qq uses only the let $path := $rhs version internally)

[Damiano Testa]

Too bad that it isn't helpful for your intended application.

I do find if let convenient sometimes, though.

[Eric Wieser]

Where exactly is pattern matching let implemented in core? If it's implemented in terms of match, can this be fixed simply by turning on the generalization flag? Or is there some reason related to do notation magic that this can't really work?

[Kyle Miller]

For do notation, there are two kinds of pattern-matching let. The first is the one that always succeeds (look for doLet in the source) and it seems to expand to the term let, and term let with a pattern expands to use a match. The second is the one with a failure case (doLetElse), and it expands your let 3 := n | failure to let __discr := n; match __discr with | 3 => ...continuation... | _ => failure

[Kyle Miller]

Maybe the match isn't generalizing through the __discr? I'm not sure why there's that let there and it's not match n with ...

[Kyle Miller]

docs#Lean.Elab.Term.Do.ToCodeBlock.doLetElseToCode

[Kyle Miller]

My guesses are that either it's to be consistent with arrow assign for mutable variables, or it's copy-paste from code for arrow assign and disabling generalization with this extra let isn't intentional.

[Eric Wieser]

Thanks!

[Eric Wieser]

I guess I'll try a patch later this week to see what happens, based on assuming the second option, unless you beat me to it!

[Eric Wieser]

(testing in lean4#3060, will clean up with a proper PR description if it succeeds)

[Eric Wieser]

Just to confirm, everything seems to work with this patch; though it seems no mathlib CI is attempted.

[Joachim Breitner]

We had some hickups with the PR testig workflow recently, mostly my fault. If you merge origin/nightly-with-mathlib into your branch and push, it should run the mathlib CI :fingers_crossed:

[Eric Wieser]

Thanks, it's running now and exposed a latent quote4 bug (but otherwise passes!)