## Stream: general

### Topic: heq hell again

#### 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

#### 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

YES!

#### Patrick Massot (Oct 09 2018 at 16:10):

Can you explain what's going on here?

#### Patrick Massot (Oct 09 2018 at 16:10):

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

#### 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!

#### 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 α)

#### 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.

#### Chris Hughes (Oct 09 2018 at 16:23):

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

not quite

#### 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

#### 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.

#### Reid Barton (Oct 09 2018 at 18:23):

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

#### 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

#### 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

#### Patrick Massot (Oct 09 2018 at 18:29):

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

#### Patrick Massot (Oct 09 2018 at 18:33):

What is a local constant?

#### Simon Hudon (Oct 09 2018 at 18:36):

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

#### 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 α

#### Reid Barton (Oct 09 2018 at 18:36):

"something you could substitute something else for"

#### Patrick Massot (Oct 09 2018 at 18:37):

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

#### 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

#### 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.

#### Mario Carneiro (Oct 09 2018 at 18:41):

Also, rcases e with rfl will do subst on terms

What?!

#### Mario Carneiro (Oct 09 2018 at 18:41):

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

#### Patrick Massot (Oct 09 2018 at 18:41):

All this becomes more and more obscure to me

#### Mario Carneiro (Oct 09 2018 at 18:41):

it's super useful to use rfl in rcases patterns

#### 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)

#### 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

#### 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

#### Mario Carneiro (Oct 09 2018 at 18:45):

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

#### Patrick Massot (Oct 09 2018 at 18:47):

I think I need to see examples to understand this

#### Patrick Massot (Oct 09 2018 at 19:05):

I have no idea where to start

#### 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?

#### 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.

#### Kevin Buzzard (Oct 09 2018 at 19:20):

Yes I just went back to that thread.

#### 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

#### 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

#### Kenny Lau (Jun 10 2019 at 11:26):

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

#### 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