Potential pattern matching bug?

Stream: new members

[Julian Sutherland]

Lean reports:
"non-exhaustive match, the following cases are missing:
is_literal _ {val := _, nodup := _} 1 (CBlockList._mut_.CId_3 _ {val := _, nodup := _} {data := _} _)"

for the following code:

image.png

However, this error disappears if the third line is commented out. I would have expected the final line to catch any possible pattern, is this a bug?

[Yaël Dillies]

Please send us the code as a #MWE rather than an image :smile: We need context.

[Julian Sutherland]

Hey! Thanks for your answer! Apologies, I'm very new. What's a #MWE?

[Sebastien Gouezel]

It's a #mwe :-)

[Julian Sutherland]

Thank you! :) I'm on it!

[Julian Sutherland]

Here is my #mwe:

import data.finset.basic
import data.fin.basic

def UInt256_max : ℕ := 2^256
def UInt256 := fin UInt256_max
def Literal := UInt256
def Identifier := string

def FTContext := Identifier → option (ℕ × ℕ)

inductive CExpr : FTContext → finset Identifier → ℕ → Type
 | CId : ∀ (Γ : FTContext) (vars : finset Identifier) (id : Identifier), id ∈ vars → CExpr Γ vars 1
 | CLit : ∀ (Γ : FTContext) (vars : finset Identifier), Literal → CExpr Γ vars 1

def is_literal : ∀ {Γ : FTContext} {vars : finset Identifier} {n : ℕ}, CExpr Γ vars n -> Prop
| _ _ _ (CExpr.CLit _ _ _) := true
-- | _ _ _ (CExpr.CId _ _ _ _)  := false
| _ _ _ _                  := false

Once again, lean reports "non-exhaustive match, the following cases are missing:
is_literal _ {val := _, nodup := _} 1 (CExpr.CId _ {val := _, nodup := _} {data := _} _)", but is happy if I comment back in the before last line. It seems to me however that this pattern should be caught by the last line.

[Eric Wieser]

If you can in your real example I'd recommend simplifying your type to:

inductive CExpr (Γ : FTContext) (vars : finset Identifier) : ℕ → Type
 | CId : ∀ (id : Identifier), id ∈ vars → CExpr 1
 | CLit : Literal → CExpr 1

That might even help the pattern matching, but I haven't tried it

[Julian Sutherland]

Doesn't seem to, thank you none the less! Also, this is a minimum working example, in the full code Γ and vars are not constant.

[Floris van Doorn]

I think you're running into this issue: https://github.com/leanprover/lean/issues/1594
I'm afraid that the workaround is to not use catch-all patterns when working with inductive families.

[Julian Sutherland]

@Floris van Doorn Thank you very much! It seems that this is the only solution yes, at least knowing exactly what the problem is allows me to infer a minimal set of matches required to get the behaviour that I would like, which is still very helpful!