## Stream: Beginner Questions

### Topic: ✔ simp add vs using

#### waynee95 (Jun 07 2022 at 12:16):

Why does `by (simp add: assms)`work here, but `using assms by simp` would not work?

``````lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "∀x. ∀y. x ⊕ y = y ⊕ x"
and "∀x. ∀y. ∀z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "∀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
``````

#### Mathias Fleury (Jun 07 2022 at 12:35):

Compare

``````lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "⋀x y. x ⊕ y = y ⊕ x"
and "⋀ x y z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "⋀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
supply [[simp_trace_new,simp_trace_depth_limit=5]]
using assms apply (simp)
``````

with:

``````lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "⋀x y. x ⊕ y = y ⊕ x"
and "⋀ x y z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "⋀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
supply [[simp_trace_new,simp_trace_depth_limit=5]]
using assms apply (simp (no_asm_simp))
``````

With `using assms` "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z" gets inverted because `x ⊕ (y ⊕ z)` is the more natural version, which cannot happen with `(simp add: assms)

(Trigger Warning: please immediately forget the existence of `no_asm_simp` and do not ever use it)

#### waynee95 (Jun 07 2022 at 12:45):

I see. For most proofs I did so far both ways always worked that's why I was confused here. Is there any documentation that explains why `using` does this?

#### Manuel Eberl (Jun 07 2022 at 15:53):

In its default setup, the simplifier picks up premises of your goal and adds them to the simpset. This is so that if e.g. you have something like `∀x. f x = g x ⟶ P x` and you do `auto` (which results in you getting a premise `f x = g x` in the goal), the simplifier will use `f x = g x` for rewriting.

#### Manuel Eberl (Jun 07 2022 at 15:54):

There is some heuristic that figures out whether to flip the equation when it gets picked up; e.g. if you have something like `f a b c = x` (where the right-hand side is just a variable and the left-hand side is something more complicated) you typically want to flip the equation for rewriting for the best effect.

#### Manuel Eberl (Jun 07 2022 at 15:55):

The `using` command really just sets up the facts you give to it as "chained facts" (i.e. they get "chained into" the proof method, in this case `simp`). Most proof methods (like `simp`) simply add the chained facts to the goal as premises.

#### Manuel Eberl (Jun 07 2022 at 15:56):

If you, on the other hand, do `simp add:` there is no reorientation going on; it just uses the rules in the form that you give it to it as rewrite rules.

#### Manuel Eberl (Jun 07 2022 at 15:56):

(Well, more or less – it still does things like if you give it a rule like `P` it turns it into `P = True` and similarly for `¬P`)

#### Manuel Eberl (Jun 07 2022 at 15:57):

So the take-away message here is: If you have facts that make good rewrite rules, do `simp add:` and not `using`.

#### Manuel Eberl (Jun 07 2022 at 15:57):

This also keeps your goal state cleaner; if you do `using` to chain in a lot of facts, it will make your goal state very big and unreadable.

#### waynee95 (Jun 07 2022 at 19:49):

@Manuel Eberl Thanks for the explanation. I didn't really know about the implications of using either style. I will keep that in mind!

#### Notification Bot (Jun 07 2022 at 19:52):

waynee95 has marked this topic as resolved.

Last updated: Aug 13 2022 at 07:19 UTC