Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: basic parser use


view this post on Zulip Jalex Stark (Aug 04 2020 at 17:43):

as an exercise, I want to write the tactic that makes this proof work

example {α : Type*} {a b : α} [linear_order α]
  (h1 : ¬ a < b) (h1 : ¬ a = b) (h1 : ¬ b < a) : false :=
begin
  trichotomy a b; contradiction
end

I'm pretty sure the answer is to write something like the following, and then to write an interactive wrapper around it

import data.real.basic
import tactic

open tactic expr

meta def tactic.trichotomy (a b : expr) (h : name) : tactic unit :=
`[rcases lt_trichotomy a b with h|h|h]

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:44):

the tactic.trichotomy above should be using some kind of anti-quoting for the a and b, e.g. the following introduces hypotheses about a and b instead of 0 and 1:

example {α : Type*} {a b : α} [linear_order α]
  (h1 : ¬ a < b) (h1 : ¬ a = b) (h1 : ¬ b < a) : false :=
begin
  tactic.trichotomy `(0) `(1) `h,
end

If i change a to %%a in the definition of trichotomy then I get a "kernel failed to type check declaration " error

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:07):

maybe i should focus on the easier task of adding lt_trichotomy a b to the local context

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:43):

You could construct the input to the interactive rcases tactic without using `[...]

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:43):

Something vaguely like this?

import tactic
open tactic expr

meta def tactic.trichotomy (a b : expr) (h : name) : tactic unit :=
do v  mk_app `h [``(lt_trichotomy), a, b],

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:45):

The thing I wrote above has lots of problems, but the one I'm most confused about is that
``(lt_trichotomy) has type expr ff instead of type expr, which I think means it's not elaborated

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:46):

meta def tactic.trichotomy (a b : expr) (h : name) : tactic unit :=
rcases none ```(lt_trichotomy a b)
  [[rcases_patt.one `h], [rcases_patt.one `h], [rcases_patt.one `h]]

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:47):

That doesn't actually use the parameters, it is equivalent to `[rcases lt_trichotomy a b with h|h|h]

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:47):

but it should be more obvious how to insert the parameters now

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:53):

it's not transparent to me after poking at it for a couple of minutes, but I feel like I'm close to having a precise question

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:53):

To do the mk_app, you should do mk_app ``lt_trichotomy [a, b]

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:55):

so this might be correct?

meta def tactic.trichotomy (a b : expr) (h : name) : tactic unit :=
do v  mk_app ``lt_trichotomy [a, b],
rcases none (pexpr.of_expr v)
  [[rcases_patt.one h], [rcases_patt.one h], [rcases_patt.one h]]

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:55):

looks good

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:55):

then i should be able to write something like this

example {α : Type*} {c d : α} [linear_order α]
  (h1 : ¬ c < d) (h1 : ¬ c = d) (h1 : ¬ d < c) : false :=
begin
  tactic.trichotomy %%(reflect c) %%(reflect d) `h,
end

view this post on Zulip Mario Carneiro (Aug 04 2020 at 18:55):

the interactive tactic should take pexprs for a and b though

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:57):

ooh, it works now

import tactic

section tactic
open tactic expr

meta def tactic.trichotomy (a b : expr) (h : name) : tactic unit :=
do v  mk_app ``lt_trichotomy [a, b],
rcases none (pexpr.of_expr v)
  [[rcases_patt.one h], [rcases_patt.one h], [rcases_patt.one h]]

namespace tactic.interactive
setup_tactic_parser

open interactive interactive.types expr
meta def trichotomy (a b : parse parser.pexpr) : tactic unit :=
do a  to_expr a, b  to_expr b,
  tactic.trichotomy a b `h

end tactic.interactive
end tactic

example {α : Type*} {c d : α} [linear_order α]
  (h1 : ¬ c < d) (h1 : ¬ c = d) (h1 : ¬ d < c) : false :=
begin
  trichotomy c d,
end

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:18):

Nice!

view this post on Zulip Billy Price (Aug 07 2020 at 03:16):

I want to do a similar thing, but essentially I'd like to abbreviate apply foo a b to Foo a b, but I'm not sure how to work with a texpr. The only thing that doesn't work for me below is apply h, since h is an expr, not a parse texpr (I don't understand what a texpr is).

namespace tactic
namespace interactive

setup_tactic_parser

meta def AndLeft_aux (a b : expr) : tactic unit :=
  do h  tactic.mk_app `and_left [a,b], apply h

meta def AndLeft (a b : parse parser.pexpr) : tactic unit :=
  do a  to_expr a, b  to_expr b, AndLeft_aux a b

end interactive
end tactic

view this post on Zulip Billy Price (Aug 07 2020 at 06:59):

So I realised there is tactic.apply, and I have a compiling definition now, but it doesn't quite work, because it can't infer one of the arguments, Is this because tactic.apply doesn't see the target or something?

meta def AndLeft (A B : parse parser.pexpr) : tactic unit :=
  do A  to_expr A, B  to_expr B, tactic.mk_app `nat_deduction.deduction.and_left [A, B] >>= tactic.apply, skip

view this post on Zulip Rob Lewis (Aug 07 2020 at 07:11):

