Zulip Chat Archive

Stream: new members

Topic: Guide to using setoid


Robert Maxton (Apr 11 2022 at 09:08):

Is there a comprehensive-ish tutorial on using setoid in specific written somewhere? There's one section on it in Theorem Proving in Lean I found, but it doesn't go into much detail and I'm having a lot of trouble actually using it in practice.

Kevin Buzzard (Apr 11 2022 at 09:43):

Here's what I wrote about them for my recent course https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_A/section06quotients/quotients.html and here are the associated exercises https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/tree/master/src/section06quotients

Robert Maxton (Apr 11 2022 at 09:47):

thanks!

Kevin Buzzard (Apr 11 2022 at 09:52):

There's also a file on quotient groups in the outtakes directory which I never got into good shape because it uses the quotient' trick which i didn't explain

Robert Maxton (Apr 11 2022 at 09:55):

hmmm
so my question in particular is, say I define the alias

def int := quotient int.setoid

(having already done the setoid setup above)

Robert Maxton (Apr 11 2022 at 09:56):

I now define a bunch of theorems and instances and so on using int, in particular, say, has_neg int and has_zero int

Riccardo Brasca (Apr 11 2022 at 09:57):

If you write a #mwe it will be easier for everyone to answer your question.

Robert Maxton (Apr 11 2022 at 09:57):

Lean doesn't seem to then pass this on to things of the form ⟦.⟧ , complaining things like failed to synthesize type class instance for failed to synthesize type class instance for ⊢ has_zero (quotient int.setoid)

Robert Maxton (Apr 11 2022 at 09:57):

hmmm, this time I maybe can

Robert Maxton (Apr 11 2022 at 09:58):

a decent chunk of my current problems are partially due to the length of this file -_-

Robert Maxton (Apr 11 2022 at 10:08):

here

Robert Maxton (Apr 11 2022 at 10:08):

import tactic tactic.basic

namespace peano

def eqv (a b :  × ) := a.1 + b.2 = b.1 + a.2

theorem eqv.refl (a) : eqv a a := by tauto
theorem eqv.symm (a b) : eqv a b  eqv b a :=
    by {repeat {rw eqv}, tauto}
theorem eqv.trans (a b c) : eqv a b  eqv b c  eqv a c :=
  assume A B,
  begin
    rw eqv at *, linarith,
  end

theorem eqv_is_eqv : equivalence eqv :=
  mk_equivalence eqv eqv.refl eqv.symm eqv.trans

instance int.setoid : setoid (nat × nat) :=
      setoid.mk eqv eqv_is_eqv

def int := quotient int.setoid

def int.mk (p m: nat) : int := (p, m)

namespace int
  instance : has_zero int := (0, 0)
end int

variables {a b c d: }

lemma foo : (c, d) = 0 := sorry

end peano

Robert Maxton (Apr 11 2022 at 10:10):

Lean complains at

failed to synthesize type class instance for
c d : 
 has_zero (quotient int.setoid)

at ⟦(c, d)⟧ = 0

Riccardo Brasca (Apr 11 2022 at 10:13):

I think you can write lemma foo : ⟦(c, d)⟧ = (0 : int) := sorry

Robert Maxton (Apr 11 2022 at 10:15):

hmmm
so you can, thanks

Robert Maxton (Apr 11 2022 at 10:15):

that said, I'm still generally just drowning in unfolds trying to work with these things

Riccardo Brasca (Apr 11 2022 at 10:16):

I am not sure, but also

@[reducible]
def int := quotient int.setoid

should work.

Robert Maxton (Apr 11 2022 at 10:16):

I'm getting the impression that you're "supposed" to just use quot.out pretty early to get to the underlying representation, at least for low-level stuff, but I'm trying not to because I'm trying to follow a book on axiomatizations/reverse mathematics and I'd rather not invoke choice so early in the game lol

Robert Maxton (Apr 11 2022 at 10:17):

