Debugging unification issues

Stream: lean4

[James Gallicchio]

Does anyone have advice for debugging when a rewrite pattern fails to match? Turning on pp.explicit and trying to compare visually gets tedious really fast.

For example:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Foldable'.Correct.fold' { n := Size.size c } (fun acc x h => acc ++ [Indexed.nth c { val := x, isLt := h }]) []
x: τ
c: C
i: Fin (Size.size c)
h: x = Indexed.nth c i
⊢ List.Mem x
  (Foldable'.Correct.fold' { n := Size.size c } (fun acc i h => acc ++ [Indexed.nth c { val := i, isLt := h }]) [])

Without increasing verbosity, no difference is visible, but turning on pp.explicit gives me huge terms that require way too much effort to compare

[Tomas Skrivan]

Sometimes turning on trace.Meta.isDefEq can be helpful, but usually the trace is huge, hard to navigate and read :(

So yeah, I would like to know a better way as well

[Tomas Skrivan]

One thing you can try is to write down a theorem that does not hold but rewrites only a subexpression, like (fun acc x h => acc ++ ...) = (fun acc x h => default) and try rewriting with that. Does it work? Or does it fail?

[Leonardo de Moura]

@Tomas Skrivan Are you using VS Code? The new trace visualization stuff is really cool (many thanks to Gabriel).
Example:

example (a : Nat) : a.succ = a + 2 :=
  set_option trace.Meta.isDefEq true in
  rfl

image.png

[Tomas Skrivan]

I'm Emacs user, but I have installed VS Code just because of the new tracing :) It is really cool!

However, I was debugging some problem in my TC instances and unfortunately the messages were not folding as I expected, the trace was too big that it was freezing VS Code. Also the option synthInstamce.subgoal disappeared :( I have to look into it again, write down what I struggled with and create mwe.

Hopefully the message folds better for isDefEq.

[Emanuel Kywal]

Good night! I'm installing Lean for the first time and I already have a version of python on my machine. How should I proceed?

[Arthur Paulino]

@Emanuel Kywal Do you want to use Lean 3 (and mathlib)? If so, you probably want to start a new thread in #new members

Or, if you want to use Lean 4, then creating a new thread in this stream (#lean4) for your questions is a better way to go

[Emanuel Kywal]

@Arthur Paulino Yes, it's Lean 3 and mathlib. thank you!