Zulip Chat Archive

Stream: lean4

Topic: Pattern matching limitations?


view this post on Zulip François G. Dorais (Jan 07 2021 at 08:51):

In the following example, the definition of Path.unmap fails with the terse message:

error: failed to compile pattern matching, constructor expected
f a:cross:

The Lean 3 analogue of this example works fine.

inductive Tree (α : Type _) : Type _
| leaf : α  Tree α
| branch : Tree α  Tree α  Tree α

inductive Path {α : Type _} : Tree α  Type _
| term (x : α) : Path (Tree.leaf x)
| left (tl tr : Tree α) : Path tl  Path (Tree.branch tl tr)
| right (tl tr : Tree α) : Path tr  Path (Tree.branch  tl tr)

section map
variables {α : Type _} {β : Type _} (f : α  β)

protected def Tree.map : Tree α  Tree β
| Tree.leaf x => Tree.leaf (f x)
| Tree.branch tl tr => Tree.branch (Tree.map tl) (Tree.map tr)

protected def Path.map : {t : Tree α}  Path t  Path (t.map f)
| Tree.leaf _, Path.term x => Path.term (f x)
| Tree.branch _ _, Path.left tl tr p => Path.left (tl.map f) (tr.map f) (Path.map p)
| Tree.branch _ _, Path.right tl tr p => Path.right (tl.map f) (tr.map f) (Path.map p)

protected def Path.unmap : {t : Tree α}  Path (t.map f)  Path t
| Tree.leaf x, Path.term _ => Path.term x
| Tree.branch tl tr, Path.left _ _ p => Path.left tl tr (Path.unmap p)
| Tree.branch tl tr, Path.right _ _ p => Path.right tl tr (Path.unmap p)

end map

This is testing the limits of Lean's pattern matching abilities. Indeed, I was pleasantly surprised when the original Lean 3 version of this worked smoothly. In any case, the Lean 4 error message isn't very detailed and doesn't help much with fixing the code. I don't know if there is a workaround I could use, or if this is work in progress. Thoughts?

view this post on Zulip François G. Dorais (Jan 07 2021 at 13:56):

Option trace.Meta.Match shows that Lean 4 does correctly fill in the blanks. I haven't yet found an option to trace where the compiler fails.

view this post on Zulip Leonardo de Moura (Jan 08 2021 at 01:41):

Thanks. Pushed a fix, and added your example to the test suite.

view this post on Zulip François G. Dorais (Jan 08 2021 at 09:39):

Thank you Leo!


Last updated: May 18 2021 at 23:14 UTC