mkCongrSimp? error for Set

Stream: lean4

[Kyle Miller]

I noticed that congr doesn't seem to work in some equalities involving Set.

For example, the following congr is a no-op

example (xs ys : Set α) (f g : α → β) (h : xs = ys) : Set.image f xs = Set.image g ys := by
  congr
  sorry

But the following congr generates the expected subgoals

example (s t u v : Set α) : s ∪ t = u ∪ v := by
  congr
  sorry
  sorry

Investigating, the first generates (using mkCongrSimp?) a congr lemma with type

∀ {α : Type ?u.18640} {β : Type ?u.18662} (f f_1 : α → β),
  f = f_1 → ∀ (s s_1 : Set α), s = s_1 → ∀ (a a_1 : β), a = a_1 → Set.image f s a = Set.image f_1 s_1 a_1

and the second generates

∀ {α : Type ?u.18238} [self : Union α] (a a_1 : α), a = a_1 → ∀ (a_2 a_3 : α), a_2 = a_3 → a ∪ a_2 = a_1 ∪ a_3

It seems that somehow the definition of Set is being unfolded in the Set.image case and Lean goes and generates a lemma with too much extensionality.

[Kyle Miller]

Here's a mathlib-free mwe:

def Set (α : Type _) := α → Prop
def Set.image (f : α → β) (s : Set α) : Set β := fun y => ∃ x, s x ∧ f x = y

example (s t : Set α) (f g : α → β) : Set.image f s = Set.image g t := by
  congr
  sorry -- congr doesn't do anything

[Kyle Miller]

I'm not sure if this is a problem in mkCongrSimp? or a problem in how congr applies the generated congr lemma.

A piece of evidence that it's the latter is that simp can navigate these expressions fine:

example (s t : Set α) (f : α → β) (h : s = t) : Set.image f s = Set.image f t := by
  simp [h]

[Gabriel Ebner]

lean4#2128

[Gabriel Ebner]

The reason this particular case works with simp is because simp has a fallback for when congruence lemmas cannot be generated.

[Kyle Miller]

Just to check, is this the fallback (along with congrArgs)?

[Gabriel Ebner]

Yes, that's it. In the beginning, Lean 4 simp didn't have support for auto-generated congruence lemmas at all. Back then, this was the only congr support it had.

[Kyle Miller]

Thanks, I was wanting to write a version of docs4#Lean.MVarId.congr? that implemented the fallback algorithm.

[Kyle Miller]

Regarding that, I have a conceptual question about isDefEq. I was under the impression that isDefEq should be enough to assign the mvarId metavariable near the end of the following function, but it appears I need to do mvarId.assign explicitly:

def Lean.MVarId.fallbackCongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  mvarId.withContext do commitWhenSomeNoEx? do
    mvarId.checkNotAssigned `fallbackCongr
    let tgt ← mvarId.getType'
    let some (_, lhs, _) := tgt.eq? | return none
    lhs.cleanupAnnotations.withApp fun f args => do
      if args.isEmpty then
        return none
      let infos := (← getFunInfoNArgs f args.size).paramInfo
      let mut goals : Array MVarId := #[]
      let mut pf ← mkFreshExprMVar (some (← mkEq f (← mkFreshExprMVar (← inferType f))))
      goals := goals.push pf.mvarId!
      let mut i := 0
      for arg in args do
        if (i < infos.size && not infos[i]!.hasFwdDeps) || (← whnfD (← inferType f)).isArrow then
          let eq ← mkFreshExprMVar (some (← mkEq arg (← mkFreshExprMVar (← inferType arg))))
          goals := goals.push eq.mvarId!
          pf ← Meta.mkCongr pf eq
        else
          pf ← Meta.mkCongrFun pf arg
        i := i + 1

      guard (← isDefEq (mkMVar mvarId) pf)
      mvarId.assign pf -- The isDefEq doesn't appear to assign the metavariable?

      return some goals.toList

[Kyle Miller]

I'm also not completely sure if I should be doing isDefEq on the terms themselves (a goal metavariable and a proof) or their types.

[Kyle Miller]

(This function is in the work-in-progress mathlib4#2606 for context.)

[Gabriel Ebner]

The fallback code isn't a great solution either (see lean4#2128).

[Gabriel Ebner]

I can't tell why the isDefEq doesn't work here. Do you have an #mwe? If I had to guess, I'd say that Lean applies proof irrelevance before assigning the metavariable. But then we're using isDefEq to assign mvars all over the place.

[Gabriel Ebner]

Oh, we use it all over the place and it's known to be broken: lean4#2054 ...

[Kyle Miller]

Thanks, that's good to know about how it's known to not work for propostions.

[Kyle Miller]

Regarding the fallback code, I just wanted to give congr! a chance at applying to some useful situations, like from earlier in the thread. Even if it can't handle dependent types, I'm hoping it can handle at least as much as simp can.

I need to rethink it a bit though, since the fallback is happy to apply congruence lemmas even if it's unfolding definitions in the types.

[Kyle Miller]

It really negatively affects expressions involving docs4#setOf for example