induction deconstruction on hypotheses

Stream: lean4

[Arthur Paulino]

Why isn't my induction deconstructing f.data in hh?

def allPos : List Nat → Prop
  | [] => True
  | h :: t => 0 < h ∧ allPos t

structure Foo where
  data  : List Nat
  allPos : allPos data

theorem Bar {f : Foo} (n : Nat) (hl : 0 < n) :
    allPos (f.data.concat n) := by
  have hh := f.allPos
  induction f.data with
    | nil => simp [allPos] exact hl
    | cons h t hi =>
      -- hh : allPos f.data     (why?)
      -- hh : allPos (h :: t)   (i wanted this instead)
      sorry

[Siddhartha Gadgil]

Inside matches (I am guessing the same for induction), the info that the pattern matches the argument is lost, but can be captured as an equality using the syntax match c:x with ....

[Siddhartha Gadgil]

Sorry, the syntax fails for induction.

[Marcus Rossel]

Maybe try generalize hd : f.data = fd first.

[Anand Rao]

I think an explicit pattern matching of the Foo structure did the trick for me:

theorem Bar (n : Nat) (hl : 0 < n) {f : Foo} : allPos (f.data.concat n) :=
  match f with
    | ⟨data, hh⟩ => by
      induction data with
        | nil =>
          simp [allPos]
          exact hl
        | cons h t hi =>
          simp [allPos]
          exact ⟨hh.1, hi hh.2⟩

[Chris B]

The code you provided works the way you want it to (showing h :: t); I'm on nightly 1-06. What version are you using?

[Arthur Paulino]

Chris B said:

The code you provided works the way you want it to (showing h :: t); I'm on nightly 1-06. What version are you using?

I'm using leanprover/lean4:nightly-2022-01-10

[Arthur Paulino]

I switched to ...-01-06 and it still shows hh : allPos f.data

[Chris B]

screenshot.png

[Chris B]

Just to make sure we're not talking about different things, this is what I'm seeing.

[Arthur Paulino]

Yeah, it's deconstructed in the goal, but if you look at hh you'll notice that it's not:

image.png