Decidable Equalities,

Stream: new members

[Jonathan Whitehead]

I read through https://hrmacbeth.github.io/math2001/10_Relations.html to get a feel for relations in Lean. The problem that I'm having is that Lean can't seem to check equality between two structs unless I first build a framework for equality. In continuation of a previous post that I made, consider the simple example of a structure:

structure Vertex :=
  (name : String)

I want to be able to say that for u, v of type Vertex that u = v when u.name = v.name. Lean apparently has the machinery to be able to check that strings are equivalent, but I don't know how to extend this to a structure. I tried to create a Prop:

def Vertex.eq (u v : Vertex) : Prop :=
u.name = v.name

But then realized that I needed something of a type similar to DecidableEq. So then I tried something like:

instance Vertex.decEq : DecidableEq Vertex :=
  fun u v => decEq u.name v.name

but I had problems with decEq and a fuzzy idea of what is going on with DecidableEq. Can anyone help me out and give me some insight into Decidable types in Lean? I didn't seem to find anything about Decidable types in the tutorial that I listed at the beginning.

[Kyle Miller]

There's at least a metaprogram to generate a DecidableEq instance for you in many cases:

structure Vertex :=
  (name : String)
  deriving DecidableEq

#synth DecidableEq Vertex
-- Succeeds, and it says this is the instance:
-- fun a b ↦ instDecidableEqVertex a b

[Kyle Miller]

Something you should know about equality is that every type comes with an equality relation. It's not something you have to define yourself. In fact, the Vertex.eq you defined is equivalent to the usual one:

def Vertex.eq (u v : Vertex) : Prop :=
u.name = v.name

theorem Vertex.eq_iff (u v : Vertex) :
  u = v ↔ Vertex.eq u v :=
by cases u; cases v; simp [Vertex.eq]

[Jonathan Whitehead]

Kyle Miller said:

There's at least a metaprogram to generate a DecidableEq instance for you in many cases:

structure Vertex :=
  (name : String)
  deriving DecidableEq

#synth DecidableEq Vertex
-- Succeeds, and it says this is the instance:
-- fun a b ↦ instDecidableEqVertex a b

Well, that seems like a nice little feature. But what if the struct had more fields and equality was only determined by one of them? Is there same way to specify which field constitutes equality?

[Kyle Miller]

Maybe a way to understand the built-in equality relation is what's more-or-less it's definition: "u = v if and only if whenever something is true for u then it is also true when v is substituted for u". This is a nice definition mathematically, but it doesn't come with any sort of way to check whether u = v holds -- you have to find some statement whether either substitution succeeds or fails.

[Kyle Miller]

This is where decidability comes in. A proposition p is called decidable if there's some program that you can evaluate that tells you whether the proposition is True or False. A type has decidable equality if for all u and v the proposition u = v is decidable.

[Kyle Miller]

Jonathan Whitehead said:

But what if the struct had more fields and equality was only determined by one of them?

If you want to adjust the definition of equality for a given type, that's what quotient types are for. You can use Quot to make more things equal (by for example forgetting about everything but a particular field).

[Jonathan Whitehead]

Kyle Miller said:

This is where decidability comes in. A proposition p is called decidable if there's some program that you can evaluate that tells you whether the proposition is True or False. A type has decidable equality if for all u and v the proposition u = v is decidable.

This is what I thought was going on. I was trying to define the program to evaluate the proposition but it appears that deriving DecidableEq does it for you.

[Jonathan Whitehead]

Kyle Miller said:

Jonathan Whitehead said:

But what if the struct had more fields and equality was only determined by one of them?

If you want to adjust the definition of equality for a given type, that's what quotient types are for. You can use Quot to make more things equal (by for example forgetting about everything but a particular field).

Great, is there some kind of source for this? Or do I just need to keep digging into the repo to figure out how to use a lot of this stuff? What do you recommend?

[Jonathan Whitehead]

As a working example of how to use quotient types consider:

structure Edge :=
  (name : String)
  (edge : Vertex × Vertex)

For edges (u,v) and (x,y), we want to say that the edges are equal when u=x and v=y, but we don't really care if they have the same labels. Is there some modification of `deriving DecidableEq ` that would allow me to do this?

[Kyle Miller]

