auto specialize

Stream: metaprogramming / tactics

[Johan Commelin]

Can someone please hack a tactic together that adds f x to the tactic state for all f and x in the local context for which f x typechecks? (It shouldn't throw away f or x.)

[Eric Wieser]

Recursively?

[Johan Commelin]

No, I can call repeat { foo } if I need that.

[Yakov Pechersky]

import tactic.basic

open lean lean.parser tactic interactive interactive.types expr

meta def tactic.specialize_all (n : name) (l : loc) : tactic unit := do
  val ← get_local n,
  hs ← l.get_locals,
  hs.mmap' (λ h,
    try (do
      let h' := expr.mk_app h [val],
      t' ← infer_type h',
      note (h.local_pp_name ++ n) none h'))

namespace tactic.interactive

meta def specialize_all (val : parse ident) (loc : parse location) : tactic unit :=
tactic.specialize_all val loc

end tactic.interactive

example {α β γ : Type*}
  (f : α → β)
  (g : α → β)
  (h : β → γ)
  (x y : α) : true := begin
    specialize_all x at *,
    extract_goal,
    trivial
  end

/--
example {α : Type ?} {β : Type ?} {γ : Type ?}
  (f g : α → β)
  (h : β → γ)
  (x y : α)
  (f.x g.x : β)
  (h.x : γ) :
  true :=
begin
  admit,
end
-/

[Yakov Pechersky]

As you can see, it's not perfect because applying x to h shouldn't work.

[Johan Commelin]

Is there an easy way to fix that?

[Johan Commelin]

Note that the version that I'm interested in is morally specialize_all * at *.

[Yakov Pechersky]

import tactic.basic

open lean lean.parser tactic interactive interactive.types expr

meta def tactic.specialize_single (n : name) (l : loc) : tactic unit := do
  val ← get_local n,
  valt ← infer_type val,
  hs ← l.get_locals,
  hs.mmap' (λ h, do
    ht ← infer_type h,
    try $ match ht with
      | (pi _ _ vt _) := do
        is_def_eq vt valt >> note (h.local_pp_name ++ n) none (h.mk_app [val]) >> pure ()
      | (lam _ _ vt _) := do
        is_def_eq vt valt >> note (h.local_pp_name ++ n) none (h.mk_app [val]) >> pure ()
      | _ := pure ()
    end)

meta def tactic.specialize_all (hs : list simp_arg_type) (l : loc) : tactic unit := do
  (lp, ln, ln', b) ← decode_simp_arg_list hs,
  lp.mmap' (λ e, do
    e ← to_expr e,
    if e.is_local_constant then tactic.specialize_single e.local_pp_name l
      else pure ()),
  if !b then pure () else (do
    ls ← tactic.local_context,
    ls.mmap' (λ e, do
      if expr.is_local_constant e then tactic.specialize_single e.local_pp_name l else pure ()),
    pure ())

namespace tactic.interactive

meta def specialize_all1 (val : parse ident) (loc : parse location) : tactic unit :=
tactic.specialize_single val loc

meta def specialize_all (vals : parse simp_arg_list) (loc : parse location) : tactic unit :=
tactic.specialize_all vals loc

end tactic.interactive

example {α β γ : Type*}
  (f : α → β)
  (g : α → β)
  (h : β → γ)
  (x y : α) (z : β) : γ := begin
    specialize_all [*] at *,
    extract_goal,
    exact h.z
  end

/--
example {α : Type ?} {β : Type ?} {γ : Type ?}
  (f g : α → β)
  (h : β → γ)
  (x y : α)
  (z f.x g.x f.y g.y : β)
  (h.z : γ) :
  γ :=
begin
  admit,
end
-/

[Yakov Pechersky]

It can be made neater with loc.try_apply, but this works for your specifications at least.

[Yakov Pechersky]

And works if you repeat it, as you expect.

[Johan Commelin]

@Yakov Pechersky wonderful! thank you so much!

[Johan Commelin]

@Yakov Pechersky one more plea:

variables {X Y Z : Type}

def surjective (f : X → Y) :=
∀ y, ∃ x, f x = y

example (f : X → Y) (g : Y → Z) (hyp : surjective (g ∘ f)) :
  surjective g :=
