heq hell again

Stream: general

[Patrick Massot]

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]

Does this lemma help?

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

[Patrick Massot]

YES!

[Patrick Massot]

Can you explain what's going on here?

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

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

[Patrick Massot]

not quite

[Patrick Massot]

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]

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]

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

[Simon Hudon]

@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]

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]

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

[Patrick Massot]

What is a local constant?

[Simon Hudon]

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

[Chris Hughes]

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

[Reid Barton]

"something you could substitute something else for"

[Patrick Massot]

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

[Mario Carneiro]

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

[Chris Hughes]

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]

Also, rcases e with rfl will do subst on terms

[Patrick Massot]

What?!

[Mario Carneiro]

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

[Patrick Massot]

All this becomes more and more obscure to me

[Mario Carneiro]

it's super useful to use rfl in rcases patterns

[Mario Carneiro]

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]

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]

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]

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

[Patrick Massot]

I think I need to see examples to understand this

[Patrick Massot]

I have no idea where to start

[Kevin Buzzard]

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]

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]

Yes I just went back to that thread.

[Andrew Ashworth]

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]

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]

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

[Kevin Buzzard]

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