Riccardo Brasca said:

I am not sure, but also

@[reducible]
def int := quotient int.setoid

should work.

ahhh, that helps a lot

Robert Maxton (Apr 11 2022 at 10:17):

thanks muchly

Riccardo Brasca (Apr 11 2022 at 10:17):

The problem is that you provided an instance of has_zero to int, that it defined to be quotient int.setoid, but Lean doesn't unfold it.

Robert Maxton (Apr 11 2022 at 10:17):

that does work

Robert Maxton (Apr 11 2022 at 10:18):

hmm

Robert Maxton (Apr 11 2022 at 10:18):

so when should I be marking things reducible?

Riccardo Brasca (Apr 11 2022 at 10:21):

I would say that the correct thing to do is the opposite: provide a good API, and then mark the definition irreducible.

Eric Wieser (Apr 11 2022 at 10:26):

Robert Maxton said:

that said, I'm still generally just drowning in unfolds trying to work with these things

Can you give an example?

Robert Maxton (Apr 11 2022 at 10:33):

why the thumbsdown :(

Robert Maxton (Apr 11 2022 at 10:33):

uh, lemme see

Robert Maxton (Apr 11 2022 at 10:35):

Riccardo Brasca said:

I would say that the correct thing to do is the opposite: provide a good API, and then mark the definition irreducible.

er
but then I end up having to constantly switch between quot.mk and my actual type to do anything

Robert Maxton (Apr 11 2022 at 10:39):

Eric Wieser said:

Robert Maxton said:

that said, I'm still generally just drowning in unfolds trying to work with these things

Can you give an example?

for example

add as setup

private def neg_int_pair (a : nat × nat) := (a.2, a.1)
private lemma neg_respects_eqv (a₁ a₂ : nat × nat):
  a₁  a₂  neg_int_pair a₁ = neg_int_pair a₂ :=
assume h_eqv,
begin
  unfold has_equiv.equiv eqv neg_int_pair at *,
  apply quot.sound, unfold setoid.r eqv at *, dsimp only, cc
end

namespace int
  def neg: int  int :=
    quotient.lift neg_int_pair neg_respects_eqv

  instance : has_neg int := neg
end int

Robert Maxton (Apr 11 2022 at 10:40):

you already can see the unfold <three or four things>, apply quot.sound, unfold <more things>, dsimp pattern I resort to a lot in order to get at the underlying representation

Robert Maxton (Apr 11 2022 at 10:41):

I realize that largely that defeats the purpose, which is why I'm trying to prove a few basic principles about add and neg and sub so I can stop doing that

Robert Maxton (Apr 11 2022 at 10:41):

anyway, I then have a helper lemma

  lemma int.neg_mk : -⟦(ap, am) = (am, ap) :=
    begin
      unfold quotient.mk has_neg.neg int.neg quotient.lift,
      rw neg_int_pair, unfold quotient.mk,
    end

Robert Maxton (Apr 11 2022 at 10:42):

which is reasonably short, but is also pretty much literally nothing but unfolds
and unfold_projs won't do it all for me

Yaël Dillies (Apr 11 2022 at 10:45):

Doesn't lemma int.neg_mk : -⟦(ap, am)⟧ = ⟦(am, ap)⟧ := rfl work?

Robert Maxton (Apr 11 2022 at 10:48):

hmmm
well, a), apparently not
but b) even if it did, it wouldn't help me in more complex cases where I actually need to do work after unfolding everything down to the underlying equivalence

Eric Wieser (Apr 11 2022 at 11:06):

Thumbs down was for "supposed to invoke choice", that usually just results in you having to work harder to prove the same thing that lift already asked for in the first place.

Robert Maxton (Apr 11 2022 at 11:11):

fair enough, guess I just misread it lol

Robert Maxton (Apr 11 2022 at 11:12):

but in this case, for example, it's not like a = -a ↔ a = 0 follows from the well-definedness of neg alone, I need to actually go digging into how neg works on the underlying representation, I think?

