Zulip Chat Archive

Stream: general

Topic: compute value of function

jmc (Mar 19 2018 at 20:11):

Hi. Lean-newbie here. I've got a function f : \N \to \Z with a pretty involved definition. I would like to see what Lean thinks that the value of f is on 0,1,2,3 for example.
My current approach has been:

example : f 0 = n := refl

and then just trying different values of n, until I am lucky. But there should be a better way...

(Ok, I just saw there is a "new members" stream. If someone can move this topic overthere, please feel free to do so.)

Simon Hudon (Mar 19 2018 at 20:14):

Try:

#eval f 0
#eval f 1
#eval f 2
#eval f 3

Moses Schönfinkel (Mar 19 2018 at 20:14):

You can just #eval f x

jmc (Mar 19 2018 at 20:15):

Aah, thanks!

Simon Hudon (Mar 19 2018 at 20:15):

It uses the virtual machine so if f is computation intensive, this will ensure swift execution

Moses Schönfinkel (Mar 19 2018 at 20:16):

If you want slow execution, you can try #reduce f x ;).

Moses Schönfinkel (Mar 19 2018 at 20:16):

(Also your refl trick made me giggle so you're awarded a pointless internet point.)

Simon Hudon (Mar 19 2018 at 20:18):

(I think we can use octopuses to award those internet points)

Moses Schönfinkel (Mar 19 2018 at 20:18):

What an excellent idea.

jmc (Mar 19 2018 at 20:19):

Thanks for the point!

Simon Hudon (Mar 19 2018 at 20:19):

thanks)

Andrew Ashworth (Mar 19 2018 at 20:19):

the rfl thing is considered good style if you go by "Software Foundations"

Andrew Ashworth (Mar 19 2018 at 20:19):

it's basically inline unit testing

Moses Schönfinkel (Mar 19 2018 at 20:19):

I have no recollection of that in SF o_O?

Moses Schönfinkel (Mar 19 2018 at 20:19):

Aaah right.

Moses Schönfinkel (Mar 19 2018 at 20:19):

You mean his auto-tests.

Andrew Ashworth (Mar 19 2018 at 20:20):

yeah, for ex

Andrew Ashworth (Mar 19 2018 at 20:20):

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil ⇒ default
  | h :: t ⇒ h
  end.
Definition tl (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ t
  end.
Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

Moses Schönfinkel (Mar 19 2018 at 20:20):

Yeah absolutely.

Moses Schönfinkel (Mar 19 2018 at 20:20):

Oh boy that book is such an excellent introduction to these things.

Moses Schönfinkel (Mar 19 2018 at 20:21):

Compare that to CPDT... :-\.

Moses Schönfinkel (Mar 19 2018 at 20:21):

(Sorry Adam...)

Andrew Ashworth (Mar 19 2018 at 20:22):

yeah, if you do 2 semesters of software foundations

Andrew Ashworth (Mar 19 2018 at 20:22):

first

Andrew Ashworth (Mar 19 2018 at 20:22):

maybe you can understand cpdt, except you still won't

jmc (Mar 19 2018 at 20:22):

Anyway, the function in question is the Ramanujan tau function (https://en.wikipedia.org/wiki/Ramanujan%27s_tau_function)
Already #reduce \tau 2 is extremely slow for my implementation.
But #eval \tau 4 is pretty fast. And the first 5 values are correct (^;

Last updated: Dec 20 2023 at 11:08 UTC