pseudo_metric_space.edist_dist_tac

Stream: mathlib4

[Yury G. Kudryashov]

Could someone port this tactic, please? Topology.MetricSpace.Basic is already in master.

[Adam Topaz]

docs#pseudo_metric_space.edist_dist_tac

[Adam Topaz]

do we have control_laws_tac yet? That's been on the todo list for a while.

[Yury G. Kudryashov]

Here is the source:

protected meta def pseudo_metric_space.edist_dist_tac : tactic unit :=
tactic.intros >> `[exact (ennreal.of_real_eq_coe_nnreal _).symm <|> control_laws_tac]

[Yury G. Kudryashov]

control_laws_tac is just intro; rfl (at least in this case)

[Adam Topaz]

Oh, so it should be very easy to make this using just a macro

[Adam Topaz]

unfortunately I'm stuck compiling forever right now :sad:

[Adam Topaz]

A first approximation:

import Mathlib.Data.Real.ENNReal

syntax "edist_dist_tac" : tactic

open Lean.Elab.Tactic in
elab_rules : tactic
| `(tactic|edist_dist_tac) => do
      evalTactic <| ← `(tactic|intros)
      evalTactic <| ← `(tactic|first | exact (ENNReal.ofReal_eq_coe_nnreal _).symm | rfl)

[Adam Topaz]

I'm not a tactic programmer so someone else should verify and/or fix :)

[Yury G. Kudryashov]

Can a macro be used in := by _?

[Adam Topaz]

A macro that expands to a tactic, yes. But the way I wrote it above it's not technically a macro.

[Yury G. Kudryashov]

The goal is to get rid of all the edist_dist fields in MetricSpace.Basic.

[Yury G. Kudryashov]

I'll test it tonight.