linarith tactic code

Stream: metaprogramming / tactics

[Ayush Agrawal]

Hi guys! I am super new to Lean and am trying to understand the meta programming stuff and tactic writing. I wanted to start with linarith tactic understanding. I have posted some of the queries in the new members stream : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/linarith.20tactic.20understanding . It would be helpful if anyone can shed some light over the doubts. thanks! PS: I have understood the idea of FM elimination.

[Kevin Buzzard]

Just to comment that when I was super-new to Lean, I tried to understand the basics of type theory, and read through all of #tpil and did all the exercises, before I started reading any of the code in mathlib.

[Ayush Agrawal]

Hi @Kevin Buzzard I have done some exercises from the tuts, NNG and read some books. Also since u mention the apt readings, I wanted to know how important is to understand the elements of monadic programming (getting hard time to understand it from H guide :) to get into Lean metaprogramming?

[Kevin Buzzard]

I have no idea about metaprogramming.

[Johan Commelin]

@Ayush Agrawal Have you seen the metaprogramming tutorial on youtube, by Rob Lewis?

[Ayush Agrawal]

Oh yes! I saw those videos. But they were hard for me to understand since I am new to functional paradigm. Can u recommend some basic resources I should go over before watching those videos again?

[Johan Commelin]

Hmmz, I'm not a meta expert either. Did you try the exercises?

[Ayush Agrawal]

Which exercises? Can u send the link to those plz..

[Johan Commelin]

Hmm, maybe I'm mistaken. I thought there were exercises, but I can't find them now.

[Ayush Agrawal]

How can we call linarith tactic inside a meta code? for example for apply, we may use tactic.applyc. Is there a similar way for linarith also?

[Mario Carneiro]

You can always call an interactive tactic directly, i.e. tactic.interactive.linarith, but many tactics also provide non-interactive versions. You can usually find the functions you want to call by looking at the source of the tactic frontend (src#tactic.interactive.linarith) to see if it immediately dispatches to some other function that you can call instead

[Mario Carneiro]

and in this case you can see that it straight away calls src#tactic.linarith

[Mario Carneiro]

although in this case, depending on what your input looks like, you may want to go one step further and call the things that tactic.linarith calls

[Ashley Blacquiere]

I've found the Hitchhiker's Guide to Logical Verification to be particularly helpful in understanding metaprogramming:
https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf

If you're new to functional programming there are suggestions in the Hitchhiker's Guide pointing to specific Haskell tutorials to follow that might help.