Zulip Chat Archive

Stream: new members

Topic: tactic preference


view this post on Zulip Damiano Testa (Oct 18 2020 at 05:56):

Dear All,

in the process of cleaning up proofs, I find myself having to make choices between using different tactics with the same final effect. In practice, I often end up with the following scheme:

simp becomes rw (if I am lucky, via squeeze_simp)
apply [...], exact [...] becomes exact [......]
rw [... \iff ...] becomes apply [(...).mp(r)...] (when reasonable/possible)
have becomes a previous lemma

I realize that tactics are not just not linearly ordered, they are probably not even a poset! Still, a proof commits you to some choices and I would like to know that I am at least going in a reasonable direction. I would like to know whether you find the scheme above reasonable. What other substitutions would you make? For instance, I rarely use subst [...] since the next tactic is almost invariably rw and then I merge them in a longer rw. Which is normally preferred: subst [...], rw [...] or rw [......]?

Sorry for the vague question: I hope that someone can still give me some pointers!

view this post on Zulip Mario Carneiro (Oct 18 2020 at 05:57):

I try to merge subst into the nearest rcases

view this post on Zulip Damiano Testa (Oct 18 2020 at 05:58):

Mario Carneiro said:

I try to merge subst into the nearest rcases

Ah, I use very rarely rcases! The fact that you mention it, makes me understand that I should use it more! Thanks!

view this post on Zulip Mario Carneiro (Oct 18 2020 at 05:59):

You can go really far with rcases and refine

view this post on Zulip Mario Carneiro (Oct 18 2020 at 05:59):

it's basically term mode proof in tactic clothing

view this post on Zulip Damiano Testa (Oct 18 2020 at 05:59):

refine I *try * a lot, but end up being able to apply it only very rarely.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:00):

refine can be used in place of almost any tactic, although the equivalent may not be pretty depending on the tactic it replaces

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:00):

so would a good measure be the length of the output of show_term to inform the choices above?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:01):

it's good for replacing split, existsi/use and intro in some combination

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:02):

ah, I did not know that splits could be avoided by refine: this will keep me busy! Ahaha

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:02):

yes, although you should be aware that some tactics do work that doesn't show up in the term, for example simp

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:02):

split is just refine <_, _>

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:02):

and you can stick a term in there if one of the sides is easy

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:02):

I never leave a simp and almost never leave even a simp only

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:03):

Mario Carneiro said:

split is just refine <_, _>

I did not know! I will stop using split, then!

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:04):

I will also point out that this doesn't necessarily match everyone's preference; this is good for making low compile time proofs but may go against one's aesthetics

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:05):

existsi a is just refine <a, _>

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:05):

Yes, I understand that. Although, to be honest, proof irrelevance has the effect in my mind of replacing "beauty" with "efficiency" in a proof.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:06):

a kindred spirit :grinning_face_with_smiling_eyes:

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:06):

Mario Carneiro said:

existsi a is just refine <a, _>

I did not even know about the tactic existsi.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:06):

use is basically the same as existsi

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:07):

Ah, good to know! I work aournd statements so as to avoid needing use whenever I can. I do not know why...

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:08):

It does a bit of postprocessing with simp to make it more user friendly I think

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:09):

check out this beautiful proof:

theorem split_bits.determ_l {n₁ n₂ l} (h₁ : split_bits n₁ l) (h₂ : split_bits n₂ l) : n₁ = n₂ :=
begin
  induction l generalizing n₁ n₂, {cases h₁, cases h₂, refl},
  rcases l_hd with _, l', rfl⟩,
  induction l' generalizing n₁ n₂,
  { cases h₁, cases h₂, exact l_ih h₁_a h₂_a },
  { have :  {n l'},
      split_bits n l' 
      l' = _, l'_hd :: l'_tl, rfl :: l_tl 
      l'_hd = nat.bodd n 
      split_bits (nat.div2 n) (⟨_, l'_tl, rfl :: l_tl),
    { intros, cases a; try {cases a_1},
      rcases a_bs with l₂, rfl⟩,
      injection a_1, cases h_2,
      cases congr_arg (λ v : Σ n, bitvec n, v.2.1) h_1,
      exact rfl, a_a },
    rcases this h₁ rfl with rfl, h₁'⟩,
    rcases this h₂ rfl with e, h₂'⟩,
    rw [ nat.bit_decomp n₁, e, l'_ih h₁' h₂', nat.bit_decomp] }
end

100% old school tactics

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:09):

I now need to resist the urge to go back to all the code that I have written and preform further substitutions... surely, alongside proof-checkers, there are "proof-spas", beautifying your code, no?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:10):

it's big business in metamath land, but lean doesn't make it so easy to optimize proofs in any large scale way

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:11):

Why do you call the proof above "old school tactics"? What are examples "new school tactics"? I feel that I am a beginner learning the old-school...

view this post on Zulip Heather Macbeth (Oct 18 2020 at 06:12):

Is this something AI can do for us someday? Take the corpus of all the lemmas and definitions in mathlib, and find its own proofs, sometimes 3 lines shorter than the existing proofs?

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:13):

