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 One of them (intoIH_listForall and intoIH_listForall₂) are is newly created in this PR. The type class itself and other instances were already created by @HaleOIC, and 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

The mechanism is basically the same as those in Rocq, but 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ₙ: note that z₁ ... zₙ is implemented as selection patterns (SelPat) and, as a result, there are no restrictions regarding the order of regular Lean variables and Iris hypothesis names.
• iinduction e with | constr₁ => tac₁ | ... | constrₙ => tacₙ: the constructor names can either be long (e.g., Nat.zero) or short (e.g., zero). Arguments are optionally given names or otherwise remain inaccessible.

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

1. Generalise the expression e if it does not directly correspond to an FVarId value.
2. (Optional, when generalizing is used) Revert Iris hypotheses explicitly specified by the user.
3. Reverts all hypotheses in the spatial context as well as hypotheses in the intuitionistic context involving the variable on which induction is being applied.
   • Hypotheses already reverted in step 1 do not need to be handled in this step.
4. (Optional, when generalizing is used) Revert pure Lean variables explicitly specified by the user.
5. (Optional, when with is used) Check that the constructor patterns (alternative names) provided by the user are valid.
6. Uses Lean.Meta.Tactic.induction to obtain the induction subgoals.
7. Moves the newly generated induction hypotheses from the regular Lean context into the intuitionistic context.
8. Introduces the reverted hypotheses from steps 1, 2 and 3 back into the spatial and intuitionistic contexts.
9. Create the induction subgoals for the tactic user.
10. Fill in the metavariable for each induction subgoal generated by Lean using the corresponding proof obtained in step 8.
11. (Optional, when with is used) Handle the tactic sequences for each induction subgoal.
12. Fill in the metavariable for the original proof goal before applying the tactic.

The tactic syntax can be used in combination:

• iinduction e using r with | constr₁ => tac₁ | ... | constrₙ => tacₙ
• iinduction e using r generalizing z₁ ... zₙ
• iinduction e generalizing z₁ ... zₙ with | constr₁ => tac₁ | ... | constrₙ => tacₙ
• iinduction e using r generalizing z₁ ... zₙ 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 => ...

One can also use underscores for the variables to remain inaccessible. This is made possible with Lean's binderIdent. For example, one can get the unnamed variable n✝ and the named induction hypothesis ih:

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

Several functions in Induction.lean are introduced to parse the syntax and handle the constructor names properly. This handles subtle caveats such as duplicate, missing and/or invalid constructor names.

Checklist

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