congr not doing anything in the presence of dependent fields

[kim-em]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

congr not working as expected

Steps to Reproduce

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
  intro m₁ m₂
  cases m₁ with
  | @mk one₁ mul₁ one_mul₁ mul_one₁ =>
    cases one₁ with | mk one₁ => 
    cases mul₁ with | mk mul₁ => 
    cases m₂ with
    | @mk one₂ mul₂ one_mul₂ mul_one₂ =>
      cases one₂ with | mk one₂ => 
      cases mul₂ with | mk mul₂ => 
        simp
        intro h
        cases h
        congr -- Does nothing
        -- So this fails
        exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Expected behavior: [What you expect to happen]

congr to change the goal to one₁ = one₂, as it would have in Lean3.

Actual behavior:

congr succeeds, but does not change the goal.

Versions

Lean (version 4.0.0-nightly-2022-10-09, commit 5ef9a2ac7d1f, Release)

[leodemoura]

@semorrison I fixed a bug in the congr tactic, but there are others.

[leodemoura]

@semorrison @digama0 @gebner

I think I found the other issue. The type of MulOneClass.mk in Lean 4 is

{M : Type u_1} → [toOne : One M] → [toMul : Mul M] → (∀ (a : M), 1 * a = a) → (∀ (a : M), a * 1 = a) → MulOneClass M

Note that the fields of the parent classes One and Mul are not flattened like in Lean 3. This is the intended behavior. However, it is problematic for the congr tactic since (in both Lean 3 and Lean 4) instance implicit arguments are "fixed." That is, the automatically generated congruence theorem treats this kind of argument as "fixed". Should we relax this restriction? Not sure how it will affect Mathlib.

Another question: I am assuming congr should fail if the lemma cannot be applied. I will fix this if you agree, ok?

[digama0]

Regarding failure, one thing that I have noticed more generally is that tactics no longer fail if they don't change the goal (simp and injections come to mind). Especially if we have a fail_if_unchanged combinator, I think this is a reasonable choice, but we should be explicit and consistent about it.

[gebner]

One option that I just pitched to Leo was to make the toOne and toMul arguments in the MulOneClass.mk constructor explicit:

{M : Type u_1} → (toOne : One M) → (toMul : Mul M) → (∀ (a : M), 1 * a = a) → (∀ (a : M), a * 1 = a) → MulOneClass M

This change by itself would introduce two regressions:

1. attribute [instance] MyClass.mk would no longer work. AFAICT this is only used by class abbrev and can be fixed trivially by writing a custom instance.
2. { : MulOneClass M } would no longer search for TC instances for One M and Mul M. Not that this feature only works in half of the cases at the moment: if a parent is a subobject, then {} will use TC synthesis to fill it, but not if it is flattened. If we add support in the structure instance elaborator to fill in fields using TC synthesis, then it would work in both cases.

[leodemoura]

Regarding failure, one thing that I have noticed more generally is that tactics no longer fail if they don't change the goal (simp and injections come to mind). Especially if we have a fail_if_unchanged combinator, I think this is a reasonable choice, but we should be explicit and consistent about it.

@digama0 This is a good point. Could you please create an issue with all the tactics that we need the adjust the behavior?

BTW, are you happy with Gabriel's proposal above?

[digama0]

Which way are we going here? Should tactics fail if they don't change the goal, or do nothing?

Re: Gabriel's suggestion, it seems like a suboptimal solution, since in most respects we do actually want the arguments to be instance implicit. This is just an issue for congr, so I would want to fix this somewhere more local to congr itself, either by analyzing the theorem to determine that they shouldn't "really" be fixed args, or that there is something else about the situation that suggests we should not treat them as fixed in this case. And there is something unusual in the example, which is that we have pattern matched on the instance arguments so there is a constructor in the instance slot.

Also, it is reasonable to have a special option or syntax like congr! to indicate that we really do want to descend into typeclass args, because this is both a rare situation and also one where it is really annoying to have to prove the theorem without congr helping.

[leodemoura]

Which way are we going here? Should tactics fail if they don't change the goal, or do nothing?

Good question. Both possibilities seem to have their own merits. Gabriel and I were guessing that would be better to keep the Lean 3 behavior since the community is already used to it, and it will probably simplify the port. What do you think?