Heather Macbeth said:

Is this something AI can do for us someday? Take the corpus of all the lemmas and definitions in mathlib, and find its own proofs, sometimes 3 lines shorter than the existing proofs?

In my proofs, I think I would be happy if it only shortened them by 3 lines! Even my one-line-proofs are long...

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:14):

It's something that can absolutely be done in principle (that's basically what GPT-f did for metamath), but the limiting factor is ease of access of the data to automated tools, which is crazy considering that it's a formal theorem prover

view this post on Zulip Heather Macbeth (Oct 18 2020 at 06:16):

Mario Carneiro said:

that's basically what GPT-f did for metamath

I don't know about this, can you suggest something for further reading?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:17):

In fact, for a long time the main metamath tool has had a proof processing tool called "minimize" that is basically a peephole optimizer: it looks at sequences of 2 or 3 steps in your proof and tries to find ways to do the same thing in 1 or 2 steps utilizing the whole library. It's computationally expensive, so it is run once a year or so on the entire library, but it can also be run in the background while you are working on your new proof

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:18):

There is some discussion about GPT-f on the #Machine Learning for Theorem Proving stream

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:20):

The upshot is that most proofs in set.mm are "locally optimal": they don't necessarily take the globally shortest path but there are no local missteps so everything proceeds straightforwardly

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:21):

a simple analogue for lean would be deleting have statements that are never used

view this post on Zulip Mario Carneiro (Oct 18 2020 at 06:22):

But none of that can happen in lean 3 because no one can parse lean except lean

view this post on Zulip Damiano Testa (Oct 18 2020 at 06:38):

@Mario Carneiro Thank you very much for your input! I have already shortened a couple of proofs using some of your ideas!

view this post on Zulip Julian Berman (Oct 18 2020 at 13:29):

What causes the parsing difficulties in Lean 3 (and what's changing)?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:29):

Well, lean 4 will be even harder to parse

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:30):

the reason lean 3 is hard to parse is because you can run arbitrary code while parsing

view this post on Zulip Julian Berman (Oct 18 2020 at 13:30):

Ah, of course.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:31):

which means that parsing correctly implies also running the VM correctly, having a typechecker and tactic framework and every other observable feature of lean

view this post on Zulip Kenny Lau (Oct 18 2020 at 13:36):

how do you run arbitrary code while parsing?

view this post on Zulip Julian Berman (Oct 18 2020 at 13:40):

notation I guess?

view this post on Zulip Julian Berman (Oct 18 2020 at 13:41):

Or are you saying how would you implement that? I mean I guess if you're sufficiently motivated you start with running a Lean process externally or embedding it in the parser, parse everything you can statically and then communicate with it for the bits you can't parse yourself or something

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:42):

Anything using the parser monad

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:42):

tactic argument parsing and user commands

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:46):

meta def tactic.interactive.even (e : interactive.parse (do
  n  lean.parser.small_nat,
  guard (2  n))) := tactic.skip

example : true := by even 1234 -- ok
example : true := by even 1233 -- parse error

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:47):

I'm saying that it is impossible to parse lean without also doing everything else lean does. It is not a separate pass

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:21):

can you get Lean to output a representation of the abstract syntax tree of a file? like in python, it's also a pain to make a third-party parser for Python code, but you don't have to do it because Python itself can use its parser and then you can walk the AST to encode it into json or something

view this post on Zulip Reid Barton (Oct 19 2020 at 17:23):

I think there never really is an abstract syntax tree, or at least, not of the whole file at the same time

view this post on Zulip Reid Barton (Oct 19 2020 at 17:24):

which isn't to say you couldn't retrofit such a concept onto Lean, but it sounds like a lot of work

view this post on Zulip Reid Barton (Oct 19 2020 at 17:25):

I looked into how the "return information for the identifier at a specific location" feature works and it just reparses the whole file up to that location

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:28):

weird

view this post on Zulip Reid Barton (Oct 19 2020 at 17:28):

In Lean 4 the parser is written in Lean and will be user-extensible in ways which hopefully include being able to capture the parsed AST for whatever nefarious purposes one might have

view this post on Zulip Reid Barton (Oct 19 2020 at 17:31):

and there's actually a Syntax Lean type which is the AST, rather than, when the parser encounters the inductive keyword, it just calling the handler for inductive commands, or however it works now

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:35):

One way to implement AST retrieval would be to have an AST structure in the parser state, and then just log all parser function calls in it, i.e. whenever you call p.inductive() the first thing it does is call ast.inductive() which pushes an inductive AST node on the stack. You end up with a preorder traversal of the AST as an array and stream that out

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:36):

