gcongr exists_congr

Stream: general

[Johan Commelin]

@Heather Macbeth @Mario Carneiro Currently exists_congr can not be tagged with the gcongr attribute. Could this possibly be an extension, or is that out of scope?

[Floris van Doorn]

This is probably because Exists is not applied to a variable p, but fun x => p x. In some places I added a reformulated lemma to tag as @[gcongr].

[Floris van Doorn]

It would be nice if @[gcongr] can just handle an argument fun x => p x as the variable p.

[Heather Macbeth]

Currently, no equality lemmas at all are tagged with @[gcongr]. It seems to me that it would lead to unpredictable behaviour to tag only a few.

Ideally we would have the right equality analogue of gcongr implemented (see my comments a few days ago, I think it should be something between congrm and congr!) and then gcongr can just do exactly that in the equality case.

[Heather Macbeth]

(so maybe we should enforce an informal rule, "equalities get tagged @[congr] not @[gcongr]")

[Joachim Breitner]

Why do we need to distinguish equality from other relations? As an entitled user, I’d probably prefer to have one tactic and one attribute that works throughout. Also, I could imagine that some congruence lemmas about some (equivalence-like) relation could have equality in the assumptions, and vice versa.

[Heather Macbeth]

Congruence lemmas for equality are weird! There's some magic I don't understand in the core implementation of congr which generates one for every function of every arity. So you need to hook into that (possibly superseding it in certain cases with tagged @[congr] lemmas), rather than just curating a list specific to the relation at hand.

[Heather Macbeth]

Certainly I would prefer gcongr also handle equality, I just don't currently have the metaprogramming chops to do it right.

[Joachim Breitner]

That’s of course fair, limited development resources is a perfectly valid justification!

[Kyle Miller]

@Heather Macbeth I think it's worth knowing that the congr tactic is taking advantage of the existing congruence lemma generator that's designed for simp, and the congr tactic is a nice application of those congruence lemmas. These congruence lemmas though are specialized to simp's design, where you want to make sure the arguments are Eqs rather than HEqs as much as possible, since simp can only do further rewrites where there are Eq arguments. It even prevents certain arguments from being rewritable (they become "fixed") to ensure later arguments are Eqs. These sorts of things probably account for a lot of the complexity you're seeing.

[Kyle Miller]

Lean.Meta.mkHCongrWithArity from core is another congruence lemma generator that generates Eqs or HEqs, depending on which is needed depending on the type of the function. The more dependent the function's type is, the more HEqs you'll see.

Mathlib also has docs#Lean.Meta.mkHCongrWithArity', which is a wrapper around mkHCongrWithArity that pre-proves certain Eqs using Subsingleton lemmas (useful for Decidable and Fintype for example). This function is used deep down by congrm (in particular, by the congr(...) quotations).

There's also docs#Lean.Meta.mkRichHCongr, which is similar to mkHCongrWithArity' but in the lemma each argument gets all the relevant previous Eqs/HEqs for convenience. This one is used by congr!.

[Kyle Miller]

The congr tactic doesn't do anything to the goal Fintype.card X = Fintype.card Y since the congruence lemma generator for simp doesn't generate a lemma with a X = Y goal. The congr! tactic should since mkRichHCongr will generate a lemma with a X = Y goal (and it can also eliminate the HEq goal for the Fintype instances automatically).