problem using quot.exists_rep

Stream: general

[Bernd Losert]

I'm trying to get the following to work:

constants G α : Type*
constants r : G × α → G × α → Prop
constant q : quot r

def foo : ℕ := let ⟨⟨b, x⟩, heq⟩ := quot.exists_rep q in 2

It complains saying

'Exists.dcases_on' can only eliminate into Prop

I'm not sure what to do here. Any tips?

[Yaël Dillies]

You should either use docs#quot.out or first define a map to G × α and then show it respects the quotient, so that it lifts to a map to quot r.

[Bernd Losert]

Let me try quot.out.

[Bernd Losert]

That works, but now I see another problem since I am trying to use this to make a has_scalar instance.

[Bernd Losert]

I guess I have to do it the longer way.

[Yaël Dillies]

Yeah, it will be cleaner. I guess you'll have to prove it respects the quotient at some point anyway.

[Bernd Losert]

Thanks.

[Kevin Buzzard]

@Bernd Losert the "mathematician's approach" of defining a function from a quotient by "lift arbitrarily to the bigger type and then apply another function" is not idiomatic Lean. The thing to use is quotient.lift and I just wrote something about this for my course. The reason the quotient.lift approach is better because of the punchline -- the very last line I wrote.

[Bernd Losert]

I see what you mean. In my work, the quotient is so obvious, it seems silly to check that it respects equivalance.

[Bernd Losert]

In the proof, I have to do a whole bunch of unfoldings (6 to be exact), in order to get back to the def defining the relation and then start simplying. Is there a tactic that will simplify things until it hits the definition of the relation?

[Yaël Dillies]

You can use change to give directly the form of what you need.

[Bernd Losert]

First time using change. Let's see if I can make it work.

[Bernd Losert]

Ah, it works pretty nicely. Cool. Thanks again.

[Kevin Buzzard]

My instinct is that you should be writing API to do this rather than using change. For example in the Lean code which went with the course notes I mentioned earlier I do things like this and this because rewriting is a lot less hassle than change especially when you don't want to write down terms in full.

[Yaël Dillies]

It's good to know that you can put underscores in a change expression.

[Ruben Van de Velde]

Kevin Buzzard said:

I just wrote something about this for my course.

Typo at the link: octonians

[Bernd Losert]

Yeah, if I see myself using the same sort of change repeatedly, I'll write a def to make it easier.