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 heqs, 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: Dec 20 2023 at 11:08 UTC