Lean equivalent of inversion tactic

Stream: lean4

[Shreyas Srinivas]

What is the lean equivalent of Coq's inversion tactic?

[Eric Wieser]

Maybe injection or cases?

[Shreyas Srinivas]

It doesn't quite work equivalently. inversion generates a bunch of equalities. I'll try to construct an #mwe to explain

[Shreyas Srinivas]

Here's a lean example:

import Mathlib.Tactic

inductive Expression where
| Lit (z : ℤ)

open Expression

inductive Value where
| LitV (z : ℤ)

open Value

def toExpr (v : Value) :=
  match v with
  | LitV z => Lit z


inductive BigStep : Expression → Value → Prop where
| LitRule (z : ℕ) : BigStep (Lit z) (LitV z)

lemma simpleExample : ∀ v w : Value, BigStep (toExpr v) w → v = w := by
  intro v w H
  cases H -- some error about dependent elimination failure
  sorry

[Shreyas Srinivas]

Here's the corresponding Coq example:

From Coq Require Import ZArith.

Inductive Expression :=
| Lit (z : Z).


Inductive Value :=
| LitV (z : Z).


Definition toExpr (v : Value) :=
  match v with
  | LitV z => Lit z
  end.


Inductive BigStep : Expression -> Value -> Prop :=
| LitRule (z : Z) : BigStep (Lit z) (LitV z).

Lemma simpleExample: forall v w : Value, BigStep (toExpr v) w -> v = w.
Proof.
  intros v w H.
  destruct v.
  inversion H.
  reflexivity.
Qed.

[Shreyas Srinivas]

As you can see Coq does some backward reasoning at H, and produces a bunch of equalities

[Eric Wieser]

cases v; cases H works there

[Eric Wieser]

Which I think is a reasonable translation of destruct v inversion H

[Shreyas Srinivas]

Okay, I think my #mwe example is not quite getting it right

[Alex J. Best]

Some previous discussion https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20.60inversion.60.20tactic.3F/near/257502550

[Shreyas Srinivas]

The error was due to an altogether different reason. In one of my alternatives for BigStep (which has other constructors ofc), one of the options was incorrectly using a substitution function.

[Shreyas Srinivas]

Essentially the last line below was missing:

inductive BigStep : LExpr → Val → Prop where
  | bsLit (n : ℤ) :
      BigStep (LitInt n) (LitIntV n)
  | bsLam (x : Binder) (e : LExpr) :
      BigStep (Lam x e) (LamV x e)
  | bsPlus {e₁ e₂ : LExpr} {z₁ z₂ : ℤ} :
      BigStep e₁ (LitIntV z₁) →
      BigStep e₂ (LitIntV z₂) →
      BigStep (Plus e₁ e₂) (LitIntV (z1 + z2))
  | bsApp {x : Binder} {e e₁ e₂: LExpr} {v₂ v': Val}:
      BigStep e₁ (LamV x e) →
      BigStep e₂ v₂ →
      BigStep (subst' x v₂ e₂) v →
      BigStep (App e₁ e₂) v

[Shreyas Srinivas]

Starting with the arrow in the previous line.