# Zulip Chat Archive

## Stream: new members

### Topic: basic tactic writing

#### Logan Murphy (Sep 28 2020 at 21:14):

I'm beginning to (try to) build a small library of tactics for a project I'm working on, but I'm still learning the ins and outs of translating interactive proofs to single-tactic proofs, although the tutorial on the community site was very helpful! I was hoping I can use this topic for asking basic questions I find myself with, and thought it would be best to start in this stream, but if I should move to the tactic stream then apologies.

First, I realize that using `simp`

in the middle of a proof is discouraged, but is there a simple way to invoke `simp`

in a tactic? The tactic source files have a bunch of simp-related stuff but I'm still a bit too green to really know what they are doing.

#### Kevin Buzzard (Sep 28 2020 at 21:18):

If I want to run simp in the middle of a tactic proof then I used to run it, copy paste the output to X, delete simp and replace with `suffices : X, by simpa`

#### Kevin Buzzard (Sep 28 2020 at 21:18):

But now I run squeeze_simp instead and then click on the output

#### Kevin Buzzard (Sep 28 2020 at 21:19):

Oh I see you're asking something else maybe. Why not just run simp in the middle of your tactic? Tidy does this and I think norm_num too

#### Logan Murphy (Sep 28 2020 at 22:05):

I couldn't seem to be able invoke `simp`

in a meta-def tactic like in an interactive proof, but i can do so with `tidy`

, thanks Kevin!

#### Mario Carneiro (Sep 28 2020 at 22:10):

You can use ` `[simp]`

to create a `tactic unit`

object which calls the interactive `simp`

tactic

#### Mario Carneiro (Sep 28 2020 at 22:10):

i.e.

```
def my_tac : tactic unit := do
x <- bla,
`[simp],
exact x
```

#### Logan Murphy (Sep 28 2020 at 22:11):

ah, good to know.

#### Mario Carneiro (Sep 28 2020 at 22:11):

you can also call `tactic.interactive.simp`

directly, or one of the more basic non-interactive tactics used by simp, but then you have to get all the arguments right which is a bit of a pain

#### Logan Murphy (Sep 29 2020 at 13:49):

Now trying something a bit more involved. I have a basic relation between a predicate and a vector of predicates I'm trying to reason about

```
def justified {α : Type} {n : ℕ}
(P : α → Prop)
(Ps : vector (α → Prop) n) : Prop :=
let Xs := λ i, {x | (Ps.nth i) x} in
(⋂ i, Xs i) ⊆ {x | P x}
```

A trivial example of its use is given here, simply splitting up the definition of `nat.prime`

into simpler predicates

```
example :
justified
nat.prime
⟨ [(λ n, n ≠ 0 ),
(λ n, n ≠ 1),
(λ n, ∀ (m : ℕ), m ∣ n → m = 1 ∨ m = n)], by refl⟩ :=
begin
intro n, simp, intros H,
have H1 : n ≠ 0:=
H ⟨0, by simp⟩,
have H2 : n ≠ 1:=
H ⟨1, by simp⟩,
have H3 : (∀ (m : ℕ), m ∣ n → m = 1 ∨ m = n):=
H ⟨2,by simp⟩,
split,
omega nat, assumption, -- omega for now just to shorten proof
end
```

what I am trying to do is to automate the above proof. At the moment, I'm trying to tactic-ify the `have H1 : n ≠ 0:`

line. I tried applying some of the techniques from the Tactic writing tutorial, something like

```
meta def mytac : tactic unit :=
do
`(justified %%a %%b) ← target,
n ← get_unused_name `n,
H ← get_unused_name `H,
expr_n ← intro n,
`[simp],
expr_H ← intro H,
H1 ← get_unused_name `H1,
«have» H1 `(ne n 0) ``(%%expr_H ⟨0, by simp⟩),
return ()
```

I'm having trouble using the constant `0`

in the second last line of the tactic. I think I'm missing some knowledge of handling names and the backtick-notation. Any pointers?

#### Logan Murphy (Oct 02 2020 at 01:03):

I'm trying to get some I/O from a tactic, specifically one that iterates/repeats a tactic. Given a simple example like the following,

```
import tactic
open tactic
meta def mytactic : tactic unit :=
do
`[repeat {split}],
(iterate
`[{assumption}])
<|>
fail "this failed",
return ()
```

I'd like to modify the tactic such that if `iterate [assumption]`

clears all goals, it will `tactic.trace`

something like `success!`

, while if there are goals left after the `iterate`

it will `tactic.trace`

`this failed`

. How could I go about doing this?

#### Scott Morrison (Oct 02 2020 at 03:44):

There is a `done`

tactic, which fails if there are any goals.

#### Scott Morrison (Oct 02 2020 at 03:45):

So `(done >> X) <|> Y`

branches on whether you've succeeded or not

#### Jason Rute (Oct 02 2020 at 11:30):

Also, if you are not familiar with it, Tutorial: tactic writing in Lean is a pretty good resource which discusses some of this stuff.

Last updated: May 13 2021 at 18:26 UTC