Stream: General

Topic: intro vs simp for equality facts

view this post on Zulip Kevin Kappelmann (Jul 14 2020 at 13:39):

What are the differences between tagging an unconditional equality fact A = B with simp or intro? I get different behaviours when trying to prove another lemma based on whether I tag such lemmas with simp or intro (the latter works, the former results in a timeout).

view this post on Zulip Lukas Stevens (Jul 14 2020 at 13:48):

Is A a subterm of B?

view this post on Zulip Kevin Kappelmann (Jul 14 2020 at 13:50):

Nope: powerset {} = {{}}"

view this post on Zulip Kevin Kappelmann (Jul 14 2020 at 13:54):

I mean, putting the non-termination issue of mine aside: all of the following should be simp lemmas, no?

  1. {} ⊆ A
  2. powerset {} = {{}}
  3. {x} ≠ x
  4. A ∈ powerset A

etc. Or is there some reason to tag them as intro instead?

view this post on Zulip Lukas Stevens (Jul 14 2020 at 13:56):

The third one is definitely not a good intro lemma since it is equivalent to ... ==> False.

view this post on Zulip Lukas Stevens (Jul 14 2020 at 13:57):

Therefore, it would always be applied if the current subgoal is False.

view this post on Zulip Kevin Kappelmann (Jul 14 2020 at 13:57):

Are you sure? Not is not an abbreviation
Nevermind, I thought you said simp lemma

view this post on Zulip Lukas Stevens (Jul 14 2020 at 14:01):

My suspicion is that the rule powerset {} = {{}} is not the problem. Adding the rule just exposes that there is already a problematic rule in the simpset.

view this post on Zulip Mohammad Abdulaziz (Jul 14 2020 at 14:03):

What does the goal look like? If you have a goal that causes the simplifier to loop when you label the lemma with simp, then that label is no good. Maybe you have a recursive definition that automatically unfolds in a way that loops when "powerset {} ={{}}" is simp.

view this post on Zulip Kevin Kappelmann (Jul 14 2020 at 14:51):

I do not quite get why it was timing out, but I added a more easier to reason about rule that solves my problem [iff]: "x ∈ powerset {} ⟷ x = {}"

view this post on Zulip Simon Wimmer (Jul 15 2020 at 14:05):

Julian likes these [iff] declarations a lot I think. Personally, I am always a bit suspicious about them and never use them :D But anyway it seems very odd to me that you had to do this and the simp lemma does not do it for you...

view this post on Zulip Kevin Kappelmann (Jul 15 2020 at 14:12):

Yeah they can get you into trouble really quickly as they add intro! tags.

Last updated: Dec 21 2024 at 12:33 UTC