# Zulip Chat Archive

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

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

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 `pexpr`

s 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
```

#### Kevin Buzzard (Aug 04 2020 at 20:18):

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