congr on iff

Stream: mathlib4

[Bhavik Mehta]

Currently congr can break down goals of the form f as = f bs and HEq (f as) (f bs), is it possible / desirable to extend this to goals of the form f as ↔ f bs?

[Kyle Miller]

congr! can do that

[Jireh Loreaux]

congr! can!

[Jireh Loreaux]

import Mathlib

example {α : Type} {f : α → Prop} {x y : α} : f x ↔ f y := by
  congr!

[Kyle Miller]

I'm not sure there are any cases where you want to use congr instead of congr!, though there are some extensions to congr syntax that are sometimes convenient, like the ones for doing ext1 between congr steps.

[Kyle Miller]

While congr! doesn't have that feature, it does have the ability to apply funext automatically, to enter lambdas. It can enter foralls too.

[Bhavik Mehta]

Oops, I should have known that! I was already using the fact that congr can apply funext : I generally use congr rather than congr! since it can enter lambdas and it gives me finer control over which ext lemmas get used, which I often need. (edit: might be misremembering here)

[Bhavik Mehta]

Thanks both!

[Kyle Miller]

Could you give an example of where the ext feature is helpful? (By the way, congr! accepts rcases patterns in its with clause.)

[Bhavik Mehta]

Yes the rcases patterns are super useful! I don't have a concrete example to hand - I will try to remember this and provide one the next time it shows up - but the general pattern is that the ext goes too far. For instance, if I have a goal about the equality of the cardinality of two sets, it might congr into a set equality, then use extensionality and give me some elements; but I'd rather stay on the level of equality of sets because I have other hypotheses involving set equalities.

[Jireh Loreaux]

Can't you control this with the numeric argument? Or does that only control the matching depth not the ext depth?

[Bhavik Mehta]

Jireh Loreaux said:

Or does that only control the matching depth not the ext depth?

Exactly this, I believe. Although now that I think about it, I'm only going off the fact that congr documentation tells you how to control both, and congr! documentation doesn't tell me how to control the ext depth, so I assumed it doesn't let me. I'm not sure I ever properly checked if it does!

[Kyle Miller]

congr! depth controls funext depth too; it counts funext as a congr step

[Bhavik Mehta]

Okay I managed to dig out an example where I use congr 1 with ... then finish the proof with a simp + aesop call, but (after a couple of attempts) none of the obvious options in congr! make the proof work as cleanly. Would it be useful to minimise this?

[Kyle Miller]

Possibly!

[Kyle Miller]

Or at least it could be useful to know what at a high level congr ... with is doing that is useful.

[Bhavik Mehta]

It seems to me like congr! 1 with is not going far enough, and congr! 2 with is going too far, but congr 1 with is getting it exactly where I want

[Bhavik Mehta]

import Mathlib.Data.Set.Card

noncomputable def foo (X : ℕ) : ℕ :=
  Set.ncard { (a, b) : ℕ × ℕ | a.Coprime b ∧ (a, b) ∈ Set.Icc (1, 1) (X, X) }

lemma foo_eq (X : ℕ) :
    foo X = ({ (a, b) | 0 < a ∧ 0 < b ∧ a.Coprime b } ∩ Set.Icc (1, 1) (X, X)).ncard := by
  rw [foo]
  -- congr! 1 with ⟨a, b⟩
  congr 1 with ⟨a, b⟩
  -- congr! 2 with ⟨a, b⟩
  simp [← Prod.mk_one_one]
  aesop

Here is the example as I currently have it - I hope this is small enough to make it clear to you what's going on?

[Kyle Miller]

I see. Doing ext is sort of problematic, because it's a step that goes in the opposite direction of congr, and it would cause infinite loops.

Here's how you can do it as separate steps:

lemma foo_eq (X : ℕ) :
    foo X = ({ (a, b) | 0 < a ∧ 0 < b ∧ a.Coprime b } ∩ Set.Icc (1, 1) (X, X)).ncard := by
  rw [foo]
  congr! 1
  ext ⟨a, b⟩
  simp [← Prod.mk_one_one]
  aesop