Mario Carneiro (Apr 11 2022 at 11:13):

Rather than unfolding everything, if you want to get at the underlying relation then state it as a lemma

Eric Wieser (Apr 11 2022 at 11:13):

If you're unfolding the same thing over and over again, it means you're missing a lemma

Eric Wieser (Apr 11 2022 at 11:13):

This is the lemma you're missing:

@[simp] lemma equiv_iff {a b : nat × nat} : a  b  a.1 + b.2 = b.1 + a.2 := iff.rfl

Eric Wieser (Apr 11 2022 at 11:14):

(in addition to the int.neg_mk above, which is also a good lemma)

Mario Carneiro (Apr 11 2022 at 11:14):

^ this, although I would write it for [(a, b)] = [(c, d)] instead

Mario Carneiro (Apr 11 2022 at 11:15):

same thing for -[(a, b)] = [(b, a)] for unfolding the definition of -

Eric Wieser (Apr 11 2022 at 11:16):

Probably you want both, since my version lets you get rid of any equivs that pop up while using quotient.lift or quotient.map

Mario Carneiro (Apr 11 2022 at 11:16):

with just a few things like that as simp lemmas you can demolish most goals about associativity or whatever using simp

Eric Wieser (Apr 11 2022 at 11:18):

Yaël Dillies said:

Doesn't lemma int.neg_mk : -⟦(ap, am)⟧ = ⟦(am, ap)⟧ := rfl work?

Robert Maxton said:

hmmm
well, a), apparently not

This works as long as int is reducible. If you choose not to make int reducible, then you can't use ⟦⟧ anywhere

Robert Maxton (Apr 11 2022 at 11:19):

hm
works in my mwe but not in my original, even though it's marked reducible in both places

Mario Carneiro (Apr 11 2022 at 11:20):

semireducible (aka default) should suffice

Robert Maxton (Apr 11 2022 at 11:20):

empirically it doesn't, though I'm starting to suspect the size of this file is getting in the way of things

Robert Maxton (Apr 11 2022 at 11:21):

also related to the above, but if I prove a bunch of things about things of the form [(a, b)], they don't seem to play nice when I then pass in ints instead, I think
though I will double check in a bit

Mario Carneiro (Apr 11 2022 at 11:21):

those lemmas won't trigger if you put in ints, and this is deliberate

Mario Carneiro (Apr 11 2022 at 11:22):

so e.g. [(a, b)] + c won't reduce

Mario Carneiro (Apr 11 2022 at 11:24):

Another thing you should do to avoid weird type inference is to explicitly redefine quotient.mk for your particular quotient and give it the right type. In this case it would be def int.mk (a b : nat) : int := [(a, b)]

Mario Carneiro (Apr 11 2022 at 11:24):

and then all of the theorems mentioned above should use int.mk instead of [(a, b)]

Robert Maxton (Apr 11 2022 at 11:25):

.... so, uh, never actually use the convenient [.] syntax?
that seems... disappointing >.>

Mario Carneiro (Apr 11 2022 at 11:25):

and you have simp lemmas like [(a, b)] = int.mk a b to make sure that any occurrences of the quotient that accidentally pop up are removed

Mario Carneiro (Apr 11 2022 at 11:25):

you can add a notation for int.mk if you want

Robert Maxton (Apr 11 2022 at 11:27):

Mario Carneiro said:

so e.g. [(a, b)] + c won't reduce

but I would like to rise above the level where I'm constantly referring back to the underlying representation someday, and that means I need to be able to write "axioms" (quote-unquote, since I'm proving them) that rely on that representation, but can be used by outside functions that only pass in black-boxed ints

Mario Carneiro (Apr 11 2022 at 11:27):

the problem with the [.] syntax is that it has type quotient <stuff>, which means that if you write [(0, 0)] = 0 then the 0 on the right will be looking for has_zero (quotient <stuff>) which is bad

