basic tactic writing

Stream: new members

[Logan Murphy]

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]

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]

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

[Kevin Buzzard]

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]

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]

You can use `[simp] to create a tactic unit object which calls the interactive simp tactic

[Mario Carneiro]

i.e.

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

[Logan Murphy]

ah, good to know.

[Mario Carneiro]

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]

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]

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]

There is a done tactic, which fails if there are any goals.

[Scott Morrison]

So (done >> X) <|> Y branches on whether you've succeeded or not

[Jason Rute]

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