I probably learned most things by using Zulip search (it's got a lot of "unwritten documentation"), looking at the Lean 3 documentation, #tpil, digging through source, and working on mathlib.

[Jonathan Whitehead]

Oh, thanks! I didn't even think to search Zulip, I've just been digging through the git repo for Mathlib.

[Kyle Miller]

Jonathan Whitehead said:

Is there some modification of `deriving DecidableEq ` that would allow me to do this?

No -- if two Edges have different labels, then they are distinguishable, so they're not equal.

[Kyle Miller]

Could we #xy a bit here? You can't mess with equality, but you can definitely create your own relations. What do you want to do with them? Prove things? or write programs that compute using the truth value?

[Kyle Miller]

There's also BEq with the == relation, which is Bool-valued rather than Prop-valued, and you're free to make it work however you want. You just don't get much in the way of proofs.

[Jonathan Whitehead]

Kyle Miller said:

Could we #xy a bit here? You can't mess with equality, but you can definitely create your own relations. What do you want to do with them? Prove things? or write programs that compute using the truth value?

Let's suppose that we want to be able to build programs/algorithms and then prove that they're correct. So I suppose we would want to do both, prove things about them and write programs.

[Jonathan Whitehead]

It seems like you're saying that what I was suggesting to do would create more problems than it solves.

[Kyle Miller]

Here's an example of Quot (though I'll warn you that usually you'd use Quotient, which is a more convenient wrapper around Quot):

structure Vertex :=
  (name : String)

structure Edge' :=
  (name : String)
  (edge : Vertex × Vertex)

def Edge'.eq (e1 e2 : Edge') : Prop := e1.edge = e2.edge

def Edge : Type := Quot Edge'.eq

