How can I force resolution to pick a particular instance?

Stream: lean4

[Alex Zani]

For practice purposes, I'm trying to prove the Applicative Functor laws for a type called Maybe. (Basically just my implementation of Option) I want to prove the homomorphism defined by this:

theorem maybe_applicative_homomorphism (v : α) (f : α → β) : (pure f) <*> (pure v) = pure (f v)

The problem I'm having is there's no way for lean to know which instance of Applicative I'm talking about. So how can I tell it?

[Abraham Solomon]

Alex Zani said:

For practice purposes, I'm trying to prove the Applicative Functor laws for a type called Maybe. (Basically just my implementation of Option) I want to prove the homomorphism defined by this:

theorem maybe_applicative_homomorphism (v : α) (f : α → β) : (pure f) <*> (pure v) = pure (f v)

The problem I'm having is there's no way for lean to know which instance of Applicative I'm talking about. So how can I tell it?

Have you tried:

attribute [-instance] (...)

where the instance (...) is of the Applicative; after your imports.

Another way would be to tag your instance as the default with

@[default_instance]
instance ...

[Edward van de Meent]

If you have your instances right, lean shouldn't have this issue? Or are you defining multiple non-defeq instances?

[Edward van de Meent]

(providing a #mwe might help provide a clearer idea of your question)

[Alex Zani]

Abraham Solomon said:

Have you tried:

attribute [-instance] (...)

where the instance (...) is of the Applicative; after your imports.

Another way would be to tag your instance as the default with

@[default_instance]
instance ...

I tried default_instance and lean still gets stuck looking for an instance.

I don't really understand what you mean by

attribute [-instance] (...)

I tried replacing (...) with Maybe and Applicative but both just gave errors.

[Kevin Buzzard]

What Edward is saying is that your quote above about "there's no way for lean to know which insurance of Applicative I'm talking about" is evidence that you're doing it wrong, but it's difficult to advise you on how to put things right because you're not posting a #mwe demonstrating your problem.

[Alex Zani]

(deleted)

[Alex Zani]

Edward van de Meent said:

(providing a #mwe might help provide a clearer idea of your question)

That makes sense. Here:

inductive Maybe (α : Type u) : Type u where
  | just : α → Maybe α
  | none
  deriving Repr

def maybe_seq : Maybe (α → β) → (Unit → Maybe α) → Maybe β
  | Maybe.none, _ => Maybe.none
  | Maybe.just f, g => match g () with
                       | Maybe.none => Maybe.none
                       | Maybe.just a => Maybe.just $ f a

instance : Applicative Maybe where
  pure := Maybe.just
  seq := maybe_seq

theorem maybe_applicative_homomorphism (α β : Type) (v : α) (f : α → β) :
    (pure f) <*> (pure v) = pure (f v) := by

[Kim Morrison]

There's nothing telling Lean what type that equality is taking place in.

[Kim Morrison]

You could write

theorem maybe_applicative_homomorphism (α β : Type) (v : α) (f : α → β) :
    (pure f) <*> (pure v) = pure (f := Maybe) (f v) := by
  sorry

[Kim Morrison]

or more conventionally

theorem maybe_applicative_homomorphism (α β : Type) (v : α) (f : α → β) :
    ((pure f) <*> (pure v) : Maybe β) = pure (f v) := by
  sorry

[Alex Zani]

Kim Morrison said:

You could write

theorem maybe_applicative_homomorphism (α β : Type) (v : α) (f : α → β) :
    (pure f) <*> (pure v) = pure (f := Maybe) (f v) := by
  sorry

Thanks. Both options work. I get how the second one works. But I don't understand how the first one works. f is already a function from alpha to beta. So how does (f := Maybe) work?

[Kevin Buzzard]

That's a different f, it's the one used in the definition of pure.

[Alex Zani]

Ok, that makes sense. Thanks!

[Kim Morrison]

Yes, it's confusing, when you used named arguments you are referring to the names at the declaration site of the function you are calling!

[Kim Morrison]

(The fact that we haven't yet done a thorough review of argument naming in the standard library makes this worse... It's coming! :-)