Induction generalization

Stream: new members

[Andrea Delmastro]

Hello, I'm having troubles (again) figuring out how to generalize arguments of an induction.
There's a lot of code needed for a mwe, but I don't think it's necessary to understand my problem, nevertheless I'm posting it at the end.

I want to prove this theorem about a typing system for security:

theorem noninterference {c : com} {s s' t t' : pstate} {l : lv}:
  (c, s) ⟹ s' → (c, t) ⟹ t' → (0 ⊢ₛ c) → s = t ⦅<= l⦆ → s' = t' ⦅<= l⦆ :=

When I do induction' ‹(c, s) ⟹ s'› the inductive hypothesis is correctly generalized over t' but not over t .

For a mwe, plese refer to https://github.com/andreadlm/thesis/blob/help/src/IMP_security.lean (the theorem is at the end).

Thanks in advance!

[Johan Commelin]

Can you revert t t' before you call the induction tactic?

[Eric Wieser]

Or use induction _ generalizing t

[Eric Wieser]

(note that docs#tactic.interactive.induction' and tactic#induction are slightly different)

[Andrea Delmastro]

The revert t t' trick seems to work, even if I don't really understand why. Thanks, I'm always surprised by the willingness of this community to help others :)

[Kevin Buzzard]

The revert trick gives you a more powerful inductive hypothesis. If you have a predicate P(s,t) depending on two inputs and you try to prove it by induction on s directly with a fixed t then your induction hypothesis will say that P(s',t) is true for s' smaller than s and your goal will be P(s,t). Here t is fixed. If you revert t first, then after applying induction your hypothesis will be "for all t, P(s',t)" and your goal will be "for all t, P(s,t)" and in particular you will now be able to use the inductive hypothesis for things other than the fixed t.

[Eric Wieser]

Note that induction ... generalizing x y is shorthand for roughly revert x y, induction ..., intros x y