Decidability of List.Mem

Stream: Program verification

[Alexander Kurz]

#eval 2 ∈ [1,2]
#eval List.Mem 2 [1,2]

I get two different results for the two. First true, second failed to synthesize Decidable (List.Mem 2 [1, 2]) Additional diagnostic information may be available using the set_option diagnostics true command. . Why do I get two different results? Afaiu the definition at https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Basic.html#List.Mem they should be the same ...

[François G. Dorais]

This one is tricky... The notation expands to Membership.mem and Membership is a class which has an instance for List and that is in turn implemented by List.Mem. The decidable instance (also a class) is implemented for the constant Membership.mem but not for the more specific constant List.mem.

[François G. Dorais]

Class synthesis only see through reducible definitions, so it never gets past the semireducible Membership.mem to its implementation.

[François G. Dorais]

Without this, tabular resolution used by Lean for class synthesis would hardly be possible.

[Alexander Kurz]

@François G. Dorais Wow, thanks! I think that is too complicated for what I want to do ... maybe best to define my own member function. I need to understand exactly how member works as I need to expand the definition of member in my proof that insertion sort sorts.

[Mario Carneiro]

There should be an instance of Decidable for List.Mem

[François G. Dorais]

Alexander Kurz said:

François G. Dorais Wow, thanks! I think that is too complicated for what I want to do ... maybe best to define my own member function. I need to understand exactly how member works as I need to expand the definition of member in my proof that insertion sort sorts.

That was a lot to digest all at once! If you provide more detailed code snippets (see #mwe) then it's much easier to provide more specialized technical support.

[François G. Dorais]

Mario Carneiro said:

There should be an instance of Decidable for List.Mem

How do you prevent diamonds doing this? I always find this very difficult.

[Eric Wieser]

Mario Carneiro said:

There should be an instance of Decidable for List.Mem

Should there really be instances for every implementation detail?

[François G. Dorais]

Alexander Kurz said:

@François G. Dorais Wow, thanks! I think that is too complicated for what I want to do ... maybe best to define my own member function. I need to understand exactly how member works as I need to expand the definition of member in my proof that insertion sort sorts.

In this kind of scenario, I often write a lemma:

theorem mem_def : x ∈ y ↔ what it should be := sorry

If I'm confident about my definition, I just leave sorry for the proof until I have time to come back to it.

When working on a theorem involving x ∈ y, I rewrite it using rw [mem_def] or even simp [mem_def] so I can work with the intended meaning more directly.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

There should be an instance of Decidable for List.Mem

Should there really be instances for every implementation detail?

I think there should be instances for all Prop producing functions where applicable, in addition to having instances for all the notation wrappers we put over these. It's not that much work to maintain both

[Mario Carneiro]

List.Mem is not even a private function, and when you pattern match on it you see the constructors directly. I don't see any argument that this type should be hidden from users and never touched directly

[Mario Carneiro]

François G. Dorais said:

Mario Carneiro said:

There should be an instance of Decidable for List.Mem

How do you prevent diamonds doing this? I always find this very difficult.

In this case the instances will be defeq so it will not cause any problem

[Eric Wieser]

Mario Carneiro said:

I think there should be instances for all Prop producing functions where applicable, in addition to having instances for all the notation wrappers we put over these. It's not that much work to maintain both

In mathlib this could manifest as Decidable (x ∈ S) vs Decidable (x ∈ S.carrier) vs Decidable (x ∈ Setlike.coe S) for S : Submonoid M, which I don't think is a path we want to have to maintain.

[Eric Wieser]

I agree that List.Mem is more user-visible, though arguably pattern matching should resolve to the nice notation too, like it does for Nat.succ.

[François G. Dorais]

Eric Wieser said:

In mathlib this could manifest as Decidable (x ∈ S) vs Decidable (x ∈ S.carrier) vs Decidable (x ∈ Setlike.coe S) for S : Submonoid M, which I don't think is a path we want to have to maintain.

Since this is in the Program Verification channel, let me point out that these "Mathlib problems" are not that relevant in this channel. In fact, once this channel gets more traction, I suspect "working around Mathlib problems" will become a more common topic.

[François G. Dorais]

Can we move the last few messages elsewhere? They're really not helpful to the main topic.

[Eric Wieser]

I was using mathlib as an example here, the issue manifests anywhere where there is more than one way to spell the argument to Decidable so isn't really about mathlib

[François G. Dorais]

I'm very sorry my comment came out as dismissive, that was not my intent. I just wanted to keep the discussion on topic.

[Eric Wieser]

I'm not really sure what topic you have in mind, unless you're suggesting splitting the thread between autoImplicit / Decidable.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

I think there should be instances for all Prop producing functions where applicable, in addition to having instances for all the notation wrappers we put over these. It's not that much work to maintain both

In mathlib this could manifest as Decidable (x ∈ S) vs Decidable (x ∈ S.carrier) vs Decidable (x ∈ Setlike.coe S) for S : Submonoid M, which I don't think is a path we want to have to maintain.

No, I think we should actually have all those instances. Many of them are implied by others so it's not like you will actually have a combinatorial explosion here, it's basically one per function

[François G. Dorais]

Sorry I wasn't clear. The topic of this thread is helping Alexander Kurz. Our digression, while interesting, is not directly helpful for that.

[Notification Bot]

22 messages were moved here from #Program verification > [x,y] vs x::y::nil by Mario Carneiro.

[François G. Dorais]

Thanks Mario!