## Stream: maths

### Topic: making an equiv

#### Ali Sever (Sep 07 2018 at 19:21):

I have f : α → α → α → α → α → α → Prop that says a ≠ b ∧ c ≠ b ∧ d ≠ e ∧ f ≠ e ∧ blah. I have shown fis reflexive, symmetric and transitive (i.e. an equiv on α × α × α), but only when a ≠ b ∧ c ≠ b. Now I want to make the equiv classes, I'm having trouble with deciding what to do.
If I set f to take a random value for a = b, then working with fis going to be annoying. If I make the equiv on α × α × α such that a ≠ b ∧ c ≠ b, then any time I talk about the class a b c I have to give proofs of a ≠ band c ≠ b. Is there different method?

In GeoCoq they cheat, instead of making an equiv, they make a new function (which is what the book does too),

Definition Q_CongA a :=
∃ A B C,
A ≠ B ∧ C ≠ B ∧ ∀ X Y Z, CongA A B C X Y Z ↔ a X Y Z.


#### Chris Hughes (Sep 07 2018 at 19:33):

You could define the equivalence relation on the subtype. It sounds like you just have to give proofs that a \ne b and stuff. Lean is all about edge cases. Why do you consider the GeoCoq solution cheating? You can define quotients on non-equivalence relations in lean, but it's not recommended.

#### Ali Sever (Sep 08 2018 at 08:21):

I want to define a function from an equivalence class, but to give the value I first need an element from the class (but every element gives the same result), how would I do this? i.e. I want to make a function which I know is well-defined

#### Reid Barton (Sep 08 2018 at 08:24):

Assuming you're using quot/quotient, then quot.lift/quotient.lift

#### Kevin Buzzard (Sep 08 2018 at 10:26):

Ali I don't know if this helps, but when Luca was learning about equivalence classes (because he wanted to define a group structure on pi_1(X,x), which is a quotient) I wrote https://github.com/kbuzzard/xena/blob/master/xenalib/m1f/zmod37.lean to show him some basic tricks. For basic questions like how to define a function on a set of equivalence classes I could recommend the relevant docs https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients from TPIL, however mathlib adds extra functions which one can use with quotients, and these are not documented here. The mathlib file is here https://github.com/leanprover/mathlib/blob/master/data/quot.lean and it defines things such as quotient.eq which are very useful in practice.

#### Ali Sever (Sep 08 2018 at 14:44):

Thanks, I was reading up on these this morning. I don't think there's a way to use the "cheat" method Coq uses (above), because I can't use exists to eliminate into something that isn't Prop.

#### Ali Sever (Sep 09 2018 at 12:59):

is there a way to do quot.lift on a set with a function that is constant over the set?

#### Chris Hughes (Sep 09 2018 at 13:03):

You mean a computable function from set \a that's based on some arbitrary element of a set?

#### Chris Hughes (Sep 09 2018 at 13:03):

The answer is probably no, because a set contains no computational content about it's elements.

#### Ali Sever (Sep 09 2018 at 13:05):

Why does it work for quotient sets, but not just normal sets?

#### Kevin Buzzard (Sep 09 2018 at 13:07):

Why don't you formalise exactly what you're asking in Lean and post it? It's good practice, and also good practice.

#### Ali Sever (Sep 09 2018 at 13:19):

Something like this,
def F {α β : Type} (A : set α) (f : α → β) : (∀ a b, a ∈ A → b ∈ A → f a = f b) → β := x

#### Johannes Hölzl (Sep 09 2018 at 13:26):

This is not enough. You need to assume that A is not empty.

#### Johannes Hölzl (Sep 09 2018 at 13:27):

Then you can use some form of choice. (or you know that β is not empty and chose a default element.

#### Reid Barton (Sep 09 2018 at 13:28):

Or if you express the nonempty condition as trunc A, which is the quotient of A by the relation which identifies everything, then you can define F (computably) using quotient.lift.

#### Reid Barton (Sep 09 2018 at 13:29):

If you use choice, then you don't even need the condition (∀ a b, a ∈ A → b ∈ A → f a = f b) to define F, which is mildly alarming, but you do need it to prove that F equals f a for any a ∈ A.

#### Ali Sever (Sep 09 2018 at 13:34):

If I use trunc, will it be annoying to switch between A and trunc A?

#### Reid Barton (Sep 09 2018 at 13:47):

Well trunc A is an alternative to nonempty A, which you would need instead.
The main annoyance of trunc A is that it isn't a proposition.

#### Kevin Buzzard (Sep 09 2018 at 13:50):

Something like this,
def F {α β : Type} (A : set α) (f : α → β) : (∀ a b, a ∈ A → b ∈ A → f a = f b) → β := x

You mean := sorry? As others have pointed out this can't yet be done (alpha and beta could both be empty at this point). So in some sense you still haven't asked the question.

#### Ali Sever (Sep 09 2018 at 13:58):

I guess I'll have to try a different approach

#### Kevin Buzzard (Sep 09 2018 at 14:04):

I'm not saying that any approach doesn't work, but I am saying that I've learnt from experience that actually formalising my question precisely as definition : blah := sorry or theorem : blah := sorry really helps me to understand what I am asking before I ask it.

Last updated: May 12 2021 at 07:17 UTC