Zulip Chat Archive

Stream: new members

Topic: Confused about functions

Pehan Amarathunge (Jan 26 2023 at 18:25):

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 :)


Gareth Ma (Jan 26 2023 at 18:35):

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 :=
  exact f x (g x) z, -- g x = g(x)

Gareth Ma (Jan 26 2023 at 18:38):

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

function expected at
term has type

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 (Jan 26 2023 at 18:40):

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 (Jan 26 2023 at 18:42):

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

Junyan Xu (Jan 26 2023 at 23:42):

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

Last updated: Dec 20 2023 at 11:08 UTC