tactic 'generalize' failed

Stream: lean4

[Marcus Rossel]

I can't for the life of me figure out how to perform induction on a list, when the goal contains a proof term that involves that list.
Here's an MWE:

def List.attach [BEq α] (l : List α) : List {x // l.contains x} := sorry

inductive B deriving BEq
structure A where bs : Nat → List B

def f {a : A} {b : B} {n} (hc : (a.bs n).contains b) : Nat := sorry

example (a : A) (n : Nat) : (a.bs n).attach.map (f ·.property) = [] := by
  induction (a.bs n)

The compiler says:

tactic 'generalize' failed, result is not type correct
  ∀ (x : List B), List.map (fun a_1 => f (_ : List.contains x a_1.val = true)) (List.attach x) = []
a : A
n : Nat
⊢ List.map (fun a_1 => f (_ : List.contains (A.bs a n) a_1.val = true)) (List.attach (A.bs a n)) = []

I can make that error go away temporarily, by doing:

example (a : A) (n : Nat) : (a.bs n).attach.map (f ·.property) = [] := by
  cases a
  case mk bs =>
    induction (bs n) <;> simp only [A.bs] at *

But then again, the simp only [A.bs] at * does not rewrite the proof term, so I'm still stuck:

case nil
n : Nat
bs : Nat → List B
⊢ List.map (fun a => f (_ : List.contains (A.bs { bs := bs } n) a.val = true)) (List.attach (bs n)) = []

case cons
n : Nat
bs : Nat → List B
head✝ : B
tail✝ : List B
tail_ih✝ : List.map (fun a => f (_ : List.contains (A.bs { bs := bs } n) a.val = true)) (List.attach (bs n)) = []
⊢ List.map (fun a => f (_ : List.contains (A.bs { bs := bs } n) a.val = true)) (List.attach (bs n)) = []

[Chris B]

Will this work for what you're doing?

example (l : List B) : ∀ (a : A) (n : Nat), l = (a.bs n) -> (a.bs n).attach.map (f ·.property) = [] := by
  induction l with
  | nil =>
    trace_state
    sorry
  | cons h t ih =>
    trace_state
    sorry

[Marcus Rossel]

Chris B said:

Will this work for what you're doing?

example (l : List B) : ∀ (a : A) (n : Nat), l = (a.bs n) -> (a.bs n).attach.map (f ·.property) = [] := by
  induction l with
  | nil =>
    trace_state
    sorry
  | cons h t ih =>
    trace_state
    sorry

Hmm, I think not. I still get stuck at not being able to rewrite the proof term.
Perhaps I don't understand what you're hinting at with this approach.
E.g. the nil case in your example should be provable, but I can't prove it because I can't rewrite the l = a.bs n (in the nil case: [] = a.bs n) in the .attach term.

[Chris B]

Marcus Rossel said:

Perhaps I don't understand what you're hinting at with this approach.

It's just generalizing it by hand, moving things rightward into the motive and then adding an equality hypothesis. The hang-up here seems to be the dependent argument to f. If you can get away with making it def f {b : B} {l : List B} (hc : l.contains b) : Nat := or def f {b : B} {l : List B} (hc : l.contains b) (h' : ∃ (a: A) (n : Nat), l = a.bs n) : Nat := sorry things should go more smoothly.

[Chris B]

As it is, you can get a little closer by filling in the implicits, but the last type-level rewrite seems a bridge too far. The rewrite gives the 'motive not type correct' error.

example (l : List B) : ∀ (a : A) (n : Nat) (h : a.bs n = l), l.attach.map (fun z => @f a z.val n (h ▸ z.property)) = [] := by
  induction l with
  | nil =>
    intro a n h
    --rw [h]
    sorry
  | cons h t ih =>
    trace_state
    sorry