Mario Carneiro (Apr 11 2022 at 11:29):

the lemmas I've been talking about, like -mk a b = mk b a, are lemmas to help you prove theorems about the int functions you actually care about like -(-a) = a

Mario Carneiro (Apr 11 2022 at 11:29):

the proof method for all of these is to use quotient.induction to replace a with int.mk x y and then simp

Kevin Buzzard (Apr 11 2022 at 11:34):

Note that I don't use unfold once in my exposition of how to make int from nat x nat here. I do however write a bunch of helper lemmas such as

def R (ab cd :  × ) : Prop :=
ab.1 + cd.2 = ab.2 + cd.1

lemma R_def (ab cd :  × ) :
R ab cd  ab.1 + cd.2 = ab.2 + cd.1 :=
begin
  sorry
end

lemma R_def' (a b c d : ) :
R (a, b) (c, d)  a + d = b + c :=
begin
  sorry
end

...

instance : has_zero myint :=
{ zero := (0,0) }

@[simp] lemma zero_def : (0 : myint) = (0, 0) :=
begin
  sorry
end

...

Kevin Buzzard (Apr 11 2022 at 11:35):

(I should think all the proofs are refl)

Robert Maxton (Apr 11 2022 at 11:57):

I do not seem to be getting anywhere near as much use out of refl as any of you do :v

Robert Maxton (Apr 11 2022 at 11:57):

admittedly, this is probably in large part because I also rewrote nat and therefore do not have quite so optimized a set of simp lemmas

Robert Maxton (Apr 11 2022 at 11:58):

I was originally planning on just implementing the entire book from scratch but at this rate I may end up just switching to existing libraries after I "re-implement" them

Yaël Dillies (Apr 11 2022 at 12:03):

You reimplemented nat? :fear: That should definitely have been part of your #mwe!

Reid Barton (Apr 11 2022 at 12:05):

Note that you would have the same issues with type classes if you defined something like def complex := real \x real

Robert Maxton (Apr 11 2022 at 12:13):

Yaël Dillies said:

You reimplemented nat? :fear: That should definitely have been part of your #mwe!

... I mean, at that point, it stops being a #mwe and starts being "here is the entirety of my code", though?

Robert Maxton (Apr 11 2022 at 12:14):

that's kind of the issue I've been having, really, is that since I reimplemented everything from scratch it's hard to isolate things into an #mwe, so I just end up asking very vague general-practice questions instead

Robert Maxton (Apr 11 2022 at 12:15):

like if you don't mind looking through my ~1k lines of code then yay, but I don't really expect that of random people on the internet :p

Reid Barton (Apr 11 2022 at 12:17):

Anyways, refl doesn't depend on what simp lemmas you wrote or didn't write.

Robert Maxton (Apr 11 2022 at 12:28):

Huh. Good to know

Jake Levinson (Apr 12 2022 at 18:29):

Robert Maxton said:

Yaël Dillies said:

You reimplemented nat? :fear: That should definitely have been part of your #mwe!

... I mean, at that point, it stops being a #mwe and starts being "here is the entirety of my code", though?

I suspect that reimplementing basic stuff can lead to weird situations like this, where each definition in mathlib already has a bunch of layers of lemmas to smooth out (e.g.) intermediate facts between an underlying representation and the intended usage.

You might be reimplementing the basics in order to learn about writing math in Lean -- I did some of that myself last year. But at the same time you're (unwittingly) forcing yourself to deal with a bunch of core type theory design choices, which might turn out to be subtler than you expect. For example, Mario's advice about defining int.mk and writing all subsequent theorems with int.mk instead of simply quotient.mk.

At least when I tried this, I eventually decided to approach reimplementing the basics with the mindset of "I'll push this as far as it goes but won't be surprised if I get stuck at some (early) point". I still found it to be a helpful exercise though!


Last updated: Dec 20 2023 at 11:08 UTC