## Stream: metaprogramming / tactics

### Topic: basic parser use

#### 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
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 (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

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

#### Mario Carneiro (Aug 04 2020 at 18:43):

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

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


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

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


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

#### Mario Carneiro (Aug 04 2020 at 18:47):

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

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

#### Mario Carneiro (Aug 04 2020 at 18:53):

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

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


looks good

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


#### Mario Carneiro (Aug 04 2020 at 18:55):

the interactive tactic should take pexprs for a and b though

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


Nice!

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


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


#### 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.

#### 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.

#### Billy Price (Aug 07 2020 at 07:13):

That's not a mwe gimme a sec

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


#### 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.

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

#### 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?

#### 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.

#### 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.

#### Billy Price (Aug 07 2020 at 09:14):

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

#### 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.

#### Billy Price (Aug 07 2020 at 09:23):

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

#### 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.

#### 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.

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