Finset.instRepr

Stream: new members

[Violeta Hernández]

What is this sorcery? docs#Finset.instRepr

[Violeta Hernández]

Surely it should be impossible to consistently print a Finset without having some extra structure like a linear order? And why is this unsafe?

[Violeta Hernández]

Is it somehow looking inside the quotient?

[Violeta Hernández]

Oh apparently the magic is happening at docs#Multiset.instRepr

[Violeta Hernández]

Oh here it is docs#Quot.unquot

[Violeta Hernández]

I guess my new question is, why does Lean allow this? Surely you can easily prove False by using this

[Violeta Hernández]

Does it count as using new axioms?

[Yakov Pechersky]

You can't prove things about unsafe

[Yakov Pechersky]

It works exactly how Quot.unquot describes. The quotient, computationally, still holds the unquotiented value in the VM. So we can repr the finset by printing the list that is wrapped.

[Yakov Pechersky]

A related question is, well, if quotient values are really the underlying base types underneath, wouldn't it be possible to sniff out if two quotients' representatives are _really_ equal by a timing attack, if evaluating the relation is faster in the equality case?

[Daniel Weber]

It seems like it should definitely be possible, yes. Isn't that the expected behaviour?

[Kyle Miller]

In general, even if x = y, the running times for #eval x and #eval y can be very different.