duplicate goals

Stream: general

[Johan Commelin]

Is there a tactic that merges identical subgoals?

[Johan Commelin]

I'm doing a blah; blah; rw foobar; blah and because the rw acts on multiple goals it creates a whole bunch of subgoals that are identical.

[Mario Carneiro]

no, but that sounds like a good exercise

[Johan Commelin]

For me?

[Mario Carneiro]

it's not much harder than assumption, you just unify all the goals together that have matching types

[Johan Commelin]

I'll see what I can do (-;

[Johan Commelin]

This is what I have so far

namespace tactic

#print assumption

-- Copied from all_goals_core
private meta def merge_goals_core : list expr → list expr → tactic unit
| []        ac := set_goals ac
| (g :: gs) ac :=
  mcond _ (merge_goals_core gs ac) $
    do t ← infer_type g,
       _
       new_gs ← _,
       all_goals_core gs (ac ++ new_gs)

meta def merge_goals : tactic unit :=
do gs ← get_goals,
   merge_goals_core gs []

namespace interactive

meta def merge_goals : tactic unit :=
tactic.merge_goals

end interactive

end tactic

[Johan Commelin]

Can any of the tactic-writing experts give me a hint on how to continue?

[Johan Commelin]

Aah, wait, the mcond is coming to early.

[Johan Commelin]

I should first infer the type of g

[Johan Commelin]

And then I want to check if there is a g_old ∈ gs that also has type t ← infer_type g

[Johan Commelin]

If so, I want to say that a proof of g_old is also a proof of g.

[Johan Commelin]

How do I do that?

[Kenny Lau]

might tactic.unify help?

[Johan Commelin]

Ah, interesting, let me try...

[Johan Commelin]

namespace tactic

private meta def map_unify (g : expr) : list expr → tactic unit
| []        := fail ()
| (x :: xs) := unify g x <|> map_unify xs

private meta def merge_goals_core : list expr → list expr → tactic unit
| []        ac := set_goals ac
| (g :: gs) ac := (map_unify g ac >> merge_goals_core gs ac) <|> merge_goals_core gs (ac ++ [g])

meta def merge_goals : tactic unit :=
do gs ← get_goals,
   merge_goals_core gs []

namespace interactive

meta def merge_goals : tactic unit :=
tactic.merge_goals

end interactive

example : ((true ∧ true) ∧ (true ∧ true)) ∧
  (((∀ (x y : ℕ), x + y = y + x) ∧ true) ∧ (true ∧ true)) :=
begin
  split; split; split,
  merge_goals,
  exact trivial,
  exact nat.add_comm,
end

end tactic

[Johan Commelin]

I guess map_unify can be inlined. But I don't know which runes to use (-;

[Alex J. Best]

Is the tactic in this thread (from a year ago) still interesting to people? It seems useful to me, and no version of this made it to mathlib right?

[Bryan Gin-ge Chen]

Looks worthy of a PR to me.

[Scott Morrison]

What's the intended behaviour here? If I have two nat goals, is this meant to insist they are the same?

[Scott Morrison]

If I have three goals, a nat, a Type, and a term of that type, will it insist that the Type is nat, and we give the same answer for both term goals??

[Alex J. Best]

I would say it should be conservative, probably that means only working on subsingletons (or just Props).