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