Many of the proofs in Syntax.* are by mutual induction, but our mutual_induction tactic does not support any convenience features. The task is to simplify these proof scripts, either by improving the tactic, writing a new one, or using https://github.com/ionathanch/MutualInduction assuming it supports the necessary features.
The ideal tactic might support (see also here and Zulip):
- Automatic abstraction and reverting of non-variable indices.
generalize syntax- Multiple goals rather than one big conjunctive goal.
- Declaring multiple theorems at once in a
mutual block, rather than as consequences of one big theorem.
The Lean language reference on mutual inductive types is here.
Many of the proofs in
Syntax.*are by mutual induction, but ourmutual_inductiontactic does not support any convenience features. The task is to simplify these proof scripts, either by improving the tactic, writing a new one, or using https://github.com/ionathanch/MutualInduction assuming it supports the necessary features.The ideal tactic might support (see also here and Zulip):
generalizesyntaxmutualblock, rather than as consequences of one big theorem.The Lean language reference on mutual inductive types is here.