compiler IR check failed

Stream: mathlib4

[Shaopeng]

Shaopeng said:

Yet another instance involving FirstOrder.Language.Formula.varFreeFinset and Finset.toList, the latter of which is noncomputable. Will comment at lean4#1785 as well.

import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Syntax
import Mathlib.Data.Finset.Basic
set_option linter.unusedVariables false

open FirstOrder List Finset
def freeVarFinset_Equal_Min {𝓛: Language}(β : Type ut)[DecidableEq β](φ: 𝓛.Formula β)(t1 t2: 𝓛.Term β)
  : 𝓛.Formula (β)
  :=
  match φ.freeVarFinset.toList with
    | nil => Language.Term.equal t1 t2
    | List.cons a l => Language.Term.equal t2 t1

/- cf. Weirdly the following works. Note the only diff is the order of terms in the last line,
    making the match essentially uniform. -/
def freeVarFinset_Equal_Min2 {𝓛: Language}(β : Type ut)[DecidableEq β](φ: 𝓛.Formula β)(t1 t2: 𝓛.Term β)
  : 𝓛.Formula (β)
  :=
  match φ.freeVarFinset.toList with
    | nil => Language.Term.equal t1 t2
    | List.cons a l => Language.Term.equal t1 t2

By the way is there a way to circumvent the above issue for the following purposes? Essentially I
wanted to write a function L.Formula β → L.Formula (β ⊕ β) which converts φ with freevariables
x₁,..., xₙto the formula x₁=x₁' ∧ ... ∧ xₙ=xₙ'. A natural way would be to use pattern matching
on the finite list of free variables but it gets stuck at similar compiler IR issues minimized as above.

Any help or advice would be much appreciated!

[Eric Wieser]

I think the answer here is to add a freeVarList definition (implemented from scratch), prove that freeVarList.toFinset = freeVarFinset, and use that list version instead

[Shaopeng]

Thank you so much for the advice, Eric. That looks reasonable. Will try!