## Stream: general

### Topic: Using the rw tactic inside a tactic

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

#### Mario Carneiro (May 15 2020 at 19:06):

does cases h, rw [exists_prop] work?

#### Mario Carneiro (May 15 2020 at 19:07):

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

#### Jalex Stark (May 15 2020 at 19:07):

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

no

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

#### Johan Commelin (May 15 2020 at 19:08):

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

#### Frédéric Le Roux (May 15 2020 at 19:15):

@Johan Commelin Thanks, it looks better now!

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

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

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

#### Mario Carneiro (May 15 2020 at 20:54):

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

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


#### Patrick Massot (May 15 2020 at 20:58):

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

#### Patrick Massot (May 15 2020 at 20:59):

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

#### Mario Carneiro (May 15 2020 at 21:11):

Aha, this is exists intro not elim

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

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

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


#### Kevin Buzzard (May 16 2020 at 12:56):

Would this problem go away if we made posreal?

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

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