basic tactic writing & IO

Stream: new members

[Logan Murphy]

a slightly different question, is there any support for defining lean functions from standard input? For instance, is there a way to use get_line to read a string like

fun n : nat, ne n 0

and turn this into a lean expression, which could be used in a tactic? I looked around in tactic.expr and system.io but I can't seem to find anything of this kind. I can write a simple parser for now, but it would be nice to know if there's a general function or something

[Mario Carneiro]

You can only do this from the parser monad

[Mario Carneiro]

@Logan Murphy Here's a proof of concept:

import system.io

open lean lean.parser tactic interactive

meta def from_file {α} (f : string) (p : parser α) : parser α :=
do buf ← tactic.unsafe_run_io (io.fs.read_file f),
  prod.fst <$> with_input p buf.to_string

meta def load_parser {α} (p : parser α) : parser α :=
do t ← types.texpr,
  f ← ↑(to_expr t >>= eval_expr string),
  from_file f p

meta def tactic.interactive.load (e : parse (load_parser types.texpr)) : tactic unit :=
interactive.exact e

example : true :=
begin
  let foo := by load "foo.txt",
-- foo : ℕ → Prop := λ (n : ℕ), n ≠ 0
end

foo.txt:

λ n : ℕ, n ≠ 0

[Logan Murphy]

That’s very helpful Mario, thank you very much!

[Mario Carneiro]

Here's a version that doesn't do any file IO and just does the string -> expr part

open lean lean.parser tactic interactive

meta def parse_parser {α} (p : parser α) : parser α :=
do t ← types.texpr,
  f ← ↑(to_expr t >>= eval_expr string),
  prod.fst <$> with_input p f

meta def tactic.interactive.parse (e : parse (parse_parser types.texpr)) : tactic unit :=
interactive.exact e

example : true :=
begin
  let foo := by parse "λ (n : ℕ), n ≠ 0",
-- foo : ℕ → Prop := λ (n : ℕ), n ≠ 0
end

[Logan Murphy]

I'm not super familiar yet with monads as a programming structure, would it be hard to write a version of io.iterate as a tactic unit? Just looking at how it's used in Lean 3 for Hackers, it would be useful to have a counter of some kind in an iteration.

Specifically, the proof I'm trying to automate is of the form

import system.io tactic data.list
open  io tactic list

def aList : list Prop := [true, true, true]

example (H : ∀ i : fin aList.length, (aList.nth_le i.val i.property)) : false :=
begin
  rw aList at H,
  have h1 := H ⟨0, dec_trivial⟩,
  have h2 := H ⟨1, dec_trivial⟩,
  have h3 := H ⟨2, dec_trivial⟩,
end

It seems that the simplest way to automate this would be to iterate a counter i from 0 to aList.length (for any aList)

tactic.interactive.iterate allows one to specify the size of the loop, but not to refer to the counter variable

[Mario Carneiro]

It's easy to do unbounded iteration using a recursive function

[Mario Carneiro]

you don't need io for that

[Mario Carneiro]

By the way, your proof looks a lot like fin_cases

[Mario Carneiro]

Here's a really literal interpretation of how you could automate that:

example (H : ∀ i : fin aList.length, (aList.nth_le i.val i.property)) : false :=
begin
  rw aList at H,
  (do (list.range 3).mmap' (λ i, do
    let h : name := ("h" ++ to_string (i+1) : string),
    tactic.interactive.«have» h none ```(H ⟨%%(reflect i), dec_trivial⟩))),
end

[Logan Murphy]

Hey @Mario Carneiro (or anyone), would you be able to help me understand how some of the parser code you sent works? I'm not familiar with using a monad for parsing.

import system.io tactic data.list
open  io tactic list
open lean lean.parser tactic interactive

meta def from_file {α : Type}
(f : string)
(p : lean.parser α) : lean.parser α :=
do
  buf ← unsafe_run_io (io.fs.read_file f), -- this is clear
  x ← with_input p buf.to_string,  -- not sure what this is doing
  return (prod.fst x) -- returns something of type lean.parser (types.texpr)

meta def load_parser
{α : Type}
(p : lean.parser α) : lean.parser α :=
do t ← types.texpr, -- fine
   f ← ↑(to_expr t >>= eval_expr string),  -- not sure what this does
   from_file f p

meta def tactic.interactive.load
(e : parse (load_parser types.texpr)) : tactic unit :=
interactive.exact e

Additionally, I'm wondering if there's a way to get expressions which are loaded by the parser in this fashion into the scope of a begin...end block, in the following sense. I want to parse an expression from, say a file, and call a tactic from io.run_cmd which sets the goal to be something containing that expression, and prove it. For instance, I'd like to be able to write something like

inductive even : ℕ → Prop
| zero : even 0
| add2 : ∀ n : ℕ, even n → even (n+2)

meta def silly : tactic unit :=
applyc `even.zero

-- input.txt :
-- 0

meta def main : io unit :=
 let INPUT := by `[load "/path/to/input.txt"] in
 io.run_tactic $ do `[have : even INPUT], silly,
 return ()

But I don't think I can refer to things like INPUT outside the [ block ] like this.

Any help greatly appreciated :)

