Using the rw tactic inside a tactic

Stream: general

[Frédéric Le Roux]

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]

does cases h, rw [exists_prop] work?

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

no

[Mario Carneiro]

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

[Johan Commelin]

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

[Frédéric Le Roux]

@Johan Commelin Thanks, it looks better now!

[Frédéric Le Roux]

@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]

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]

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]

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

[Patrick Massot]

import tactic

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

Aha, this is exists intro not elim

[Mario Carneiro]

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]

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]

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]

Would this problem go away if we made posreal?

[Frédéric Le Roux]

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]

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.