# Zulip Chat Archive

## Stream: general

### Topic: dcongr

#### Johan Commelin (May 06 2020 at 07:55):

Can we have a dependent congr tactic? One that doesn't generate `==`

s by generating smarter goals? Or is this a hard problem?

#### Mario Carneiro (May 06 2020 at 13:01):

what do you want the theorem to say?

#### Scott Morrison (May 06 2020 at 13:21):

the alternative is to produce goals that look like `_ = eq.rec _ _`

, and leave it to the user to deal with the `eq.rec`

instead of the `heq`

.

#### Chris Hughes (May 06 2020 at 13:25):

Another alternative is to not go any deeper if it's going to make an `heq`

goal.

#### Chris Hughes (May 06 2020 at 13:26):

But it should check if it can apply `heq_of_eq`

to the new `heq`

goal.

#### Chris Hughes (May 06 2020 at 13:28):

Or you could give theorems of the form `A = B -> equiv (F A) (F B)`

an attribute and use the equiv to state the `heq`

goal.

#### Johan Commelin (May 06 2020 at 13:59):

:up: something like what Chris is suggesting sounds good.

#### Mario Carneiro (May 06 2020 at 14:22):

I don't know when this is ever actually a good proof strategy though. I like the idea of `congr`

just giving up and falling back to a stricter version if it can't get rid of the `heq`

s, but these pathover style goals are just an indication that you've messed up

#### Mario Carneiro (May 06 2020 at 14:23):

Another possibility is to produce an equality of dependent pairs. This is the most concise way I know to represent an equality of telescopes (dependent values), but it only yields one subgoal and in a sense you can say it hasn't made progress

#### Mario Carneiro (May 06 2020 at 14:26):

also, the proposed fallback doesn't really work either. Either the first argument is defeq so congr will automatically make an eq on the second argument, or the first argument is not defeq in which case congr can't do anything. (It can't apply the stricter congruence lemma because the first arguments are not defeq). So really the only alternative is to fail outright

#### Sebastien Gouezel (May 06 2020 at 14:27):

I use several times the "`congr`

to break a dependent pair, and then get rid of the `heq`

using another lemma" approach in #2513. If `congr`

stopped working in this kind of situation things would be much more cumbersome.

#### Sebastien Gouezel (May 06 2020 at 14:29):

See around https://github.com/leanprover-community/mathlib/blob/429356860f556eaeff04f0aa00d47d530ff3ffed/src/analysis/analytic/composition.lean#L1122 for instance

#### Mario Carneiro (May 06 2020 at 14:29):

I'm not sure how useful it would be, but one option is to have `f x y = f z w`

become `|- x = y`

and `h : x = y |- f x y = f z w`

, with the second goal only generated if it's masking some heqs

#### Mario Carneiro (May 06 2020 at 14:30):

of course this is just `have`

, but `congr`

is doing the dirty work to find out what the right assumption is

#### Johan Commelin (May 06 2020 at 14:36):

Right, I want `congr`

to do some dirty work

#### Mario Carneiro (May 06 2020 at 14:41):

Actually, congr can do a bit better on the second goal. If `x`

or `y`

is a variable, or if it can be generalized to a variable without making the goal type incorrect, then it can generalize and then subst that side, resulting in a goal `|- f x z = f x w`

, and it can then try to do `congr`

again, presumably progressing to `|- z = w`

as desired

#### Mario Carneiro (May 06 2020 at 14:49):

Where it gets interesting is when both `x`

and `y`

are complicated terms and `f`

also contains references to subterms of it. For example, maybe `f : \forall n, fin (g n) -> A`

, `g h : nat -> nat`

, and `g (h x)`

is defeq to `x`

, and you want to prove `x y : nat, z : fin x, w : fin y |- f (h x) z = f (h y) w`

, assuming `x = y`

is provable.

Here if we apply `congr 1`

once we get the first subgoal `h x = h y`

, but it will not help us to solve the second goal `z : fin x, w : fin y, h' : h x = h y |- f (h x) z = f (h y) w`

because we need to subst using `x = y`

instead.

#### Mario Carneiro (May 06 2020 at 15:08):

Here's an idea: We know that at minimum, to solve this goal we have to prove `h x = h y`

(the first components are equal) and `fin x = fin y`

(the second components must be heq meaning that their types must be equal). If we assume that type constructors are essentially injective, we can simplify the second goal to `x = y`

WLOG, which is the equality we want.

In general, when we get a heq goal, we compute the types of the two sides and apply congr recursively on any equality of types until we either reach an equality involving a variable, or we get an equality of non-types. Together with the equalities of nondependent arguments, this produces a whole bunch of equalities, some of which probably follow from others. In the example, we would congr `fin x = fin y`

because it is an equality of types, so we would end up with `h x = h y`

from the first argument and `x = y`

from the second. We can use some heuristic to try to prove one from the other, discharging `h x = h y`

, and so at the first level congr has decided to pass `|- x = y`

back to the user, and `x = y |- f (h x) z = f (h y) w`

can be successfully subst'd, so the problem is reduced to `z w : fin x |- f (h x) z = f (h x) w`

, and congr recurses to the next level. Now it is easy, and congr will pass back `z w : fin x |- z = w`

as the second subgoal.

#### Johan Commelin (May 06 2020 at 15:16):

Sounds good!

Last updated: Aug 03 2023 at 10:10 UTC