Zulip Chat Archive

Stream: general

Topic: duplicate goals


view this post on Zulip Johan Commelin (Feb 15 2019 at 11:52):

Is there a tactic that merges identical subgoals?

view this post on Zulip Johan Commelin (Feb 15 2019 at 11:53):

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.

view this post on Zulip Mario Carneiro (Feb 15 2019 at 11:59):

no, but that sounds like a good exercise

view this post on Zulip Johan Commelin (Feb 15 2019 at 11:59):

For me?

view this post on Zulip Mario Carneiro (Feb 15 2019 at 12:03):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 12:05):

I'll see what I can do (-;

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:33):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:33):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:34):

Aah, wait, the mcond is coming to early.

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:35):

I should first infer the type of g

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:35):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:36):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:36):

How do I do that?

view this post on Zulip Kenny Lau (Feb 15 2019 at 14:38):

might tactic.unify help?

view this post on Zulip Johan Commelin (Feb 15 2019 at 14:39):

Ah, interesting, let me try...

view this post on Zulip Johan Commelin (Feb 15 2019 at 15:04):

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

view this post on Zulip Johan Commelin (Feb 15 2019 at 15:04):

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

view this post on Zulip Alex J. Best (Apr 17 2020 at 00:51):

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?

view this post on Zulip Bryan Gin-ge Chen (Apr 17 2020 at 00:52):

Looks worthy of a PR to me.

view this post on Zulip Scott Morrison (Apr 17 2020 at 00:55):

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

view this post on Zulip Scott Morrison (Apr 17 2020 at 00:56):

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??

view this post on Zulip Alex J. Best (Apr 17 2020 at 00:58):

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


Last updated: May 14 2021 at 22:15 UTC