In more detail, congr! 1; ext ⟨a, b⟩ is doing what congr 1 with ⟨a, b⟩ is doing, and the result is

⊢ (a, b) ∈ {(a, b) | a.Coprime b ∧ (a, b) ∈ Set.Icc (1, 1) (X, X)} ↔
  (a, b) ∈ {(a, b) | 0 < a ∧ 0 < b ∧ a.Coprime b} ∩ Set.Icc (1, 1) (X, X)

Applying congr! 1 to this brings us right back to the goal before the first congr! 1.

By the way, funext in congr! is handled carefully. It is sure to only try funext if at least one of the two sides of the equality is a fun. Since otherwise, if it starts with f = g and uses funext to turn it into f x = g x, then the next congr step reduces this to f = g, and we loop.

[Bhavik Mehta]

I see, thanks for the explanation. Nonetheless I hope this makes it clearer why the behaviour of congr is sometimes more convenient in practice: I end up with a shorter proof, and I can use the fact that congr/congr! can do an ext step rather than needing to do it manually with ext

[Kyle Miller]

Is using a with clause to tack on a "free" ext shorter? You still have to write with.

I'm not sure I understand the logic of making congr use ext per se. Why not have special clauses for other tactics too?

Or, why not congr! 1; ext ⟨a, b⟩, which is the same number of characters as congr! 1 with ⟨a, b⟩?

[Bhavik Mehta]

Kyle Miller said:

I'm not sure I understand the logic of making congr use ext per se. Why not have special clauses for other tactics too?

Isn't this precisely what congr! does here too? As you mentioned earlier:

While congr! doesn't have that feature, it does have the ability to apply funext automatically, to enter lambdas.

Or am I misunderstanding your meaning somewhere?

[Bhavik Mehta]

Similarly, congr! also uses with notation, so both of these points apply equally to congr and congr!. The distinction - to me - is that these two tactics both apply congruence lemmas and extensionality lemmas in various ways, and in the situation above one of them works while the other fails. One of the features of congr! according to its documentation is that it uses funext, and similarly for congr: I personally would prefer to use a congruence + funext tactic in a way which doesn't require me to use funext myself.

[Kyle Miller]

This is the subtle detail:
Kyle Miller said:

By the way, funext in congr! is handled carefully. It is sure to only try funext if at least one of the two sides of the equality is a fun. Since otherwise, if it starts with f = g and uses funext to turn it into f x = g x, then the next congr step reduces this to f = g, and we loop.

It's not that it uses extensionality exactly, but that it's willing to eta expand one side to make it possible to use funext. It won't eta expand both sides.

Funext for congr! means transforming

|- (fun x => A) = (fun x => B)

into

x : X
|- A = B

The with clause is purely for naming (and possibly destructuring) the introduced x.

[Kyle Miller]

The congr ... with's notion of extensionality is more like eta expanding both sides, which is problematic as it goes in the exact opposite direction of what congr is trying to do.

[Bhavik Mehta]

I think I see now - you're saying that congr! isn't meant to be viewed as "congruence and extensionality", but instead "congruence and extensionality in certain cases".

[Bhavik Mehta]

Kyle Miller said:

The congr ... with's notion of extensionality is more like eta expanding both sides, which is problematic as it goes in the exact opposite direction of what congr is trying to do.

Is there a plan to deprecate / disallow congr because of it being problematic in this way?

[Bhavik Mehta]

Playing with it some more in the example you give, I wonder why

example {α β : Type*} {f g : α → β} : f = g := by
  congr with x

doesn't loop, similarly with congr 3 with x, congr 4 with x etc.

[Kyle Miller]

Ah, it's just a macro for congr <;> ext x

macro_rules
  | `(tactic| congr $(cfg)? $(depth)? with $ps* $[: $n]?) =>
    match cfg with
    | none => `(tactic| congr $(depth)? <;> ext $ps* $[: $n]?)
    | some cfg => `(tactic| congr $cfg $(depth)? <;> ext $ps* $[: $n]?)

[Bhavik Mehta]

That explains it! And rcongr instead detects when the loop can happen and quits

[Jireh Loreaux]

I didn't even know rcongr existed.