Confused about functions

Stream: new members

[Pehan Amarathunge]

Hi there.

I have just started learning Lean and I am confused about how functions work.

I was able to solve the below example in a sequence of steps, but I don't understand why the following code does not solve the same problem in one line. I would really appreciate some sort of help on this.

Thank you :)

image.png

[Gareth Ma]

Hey, next time post the code directly instead, enclosed using \`\`\`, so that people can copy and paste :) Anyways, try this:

example {A B C D : Type} (f : A → B → C → D) (g : A → B) (x : A) (z : C) : D :=
begin
  exact f x (g x) z, -- g x = g(x)
end

[Gareth Ma]

The problem can be seen if you run your code and look at the error:

function expected at
  x
term has type
  A

which occurs in your parentheses (x g(x) z). It is because if you put parentheses around them, it will treat it as a single expression and try to compute/evaluate it. And since you wrote x _ _, it only makes sense if x is a function, but it is not - it is just a type A

[Gareth Ma]

If you remove the parentheses like I did, this is what happens:

f         -- Type: A -> B -> C -> D
  x       -- We evaluate the above line at x. Now (f x) has type B -> C -> D
    (g x) -- We evaluate the above line at (g x). (g x) = g(x) has type B,
          -- so (f x g(x)) has type C -> D
      z   -- Finish it

[Gareth Ma]

Oh also if you write f x g(x) z it will be interpreted as (f x g)(x) z.

[Junyan Xu]

f (x g(x) z) is the same as f (x g x z) I think ...