import breaking simp

Stream: new members

[Jayde Massmann]

I'm working on a formalization of some mathematics in Lean. I'm currently somewhat confused, as an import breaks a proof, despite not e.g. introducing any new lemmas that the simplifier would try to use instead.

Without the import, simp? [...] yields the following list:

simp only [union_range, Fin.isValue, evalComp, eval_rudunorderedtuple_eq_range, eval_rudunion_eq_union, ZFSet.mem_sUnion, ZFSet.mem_range, Set.mem_range, exists_exists_eq_and, g]

When I import Mathlib.SetTheory.Ordinal.Rank, it complains that some of these tactics are unused, and simp? [...] yields the following, shorter list:

simp only [union_range, Fin.isValue, evalComp, eval_rudunion_eq_union, ZFSet.mem_sUnion, g]

What's going on here?

Here's an (unfortunately quite long) MWE; said simp is on L133.

import Mathlib.SetTheory.ZFC.Basic
-- import Mathlib.SetTheory.Ordinal.Rank

inductive RudFunc : (ar: Nat) -> Type where
  | proj: Fin ar -> RudFunc ar
  | diff: Fin ar -> Fin ar -> RudFunc ar
  | pair: Fin ar -> Fin ar -> RudFunc ar
  | comp: (Fin ar2 -> RudFunc ar) -> RudFunc ar2 -> RudFunc ar
  | union: RudFunc ar -> RudFunc ar

export RudFunc (proj diff pair comp union)

-- Often, ar = 0 requires no special treatment, so we don't bother banning it outright.
theorem no_nullary_rudfuncs : RudFunc 0 -> False := by sorry

attribute [instance] Classical.allZFSetDefinable

noncomputable def do_union (f: (Fin ar -> ZFSet) -> ZFSet) (x: Fin ar -> ZFSet): ZFSet :=
  match ar with
  | 0 => ∅
  | _ + 1 => ⋃₀ ZFSet.image (λz => f (λi => if i = 0 then z else x i)) (x 0)

@[simp]
theorem mem_do_union [nz: NeZero ar] (f: (Fin ar -> ZFSet) -> ZFSet) :
    x ∈ do_union f y ↔ ∃z : ZFSet, z ∈ y 0 ∧ x ∈ f (λi => if i = 0 then z else y i) := by
  rw [do_union.eq_def]
  cases ar
  · cases nz.out rfl
  · simp

noncomputable def eval : RudFunc ar -> (Fin ar -> ZFSet) -> ZFSet
  | proj i => λx => x i
  | diff i j => λx => x i \ x j
  | pair i j => λx => {x i, x j}
  | comp inner outer => λx => eval outer λi => eval (inner i) x
  | union f => do_union (eval f)

@[simp] lemma evalProj : eval (proj i) = λx => x i := by rfl
@[simp] lemma evalPair : eval (pair i j) = λx => {x i, x j} := by rfl
@[simp] lemma evalComp : eval (comp inner outer) = λx => eval outer λi => eval (inner i) x := by rfl
@[simp] lemma evalUnion : eval (union f) = do_union (eval f) := by rfl

-- Converting a rud function into a higher-arity one by adding dummy variables.

def dummy (k: Nat): RudFunc ar -> RudFunc (ar + k)
  | proj i => proj (Fin.castAdd k i)
  | diff i j => diff (Fin.castAdd k i) (Fin.castAdd k j)
  | pair i j => pair (Fin.castAdd k i) (Fin.castAdd k j)
  | comp inner outer => comp (λi => dummy k (inner i)) outer
  | union f => union (dummy k f)

@[simp]
theorem eval_dummy_eq_eval (f: RudFunc ar) (k: Nat) :
    eval (dummy k f) = λx => eval f (λi => x (Fin.castAdd k i)) := by sorry

-- Jen71, Prop. 1.1(a) - (d); (e) is completely analogous to (d), just slightly uglier.
def rudUnion [NeZero ar] : Fin ar -> RudFunc ar := λi => comp (λ_ => proj i) (union (proj (0: Fin ar)))

def rudBinaryUnion [NeZero ar] : Fin ar -> Fin ar -> RudFunc ar := λi j => comp (λ_ => pair i j) (union (proj (0: Fin ar)))

@[simp]
theorem eval_rudunion_eq_union [NeZero ar] (i: Fin ar) (x: Fin ar -> ZFSet) :
    eval (rudUnion i) x = ⋃₀ x i := by
  ext; simp [rudUnion]

@[simp]
theorem eval_rudbinaryunion_eq_binaryunion [NeZero ar] (i j: Fin ar) (x: Fin ar -> ZFSet) :
    eval (rudBinaryUnion i j) x = (x i) ∪ (x j) := by
  ext; simp [rudBinaryUnion]

-- The only way I see to construct f(x1, x2, ..., xn) = {x1, x2, ..., xn} is via recursion on n.
def rudUnorderedTuple (ar: Nat) : RudFunc (ar + 1) :=
  match ar with
  | 0 => pair 0 0
  | ar' + 1 => comp (λ(x: Fin 2) => if x = 0 then dummy 1 (rudUnorderedTuple ar') else pair (Fin.last (ar' + 1)) (Fin.last (ar' + 1))) (rudBinaryUnion 0 1)

@[simp]
theorem eval_rudunorderedtuple_eq_range (x: Fin (ar + 1) -> ZFSet) :
    eval (rudUnorderedTuple ar) x = ZFSet.range x := by
  induction ar with
  | zero => ext; simp [rudUnorderedTuple]
            apply Iff.intro
            · intro h; tauto
            · intro h; obtain ⟨y, rfl⟩ := h; obtain rfl := Unique.eq_default y; rfl
  | succ _ h1 => ext; simp [rudUnorderedTuple, h1];
                 apply Iff.intro
                 · intro h2; cases h2 <;> tauto
                 · intro h2; obtain ⟨y, h2⟩ := h2
                   cases y using Fin.lastCases <;> tauto

