Sub-goals for steps in an induction

Stream: new members

[N Gelwan]

Can anyone think of a way to turn a goal for the following inductive proposition into a collection of sub-goals for each step in the induction?

/-- If `R` is a relation between inhabitants of a type and lists of that type, `ConsWise R l` is a
proposition that `R` holds between all elements in the list `l` and their respective "initial
sections". -/
inductive ConsWise (R : α → (List α) → Prop) : List α → Prop where
  | nil  : ConsWise R []
  | cons : ∀ {a : α} {l : List α}, R a l → ConsWise R l → ConsWise R (a :: l)


def GreaterThanSum : Nat → List Nat → Prop := fun n l ↦ List.sum l ≤ n


def somePowersOfTwo : List Nat := [16, 8, 4, 2, 1]


example : ConsWise GreaterThanSum somePowersOfTwo := by
  apply ConsWise.cons
  · dsimp only [GreaterThanSum]
    norm_num
  · apply ConsWise.cons
    · dsimp only [GreaterThanSum]
      norm_num
    · apply ConsWise.cons
      · dsimp only [GreaterThanSum]
        norm_num
      · apply ConsWise.cons
        · dsimp only [GreaterThanSum]
          norm_num
        · apply ConsWise.cons
          · dsimp only [GreaterThanSum]
            norm_num
          · apply ConsWise.nil
  done

I've been looking into writing a tactic for it, but it's a looking to be hairy and I thought I'd reach out to see if anyone out there had any shortcuts.

[Damiano Testa]

In your case, the example can be proved with

example : ConsWise GreaterThanSum somePowersOfTwo := by
  repeat
    apply ConsWise.cons
    · dsimp only [GreaterThanSum]
      norm_num
  apply ConsWise.nil
  done

[N Gelwan]

Ah, I had no idea that you can drop the cases down out of the tree. Very cool. Thanks @Damiano Testa.

[Notification Bot]

N Gelwan has marked this topic as resolved.

[Notification Bot]

N Gelwan has marked this topic as unresolved.

[Notification Bot]

N Gelwan has marked this topic as resolved.

[Notification Bot]

N Gelwan has marked this topic as unresolved.

[N Gelwan]

Sorry for the spam. Working through something.

Yeah, I actually need a more general case, in which the tactic for each step in the induction is not the same.
Let's see if I can work up an MWE.

[Damiano Testa]

Probably a more structured approach would be to define lemmas that take care of each small step and then use simp to take care of combining them together.

[N Gelwan]

That's a great idea. I'm going to test it out.