Getting Started with Tactics

Stream: lean4

[Daniel Bourgeois]

I'd like to create a tactic that

1. reads in all ?x < ?y, ?u = ?v hypothesis (for Int's)
2. applies transitive rules to get the complete set of possible relations
3. adds in the not cases -- like ?x < ?y -> Not ?x = ?y
4. searches for a contradiction to prove the goal

However, I don't know where to get started and have only a rudimentary
idea of how tactics work.

Any suggestions?

[James Gallicchio]

Definitely check out Arthur et al's metaprogramming book here. Goes through all the basics of metaprogramming in Lean!

[James Gallicchio]

(btw, is the tactic you're describing covered by linarith? though maybe that's a bit heavy of a tactic for your purposes)

[Martin Dvořák]

I cannot comment on how tactics are implemented because I never implemented one in my life. Just two cents:
(1) I think your step 3 is unnecessary.
(2) You will obtain something strictly weaker than linarith.

[Martin Dvořák]

Has omega been implemented in Lean 4 btw?

[Johan Commelin]

No, not yet

[Martin Dvořák]

So omega might be a great project for @Daniel Bourgeois instead!

[Martin Dvořák]

Not necessarily full omega but something along the lines @Daniel Bourgeois described but for Nat instead of Int.

[Johan Commelin]

I don't know much about this stuff, but I think implementing a performant version of omega is highly non-trivial.

[Martin Dvořák]

I feel a strong temptation to become a troll and say that omega was never performant.

[Martin Dvořák]

Anyways, I better shut up. Especially when I don't know shit about how tactics work inside.

[Mario Carneiro]

There is a micromega branch on mathlib4

[Mario Carneiro]

which apparently hasn't been touched since july

[Martin Dvořák]

https://github.com/leanprover-community/mathlib4/commits/micromega

[Mario Carneiro]

it's basically a port of https://github.com/coq/coq/tree/master/plugins/micromega

[Martin Dvořák]

Does Coq have something better than the micromega tho?

[Mario Carneiro]

don't let the name fool you, micromega is huge

[Mario Carneiro]

it is leagues better than lean 3 omega

[Mario Carneiro]

it also includes the equivalent of linarith and nlinarith

[Mario Carneiro]

(as separate tactics)

[Mario Carneiro]

micromega is the name of the overall package

[Mario Carneiro]

https://coq.github.io/doc/V8.11.0/refman/addendum/micromega.html

[Martin Dvořák]

Mario Carneiro said:

There is a micromega branch on mathlib4

Oh. I somehow wrongly assumed that micromega was supposed to be a temporary replacement for omega until the full omega gets implemented in Lean 4.

[Mario Carneiro]

no, lean 3 omega is not something we want to port. It was never complete in the first place

[Martin Dvořák]

I have a strong love-hate relationship with omega in Lean 3.

[Mario Carneiro]

if you are motivated I encourage you to pick up the branch and port the rest

[Martin Dvořák]

I am motivated but definitely not competent to do it.

[Mario Carneiro]

if you can read coq/ML it's mostly straightforward

[Mario Carneiro]

I stopped about a third of the way into https://github.com/coq/coq/blob/master/plugins/micromega/polynomial.ml

[Martin Dvořák]

I can hardly read Lean, let alone other languages.

[Mario Carneiro]

compare https://github.com/leanprover-community/mathlib4/blob/micromega/Mathlib/Tactic/Micromega/Polynomial.lean

[Mario Carneiro]

for me the hard part was knowing the types of things in the ML code, since I was just reading it from github and ML does global type inference so it's hard to see the types

[Daniel Bourgeois]

linarith worked, except it was necessary to insert have x : False := by linarith and then use x otherwise linarith complains that it can't synthesize LinearOrder

For learning purposes, I still want to have a go at implementing the tactic described.

[James Gallicchio]

Mario Carneiro said:

for me the hard part was knowing the types of things in the ML code, since I was just reading it from github and ML does global type inference so it's hard to see the types

highly recommend installing Millet (language server for ML), there's a vscode extension with everything packaged nicely