basic parser use

Stream: metaprogramming / tactics

[Jalex Stark]

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]

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

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],

[Jalex Stark]

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

[Mario Carneiro]

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]]

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

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]]

[Mario Carneiro]

looks good

[Jalex Stark]

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

[Mario Carneiro]

the interactive tactic should take pexprs for a and b though

[Jalex Stark]

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

[Kevin Buzzard]

Nice!

[Billy Price]

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

[Billy Price]

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

[Rob Lewis]

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.

[Rob Lewis]

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

[Billy Price]

That's not a mwe gimme a sec

[Billy Price]

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

[Rob Lewis]

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

[Billy Price]

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 =?= ℕ)

[Billy Price]

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?

[Rob Lewis]

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.

[Billy Price]

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

[Billy Price]

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

[Rob Lewis]

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.

[Billy Price]

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

[Rob Lewis]

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.

[Billy Price]

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

[Jannis Limperg]

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.