Dependent elimination failure when casing on Finset quotient

Stream: lean4

[MBN]

I am trying to prove a subject-reduction–style theorem relating process steps and environment steps. Roughly, if a well-typed process can take a step and its corresponding environment can follow that label, then the resulting process is well-typed under the resulting environment.

The setup is roughly as follows (MWE):

abbrev Env := Finset (Nat × Nat)
def Env.mk (x y : Nat) : Env := {(x, y)}

abbrev HyperEnv := Finset Env
instance : Coe Env HyperEnv := ⟨fun Γ => ({Γ} : HyperEnv)⟩

inductive Proc : Type where
  | one     (x : Nat) (P : Proc)

inductive Typing : HyperEnv → Proc → Prop where
  | one {P : Proc} {x : Nat} :
      Typing ∅ P →
      Typing (Env.mk x 1) (Proc.one x P)

inductive Lbl : Type
  | one (x : Nat)

inductive EnvStep : HyperEnv → Lbl → HyperEnv → Prop where
  | one {x : Nat} :
      EnvStep (Env.mk x 1) (.one x) ∅

inductive ProcStep : Proc → Lbl → Proc → Prop where
  | one {P : Proc} {x : Nat} :
      ProcStep (Proc.one x P) (.one x) P

And the theorem I want to prove is:

theorem TypingStep {𝒢 ℋ : HyperEnv} {P Q : Proc} {L : Lbl}
  (hT : Typing 𝒢 P) (hPS : ProcStep P L Q) (hES : EnvStep 𝒢 L ℋ) :
  Typing ℋ Q := by
  induction hPS

  case one =>
    cases hT
    cases hES

But after doing induction on hPS, doing cases hT and then hES fails with a dependent elimination error:

Dependent elimination failed: Failed to solve equation
  Quot.mk ⇑(List.isSetoid Env) [x' ∶ 1] = Quot.mk ⇑(List.isSetoid Env) [x✝ ∶ 1]

As I've gathered, this seems to be a definitional equality issue related to Finset being a quotient, but I am not entirely sure. Is the problem fundamentally the use of Finset here, or is there an idiomatic way to structure this proof so that Lean can eliminate these cases?

[Aaron Liu]

The problem isn't specifically about the quotient, but that Lean can't solve the equation {Env.mk x y} = {Env.mk z w}

[Aaron Liu]

this is not a definitional equality issue

[Jakub Nowak]

This works (but doesn't really solve the problem)

theorem TypingStep {𝒢 ℋ : HyperEnv} {P Q : Proc} {L : Lbl}
  (hT : Typing 𝒢 P) (hPS : ProcStep P L Q) (hES : EnvStep 𝒢 L ℋ) :
  Typing ℋ Q := by
  induction hPS
  case one =>
    cases hT
    set e := _
    conv at hES =>
      arg 1
      change e
    generalize h : e = e' at hES
    cases hES
    clear! e

[MBN]

I have also gotten this to work:

theorem TypingStep {𝒢 ℋ : HyperEnv} {P Q : Proc} {l : Lbl}
  (hT : ⊢ P ∷ 𝒢) (hPS : P -[l]->ₚ Q) (hES : 𝒢 -[l]->ₑ ℋ) : ⊢ Q ∷ ℋ := by
  induction hPS
  case one x =>
    cases hT
    generalize h𝒢 : ({x ∶ 1} : HyperEnv) = 𝒢 at hES
    cases hES

This seems to yield the same result as what Jakub Nowak suggested. However, in the full version of EnvStep (more constructors), generalizing hES causes cases hES to consider additional, spurious matches, which I would ideally like to avoid. In particular, I would prefer to pattern-match on the non-generalized hES and only consider the relevant rule.

I was therefore wondering whether it would be better to redesign the step relation to make matching more precise, or whether it is more idiomatic to keep the relation as is and refute the additional cases?

[Kyle Miller]

One trick is to adjust the type — at the cost of spurious cases — to use equalities to constrain indices:

inductive EnvStep : HyperEnv → Lbl → HyperEnv → Prop where
  | one {e : HyperEnv} {x : Nat} (h : e = Env.mk x 1) :
      EnvStep e (.one x) ∅

Connor McBride calls this "fording" (as in Henry Ford saying "any color the customer wants, as long as it's black".)

When you use cases ... with syntax, you can put a tactic right after with, for example try (simp_all; done), to attempt to dispatch cases automatically.

[Jakub Nowak]

Isn't there some cases' tactic that will give you equalities as hypotheses without trying to do subst on them?