def RudRelation (R: (Fin ar -> ZFSet) -> Prop) : Prop :=
  ∃f: RudFunc ar, ∀x: Fin ar -> ZFSet, R x = true ↔ ZFSet.Nonempty (eval f x)

theorem rudfunc_by_if_else (R: (Fin ar -> ZFSet) -> Prop) (f: RudFunc ar) [∀x: Fin ar -> ZFSet, Decidable (R x)] :
    RudRelation R -> ∃g: RudFunc ar, ∀x: Fin ar -> ZFSet, eval g x = if R x then eval f x else ∅ := by
  intro h; rw [RudRelation] at h; obtain ⟨r, h⟩ := h; simp at h
  cases ar
  · exfalso; exact no_nullary_rudfuncs f
    -- g(x) = U[z in r(x)] f(x). The z doesn't matter; this is nonempty iff both r(x) and f(x) are.
  · let g := comp (λ(i: Fin 2) => if i = 0 then r else f) (union (proj 1))
    use g; intro x; ext; split
    · simp [g]; intro; simp [← ZFSet.nonempty_def, ← h]; tauto
    · simp [g]; intro _ h2;
      apply ZFSet.nonempty_of_mem at h2; rw [← h] at h2; tauto

-- We don't actually need "for all x, there is i s.t. R(i, x)", because we phrase rud_runc_piecewise by assuming
-- this, to avoid speaking about "the unique i s.t..." and relying on disjointness for uniqueness of the one we've
-- already picked.
def RudRelationPartition (R: Fin n -> (Fin ar -> ZFSet) -> Prop) : Prop :=
  (∀i: Fin n, RudRelation (λx => R i x)) ∧
  (∀i j: Fin n, ∀x: Fin ar -> ZFSet, i ≠ j → ¬(R i x ∧ R j x))

-- Clearly, eval union_range = λx => ⋃₀ ZFSet.range x.
-- We def this because inlining it seems to confuse the type checker.
def union_range : RudFunc (ar + 1) := comp (λ(_: Fin 1) => rudUnorderedTuple ar) (rudUnion 0)

theorem rudfunc_piecewise (R: Fin n -> (Fin ar -> ZFSet) -> Prop) (f: Fin n -> RudFunc ar) [∀i: Fin n, ∀x: Fin ar -> ZFSet, Decidable (R i x)]:
    RudRelationPartition R -> ∃g: RudFunc ar, ∀x, R i x → eval g x = eval (f i) x := by
  cases ar
  · cases n
    · exact i.elim0
    · exfalso; exact no_nullary_rudfuncs (f 0)
  · cases n
    · exact i.elim0
    · intro h; rw [RudRelationPartition] at h
      -- p(i, x) tells us there is some rud function that evaluates to f(i, x) when R(i, x) and {} else.
      -- g(i, x) picks some such function; it can probably be made constructive in the future. h4(i) tells us
      -- that g(i, x) indeed has this property.

      let p := λi => rudfunc_by_if_else (R i) (f i) (h.left i)
      let g := comp (λi => Classical.choose (p i)) union_range
      let h4 := λi => Classical.choose_spec (p i)
      use g; intro x h2; ext; simp [g, union_range]; apply Iff.intro
      · intro h3; obtain ⟨a, h3⟩ := h3
        specialize h4 a x
        by_cases hai: a = i
        · simp [hai, h2] at h4; simp [← h4]; simp [← hai]; exact h3
        · let hdis := h.right; specialize hdis a i x hai
          simp [h2] at hdis; simp [hdis] at h4; simp [h4] at h3
      · intro h3
        specialize h4 i x; simp [h2] at h4; rw [← h4] at h3
        use i

[Kevin Buzzard]

Not an answer to your question, but if you set_option autoImplicit false then you get a lot of errors in your code, making me quite nervous about whether definitions such as RudFunc definitely say what you expect them to say.

[Kevin Buzzard]

I agree that the behaviour is weird. Squeezing the simp should make it pretty immune to import changes, but here it doesn't. If you want to get to the bottom of this then you could switch on some options e.g. set_option trace.Meta.Tactic.simp true (I think there might be better options than this, I don't usually trace simps) and then get two copies of the file, both with the simp squeezed, one copy with the extra import and the other without, and plough through the logs to see what has changed.

[Violeta Hernández]

@Jayde Massmann I found the error, and it's really perplexing. Your code works (with both imports) if you replace the declaration of eval_rudunorderedtuple_eq_range by

theorem eval_rudunorderedtuple_eq_range.{u} {ar: Nat} (x: Fin (ar + 1) -> ZFSet.{u}) :

[Violeta Hernández]

For whatever reason, adding the import changes the universe to ZFSet.{0}, which then means it doesn't match your goal anymore. I have no idea why that is, maybe something going on with the Small instance param in ZFSet.range?

[Violeta Hernández]

It's good practice to be excessive with universe parameters, avoids other weird issues of the sort

[Violeta Hernández]

Here's a minimal working example:

import Mathlib.SetTheory.ZFC.Basic
import Mathlib.SetTheory.Ordinal.Rank -- Code only works without this import!

universe u

theorem foo (x : ℕ -> ZFSet) : ZFSet.range x = ∅ := sorry
example (x : ℕ -> ZFSet.{u}) : ZFSet.range x = ∅ := foo x

[Violeta Hernández]

I think people might not see this in this thread, I'll make a thread in general about this behavior