RFC: Induction should (like cases) allow non-variable targets

Proposal

Reasoning about e.g. Big-Step Semantics needs induction over a Predicate containing a tuple.
Cases works nicely with this, however induction doesn't, and sometimes one really needs the induction hypothesis:

def State : Type :=
  String → Nat

inductive Stmt : Type where
  | skip       : Stmt
  | seq        : Stmt → Stmt → Stmt

infixr:90 "; " => Stmt.seq

inductive BigStep : Stmt × State → State → Prop where
  | skip (s) :
    BigStep (Stmt.skip, s) s
  | seq (S T s t u) (hS : BigStep (S, s) t)
      (hT : BigStep (T, t) u) :
    BigStep (S; T, s) u

infix:110 " ⟹ " => BigStep

theorem BigStep_deterministic {S s l r} (hl : (S,s) ⟹ l)
      (hr : (S,s) ⟹ r) :
    l = r :=
  by
    induction hl --fails, but cases is not enough here (for the 2nd goal)

The only workaround i know for this, is to express everything in terms of a tuple Ss.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the failing induction hl example and compare it with cases. The payload names no source file or test; trace the induction elaboration path and define done as making the theorem work with a non-variable target while preserving existing cases behavior.