Strong Induction

Stream: general

[Kevin Kappelmann]

Does anyone know how to use strong induction on a term that does not appear in the goal? For example, given variable {P : list ℕ → Prop}, I want to prove that ∀ (l : list ℕ), P l. Here are some failed attempts:

lemma needs_induction (l : list ℕ) : P l :=
begin
  induction l.length, -- failed to find expression in the target
  sorry
end

lemma needs_induction (l : list ℕ) : P l :=
@nat.strong_induction_on P (l.length) sorry -- type mismatch

lemma needs_induction_hack (l : list ℕ) : (λ n, n = l.length → P l) l.length :=
nat.strong_induction_on (l.length)
begin
  assume n IH n_eq_length, -- l is not generalised in IH
  sorry
end

lemma needs_induction_fix (l : list ℕ) : P l := needs_induction_hack l rfl

[Reid Barton]

One way is to prove forall n l (h : l.length = n), P l

[Reid Barton]

Then apply it to _ l rfl

[Mario Carneiro]

You can do this in tactic mode using generalize e : l.length = n, induction n generalizing l

[Chris Hughes]

You can also use the equation compiler or well_founded.fix

variable {P : list ℕ → Prop}

lemma needs_induction : ∀ (l : list ℕ), P l
| l := sorry
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf list.length⟩] }

lemma needs_induction₂ (l : list ℕ) : P l :=
well_founded.fix (measure_wf list.length) _ l

[Kevin Kappelmann]

Cool, thank you all! well_founded.fix is the thing I was looking for - the trick by Mario cannot be done with strong induction, or am I wrong?

[Chris Hughes]

lemma needs_induction (l : list ℕ) : P l :=
begin
  generalize hn : l.length = n,
  induction n using nat.strong_induction_on generalizing l,

end

[Patrick Massot]

That seems pretty hard to figure out. Is this documented somewhere? Can you name the inductions variables and assumptions?

[Mario Carneiro]

yes, in the usual way (with)

[Patrick Massot]

I couldn't get it to work

[Mario Carneiro]

I don't use the using clause very often because it usually fails

[Mario Carneiro]

there is an order to the clauses, try reordering them if there is a parse error

[Patrick Massot]

Indeed, I manage to find the correct order by looking at the tactic definition...

[Mario Carneiro]

that works too

[Patrick Massot]

For the record, the order is "using" then "with" then "generalizing"

[Patrick Massot]

We need to invent a mnemonic

[Mario Carneiro]

U Won't Get it right

[Patrick Massot]

It's tempting to say we need a tactic to do that (and the obvious beta reduction in the induction hypothesis), but it's not so easy to see what would be the general pattern...

[Mario Carneiro]

There is an equality hypothesis in cases, but it is deliberately omitted in induction because it's usually the wrong thing

[Patrick Massot]

Are you replying to something here?