tactic.apply does see the target. But mk_app is expecting to create a fully elaborated expr. So if you're not giving that enough info it could fail to infer an argument.

view this post on Zulip Rob Lewis (Aug 07 2020 at 07:11):

(Oops, mwe is above, sorry. I only saw the last post.) Well, kind of, I still can't test it and see the error.

view this post on Zulip Billy Price (Aug 07 2020 at 07:13):

That's not a mwe gimme a sec

view this post on Zulip Billy Price (Aug 07 2020 at 07:32):

I'd like to replace apply deduction.and_left p q in the first line of the example proof with ⋀E₁ p q, (but intermediately I need AndLeft p q to work)

import tactic

@[derive decidable_eq]
inductive Form : Type
| bot : Form
| atom :   Form
| and : Form  Form  Form
| or  : Form  Form  Form
| imp : Form  Form  Form

def Form.neg (A : Form) : Form := Form.imp A Form.bot

instance nat_coe_Form : has_coe  Form := Form.atom

infix `  `:75 := Form.and
infix `  `:74 := Form.or
infix `  `:75 := Form.imp
notation `` := Form.bot
prefix `¬` := Form.neg
notation `` := ¬

inductive deduction : set Form  Form  Type
| weakening  {X} {A Y}     : deduction X A  deduction (X  Y) A
| assumption {X} {A}       : (A  X)  deduction X A
| and_intro  {X} {A B}     : deduction X A  deduction X B  deduction X (A  B)
| and_left   {X} (A B)     : deduction X (A  B)  deduction X A
| and_right  {X} (A B)     : deduction X (A  B)  deduction X B
| imp_intro  {X} {A B}     : deduction (X  {A}) B  deduction X (A  B)
| imp_elim   {X} (A) {B}   : deduction X (A  B)  deduction X A  deduction X B
| or_left    {X} {A B}     : deduction X A  deduction X (A  B)
| or_right   {X} {A B}     : deduction X B  deduction X (A  B)
| or_elim    {X} (A B) {C} : deduction X (A  B)  deduction (X  {A}) C  deduction (X  {B}) C  deduction X C
| falsum     {X} {A}       : deduction X   deduction X A

infix `  `:60 := deduction

namespace tactic
namespace interactive

setup_tactic_parser

meta def AndLeft (A B : parse parser.pexpr) : tactic unit :=
  do A  to_expr A, B  to_expr B, tactic.mk_app `nat_deduction.deduction.and_left [A, B] >>= tactic.apply, skip

end interactive
end tactic

variables {p q r : }

open deduction

example : {p  q}  p :=
begin
  apply deduction.and_left p q,
  apply deduction.assumption,
  exact set.mem_singleton _
end

view this post on Zulip Rob Lewis (Aug 07 2020 at 09:05):

I get an error when I try to apply AndLeft p q because the example doesn't contain nat_deduction.deduction.and_left.

view this post on Zulip Billy Price (Aug 07 2020 at 09:09):

Ah yeah that was a translation to mwe error, removing the prefix nat_deduction. fixes it, and introduces the original problem [app_builder] failed to create an 'deduction.and_left'-application, failed to solve unification constraint for #2 argument (?x_0 ≻ ?x_1 ⋀ ?x_2 =?= ℕ)

view this post on Zulip Billy Price (Aug 07 2020 at 09:11):

So clearly tactic.mk_app is trying to unify the metavariables - but can't expr's have meta variables in them? Why is it trying to figure them out?

view this post on Zulip Rob Lewis (Aug 07 2020 at 09:12):

Ah. Yes, as I assumed the problem is with the mk_app. deduction.and_left takes an implicit X and explicit A, B. You give it the later arguments but not enough info to infer the former.

view this post on Zulip Billy Price (Aug 07 2020 at 09:12):

Do I need to do it all within apply directly somehow? I failed to get that to compile earlier.

view this post on Zulip Billy Price (Aug 07 2020 at 09:14):

And why can't mk_app just leave the metavariables in place?

view this post on Zulip Rob Lewis (Aug 07 2020 at 09:18):

You can do

meta def AndLeft (A B : parse parser.pexpr) : tactic unit :=
  do to_expr ``(deduction.and_left %%A %%B) >>= tactic.apply, skip

which will leave the uninstantiated mvars as new goals.

view this post on Zulip Billy Price (Aug 07 2020 at 09:23):

Awesome! Why does that work and the mk_app version doesn't?

view this post on Zulip Rob Lewis (Aug 07 2020 at 09:27):

mk_app won't create new goals when you don't provide it enough information to fill in the implicit arguments. It also won't insert coercions like you're doing here.

view this post on Zulip Billy Price (Aug 07 2020 at 09:38):

Gotcha. What about concat_tags? What does that do? I saw it in the definition of apply.

view this post on Zulip Jannis Limperg (Aug 07 2020 at 11:30):

concat_tags and propagate_tags create goal tags for the new goals produced by apply. A goal tag is the annotation that tells you which case of an induction or cases you're in, e.g. nat.succ, list.nil. New goals don't have any tag associated with them by default, so concat_tags/propagate_tags take the tags from the original goal and munge them appropriately. If you're writing tactics for your own specialised use, you don't need to worry about this. Otherwise just copy whatever apply uses.


Last updated: May 09 2021 at 21:10 UTC