Tactic `generalize` failed: result is not type correct

Stream: lean4

[Jannis]

Hi!

For context:
I'm currently proving some bery basic graph theory from scratch, including my own definition of graphs, walks, paths etc.
I have arrived at the point where I'm trying to construct appending paths to another, but I've come across an issue with the cases tactic.
This context is not inherently relevant, I just can't seem to minimize my example.

This is the goal state I'm currently trying to reach:

⊢ (op1.walk.vertices ++ op2.walk.vertices.tail).getLast ⋯ = w

I tried to apply the cases tactic to op2.walk.vertices, which is a List, but it failed with the following error:

Tactic `generalize` failed: result is not type correct
  ∀ (x : List (Vertex n✝)), (op1.walk.vertices ++ x.tail).getLast ⋯ = w

Help very much appreciated!

[Snir Broshi]

#mwe

theorem foo (l₁ l₂ : { l : List Nat // l.Nodup }) (x : Nat) (h₂ne : l₂.val ≠ [])
    (h₂ : l₂.val.getLast h₂ne = x) (hne : l₁.val ++ l₂.val ≠ []) :
    (l₁.val ++ l₂.val).getLast hne = x := by
  cases l₁.val
  · sorry
  · sorry

[Snir Broshi]

And here's a solution, not sure how great it is but it works:

theorem foo (l₁ l₂ : { l : List Nat // l.Nodup }) (x : Nat) (h₂ne : l₂.val ≠ [])
    (h₂ : l₂.val.getLast h₂ne = x) (hne : l₁.val ++ l₂.val ≠ []) :
    (l₁.val ++ l₂.val).getLast hne = x := by
  generalize l₁.val = l₁' at *
  cases l₁'
  · sorry
  · sorry

[Snir Broshi]

So try generalize op1.walk.vertices = foo at * and then cases foo

[Snir Broshi]

I'm not an expert, but I believe that the issue is that cases works differently on variables vs expressions.
When you do cases on an expression it doesn't work very well, and specifically it doesn't fix the mention of the expression in the proof you give to getLast, so everything breaks since it's basically doing a.getLast h where h is a proof of b ≠ [], which isn't related to a.

[Snir Broshi]

(hopefully Lean experts can weigh in on whether I'm correct)

[Aaron Liu]

you might want to have some way of remembering that l₁'.Nodup

[Snir Broshi]

Well you can generalize h : l₁.val = l₁' at * I guess, then h will get you back from l₁' to l₁

[Aaron Liu]

does cases h : l₁.val also work?

[Snir Broshi]

No, it seems to also use generalize under the hood (based on the error messages) but not at * for some reason.

theorem foo (l₁ l₂ : { l : List Nat // l.Nodup }) (x : Nat) (h₂ne : l₂.val ≠ [])
    (h₂ : l₂.val.getLast h₂ne = x) (hne : l₁.val ++ l₂.val ≠ []) :
    l₁.val ++ l₂.val = l₁.val ++ l₂.val := by
  cases h : l₁.val
  · sorry
  · sorry

It seems to only generalize at the goal and not at hne, which is why OP got an error

[Edward van de Meent]

A trick that's good to know is that sometimes these errors can be circumvented by using revert on the hypothesis that causes the error

[Jannis]

Hi, thanks for your ideas.
However, generalize doesn't seem to work for op2.walk.vertices = foo (and neither for op1.walk.vertices).
I get the following error:

Tactic `generalize` failed: result is not type correct
  ∀ (foo : List (Vertex n✝)),
    foo = p2.walk.vertices ∨ foo = p2.walk.vertices.reverse → (op1.walk.vertices ++ foo.tail).getLast ⋯ = w

I tried adding some context, but I just don't seem to get the error.
I'd be willing to share the entire code, but it's quite a bit and I wouldn't call my proofs idiomatic.

[Jannis]

The closest MWE I can come up with is the following:

theorem foo (l₁ l₂ : { l : List Nat // l.Nodup }) (x : Nat) (h₂ne : l₂.val ≠ [])
    (h₂ : l₂.val.getLast h₂ne = x) (hne : l₁.val ++ l₂.val ≠ []) :
    (l₁.val ++ l₂.val).getLast _ = x := by
  generalize l₁.val = l₁' at *
  cases l₁'
  · sorry
  · sorry

It has the same goal state with the proof for getLast being unnamed (or unknown rather), but I don't know how to express this in a way that it's actually correct and not just an error.

[Robin Arnez]

Yeah the problem is that the proof term for getLast can't be rewritten so easily (rw will have similar trouble). You can try

have (eq := verts_eq) verts := op2.walk.vertices
simp only [← verts_eq]
rcases verts with _ | ⟨head, tail⟩
· ...
· ...

simp can handle these proof rewrites better than generalize (which does the same thing as rw and thus produces similarly cryptic "motive not type correct" errors).

[Robin Arnez]

Notably, your error comes from the fact that rw [← verts_eq] would fail with a similar error message.

[Jannis]

I actually managed to solve it just now!
I changed the goal to use a named proof for getLast:

change (op1.walk.vertices ++ op2.walk.vertices.tail).getLast (by simp [op1.walk.isNonempty]) = w

Then you can just do cases as usual.

[Jannis]

theorem foo (l₁ l₂ : { l : List Nat // l.Nodup }) (x : Nat) (h₂ne : l₂.val ≠ [])
    (h₂ : l₂.val.getLast h₂ne = x) (hne : l₁.val ++ l₂.val ≠ []) :
    (l₁.val ++ l₂.val).getLast _ = x := by
  change (l₁.val ++ l₂.val).getLast hne = x
  cases l₁
  · sorry
  · sorry

So I guess this would be the proposed solution for the MWE.

[Jannis]

What I don't understand is, how would I deal with rw in general, if it can't deal well with rewriting when proofs are involved?

[Jannis]

But I guess I'll open another thread for this.

[Kevin Buzzard]

rw! might be a good solution for you