Tactics and automation

Exercises

• Exercise 7.1 page 204 Some lemmas about divisibility
• Exercise 7.2 page 209 Rewriting with exceptions
• using omega Using omega

Errata

1. Page 195, section 7.3.2:
   read: "The subst tactic looks for hypotheses of the form x = exp or exp = x "
2. Page 196, end of the first paragraph: read: "It is however, a good complement to our caseEq tactic ..."
3. Section 7.1.2.2, paragraph 2, page 189:
   read "Moreover, the argument delta" instead of "Moreover, the argument Delta"
4. Page 209. "[|- context [(S ?1)]]" should be replaced by "[|- context [(S ?X1)]]"
5. Page 209 (fifth paragraph) replace "match ?1" by "match X1"
6. Page 210 (last paragraph) read "simpl_on" instead of "simpl_On"
7. Section 7.6.2.1, page 203:
   read "The patterns have the form
   [h1:t1, h2:t2, ... |- C]"
   (instead of [h1:t1; h2:t2, ... |- C]