fix(04,08,11,13): fix chapters to reflect changes in Lean. Closes lea…

…nprover#196.

04_Quantifiers_and_Equality.org

@@ -817,9 +817,9 @@ open nat algebra
 
 -- BEGIN
 variable f : ℕ → ℕ
-premise H : ∀ x : ℕ, f x ≤ f (x + 1)
 
-example (H' : ∃ x, f (x + 1) ≤ f x) : ∃ x, f (x + 1) = f x :=
+example (H : ∀ x : ℕ, f x ≤ f (x + 1)) (H' : ∃ x, f (x + 1) ≤ f x) :
+  ∃ x, f (x + 1) = f x :=
 obtain x `f (x + 1) ≤ f x`, from H',
 exists.intro x
   (show f (x + 1) = f x, from le.antisymm `f (x + 1) ≤ f x` (H x))
@@ -853,7 +853,7 @@ have even b,
 have 2 ∣ gcd a b,
   from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
 have 2 ∣ (1 : ℕ),
-  begin+ rewrite [gcd_eq_one_of_coprime co at this], exact this end,
+  by rewrite [gcd_eq_one_of_coprime co at this]; exact this,
 show false, from absurd `2 ∣ 1` dec_trivial
 #+END_SRC
 

08_Building_Theories_and_Proofs.org

@@ -828,64 +828,66 @@ checker, for each definition and theorem processed. If you ever find
 the system slowing down while processing a file, this can help you
 locate the source of the problem.
 
-** Making Auxiliary Facts Visible
-:PROPERTIES:
-  :CUSTOM_ID: Making_Auxiliary_Facts_Visible
-:END:
-
-We have seen that the =have= construct introduces an auxiliary subgoal
-in a proof, and is useful for structuring and documenting proofs.
-Given the term =have H : p, from s, t=, by default, the hypothesis =H=
-is not "visible" by automated procedures and tactics used to construct
-=t=. This is important because too much information may negatively
-affect the performance and effectiveness of automated procedures. You
-can make =H= available to automated procedures and tactics by using
-the idiom =assert H : p, from s, t=. Here is an example:
-#+BEGIN_SRC lean
-example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
-assume Hpqr : p ∧ q ∧ r,
-assert Hp   : p,     from and.elim_left Hpqr,
-have   Hqr  : q ∧ r, from and.elim_right Hpqr,
-assert Hq   : q,     from and.elim_left Hqr,
-proof
-  -- Hp and Hq are visible here,
-  -- Hqr is not because we used "have".
-  and.intro Hq Hp
-qed
-#+END_SRC
-Recall that =proof ... qed= block is implemented using tactics,
-so any hypothesis introduced using =have= is invisible inside it.
-In the example above, =Hqr= is not visible in the =proof ... qed=
-block.
-
-The =have=, =show= and =assert= terms have a variant which provide
-even more control over which hypotheses are available in =from s=.
-#+BEGIN_SRC text
-have   H : p, using H_1 ... H_n, from s, t
-assert H : p, using H_1 ... H_n, from s, t
-show   H : p, using H_1 ... H_n, from s
-#+END_SRC
-In all three terms, the hypotheses =H_1= ... =H_n= are available for
-automated procedures and tactics used in =s=.
-#+BEGIN_SRC lean
-example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
-assume Hpqr : p ∧ q ∧ r,
-have   Hp   : p,      from and.elim_left Hpqr,
-have   Hqr  : q ∧ r,  from and.elim_right Hpqr,
-assert Hq   : q,      from and.elim_left Hqr,
-show q ∧ p, using Hp, from
-proof
-  -- Hp is visible here because of =using Hp=
-  and.intro Hq Hp
-qed
-#+END_SRC
-See Chapter [[file:11_Tactics-Style_Proofs.org::#Tactic-Style_Proofs][Tactic-Style Proofs]] for a discussion of Lean's tactics.
-
-There are even situations where an auxiliary fact needs to be visible
-to the elaborator, so that it can solve unification problems that
-arise. This can arise when the expression to be synthesized depends on
-an auxiliary fact, =H=. We will see an example of this in Section
-[[file:11_Axioms.org::#Choice_Axioms][Choice Axioms]], when we discuss the Hilbert choice operator.
+# This section is no longer valid.
+#
+# ** Making Auxiliary Facts Visible
+# :PROPERTIES:
+#   :CUSTOM_ID: Making_Auxiliary_Facts_Visible
+# :END:
+
+# We have seen that the =have= construct introduces an auxiliary subgoal
+# in a proof, and is useful for structuring and documenting proofs.
+# Given the term =have H : p, from s, t=, by default, the hypothesis =H=
+# is not "visible" by automated procedures and tactics used to construct
+# =t=. This is important because too much information may negatively
+# affect the performance and effectiveness of automated procedures. You
+# can make =H= available to automated procedures and tactics by using
+# the idiom =assert H : p, from s, t=. Here is an example:
+# #+BEGIN_SRC lean
+# example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
+# assume Hpqr : p ∧ q ∧ r,
+# assert Hp   : p,     from and.elim_left Hpqr,
+# have   Hqr  : q ∧ r, from and.elim_right Hpqr,
+# assert Hq   : q,     from and.elim_left Hqr,
+# proof
+#   -- Hp and Hq are visible here,
+#   -- Hqr is not because we used "have".
+#   and.intro Hq Hp
+# qed
+# #+END_SRC
+# Recall that =proof ... qed= block is implemented using tactics,
+# so any hypothesis introduced using =have= is invisible inside it.
+# In the example above, =Hqr= is not visible in the =proof ... qed=
+# block.
+
+# The =have=, =show= and =assert= terms have a variant which provide
+# even more control over which hypotheses are available in =from s=.
+# #+BEGIN_SRC text
+# have   H : p, using H_1 ... H_n, from s, t
+# assert H : p, using H_1 ... H_n, from s, t
+# show   H : p, using H_1 ... H_n, from s
+# #+END_SRC
+# In all three terms, the hypotheses =H_1= ... =H_n= are available for
+# automated procedures and tactics used in =s=.
+# #+BEGIN_SRC lean
+# example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
+# assume Hpqr : p ∧ q ∧ r,
+# have   Hp   : p,      from and.elim_left Hpqr,
+# have   Hqr  : q ∧ r,  from and.elim_right Hpqr,
+# assert Hq   : q,      from and.elim_left Hqr,
+# show q ∧ p, using Hp, from
+# proof
+#   -- Hp is visible here because of =using Hp=
+#   and.intro Hq Hp
+# qed
+# #+END_SRC
+# See Chapter [[file:11_Tactics-Style_Proofs.org::#Tactic-Style_Proofs][Tactic-Style Proofs]] for a discussion of Lean's tactics.
+
+# There are even situations where an auxiliary fact needs to be visible
+# to the elaborator, so that it can solve unification problems that
+# arise. This can arise when the expression to be synthesized depends on
+# an auxiliary fact, =H=. We will see an example of this in Section
+# [[file:11_Axioms.org::#Choice_Axioms][Choice Axioms]] when we discuss the Hilbert choice operator.
 
 ** Sections
 

11_Tactic-Style_Proofs.org

@@ -432,46 +432,48 @@ end
 # out proofs by induction, when it is often needed to obtain
 # the right induction hypothesis.
 
-** Managing Auxiliary Facts
-
-Recall from Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]] that we need to use
-=assert= instead of =have= to state auxiliary subgoals if we wish to
-use them in tactic proofs. For example, the following proofs fail, if
-we replace any =assert= by a =have=:
-#+BEGIN_SRC lean
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-assert Hp : p, from and.left H,
-assert Hq : q, from and.right H,
-begin
-  apply (and.intro Hp),
-  apply (and.intro Hq),
-  exact Hp
-end
-
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-assert Hp : p, from and.left H,
-assert Hq : q, from and.right H,
-begin
-  apply and.intro,
-  assumption,
-  apply and.intro,
-  repeat assumption
-end
-#+END_SRC
-Alternatively, we can explicitly put a =have= statement into the
-context with the keyword =using=:
-#+BEGIN_SRC lean
-example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
-have Hp : p, from and.left H,
-have Hq : q, from and.right H,
-show _, using Hp Hq,
-begin
-  apply and.intro,
-  assumption,
-  apply and.intro,
-  repeat assumption
-end
-#+END_SRC
+# This section is no longer valid!
+#
+# ** Managing Auxiliary Facts
+
+# Recall from Section [[file:08_Building_Theories_and_Proofs.org::#Making_Auxiliary_Facts_Visible][Making Auxiliary Facts Visible]] that we need to use
+# =assert= instead of =have= to state auxiliary subgoals if we wish to
+# use them in tactic proofs. For example, the following proofs fail, if
+# we replace any =assert= by a =have=:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# assert Hp : p, from and.left H,
+# assert Hq : q, from and.right H,
+# begin
+#   apply (and.intro Hp),
+#   apply (and.intro Hq),
+#   exact Hp
+# end
+
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# assert Hp : p, from and.left H,
+# assert Hq : q, from and.right H,
+# begin
+#   apply and.intro,
+#   assumption,
+#   apply and.intro,
+#   repeat assumption
+# end
+# #+END_SRC
+# Alternatively, we can explicitly put a =have= statement into the
+# context with the keyword =using=:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p :=
+# have Hp : p, from and.left H,
+# have Hq : q, from and.right H,
+# show _, using Hp Hq,
+# begin
+#   apply and.intro,
+#   assumption,
+#   apply and.intro,
+#   repeat assumption
+# end
+# #+END_SRC
 
 ** Structuring Tactic Proofs
 

13_More_Tactics.org

@@ -253,32 +253,34 @@ the introduction rule for =true=, respectively.
 
 Combinators are used to combine tactics. The most basic one is the
 =and_then= combinator, written with a semicolon (=;=), which applies tactics
-successively. This is not the same as listing tactics separated by
-commas in a =begin ... end= block, since when multiple solutions are
-available, =and_then= will backtrack until it finds a solution or
-exhausts all the possibilities. The following example fails if we
-replace the semicolon by a comma:
-#+BEGIN_SRC lean
-example (p q : Prop) (Hq : q) : p ∨ q :=
-begin constructor; assumption end
-#+END_SRC
-The =constructor= tactic creates a /stream/ of outcomes, one for each
-possible result. A comma forces the tactic to commit to an answer at
-that point, whereas the semicolon causes Lean to systematically try
-all the possibilities. Here is a more elaborate example:
-#+BEGIN_SRC lean
-variable p : nat → Prop
-variable q : nat → Prop
-variables a b c : nat
-
-example : p c → p b → q b → p a → ∃ x, p x ∧ q x :=
-by intros; apply exists.intro; split; eassumption; eassumption
-#+END_SRC
-The =eassumption= tactic is stronger than =assumption= in that it is
-more aggressive when it comes to reducing expressions, and in that it
-returns a stream of solutions rather than the first one that
-matches. In this case, the first solution that matches =p ?x= is
-ultimately not the right choice, and backtracking is crucial.
+successively. 
+
+# This is not the same as listing tactics separated by
+# commas in a =begin ... end= block, since when multiple solutions are
+# available, =and_then= will backtrack until it finds a solution or
+# exhausts all the possibilities. The following example fails if we
+# replace the semicolon by a comma:
+# #+BEGIN_SRC lean
+# example (p q : Prop) (Hq : q) : p ∨ q :=
+# begin constructor; assumption end
+# #+END_SRC
+# The =constructor= tactic creates a /stream/ of outcomes, one for each
+# possible result. A comma forces the tactic to commit to an answer at
+# that point, whereas the semicolon causes Lean to systematically try
+# all the possibilities. Here is a more elaborate example:
+# #+BEGIN_SRC lean
+# variable p : nat → Prop
+# variable q : nat → Prop
+# variables a b c : nat
+
+# example : p c → p b → q b → p a → ∃ x, p x ∧ q x :=
+# by intros; apply exists.intro; split; eassumption; eassumption
+# #+END_SRC
+# The =eassumption= tactic is stronger than =assumption= in that it is
+# more aggressive when it comes to reducing expressions, and in that it
+# returns a stream of solutions rather than the first one that
+# matches. In this case, the first solution that matches =p ?x= is
+# ultimately not the right choice, and backtracking is crucial.
 
 The =par= combinator, written with a vertical bar (=|=), tries one tactic and then the other,
 using the first one that succeeds. The =repeat= tactic applies a
@@ -297,15 +299,15 @@ open set function eq.ops
 
 variables {X Y Z : Type}
 
-lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
+lemma image_comp (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
 set.ext (take z,
   iff.intro
     (assume Hz,
       obtain x Hx₁ Hx₂, from Hz,
       by repeat (apply mem_image | assumption | reflexivity))
     (assume Hz,
       obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
-      by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))
+      by repeat (apply mem_image | assumption | esimp [comp] | rewrite Hz₂)))
 #+END_SRC
 
 # TODO: need more and better examples, both above and below.