Usability issue
When using the elim-Vec tactic, users must manually supply a motive and length argument. The other eliminators (elim-Nat, elim-List) auto-generate their motives from the goal, making elim-Vec feel inconsistent and significantly harder to use.
Context
Encountered when trying to prove properties about Vec in the interactive proof assistant. Applying elim-Nat or elim-List on a goal works with minimal input, but switching to elim-Vec on a Vec goal requires writing a full motive by hand, which requires deep knowledge of how ind-Vec works internally.
Suggested improvement
Auto-generate the motive for elim-Vec from the current proof goal, consistent with how elim-Nat and elim-List behave. Users should only need to provide the base case and inductive step, not a manually constructed motive.
Usability issue
When using the
elim-Vectactic, users must manually supply a motive and length argument. The other eliminators (elim-Nat,elim-List) auto-generate their motives from the goal, makingelim-Vecfeel inconsistent and significantly harder to use.Context
Encountered when trying to prove properties about Vec in the interactive proof assistant. Applying elim-Nat or elim-List on a goal works with minimal input, but switching to elim-Vec on a Vec goal requires writing a full motive by hand, which requires deep knowledge of how ind-Vec works internally.
Suggested improvement
Auto-generate the motive for elim-Vec from the current proof goal, consistent with how elim-Nat and elim-List behave. Users should only need to provide the base case and inductive step, not a manually constructed motive.