Zulip Chat Archive

Stream: new members

Topic: basic tactic writing


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 21:18):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Sep 28 2020 at 22:10):

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

view this post on Zulip Mario Carneiro (Sep 28 2020 at 22:10):

i.e.

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

view this post on Zulip Logan Murphy (Sep 28 2020 at 22:11):

ah, good to know.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Oct 02 2020 at 03:44):

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

view this post on Zulip Scott Morrison (Oct 02 2020 at 03:45):

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

view this post on Zulip 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