Unfolding creates now hypothesis

Stream: new members

[Pedro Minicz]

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

[Mario Carneiro]

because the goal depends on a and b

[Mario Carneiro]

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

[Mario Carneiro]

Use dunfold

[Pedro Minicz]

Interesting.

[Pedro Minicz]

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

[Pedro Minicz]

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.

[Mario Carneiro]

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

[Mario Carneiro]

you can always force it with change

[Pedro Minicz]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

works

[Kevin Buzzard]

Sometimes simp only [setoid.r] works

[Pedro Minicz]

Mario Carneiro said:

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

works

Omg, you are a wizard. :grinning_face_with_smiling_eyes:

[Mario Carneiro]

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

[Pedro Minicz]

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

[Pedro Minicz]

(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.)

[Mario Carneiro]

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

[Pedro Minicz]

Wow, that is amazing!

[Mario Carneiro]

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

[Pedro Minicz]

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:

[Mario Carneiro]

when in doubt, use lots of underscores :grinning:

[Mario Carneiro]

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

[Eric Wieser]

(deleted)

[Eric Wieser]

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