dcongr

Stream: general

[Johan Commelin]

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]

what do you want the theorem to say?

[Scott Morrison]

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]

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

[Chris Hughes]

But it should check if it can apply heq_of_eq to the new heq goal.

[Chris Hughes]

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]

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

[Mario Carneiro]

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 heqs, but these pathover style goals are just an indication that you've messed up

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

of course this is just have, but congr is doing the dirty work to find out what the right assumption is

[Johan Commelin]

Right, I want congr to do some dirty work

[Mario Carneiro]

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]

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]

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]

Sounds good!