i guess even the ast is kind of weird if you're thinking of external proof minimizers or similar

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:37):

what you really want is a reduced language... like theoretically, would it be possible to write every proof in lean as a sequence of have ___, from <existing lemma> _ _ _ type lines?

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:37):

because otherwise the minimizer has to understand norm_num, solve_by_elim, all these complex things

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:37):

That kind of thing is in the olean files and the export format, and there are already external parsers for that

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:38):

the external typecheckers work on the data from the export format, which you can get by running lean --export

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:39):

but what we don't have access to is stuff like the list of tactics used in a file

view this post on Zulip Reid Barton (Oct 19 2020 at 17:39):

But this might somehow be "too reduced"

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:40):

it's too reduced to minimize a proof - it isn't obvious how minimal a lean proof is, from its compiled form. it might be useful for something though...

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:41):

the olean files are a bit more feature rich in that they contain notations and annotations, in addition to raw logical proof data (which is all that is in the lean export files), but they don't have anything about begin end blocks

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:41):

is lean 4 going to maintain these formats

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:41):

no, olean was never meant to be a stable format

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:42):

and even the core logic has changed so the export format would have to be different

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:42):

but I think in lean 4 there won't be an export format (but there will be enough tools to roll your own)

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:42):

i wonder how painful transitioning from 3 -> 4 is going to be....

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:42):

quite

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:44):

I'm told that lean 4 is at least compatible enough to read lean 3 olean files and get "raw mathlib"

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:44):

or maybe that was the export format? @Gabriel Ebner knows

view this post on Zulip Reid Barton (Oct 19 2020 at 17:44):

olean or export?

view this post on Zulip Reid Barton (Oct 19 2020 at 17:44):

I think it was export

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:45):

that would make more sense. No one wants to parse the rats nest that is olean files

view this post on Zulip Reid Barton (Oct 19 2020 at 17:45):

says the author of olean-rs

view this post on Zulip Reid Barton (Oct 19 2020 at 17:45):

by the way, last time I checked it was out of date :upside_down:

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:46):

I should do something about that

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 17:46):

There is an importer for the text output format here: https://github.com/gebner/lean4-mathlib-import

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 17:47):

Import mathlib into Lean 4

This tool takes the text export of mathlib and creates an olean file that you can import with Lean 4.

Notation, etc., is not supported. All theorems are imported as axioms. Some names are adapted to the new convention, some aren't. This code is not intended for production.

You can build the Mathlib.olean as follows (make sure you have enough RAM):

make
make emacs    # install the lean4 emacs package yourself!

(If you're on NixOS, you might need to run everything inside nix-shell ~/lean4.)

After that, you can import mathlib and play with it in Lean 4:

import Import.Mathlib
#check (deriv : (real  real)  (real  real))

view this post on Zulip Reid Barton (Oct 19 2020 at 17:47):

Relevant Zulip thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Importing.20mathlib.20into.20Lean.204/near/187561178

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:47):

oh, you write olean files?

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:47):

so let's say I want to parse, or quasi-parse mathlib. the theory is that you could make a faster library_search if you did some preprocessing and wrote things in a faster language. I just want the names, namespaces, and signatures of the lemmas/theorems, though. enough to generate some code that refers to them. I don't need to verify the proofs. is that possible from the export format?

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:47):

so I suppose you know what lean 4 olean looks like

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 17:48):

I'm using the Lean 4 API for olean files.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:49):

You can fairly easily write an introspection tactic from lean to gather that information. That's what leandoc is

view this post on Zulip Reid Barton (Oct 19 2020 at 17:49):

You can also reconstruct this information from the export format.

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:50):

ok. so it's not the full AST but it's like the first level of the AST

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:50):

more like the last level

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:50):

it's the fully digested form

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:51):

well, if you think of the AST as a tree where the root is like a namespace, and the first level of the tree is the children of that namespace, and then the next levels are how those children start to be defined, etc

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:51):

you don't even have information about implicit args though, so generating a parseable expr from that info is tough

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:51):

lean isn't really structured like that though

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:52):

you can put stuff in namespaces in an arbitrary order

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:52):

from any file

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:53):

I mean, the file structure is like that with namespaces and sections, but none of that structure is visible in the digested theorems

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:53):

makes sense. well i'll check out what leandoc does

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 17:54):

Implicit arguments are there in the text output format. Even infix notation.

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 17:54):

But yes, please write your own exporter in lean like doc-gen.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:54):

That's another thing that you could only get at with a proper AST - we currently have no idea when namespaces and sections start and end, except when you are inside them

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:55):

and getting the current namespace is only recently available too. I think we still can't get at the list of variables in scope

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:56):

so my dream of writing a def-equivalent tactic is as yet unfulfilled


Last updated: May 11 2021 at 00:31 UTC