Zulip Chat Archive

Stream: new members

Topic: Unfolding creates now hypothesis


view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:26):

Why does unfold create new hypothesis?

import group_theory.quotient_group

variables {α : Type} [group α] {s : set α} [is_subgroup s]

def r (a b : α) : Prop := a⁻¹ * b  s

example {a b : quotient_group.quotient s} : a = b :=
begin
  unfold quotient_group.quotient at a b,
  sorry
end

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:31):

because the goal depends on a and b

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:32):

When simp runs on the reverted version of the goal, it can't rewrite inside the binder domain

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:32):

Use dunfold

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:38):

Interesting.

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:39):

Also on (d)unfold/(d)simp, how can I unfold setoid.r on the goal setoid.r (quotient.out' a) (quotient.out' b) (the goal at sorry).

import group_theory.quotient_group

variables {α : Type} [group α] {s : set α} [is_subgroup s]

def r (a b : α) : Prop := a⁻¹ * b  s

example {a b : quotient_group.quotient s} : a = b :=
begin
  rw [a.out_eq', b.out_eq'],
  apply quotient.sound',
  sorry
end

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:40):

I know that setoid.r = r defined above (it is how its defined in group_theory.quotient_group and would like to leverage that fact.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:42):

do you want the r you defined or the one in quotient_group?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:43):

you can always force it with change

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:44):

I don't seem to be able to use change. change r a.out' b.out' nor change setoid.r a.out' b.out' work.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 22:45):

I've found it frustrating in the past that sometimes one can't just say "unfold this relation". You can use set instead of let to unfold a definitional let but there's no analogue here

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:45):

  change @r _ _ s _ (quotient.out' a) (quotient.out' b),

works

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 22:45):

Sometimes simp only [setoid.r] works

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:46):

Mario Carneiro said:

  change @r _ _ s _ (quotient.out' a) (quotient.out' b),

works

Omg, you are a wizard. :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:46):

it is complicated here because it's not actually a simple unfold, r is not involved in the definition at all

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:46):

That sure is quite the work around (although not really), I would have taken a long while to figure it out myself, thanks!

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:47):

(Maybe making this whole ordeal less opaque would be good. It is not clear at all that this was even possible after a lot of messing around with unfold and simp.)

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:48):

What I actually did was change r _ _, but that didn't work until I did change _ ∈ _, change r _ _, which yields a is_subgroup s subgoal. So apparently it can't figure out the implicit arguments to r without help

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:48):

Wow, that is amazing!

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:48):

which makes sense, because r doesn't have anything in its type that would help infer s

view this post on Zulip Pedro Minicz (Jun 12 2020 at 22:49):

Thank you for explaining your thought process. I just started using change earlier today actually (but I remember someone mentioning in another thread a while ago) and am not very good at it. :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:50):

when in doubt, use lots of underscores :grinning:

view this post on Zulip Mario Carneiro (Jun 12 2020 at 22:53):

I think it helps to know that there is always the fallback of being completely explicit and providing a fully elaborated term. That will always work unless the kernel is broken, so it's really a matter of inserting more implicit info until it works and then scaling back until you have just enough for lean to close the distance

view this post on Zulip Eric Wieser (Jul 29 2020 at 16:51):

(deleted)

view this post on Zulip Eric Wieser (Jul 29 2020 at 16:53):

(sorry, caught out by zulip's filtered search)


Last updated: May 14 2021 at 07:19 UTC