## 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: Dec 07 2023 at 08:19 UTC