parse location for multiple locations

Stream: general

[Saif Ghobash]

I have been reading the tactic writing guide and have been following along, however I am playing around with trying to extend the mul_left tactic to take more than one location and I am having a difficult time understanding similar tactics like change and how it manages to accomplish multiple locations, how could I extend mul_left to do this?

meta def tactic.interactive.mul_left (q : parse texpr) : parse location → tactic unit
| (loc.ns [some h]) := do
   e ← tactic.i_to_expr q,
   H ← tactic.get_local h,
   `(%%l = %%r) ← tactic.infer_type H,
   «have» h ``(%%e*%%l = %%e*%%r) ``(congr_arg (λ x, %%e*x) %%H),
   tactic.clear H
| l := -- I do not really know what to do here

[Patrick Massot]

It will be easier if you write a non-interactive tactic that does the work at one place and then call it on a list of locations using a monadic iteration.

[Patrick Massot]

There is a monadic loop section in the tutorial.

[Patrick Massot]

open interactive (loc.ns)
open interactive.types (texpr location)
open interactive (parse)
open tactic.interactive («have»)
open tactic (get_local infer_type)

meta def tactic.mul_left (e : expr) (h : name) : tactic unit :=
do H ← get_local h,
   `(%%l = %%r) ← infer_type H,
   «have» h ``(%%e*%%l = %%e*%%r) ``(congr_arg (λ x, %%e*x) %%H),
   tactic.clear H

meta def tactic.interactive.mul_left (q : parse texpr) : parse location → tactic unit
| (loc.ns l) := do
   e ← tactic.i_to_expr q,
   l.mmap' (λ x, match x with
                 | some y := tactic.mul_left e y
                 | none := tactic.fail "Can't mul_left on goal"
                 end)
| _ := tactic.fail "mul_left cannot act on *"

example (a b c : ℤ) (hyp : a = b) (hyp' : (a+c) = b): c*a = c*b :=
begin
  mul_left c at hyp hyp',
  exact hyp
end

[Patrick Massot]

If you are serious about learning tactic writing, you should also watch Rob's full series of tutorials at https://www.youtube.com/watch?v=o6oUjcE6Nz4&list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

[Saif Ghobash]

Sorry for the delay, I was implementing your suggestion, I came up with this

meta def mul_left_other (e : expr) : option name → tactic unit
| none := return ()
| (some h) := do
  H ← tactic.get_local h,
  `(%%l = %%r) ← tactic.infer_type H,
   «have» h ``(%%e*%%l = %%e*%%r) ``(congr_arg (λ x, %%e*x) %%H),
   tactic.clear H


meta def tactic.interactive.mul_left (q : parse texpr) : parse location → tactic unit
| (loc.ns l) := do
  e ← tactic.i_to_expr q,
  l.mmap' (λ h, mul_left_other e h)
| _ := tactic.fail "no wildcards yet"

Thank you for the help @Patrick Massot

[Saif Ghobash]

I'll look at Robs tutorials as well :)