Eliminate/generalize terms, not just hypotheses

[dranov]

In the proof of last_ind in Seq.v, one needs to generalize a term []. This is done by elim: s [] Hnil, but this is currently not supported in Ssrlean.

Lemma last_ind P :
  P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.
Proof.
move=> Hnil Hlast s; rewrite -(cat0s s).
elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0.
by rewrite -cat_rcons; apply/IHs/Hlast.
Qed.

Here's the equivalent Lean proof:

theorem last_ind (P : Seq α → Prop) :
  P [] → (∀ s x, P s → P (rcons s x)) → ∀ s, P s := by
  move=> Hnil Hlast s <;> srw -(cat0s s);
  revert Hnil; generalize [] = s1; revert s1
  elim: s=>[|x s2 IHs] s1 Hs1
  { sby srw cats0 }
  { sby srw -cat_rcons; apply IHs; apply Hlast }

[dranov]

I tried implementing this, but ran into an issue with term taking over the case for ident when defining the elab_rules – I think there must be some way of properly defining priorities, but I couldn't figure it out.

[volodeyka]

I don't know how to resolve this issue with precedence. For now, if you want to revert a term t, just put it inside parentheses:

 elim: s ([]) Hnil=> [|x s2 IHs] s1 Hs1

Time permitting, let's extract the minimal example and post a question on Zulip