[Logan Murphy]

The whole idea being that i can call main from some other process and see what Lean does with the contents of the file

[Jason Rute]

There are three ways you can get to io: (1) A main : io unit def, (2) inside a tactic monad via tactic.unsafe_run_io and (3) inside a parser monad via parser.of_tactic t where t calls tactic.unsafe_run_io. Only the parser has access to the parser monad. However, you can make your own custom lean command which runs the parser monad and that can then get information from a file and parse it. (You can even pass around the parser state to other monads so they can use it to parse stuff.) I need to think through your use case and then I can give you more advice with some code.

[Jason Rute]

Also, I have a fairly involved private WIP repo which uses these techniques to have lean communicate with stdin/stdout or with python as a subprocess. If you want an invite, I can give you one.

[Jason Rute]

Also, I should say that if you are only parsing simple things like numbers or such, you could also do one of the following:

1. write your own parser in lean which parses a string from scratch into whatever type of object you like. Lean has a few built in operations already for converting strings to numbers, etc, for example string.to_nat. You probably want to use meta, but you shouldn't need to use tactic, io, or parse monads unless you want to use them for convenience of error handling.
2. Use the library data.buffer.parser which despite its name is a separate parser monad from lean.parser. For example, I've used this to write a JSON parser. However, it is really slow and something Mario said, makes me think that this is a necessary consequence of using a parsing monad like this.

Both of these are available to be used inside the tactic or io monads. However, they don't have good support for parsing Lean expressions.

[Logan Murphy]

Thank you very much Jason, I'll digest this and let you know re: your repo :)

[Jason Rute]

I'll try to write code up some examples, but I don't know if I'll get to it tonight.

[Jason Rute]

Oh, I just looked at Mario's code that you posted. I'll comment what the pieces are doing and show you how to use it to set the goal. I was in the same place a few months ago. This was all very confusing. If you haven't read them, I also recommend the following background material:

• https://leanprover-community.github.io/extras/tactic_writing.html
• https://agentultra.github.io/lean-for-hackers/

[Jason Rute]

Here is a heavily commented version of Mario's code. Hopefully, this will help to understand what is going on. I tried to avoid too much fancy notation to make it a bit easier to follow.

import system.io
open io tactic list
open lean lean.parser tactic interactive

/-- Runs parser `p` on the contents of the file path `f`.
This parser is nonstandard.  It ignores the buffer it
is supposed to parse and instead does an io operation to
read the contents of file path `f` into another buffer
and runs the parser `p` on that buffer. -/
meta def from_file {α : Type}
(f : string)
(p : lean.parser α) : lean.parser α :=
do
  -- converts the io monad operation of reading a file
  -- into a parser monad operation,
  -- returning the file buffer.
  buf ← unsafe_run_io (io.fs.read_file f),
  -- with_input temporarily replaces the buffer being
  -- parsed with a string (`buf.to_string` in this case)
  -- and runs the parser `p` on that string.
  (a, s) ← with_input p buf.to_string,
  -- with_input returns a pair `(a, s)` where
  -- `a` is the result of parser `p`
  -- and `s` is the string that was parsed.
  -- we only want to return the result `a`.
  return a

