function definition and #check

Stream: new members

[Huub Vromen]

I have defined a function g as follows:

variable (α β : Type)
variable (a : α) (b : β) (φ : Prop)
variable (f : α → β  → Prop → Prop)
def g (a : α) (φ : Prop) : Prop := ∃ (b : β), f a b φ

But #check g a φ gives the error message
"g (sorryAx Type true) (sorryAx Type true) : (sorryAx Type true → sorryAx Type true → Prop → Prop) → sorryAx Type true → Prop → Prop".
However, #check g α β f a φ does work. But why should I give more arguments to g than the two in the definition of g?

[Yaël Dillies]

because you wrote variable (α β : Type), not variable {α β : Type}

[Kevin Buzzard]

You can edit your original post to use #backticks to make it easier to read

[Huub Vromen]

(deleted)

[Huub Vromen]

(deleted)

[Huub Vromen]

(deleted)

[Ruben Van de Velde]

Note that your "solution" means something else entirely: it's now generic over any g rather than referring to your def g. What's the error you get?

[Huub Vromen]

Yaël Dillies said:

because you wrote variable (α β : Type), not variable {α β : Type}

Thank you! The definition of g now works fine. My next problem is that the definition of h1 gives an error message.

variable {α β : Type}
variable (a : α) (b : β) (φ : Prop)
variable {f : α → β  → Prop → Prop}
def g (a : α) (φ : Prop) : Prop := ∃ (b : β), f a b φ
def h1 (a : α) (φ : Prop) (ψ : Prop) : Prop := g a (φ → ψ)

I can solve the problem by writing

def h2 {g : α → Prop →  Prop} (a : α) (φ : Prop) (ψ : Prop) : Prop := g a (φ → ψ)

But this gets cumbersome if I have to define another function that, for example, refers to f and g. Is there another way to solve the problem with h1?

[Huub Vromen]

Ruben Van de Velde said:

Note that your "solution" means something else entirely: it's now generic over any g rather than referring to your def g. What's the error you get?

don't know how to synthesize implicit argument @g

[Ruben Van de Velde]

So g takes an implicit argument f but there's no way for lean to know which f to use. You can write g (f := f) a ...

[Kevin Buzzard]

@Huub Vromen I suggest you read about explicit and implicit inputs to functions in a standard source like #tpil . It's covered very carefully in chapter 2.