Guide to using setoid

Stream: new members

[Robert Maxton]

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]

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]

thanks!

[Kevin Buzzard]

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]

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]

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]

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

[Robert Maxton]

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]

hmmm, this time I maybe can

[Robert Maxton]

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

[Robert Maxton]

here

[Robert Maxton]

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]

Lean complains at

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

at ⟦(c, d)⟧ = 0

[Riccardo Brasca]

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

[Robert Maxton]

hmmm
so you can, thanks

[Robert Maxton]

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

[Riccardo Brasca]

I am not sure, but also

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

should work.

[Robert Maxton]

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]

Riccardo Brasca said:

I am not sure, but also

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

should work.

ahhh, that helps a lot

[Robert Maxton]

thanks muchly

[Riccardo Brasca]

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]

that does work

[Robert Maxton]

hmm

[Robert Maxton]

so when should I be marking things reducible?

[Riccardo Brasca]

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

[Eric Wieser]

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]

why the thumbsdown :(

[Robert Maxton]

uh, lemme see

[Robert Maxton]

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]

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]

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]

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]

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]

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]

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

[Robert Maxton]

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]

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]

fair enough, guess I just misread it lol

[Robert Maxton]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

semireducible (aka default) should suffice

[Robert Maxton]

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

[Robert Maxton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Robert Maxton]

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

[Mario Carneiro]

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]

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

[Robert Maxton]

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]

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]

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]

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]

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]

(I should think all the proofs are refl)

[Robert Maxton]

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

[Robert Maxton]

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]

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]

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

[Reid Barton]

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

[Robert Maxton]

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]

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]

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]

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

[Robert Maxton]

Huh. Good to know

[Jake Levinson]

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!