/- This parser reads a file path from the buffer
(which will be a particular location in the lean
file where this is run)
as a quoted string, e.g. "myfile.txt", and
runs the parser `p` on the file contents. -/
meta def load_parser
{α : Type}
(p : lean.parser α) : lean.parser α :=
do
   -- read a filename from the buffer
   -- as a pre-expression
   t ← types.texpr,
   -- that pre-expression needs to be converted
   -- a string.  This is usually done at the
   -- tactic level, but we need to stay at the parser
   -- level to run the parser `p` later, so we do a
   -- a computation in the tactic monad and lift it
   -- back up to the parser monad.
   f ← of_tactic (do
      -- now we are in the tactic monad
      -- convert the pre-expression `t` to an expression `e`
      e <- to_expr t,
      -- evaluate this expression as a string
      s <- eval_expr string e,
      -- return that string as the result of this tactic block
      return s
   ),
   -- run parser `p` on contents of file path `f`
   e <- from_file f p,
   return e

-- There are now two ways we can run our load_parser:
--   1. As the parameter of an interactive tactic.
--   2. Via a user command.

-- Here we do the first approach.
-- We will read a proof from a file and apply that
-- to our goal.

/-- This tactic will run a proof stored in a file.
Specifically `load "myfile.txt"` will load a proof
term saved in the file "myfile.txt" and use that
(inside an `exact` tactic) to complete the proof. -/
meta def tactic.interactive.load
-- In interative tactics, parameters take the form
-- `(<var> : parse <some_parser>)`
-- This means after the `load` tactic keyword, run
-- the parser `<some_parser>` to parse what the first
-- argument should be, and set `<var>` to be that value.
-- In this case, `e` will be the pre-expression
-- stored in the file path string which comes after
-- the `load` keyword.
(e : parse (load_parser types.texpr)) : tactic unit :=
-- take our expression e (which should be a proof term)
-- and attempt to prove the goal with it
interactive.exact e

example (x : ℕ) (h : x > 0) : ∃ y, y < x := begin
   load "/tmp/my_file1.txt"  -- exists.intro 0 h
end

[Jason Rute]