begin
  intro z,
  unfold surjective at hyp, -- can we avoid this step?
  specialize_all [*] at *,
  tactic.auto_cases,
  tactic.auto_cases,
  simp * at *,
end

[Johan Commelin]

I think that currently it is not "aggresive" enough. It only works for things that are visibly pi-like.

[Eric Wieser]

how docs tactic#specialize do it? Can we just copy the approach used there?

[Yakov Pechersky]

specialize f x y z does it by basically doing replace f := f x y z. I don't know what happens if one did a type-illogical specialize f f nat or something like that. So specialize does no typechecking other than what happens in i_to_expr. I can fake it with something like e <- (%%hyp %%val)` and hope that this deals with reducibility properly.

[Jannis Limperg]

Should be enough to whnf before the match with the right reducibility setting.

[Johan Commelin]

I tried

    ht' ← whnf ht transparency.reducible,
    try $ match ht' with

but that didn't help

[Yakov Pechersky]

import tactic.basic

open lean lean.parser tactic interactive interactive.types expr

meta def tactic.specialize_single (n : name) (l : loc) : tactic unit := do
  val ← get_local n,
  valt ← infer_type val,
  hs ← l.get_locals,
  hs.mmap' (λ h, try (do
    ht ← infer_type h,
    e ← to_expr ``(%%h %%val),
    et ← infer_type e,
    note (h.local_pp_name ++ n) none e))

meta def tactic.specialize_all (hs : list simp_arg_type) (l : loc) : tactic unit := do
  (lp, ln, ln', b) ← decode_simp_arg_list hs,
  lp.mmap' (λ e, do
    e ← to_expr e,
    if e.is_local_constant then tactic.specialize_single e.local_pp_name l
      else pure ()),
  if !b then pure () else (do
    ls ← tactic.local_context,
    ls.mmap' (λ e, do
      if expr.is_local_constant e then tactic.specialize_single e.local_pp_name l else pure ()),
    pure ())

namespace tactic.interactive

meta def specialize_all1 (val : parse ident) (loc : parse location) : tactic unit :=
tactic.specialize_single val loc

meta def specialize_all (vals : parse simp_arg_list) (loc : parse location) : tactic unit :=
tactic.specialize_all vals loc

end tactic.interactive

variables {X Y Z : Type}

def surjective (f : X → Y) :=
∀ y, ∃ x, f x = y

example (f : X → Y) (g : Y → Z) (hyp : surjective (g ∘ f)) :
  surjective g :=
begin
  intro z,
  specialize_all [*] at *,
  tactic.auto_cases,
  tactic.auto_cases,
  simp * at *,
end

[Yakov Pechersky]

So my brute-force "create pexpr, elaborate it, make sure it is valid type" approach also works.

[Johan Commelin]

Great! That does exactly what I want!

[Johan Commelin]

I think this is a tactic that could potentially be nice to add to tidy.

[Johan Commelin]

But there is one catch: currently, if you have f : X -> Y and x : X, then repeatedly calling specialize_all [*] at * will add many copies of f x : Y. So we somehow need to teach the tactic that it should fail if it isn't adding anything "new".

[Johan Commelin]

But even then there is a catch. Because with endomorphisms f : X -> X and x : X, you will end up getting f (f (f x)) etc...

[Johan Commelin]

I'm not sure whether such loops can be easily detected. So we might need to run the tactic on some gas (and if it is added to tidy, then tidy would need to run on gas as well).

[Johan Commelin]

Finally, I think that tidy could use a auto_choose tactic, that breaks open existential hypotheses, even if the goal is a type, instead of a prop.

[Johan Commelin]

With a combi of specialize_all and auto_choose, we could have a tidy that automatically proves surjective (g \circ f) -> surjective g.

[Eric Wieser]

Why do you need auto_choose for that surjective proof?

[Johan Commelin]

Because fsplit might turn \ex x, f x = y into two goals x : X and f m_1? = y before we get a chance to do cases on the existential hyp.

[Johan Commelin]

So then you are left with the X goal, and you need to use choice to extract a witness out of the existential hyp.

[Johan Commelin]

I agree that this will produce a "overpowered" proof, and choice can be avoided. But I don't really care too much, in the case of tidy proofs.