def Edge.mk (e : Edge') : Edge := Quot.mk Edge'.eq e

theorem Edge.eq_iff (e1 e2 : Edge') :
    Edge.mk e1 = Edge.mk e2 ↔ e1.edge = e2.edge := by
  sorry -- not so hard, but it'd be one line with Quotient

But this is almost surely not what you want. This Edge type is equivalent to

structure Edge :=
  (edge : Vertex × Vertex)

When we form the quotient with Quot we said we wanted a type where edges are equal if their edge fields are equal, and that means that name is effectively something we no longer have access to. It's not exactly erased, but Lean will prevent us from ever writing any computation that can distinguish Edges according to their name in any way.

[Jonathan Whitehead]

Thanks for the example, I see how Quot is being used now, but I guess the take-away is that we should take care to define our structs in such a way that we don't have unnecessary fields. With my limited knowledge of these kinds of objects I suppose that I'll have to exercise a little trust in that we typically don't want to do this. Thanks for the help! I learned a lot.

[Kyle Miller]

Jonathan Whitehead said:

It seems like you're saying that what I was suggesting to do would create more problems than it solves.

Lean sort of forces you to take equality seriously. If you can distinguish two terms of a type in any way (i.e., if you can't just substitute one for the other) then they're simply not equal. If two edges have different name labels, then they are distinguishable, so they are not equal. You could either make your own relation (like use BEq and prove theorems about your definition to make it useful), or you could accept that the name field is significant, or you could remove the name field because it would ruin the theory.

Or, if you want the name field only for pretty printing, say, I think you could do a hack where you use Quot and then write unsafe code to extract the name field while printing. A downside is that then you'll have to deal with quotients, which you shouldn't avoid, but it's easier if you don't have to use a Quot.

[Jonathan Whitehead]

Kyle Miller said:

Jonathan Whitehead said:

It seems like you're saying that what I was suggesting to do would create more problems than it solves.

Lean sort of forces you to take equality seriously. If you can distinguish two terms of a type in any way (i.e., if you can't just substitute one for the other) then they're simply not equal. If two edges have different name labels, then they are distinguishable, so they are not equal. You could either make your own relation (like use BEq and prove theorems about your definition to make it useful), or you could accept that the name field is significant, or you could remove the name field because it would ruin the theory.

Or, if you want the name field only for pretty printing, say, I think you could do a hack where you use Quot and then write unsafe code to extract the name field while printing.

Yeah, I was thinking of the name field as being something that's just for user friendly support like printing. But in my own curiosity I just imagined that there would be structs that we would want to call "equal" in a certain "context". Like, maybe a struct for a Point with the two fields "label" and "(x,y,z)". We might have point A and point B with (1,2,3) and (1,2,4). We might want to make some equality statement about how these two points coincide (are equal in some sense) in a plane. It seems like you would either use the Quot type or you would just define a new struct for (x,y) coordinates and some sort of framework that forgets the third parameter of (x,y,z).

[Kyle Miller]

Jonathan Whitehead said:

I guess the take-away is that we should take care to define our structs in such a way that we don't have unnecessary fields.

Yeah, part of the design work you need to do in formalization is to make sure equality is what you think it is. (For example, SimpleGraph.Subgraph took a couple of iterations before there was exactly one subgraph per Subgraph. If I remember correctly, one version allowed vertices outside the subgraph to be adjacent, which doesn't matter if you're only working with vertices in the subgraph, but then the cardinality of Subgraph is wrong.)

[Kyle Miller]

Jonathan Whitehead said:

It seems like you would either use the Quot type or you would just define a new struct for (x,y) coordinates and some sort of framework that forgets the third parameter of (x,y,z).

Yeah, you don't have to literally use Quot to form quotient types. The best kind of quotient is when you can write down a convenient type that's equivalent to the quotient. (Quotients in math are defined using universal properties after all, and not by a particular construction.)

[Kyle Miller]

But it's worth knowing that at runtime, a Quot is still the original type, so all the additional "forgotten" data is still there.

[Kyle Miller]

It's just that the surrounding theory prevents you from making use of it, in the sense that you have to keep proving that functions you define on a quotient give the same result even if you substitute one value for another that's related by your new equality relation (see Quot.lift)

[Kyle Miller]

Here's a DecidableEq instance by the way:

structure Vertex :=
  (name : String)

instance Vertex.decEq : DecidableEq Vertex :=
  fun u v =>
    if h : u.name = v.name then
      isTrue (by revert h; cases u; cases v; simp)
    else
      isFalse (by intro h'; subst_vars; exact h rfl)

[Kyle Miller]

think of isTrue and isFalse being fancy booleans that come with a proof of their truth

[Kyle Miller]

(at runtime, this proof is erased, but at proving time it's important for correctness)

[Kyle Miller]

if statements are one of the main interfaces to use Decidable instances. There's already a DecidableEq String instance, so I'm able to do this if without Lean complaining. The h : notation is a way to grab ahold of a proof or disproof of the condition

[Jonathan Whitehead]

Kyle Miller said:

Here's a DecidableEq instance by the way:

structure Vertex :=
  (name : String)

instance Vertex.decEq : DecidableEq Vertex :=
  fun u v =>
    if h : u.name = v.name then
      isTrue (by revert h; cases u; cases v; simp)
    else
      isFalse (by intro h'; subst_vars; exact h rfl)

I actually had a very close implementation of this but for isTrue I couldn't figure out the appropriate tactics. I needed revert h. I felt like I was way off-base and ultimately abandoned finding the correct tactics.

[Jonathan Whitehead]

I also found it weird that within the proof, Lean didn't recognize refl. But in the Natural Number game, you use refl. Is this a new change?

[Jonathan Whitehead]

Also, I tried to use rw h but Lean complained and made me use rw [h].

[Kyle Miller]

(You don't really need revert here. I just know it'll set up simp to be able to finish it off quick. That way I don't need simp at h; simp [h] or something like that.)

[Kyle Miller]

Lean 3 -> Lean 4 has refl -> rfl and rw h -> rw [h]

[Kyle Miller]

Outside of tactics, refl takes an explicit argument, vs rfl which doesn't.

#check refl -- ∀ {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a a
#check rfl -- ∀ {α : Sort u} {a : α}, a = a

[Eric Wieser]

Kyle Miller said:

Or, if you want the name field only for pretty printing, say, I think you could do a hack where you use Quot and then write unsafe code to extract the name field while printing. A downside is that then you'll have to deal with quotients, which you shouldn't avoid, but it's easier if you don't have to use a Quot.

You can remove most of this pain with

structure Edge where
    name : Trunc String
    edge : Vertex × Vertex

[Eric Wieser]

Here the quotient is around just one field of the structure rather than the whole thing.