Stream: General

Topic: intro vs simp for equality facts

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).

Lukas Stevens (Jul 14 2020 at 13:48):

Is A a subterm of B?

Kevin Kappelmann (Jul 14 2020 at 13:50):

Nope: powerset {} = {{}}"

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?

Lukas Stevens (Jul 14 2020 at 13:56):

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

Lukas Stevens (Jul 14 2020 at 13:57):

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

Kevin Kappelmann (Jul 14 2020 at 13:57):

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

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.

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.

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 = {}"

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

Kevin Kappelmann (Jul 15 2020 at 14:12):

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

Last updated: Apr 20 2024 at 08:16 UTC