Basic theorem with rfl failing

Stream: general

[Enrico Borba]

I'm writing some propositional logic proofs and am confused on an attempt of mine to prove a basic property of substitution:

import Mathlib.Data.Nat.Basic

notation "[" α ";" n "]" => Fin n → α

/--
  A boolean signature is made up of sets of symbols for each arity `n`.
-/
structure Signature where
  /-- For each arity `n`, a set of symbols. -/
  symbols : ℕ → Type u

/-- Formulas of a signature with at most `n` unbound variables. -/
inductive Signature.Formula {S: Signature} (n : ℕ) where
  /-- Variables. -/
  | var (i : Fin n) : Formula n
  /-- Function application. -/
  | app (a : ℕ) (s : S.symbols a) (φs : [S.Formula n; a]) : Formula n

/-- Substitutes instances of `α` with `β` in `φ`. -/
def subst {S : Signature} [DecidableEq (S.Formula n)] (α β φ : S.Formula n) : S.Formula n :=
  if φ = α then
    β
  else
    match φ with
    | .var i => .var i
    | .app a s φs => .app a s (fun i => subst α β (φs i))

theorem subst_eq {S : Signature} [DecidableEq (S.Formula n)] (α β : S.Formula n) : (subst α β α) = β :=
  by
  /-
    n : ℕ
    S : Signature
    inst✝ : DecidableEq (Signature.Formula n)
    α β : Signature.Formula n
    ⊢ subst α β α = β
    Messages (1)
    Section2.lean:68:63
    type mismatch
      HEq.rfl
    has type
      HEq ?m.11025 ?m.11025 : Prop
    but is expected to have type
      subst α β α = β : Prop
  -/
  rfl

I wasn't able to use simp [subst] in another theorem, an in an attempt to minimize an example of my difficulty, I realized that subst_eq can't be proven with rfl. Any ideas why rfl doesn't work here? Also please let me know if the definitions of Signature or Formula would help at all.

[Yaël Dillies]

Have you tried if_pos rfl?

[Enrico Borba]

theorem subst_eq (α β : S.Formula n) : (subst α β α) = β := if_pos rfl

results in

type mismatch
  if_pos rfl
has type
  (if ?m.11026 = ?m.11026 then ?m.11028 else ?m.11029) = ?m.11028 : Prop
but is expected to have type
  subst α β α = β : Prop

[Enrico Borba]

I feel like lean isn't simplifying the definition of subst. Doing this

theorem subst_eq (α β : S.Formula n) : (subst α β α) = β := by
  simp [subst]

gives a simp made no progress, which is surprising because it should unfold the definition of subst at least.

[Yaël Dillies]

You will need to read #mwe (this is a link) and update your message accordingly so that we can help you further.

[Enrico Borba]

I've updated the original question so it is a MWE.

[Enrico Borba]

I feel like subst is not being unfolded for some reason.

[Kevin Buzzard]

Try unfold subst?

[Enrico Borba]

That does work! Hadn't seen that tactic before

[Enrico Borba]

I'm used to using simp in these cases, still unsure why it doesn't work here.

[Kevin Buzzard]

I agree that I would expect simp [subst] to work.

[Yaël Dillies]

This is because of well-founded recursion, right?

[Enrico Borba]

Oh that's likely it. subst being recursive would cause simp to apply it indefinitely.

[Enrico Borba]

would be nice to see an error that simp is ignoring one of it's terms though, assuming that is what is happening.

[Joachim Breitner]

IIRC then simp [foo] works well if foo is defined by pattern matching and one of the patterns applies, via the generated “equation” lemmas. In this case, there is an if on the RHS, so no equations exist, and you have to manually unfold.

Presumably one could imagine a top-level if to cause two equations with preconditions to be created and applied by simp. Not sure if that would help in general, or be too unpredictable.