Zulip Chat Archive

Stream: general

Topic: strange [ ]'s in my goal


view this post on Zulip Kevin Buzzard (Apr 21 2019 at 04:49):

1 goal
A : Huber_pair,
v : Spv ↥A,
hv : v ∈ Spa A
⊢ [comm_ring.zero (ring_completion.comm_ring (valuation_field (out (⟨v, hv⟩.val))))] =
    [domain.zero division_ring.to_domain]

Where did those square brackets come from? They're there whether or not I have notation on.

view this post on Zulip Mario Carneiro (Apr 21 2019 at 04:50):

That's the projection macro, you probably unfolded something you shouldn't have

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 04:52):

Yeah, I was trying to get to the bottom of things.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 04:52):

I was using delta :-)

view this post on Zulip Keeley Hoek (Apr 21 2019 at 04:53):

Is that something unfold_projs can fix

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 04:59):

I decided to take a different route. I'll go back and take a look.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:01):

unfold_projs failed to simplify
state:
A : Huber_pair,
v : Spv A,
h1 : is_continuous v,
h2 :  (r : A), r  (λ (A : Huber_pair), A.Rplus) A  v r  1
 [comm_ring.zero (ring_completion.comm_ring (valuation_field (out v)))] =
    [discrete_field.zero (completable_top_field.discrete_field (valuation_field (out v)))]

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:01):

They are a dead end for me.

view this post on Zulip Keeley Hoek (Apr 21 2019 at 05:01):

ok :'(

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:02):

Is it likely that, if what I'm trying to prove is provable (possibly noncomputably), then there will be a proof which avoids those weird square brackets? Do I ever have to deal with them as an end user?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:05):

It is possible to unfold them to a comm_ring.rec application, but it's a sign that you are unfolding things that you shouldn't

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:05):

you should not ever have to see them as an end user

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:06):

I assume rfl doesn't work?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 05:07):

you can always use change to say what the zero is

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:07):

I assume rfl doesn't work?

That's right -- that's what I'm trying to debug.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 05:07):

The zero is some gigantic term when I unfold it.


Last updated: May 11 2021 at 00:31 UTC