Also, an object of type parser α is roughly a function of type parser_state -> parser_state × α. The parser_state is essentially some buffer being parsed (i.e. usually the lean file) and the current position being read. (It also has some information about the environment and settings, but I'm ignoring that.) So a parser reads in a state and returns a new state and the parsed value. The monadic stuff hides the parser state so each line a <- my_parser in the do block is essentially saying run the parser on the buffer (possibly changing the parser state) and return the result a. The final return a is saying to return a : α, but in actuality we aren't building an object of type α, but instead an object of type parser α which is itself (roughly) a function. A parser is basically a delayed execution which will only return the result a at the point when it has some actual buffer to parse. This happens when it is run as part of an interactive tactic.

[Jason Rute]

I'm also working on coding up your other request which reads from a file, sets the goal, and runs a tactic on that goal.

[Logan Murphy]

That's incredible Jason, thanks so much for taking the time to help me understand this!

[Jason Rute]

@Logan Murphy Here is one (of many) ways you can solve the second half of your question. As I said above, you can't access the lean parser framework inside the io monad, so you can't use it inside tactics or a main : io unit. But you can use a user command instead. Here is an example (which reuses Mario's code above):

[Jason Rute]

inductive even : ℕ → Prop
| zero : even 0
| add2 : ∀ n : ℕ, even n → even (n+2)

-- we break down the task into a few helper
-- tactics.  These might already be in mathlib.

/-- Sets the goal to the given expression,
ignoring the current goal. -/
meta def set_goal (goal : expr) : tactic unit :=
do
   -- Set metavariable for our goal.
   v <- mk_meta_var goal,
   -- Replace goal list with our goal
   set_goals [v],
   return ()

/-- Returns tt if no more goals, else false -/
meta def is_solved : tactic bool :=
-- the pattern ... >> ... <|> ...
-- is like a monadic if then else
done >> return tt <|> return ff


/-- Replaces the  current goals with `goal`,
applies `tac`, and returns if the goal is
solved. -/
meta def try_tactic_on_goal (tac: tactic unit)
(goal : expr) : tactic bool := do
   -- We will ignore the current goal
   -- (which is `|- true` inside a parser).
   set_goal goal,
   -- For debugging:
   trace_state,
   -- apply tac
   try tac,
   -- For debugging:
   trace_state,
   -- check if solved
   -- (and since this is the last tactic,
   -- in the do block, return it's result)
   is_solved

/-- A user command.  It is technically a
parser, but we will actually be using it
to run some code.  However, since it is
a parser we can use our `from_file`
parser from above in the code. -/
@[user_command]
meta def main_app
(meta_info : decl_meta_info)
(_ : parse (tk "main_app")) : lean.parser unit :=
-- the above is user command boilerplate
-- below is the code
do
   -- get contents of file as a pre-expression
   t <- from_file "/tmp/my_file2.txt" types.texpr,
   -- now that we are done with the parser,
   -- everything else can be done in the tactic monad
   of_tactic (do
      e <- to_expr t,
      n <- eval_expr ℕ e,
      let goal := `(even n),
      let tac := `[apply even.zero],
      success <- try_tactic_on_goal tac goal,
      if success then
         trace "Solved!"
      else
         trace "Not solved :("
   )

-- We put a period here to let lean know to stop
-- parsing the above definition.  I don't know
-- exactly why it is needed.
.
-- /tmp/my_file2.txt  0
main_app   --  |- even 0
           --  Solved!

[Jason Rute]

You could run the above as a stand alone program with lean your_file.lean. Right now it outputs via traces, but you could use the IO framework instead and output to stdout. (Traces are easier to work with in VS Code.)

[Jason Rute]

One thing you will notice about the above code is that all the work is done in the tactic monad, but we need the parser monad for just some key parsing tasks. One fancy trick I've discovered is that we could "steal" the parser state from the parser monad and give it as an argument to a tactic. This allows us to better organize the code. Here is what that would look like.

/-- Run a parser inside as a tactic.
It's unsafe in that you don't expect a
tactic to consume the buffer being parsed.
Best to only use with parsers that don't
consuming the buffer. -/
meta def unsafe_run_parser (ps : parser_state)
{α : Type} (p : parser α) : tactic α :=
-- Since parser and tactic frameworks are
-- the same, can replaces the parser state
-- with the tactic state.
λ ts : tactic_state, match (p ps) with
| result.success a _ := result.success a ts
| result.exception fmt pos _ := result.exception fmt pos ts
end

/-- The tactic which does all the work -/
meta def main_t (ps : parser_state) : tactic unit :=
do
   -- now that I have a parser state,
   -- I can do parser things inside tactics:
   buf ← unsafe_run_io (io.fs.read_file "/tmp/my_file.txt"),
   (t, s) ← unsafe_run_parser ps (
      with_input types.texpr buf.to_string
   ),
   e <- to_expr t,
   n <- eval_expr ℕ e,
   let goal := `(even n),
   let tac := `[apply even.zero],
   success <- try_tactic_on_goal tac goal,
   if success then
      trace "Solved!"
   else
     trace "Not solved :("

/-- Return the parser_state. -/
meta def get_state : parser parser_state :=
λ ps, result.success ps ps

@[user_command]
meta def main_app2
(meta_info : decl_meta_info)
(_ : parse (tk "main_app")) : lean.parser unit :=
do
  ps <- get_state,
  of_tactic (main_t ps)

[Jason Rute]

This trick is only good for user commands I think. I don't think you could use it in Mario's example.

[Mario Carneiro]

Well, whenever lean calls out to the parser monad you can do it. In my example I used tactic argument parsing to capture a parser_state

[Jason Rute]

But you can’t pass that state to the body of the interactive tactic. It would seem clearer to do the file IO in the tactic body.

[Mario Carneiro]

Actually you can, although I have no idea what would happen if you did

[Mario Carneiro]

you can just use parse read where def read : parser parser_state := \lam s, (return s) s

[Mario Carneiro]

Oh, that probably doesn't work because parser_state is not serializable

[Mario Carneiro]

it doesn't implement has_reflect and I think this is required by parse because it is used during the desugaring of the tactic block to an expression that will be eval_expr'd

[Jason Rute]

Exactly.

[Jason Rute]

Sorry for all the messages. I've been thinking about this subject a lot. One final point I want to make (again), is that one often doesn't need the Lean parser as much as one thinks. The one thing the lean parser is really good at is parsing "user readable" Lean expressions with special notation, overloaded operators, etc. But usually what one wants to store in a file is data. Here are two common cases:

• store data in a standard format, e.g. JSON. This is what we were doing with the setting a goal example. We read in a number string and converted that to a number in Lean. Using the lean parser was overkill, since we could just use string.to_nat. I also just discovered that newer versions of Lean have a JSON parser built in. And even if it didn't you could write your own in Lean (I'll send you an example). This doesn't require the lean parser at all.
• store Lean expressions as text. This is what Mario's example does. All we needed the lean parser for was to turn a string into an expression. But again, we could have stored that proof term in a more machine readable form. Lean IO has a few built-in ways to serialize and deserialize expressions to/from a file. Also, one can serialize an expression to a string. The built in ones might not suit your needs, but again it is not very hard to write a serializer and deserializer for expressions in Lean that don't require the lean parser (I'll also send you an example serializing and deserializing expressions into/from s-expressions).

[Logan Murphy]

This is great Jason, thank for being so thorough. This will be great for helping me move my project forward.

I'm seeing how I can use your code for the particular task I'm trying to automate. I think this is only tangentially related to what you wrote, but I'm basically trying to substitute some custom structures instead of the natural numbers in the example, and trying to figure out how to resolve a reflected instance. I think from reading the docs that reflected is closely related to has_repr, but aside from that I'm not sure what I need to be doing in this case. Here are the structures I'm trying to use.

If Lean just needs some string formatting for the structure, I'm happy with just using some placeholder string for now, just don't know how to tell Lean what to use (if I understand the nature of the type class reflected).

def Property (α : Type) : Type := α → Prop

structure Claim (α : Type) :=
(X : set α)
(P : Property α)

structure strategy (α : Type) :=
(Clm : Claim α)
(Props : list (Property α))

@[derive fintype]
inductive foo
| a
| b
| c
| d

def contra (α : Type)
(S : strategy foo ) : Prop :=
∀ x, ¬(S.Clm.P x) → (∃ i : fin (S.Props.length), (S.Props.nth_le i.1 i.2) x)

meta def silly_tactic : tactic unit :=
 do
 `[  intros n H,
     fin_cases n,
     simp at *,
     exfalso, assumption,
     use 0, simp, dsimp, refl,
     use 1, simp, dsimp, refl,
     use 2, simp, dsimp, refl]

--- path/to/input.txt file :
-- (strategy.mk
-- (Claim.mk {foo.a} (λ n, n = foo.a))
-- [(λ n, n=foo.b),
--  (λ n, n=foo.c),
--  (λ n, n=foo.d)])


@[user_command]
meta def main_app
(meta_info : decl_meta_info)
(_ : parse (tk "main_app")) : lean.parser unit :=
-- below is the code
do
   -- get contents of file as a pre-expression
   t <- from_file "/path/to/input.txt" types.texpr,
   -- now that we are done with the parser,
   -- everything else can be done in the tactic monad
   of_tactic (do
      e <- to_expr t,
      S <- eval_expr (strategy foo) e,
      let goal := `(contra foo S),
      --  failed to synthesize type class instance for
      --  ⊢ reflected (contra foo S)
      let tac := `[silly_tactic],
      success <- try_tactic_on_goal tac goal,
      if success then
         trace "Solved!"
      else
         trace "Not solved :("
   )

[Mario Carneiro]

You can @[derive has_reflect] on inductives

[Logan Murphy]

Still getting the same error, should I be making a local instance like

@[instance]
meta def contra_foo.refl {S : strategy foo} : has_reflect (contra foo S) := sorry

[Mario Carneiro]

what's the #mwe?

[Mario Carneiro]

the code above is missing imports and also doesn't have a failing example

[Mario Carneiro]

If the error you are talking about is the let goal, you should try let goal := `(contra foo %%S),, since S is coming from the tactic context

[Logan Murphy]

Sorry, I think this is as minimal as I can get it right now

import system.io tactic
open io tactic list
open lean lean.parser tactic interactive


/-- Jason and Mario's parser code --/
meta def from_file {α : Type}
(f : string)
(p : lean.parser α) : lean.parser α :=
do
  buf ← unsafe_run_io (io.fs.read_file f),
  (a, s) ← with_input p buf.to_string,
  return a

meta def load_parser
{α : Type}
(p : lean.parser α) : lean.parser α :=
do
   t ← types.texpr,
   f ← of_tactic (do
      e <- to_expr t,
      s <- eval_expr string e,
      return s
   ),
   e <- from_file f p,
   return e

meta def tactic.interactive.load
(e : parse (load_parser types.texpr)) : tactic unit :=
interactive.exact e


meta def set_goal (goal : expr) : tactic unit :=
do
   v <- mk_meta_var goal,
   set_goals [v],
   return ()

/-- My custom structures/types --/

def Property (α : Type) : Type := α → Prop

structure Claim (α : Type) :=
(X : set α)
(P : Property α)

structure strategy (α : Type) :=
(Clm : Claim α)
(Props : list (Property α))

@[derive [fintype, has_reflect]]
inductive foo
| a
| b
| c
| d

def contra (α : Type)
(S : strategy foo ) : Prop :=
∀ x, ¬(S.Clm.P x) → (∃ i : fin (S.Props.length), (S.Props.nth_le i.1 i.2) x)

meta def silly_tactic : tactic unit :=
 do
 `[  intros n H,
     fin_cases n,
     simp at *,
     exfalso, assumption,
     use 0, simp, dsimp, refl,
     use 1, simp, dsimp, refl,
     use 2, simp, dsimp, refl]

--- path/to/input.txt file :
-- (strategy.mk
-- (Claim.mk {foo.a} (λ n, n = foo.a))
-- [(λ n, n=foo.b),
--  (λ n, n=foo.c),
--  (λ n, n=foo.d)])


@[user_command]
meta def main_app
(meta_info : decl_meta_info)
(_ : parse (tk "main_app")) : lean.parser unit :=
-- below is the code
do
   -- get contents of file as a pre-expression
   t <- from_file "/path/to/input.txt" types.texpr,
   -- now that we are done with the parser,
   -- everything else can be done in the tactic monad
   of_tactic (do
      e <- to_expr t,
      S <- eval_expr (strategy foo) e,
      let goal := `(contra foo S),
      --  failed to synthesize type class instance for
      --  ⊢ reflected (contra foo S)
      let tac := `[silly_tactic],
      return ()
   )
.
main_app

[Mario Carneiro]

I think you actually just need `(contra foo %%e), and skip the eval_expr

[Logan Murphy]

Yes, that 's what I needed . Thank you Mario.

[Logan Murphy]

So by using the antiquotations, we postpone the evaluation of the expr to when main_app is invoked?

[Logan Murphy]

And it's the expr that's reflected, not anything at the object level,e.g. any Prop

[Mario Carneiro]

No, we never evaluate anything here

[Mario Carneiro]

so we don't need has_reflect

[Mario Carneiro]

we're just splicing the expression e we elaborated directly into the term we're making

[Mario Carneiro]

eval_expr is a way for turning expressions into values of various types, and has_reflect is a way to turn values back into expressions

[Mario Carneiro]

they are just canceling each other out here

[Mario Carneiro]

Now it's not entirely correct that they are inverses, for example the expression `(2 + 2 : nat) gets eval_expr'd into 4, which is then reflected into `(4 : nat). So if you wanted to make sure your terms were "normalized" then this would be a way to do it

[Mario Carneiro]

but if you just use the expr as is you don't have to worry about all the ways in which eval_expr fails, for example if it runs across something noncomputable like a variable or an axiom or a pi

[Logan Murphy]

Ah I see. Thank you.

[Joe Palermo (S2'17)]

Is there an easy way to modify a function : x -> tactic x, so that it becomes x -> x? For example, the function tactic.infer_type : expr -> tactic expr. I'd like to create a function that does the same thing but yields 'expr' instead of 'tactic expr'.

I'm aware of mjoin, but my understanding that requires 2 levels of structure in order to apply it (i.e. it's a form of concat).

If you're wondering what I'm actually trying to do, I'm trying to implement the tactic 'extract_theorems' below, and the implementation I thought of requires a modification to tactic.infer_type. I wouldn't be surprised if there's a much better way to implement 'extract_theorems 'as I'm just getting started with Lean metaprogramming and don't really know what I'm doing :P, so I'd appreciate any tips. Thanks!

import meta.expr
open tactic
set_option pp.all true


meta def process_thm (d : declaration) : option declaration :=
let n := d.to_name in
  if ¬ d.is_trusted ∨ n.is_internal then none
  else match d with
       | declaration.defn _ _ _ _ _ _ := none
       | t@(declaration.thm n ns e te) := some t
       | declaration.cnst _ _ _ _ := none
       | declaration.ax _ _ _ := none
       end


meta def library_thms : tactic $ list declaration :=
  environment.decl_filter_map <$> get_env <*> return process_thm


meta def get_all_proofs : tactic $ list expr :=
  do library_thms >>= λ x, return (declaration.value <$> x)


meta def print_proofs : tactic unit :=
  do get_all_proofs >>= λ x, tactic.trace x


meta def extract_theorems : list expr :=
  do get_all_proofs >>= λ exprs, (<MODIFIER FOR INFER_TYPE> ∙ infer_type) <$> exprs

  --exprs : list expr
  --infer_type : expr -> tactic expr
  --<MODIFIER FOR INFER_TYPE> ∙ infer_type : expr -> expr
  --(<MODIFIER FOR INFER_TYPE> ∙ infer_type) <$> exprs : list expr

[Yakov Pechersky]

You can't really change a x -> tactic x into a x -> x. But you can definitely change a list (tactic expr) into a tactic (list expr), using list.traverse

[Yakov Pechersky]

An exercise for you to get a feel for such monadic transformations would be to write your own implementation of list.traverse

[Yakov Pechersky]

Also, since you're writing things with a combo of >>=, <$> and return, you might just switch to do notation

[Yakov Pechersky]

you already have two levels of structure here, you have the tactic monad and the list monad

[Yakov Pechersky]

you might want to restructure your code to have a

declaration -> expr

[Yakov Pechersky]

Because your get_all_proofs is really a tactic.map (list.map declaration.value))

[Yakov Pechersky]

When you have a >>= λ x, return ..., that is just <$>

[Yakov Pechersky]

Provably: docs#is_lawful_monad.bind_pure_comp_eq_map

[Joe Palermo (S2'17)]

@Yakov Pechersky Thanks for the recommendation to use list.traverse. With it I wrote up proofs >>= λ exprs, (list.traverse tactic.infer_type exprs) to get theorem exprs from proof exprs. Then I merged things together using do notation:

meta def extract_theorems : tactic $ list string := do
  library_theorem_decls <- return (environment.decl_filter_map <$> tactic.get_env <*> return process_thm),
  proofs <- return (library_theorem_decls >>= λ x, return (declaration.value <$> x)),
  theorems <- proofs >>= λ exprs, (list.traverse tactic.infer_type exprs),
  return ((λ x: expr, x.to_string ++ "\n") <$> theorems)

I'd like to cleanup the line with "proofs <- ...", using tactic.map as recommended, but I get the error message "unknown identifier 'tactic.map'". I tried import tactic, but apparently there is no tactic.map? Not sure what I'm doing wrong

[Yakov Pechersky]

If you have a

do
  var <- return (op)

that is the same at

do
  let var := op

[Yakov Pechersky]

There is no tactic.map, I just meant functor.map specialized to functor, which you can just write as <$>

[Yakov Pechersky]

Your <*> return ... can also be simplified to a <$>: docs#is_lawful_applicative.seq_pure

[Yakov Pechersky]

What about something like:

meta def decl_to_theorem (d : declaration) : tactic expr := infer_type d.value

meta def extract_theorems : tactic $ list string := do
  env <- tactic.get_env
  let ds := env.decl_filter_map process_thm
  theorems <- ds.traverse decl_to_theorem
  return ((λ x: expr, x.to_string ++ "\n") <$> theorems)

[Joe Palermo (S2'17)]

That's much cleaner! Thank you

[Yakov Pechersky]

Modulo any errors, I'm just guessing the types/API here. One might say, why not just make a decl -> tactic string and print over those?

[Joe Palermo (S2'17)]

Yeah that would be a reasonable way to structure it too

[Yakov Pechersky]

I gather you'll be printing these. I think you should just use list.intersperse theorems "\n", that way you're not just doing the many O(n) list appends, since you're just relying on the "\n" for nice printing

[Yakov Pechersky]

Then you might factor out env <- tactic.get_env to make a env -> tactic (list string), because you might be doing other things with an env

[Yakov Pechersky]

So that you don't have to tactic.get_env elsewhere (if that is an expensive computation, idk if it is)