Zulip Chat Archive

Stream: general

Topic: Using the rw tactic inside a tactic


view this post on Zulip Frédéric Le Roux (May 15 2020 at 19:05):

I would like to have a tactic exist_elim that, when we have something like
∃ (r : ℝ) (H : r > 0)
introduces a variable r and get rid of the ∃ (H : r > 0)
by applying rw [exists_prop].

But I do not know how to use rwinside a tactic.
So far I have tried this:
meta def existeelim (names : parse ident*) : tactic unit := match names with | [nom_var, nom_hypo] := do nom_h ← get_local nom_hypo, cases_core nom_h [nom_var, nom_hypo], rewrite_hyp exists_prop nom_hypo | _ := fail "existe demande un nom de propriété et un nom de variable" end
But rewrite_hyp fails because exists_prop does not have type expr.

view this post on Zulip Mario Carneiro (May 15 2020 at 19:06):

does cases h, rw [exists_prop] work?

view this post on Zulip Mario Carneiro (May 15 2020 at 19:07):

I could have sworn that someone implemented this already (@Patrick Massot ?)

view this post on Zulip Jalex Stark (May 15 2020 at 19:07):

Is this what erw is about?
EDIT: no, per mario below

view this post on Zulip Mario Carneiro (May 15 2020 at 19:07):

no

view this post on Zulip Mario Carneiro (May 15 2020 at 19:08):

You can write `[rw [exists_prop]] to call the interactive tactic rw [exists_prop] inside another (non-interactive) tactic

view this post on Zulip Johan Commelin (May 15 2020 at 19:08):

@Frédéric Le Roux tip: #backticks use ``` for code formatting in blocks

view this post on Zulip Frédéric Le Roux (May 15 2020 at 19:15):

@Johan Commelin Thanks, it looks better now!

view this post on Zulip Frédéric Le Roux (May 15 2020 at 19:34):

@Mario Carneiro
But how do I specify the location? I tried `[rw [exists_prop] at nom_h] and `[rw [exists_prop] at nom_hypo]
and both fail:
get_local tactic failed, unknown 'nom_hypo' local
get_local tactic failed, unknown 'nom_h' local

view this post on Zulip Mario Carneiro (May 15 2020 at 19:43):

If you have variables, then you probably can't use the interactive tactics and have to instead mimic what they do. In this case, I think rewrite_hyp takes an expr, so you should convert ```(exists_prop), which is a pexpr to an expr using to_expr

view this post on Zulip Patrick Massot (May 15 2020 at 20:52):

Mario Carneiro said:

I could have sworn that someone implemented this already (Patrick Massot ?)

I'd love to answer that question but I don't understand what Frédéric wants to do.

view this post on Zulip Mario Carneiro (May 15 2020 at 20:54):

turn |- \exists (r : A) (h : p r), q r into |- p r /\ q r

view this post on Zulip Patrick Massot (May 15 2020 at 20:58):

import tactic

example (p q :   Prop) :  (r : ) (h : p r), q r :=
begin
  use 1,
  sorry
end

view this post on Zulip Patrick Massot (May 15 2020 at 20:58):

I don't remember whether I implemented this myself but i certainly asked for it

view this post on Zulip Patrick Massot (May 15 2020 at 20:59):

Git blame says I did: https://github.com/leanprover-community/mathlib/pull/1882

view this post on Zulip Mario Carneiro (May 15 2020 at 21:11):

Aha, this is exists intro not elim

view this post on Zulip Mario Carneiro (May 15 2020 at 21:13):

Frédéric is actually turning h : \exists (r : A) (h : p r), q r |- goal into r : A, h : p r /\ q r |- goal, although I don't know why this would be preferred over r : A, h : p r, h2 : q r |- goal

view this post on Zulip Frédéric Le Roux (May 16 2020 at 10:10):

Exactly, I would like to do for "exists intro" what Patrick did for "exists elim". The motivation is the same: ∃ (H : δ > 0), P δ is confusing for beginners.
At the moment I am still unable to make it work (I am still very confused by all these types in metaprogramming). I will try to mimic the syntax of use.

view this post on Zulip Patrick Massot (May 16 2020 at 12:10):

I see. Maybe the following will put you back on track:

import tactic

namespace tactic.interactive
setup_tactic_parser
open tactic
meta def existeelim (hyp : parse ident) (nom : parse (tk "with" *> ident)) : tactic unit :=
 do
   nom_h  get_local hyp,
   cases_core nom_h [nom, hyp],
   lem  to_expr ```(exists_prop),
   nom_h  get_local hyp,
   rewrite_hyp lem nom_h,
   skip
end tactic.interactive

example (p q :   Prop) (h :  (r : ) (h : p r), q r) : true :=
begin
  existeelim h with a,
  trivial,
end

view this post on Zulip Kevin Buzzard (May 16 2020 at 12:56):

Would this problem go away if we made posreal?

view this post on Zulip Frédéric Le Roux (May 18 2020 at 12:05):

Thanks Patrick, that works! Although I do not really understand why we need the with (it is clearer this way though), and above all why we need to call get_local hyptwice?

view this post on Zulip Patrick Massot (May 18 2020 at 14:09):

After the cases_core the new hyp has nothing to do with the old one. It would be clearer to use a different name, but I tried to stay close to your code.


Last updated: May 13 2021 at 22:15 UTC