How to conditionally ban certain typeclass instances?

Stream: new members

[CalculiLime325]

As the title states, I am looking for a way to ban some typeclass instances. See this playground.
What I desire is to have Lean4 raise an error when it detects, for all Humans P and C,
a ParentRel P C instance and a ParentRel C P in that same scope. I know I could define an axiom that implies false given the two instances, but that doesn't prevent both instances from being defined in the first place.

[Aaron Liu]

why do you want to do this?

[CalculiLime325]

It was for the purpose of having fun. I was inspired by https://cliplab.org/~logalg/doc/The_Art_of_Prolog.pdf and wanted to see if Lean's typeclass system was sufficient for creating logical statements like in Prolog. In summary, It's not really critical that I insist on doing this.

[CalculiLime325]

I also wanted to express the fact that the ParentRel relation isn't reversible. I.E Alice can be the parent of Bob, but Bob cannot also be the parent of Alice.

[Aaron Liu]

CalculiLime325 said:

I also wanted to express the fact that the ParentRel relation isn't reversible. I.E Alice can be the parent of Bob, but Bob cannot also be the parent of Alice.

clearly with what you have set up so far this is just not true

[Aaron Liu]

I'm still not sure what you want to do

[Jakub Nowak]

I don't think that's possible. If I were to use your example I would model it probably like this:

class ParentRel where
  Parent : Human → Human → Prop
  ne_Parent_of_Parent (P C : Human) : Parent P C → ¬Parent C P

[Jakub Nowak]

The feature you want would also be quite hard to implement. Available typeclass instances depend on the set of imports in the file you're working in.

[CalculiLime325]

@Aaron Liu I am confused here as to what you mean. Sure my playground doesn't actually express that fact in its current state, but I want to learn as to how I can modify my playground to do just that.

@Jakub Nowak I see, that's unfortunate. I will experiment with your definition and see what I can gleam.

[Aaron Liu]

it is possible to hook the decl elaborator and throw an error if it's adding a ParentRel whose reverse is inferable by typeclass

[Aaron Liu]

I don't recommend it and it doesn't actually stop you from having both directions of ParentRel at once

[Jakub Nowak]

I don't know if that would be helpful to you, but the closest thing to logic programming in functional languages is List monad. However, it lacks some important features of logic programming languages like prolog.