Zulip Chat Archive

Stream: general

Topic: heq hell again


view this post on Zulip Patrick Massot (Oct 09 2018 at 15:59):

My current goal looks like eq.mpr comm_ring._proof_2 (quotient_ring.comm_ring (closure (is_ideal.trivial α))) == quotient_ring.comm_ring (closure (is_ideal.trivial α)) I'm ready to believe this is a rightful punishment for an earlier sin, but I'd like to know whether there is any hope to escape, or I should go back and think about what I'm doing

view this post on Zulip Chris Hughes (Oct 09 2018 at 16:06):

Does this lemma help?

universe u
lemma for_patrick {α β : Sort u} (h : β = α) (x : α) : eq.mpr h x == x :=
by subst h; refl

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:07):

YES!

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:10):

Can you explain what's going on here?

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:10):

@Mario Carneiro should this be added as a simp lemma in mathlib?

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:14):

Let's see how bad things are. What I wanted to write was:

instance [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
  topological_ring (quotient (separation_setoid α)) :=
by  rw ring_sep_rel ; apply_instance

What I actually wrote (after adding Chris's simp lemma):

instance [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
  topological_ring (quotient (separation_setoid α)) :=
begin
  convert topological_ring_quotient (closure (is_ideal.trivial α)),
  { apply ring_sep_rel },
  { dsimp [topological_ring_quotient_topology, quotient.topological_space, to_topological_space],
    congr,
    apply ring_sep_rel,
    apply ring_sep_rel },
  { apply ring_sep_rel },
  { simp [uniform_space.comm_ring] },
end

Like: come one Lean: apply ring_sep_rel!

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:15):

where lemma ring_sep_rel (α) [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] : separation_setoid α = quotient_ring.quotient_rel (closure $ is_ideal.trivial α)

view this post on Zulip Chris Hughes (Oct 09 2018 at 16:18):

subst is a better version of rw, that can rw the types of proofs as well. before subst h the goal is @eq.mpr β α h x == x, after subst hthe goal is @eq.mpr β β (@eq.refl (Sort u) β) x == x, and now the types are the same on each sude of the equality, and eq.mpr can iota-reduce, since eq.refl is a constructor, so it's just refl.

The trouble with subst is it only works with local constants, so these proofs often require you to turn your goal into a lemma where you can use subst on local constants. A good version of subst that handles things other than local constants is something that needs to be written I think.

view this post on Zulip Chris Hughes (Oct 09 2018 at 16:23):

eq_rec_heq is exactly the same as the lemma I wrote by the way.

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:25):

not quite

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:43):

Chris, do you know if there is some more documentation about this magic subst? It sounds like it could be very useful. Lately I've been fighting that kind of rw issues a lot

view this post on Zulip Chris Hughes (Oct 09 2018 at 18:14):

I don't think there's any documentation. The strategy to use it is to make sure that the expression you're substituting is a local constant, and if it isn't, then make an intermediate lemma. In the example I gave, only α had to be a local constant.

view this post on Zulip Reid Barton (Oct 09 2018 at 18:23):

I always assumed subst was just induction on eq, is it actually something different?

view this post on Zulip Simon Hudon (Oct 09 2018 at 18:29):

@Reid Barton That's a useful way to see it. The thing is that by doing induction on eq, you're substitution everywhere at once so when your variable is used as a parameter for a function with a dependent type, it can help do the substitution in every term and type at once so that the goal remains type correct

view this post on Zulip Chris Hughes (Oct 09 2018 at 18:29):

Looking at the definition it appears to not be based on the induction tactic. cases also works in this example, but basically subst is for when the motive is hard to compute due to dependent arguments. The proof terms use eq.drec instead of eq.rec

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:29):

It sounds exactly like what I've needed for one week

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:33):

What is a local constant?

view this post on Zulip Simon Hudon (Oct 09 2018 at 18:36):

It's a free variable in your goal, not a definition and not a bound variable.

view this post on Zulip Chris Hughes (Oct 09 2018 at 18:36):

I think it's basically a variable in your local context, so α is, but not or f α

view this post on Zulip Reid Barton (Oct 09 2018 at 18:36):

"something you could substitute something else for"

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:37):

It's hard to see how such a restrictive condition can be satisfied

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:40):

Only one side has to be a variable. e.g. x = 1 |- P x reduces to P 1

view this post on Zulip Chris Hughes (Oct 09 2018 at 18:40):

You turn your goal into a lemma about local constants, and then substitute your expression into that lemma, like I did with for_patrick A bit messy, but reliable.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:41):

Also, rcases e with rfl will do subst on terms

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:41):

What?!

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:41):

and rcases e with <> will do cases instead, which has slightly different effects wrt unfolding

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:41):

All this becomes more and more obscure to me

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:41):

it's super useful to use rfl in rcases patterns

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:43):

If your assumption is f x = g y then it's difficult to eliminate the equality once and for all, it could make lots of things equal to other things in an unpredictable way (see: word problem)

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:43):

but when one side is a fresh variable, like x = g y, then we can just replace x with g y everywhere in the context to eliminate x

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:44):

The nice thing is that this works regardless of any dependencies, which is a big plus compared to rw with this equality everywhere

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:45):

Basically all facts about eq and heq are proved using this trick

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:47):

I think I need to see examples to understand this

view this post on Zulip Patrick Massot (Oct 09 2018 at 19:05):

I have no idea where to start

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 19:10):

Patrick I have heard Chris moaning about this heq stuff. But I have never once had to use it? Why is that? Am I avoiding a certain kind of mathematics? Why do you need it?

view this post on Zulip Reid Barton (Oct 09 2018 at 19:11):

When you didn't use the identity map as a map from F (id '' U) to F U, this is the kind of thing you avoided.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 19:20):

Yes I just went back to that thread.

view this post on Zulip Andrew Ashworth (Oct 09 2018 at 19:21):

I found a pretty good summary of all the different types of equality here: https://jozefg.bitbucket.io/posts/2014-08-06-equality.html

view this post on Zulip Patrick Massot (Oct 09 2018 at 19:21):

I have no idea what heq is. I can only tell you that when arguments of a term depend on other arguments then rw and simp often don't work. convert works but spawns heq goals. I understand nothing about Mario's explanations unfortunately

view this post on Zulip Kenny Lau (Jun 10 2019 at 11:26):

do we have some general tips to avoid heq hell? @Mario Carneiro

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 12:10):

If congr' produced them, then consider doing cases on an equality instead.


Last updated: May 14 2021 at 12:18 UTC