Zulip Chat Archive

Stream: lean4

Topic: induction deconstruction on hypotheses


Arthur Paulino (Jan 12 2022 at 03:11):

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 (Jan 12 2022 at 06:37):

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 (Jan 12 2022 at 06:40):

Sorry, the syntax fails for induction.

Marcus Rossel (Jan 12 2022 at 07:26):

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

Anand Rao (Jan 12 2022 at 08:14):

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 (Jan 12 2022 at 12:59):

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 (Jan 12 2022 at 13:28):

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 (Jan 12 2022 at 13:33):

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

Chris B (Jan 12 2022 at 14:45):

screenshot.png

Chris B (Jan 12 2022 at 14:45):

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

Arthur Paulino (Jan 12 2022 at 14:46):

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

image.png


Last updated: Dec 20 2023 at 11:08 UTC