feat: iinduction

[alvinylt]

Description

Implements the iinduction tactic.

Addresses #360.

This tactic uses the type class IntoIH and its instances, which are ported from coq_tactics.v in the Rocq version. Two of them (intoIH_listForall and intoIH_listForall₂) are newly created in this PR. The type class itself and other instances were already created by @HaleOIC, and they have now been moved from Induction.lean to Classes.lean and Instances.lean, respectively.

Type class/type class instance in Lean	Located in	Corresponding definition in Rocq
IntoIH	Classes.lean	IntoIH
intoIH_entails	Instances.lean	into_ih_entails
intoIH_forall	Instances.lean	into_ih_forall
intoIH_imp	Instances.lean	into_ih_impl
intoIH_listForall	Instances.lean	into_ih_Forall
intoIH_listForall₂	Instances.lean	into_ih_Forall2

In a nutshell, the iinduction tactic performs the following steps:

1. Reverts all hypotheses in the spatial context as well as hypotheses in the intuitionistic context involving the variable on which induction is being applied.
2. Uses Lean.Meta.Tactic.induction to obtain the induction subgoals.
3. Moves the newly generated induction hypotheses from the regular Lean context into the intuitionistic context.
4. Introduces the reverted hypotheses from Step 1 back into the spatial and intuitionistic contexts.

While the above steps are basically the same as those in Rocq, the tactic syntax for induction is quite different in Lean. The implementation of iinduction therefore intends to follow the syntax of induction as detailed in the language specifications of Lean:

• iinduction e
• iinduction e using r
• iinduction e generalizing z₁ ... zₙ
• iinduction x with | constr₁ => tac₁ | ... | constrₙ => tacₙ

Similar to the built-in induction tactic in Lean, the variables and induction hypotheses are assigned inaccessible names unless the user specifies them using the with syntax. For example, by using iinduction n where n : Nat, one may get n✝ and n_ih✝ in the step case. Meanwhile, the following assigns the variable and the induction hypothesis the names n and ih, respectively.

iinduction n with
| zero      => ...
| succ n ih => ...

Several functions in Induction.lean are introduced to parse the syntax and handle the constructor names properly.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files