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"
  by (simp add: assms)

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: Dec 21 2024 at 16:20 UTC