Zulip Chat Archive

Stream: general

Topic: Strong Induction


Kevin Kappelmann (Sep 03 2019 at 12:09):

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 (Sep 03 2019 at 12:29):

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

Reid Barton (Sep 03 2019 at 12:29):

Then apply it to _ l rfl

Mario Carneiro (Sep 03 2019 at 12:30):

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

Chris Hughes (Sep 03 2019 at 12:32):

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 (Sep 03 2019 at 12:45):

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 (Sep 03 2019 at 12:48):

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 (Sep 03 2019 at 13:15):

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

Mario Carneiro (Sep 03 2019 at 13:18):

yes, in the usual way (with)

Patrick Massot (Sep 03 2019 at 13:18):

I couldn't get it to work

Mario Carneiro (Sep 03 2019 at 13:18):

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

Mario Carneiro (Sep 03 2019 at 13:19):

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

Patrick Massot (Sep 03 2019 at 13:19):

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

Mario Carneiro (Sep 03 2019 at 13:19):

that works too

Patrick Massot (Sep 03 2019 at 13:20):

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

Patrick Massot (Sep 03 2019 at 13:20):

We need to invent a mnemonic

Mario Carneiro (Sep 03 2019 at 13:24):

U Won't Get it right

Patrick Massot (Sep 03 2019 at 13:27):

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 (Sep 03 2019 at 13:36):

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

Patrick Massot (Sep 03 2019 at 13:37):

Are you replying to something here?


Last updated: Dec 20 2023 at 11:08 UTC