diff --git a/Appendix.qmd b/Appendix.qmd index 413408f..92efb9c 100644 --- a/Appendix.qmd +++ b/Appendix.qmd @@ -67,7 +67,7 @@ We have mostly used these tactics to reexpress negative statements as more usefu * #### `by_cases on` -If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `cases' h with hP hQ`. In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`. In both cases, you have to prove the original goal. You may also want to learn about the tactics `cases` and `rcases`. +If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `obtain hP | hQ := h`. In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`. In both cases, you have to prove the original goal. You may also want to learn about the tactics `cases` and `rcases`. * #### `by_induc`, `by_strong_induc` @@ -136,7 +136,7 @@ If your goal is `∃! (x : U), P x` and you think that `a` is the unique value o * #### `obtain` -There is an `obtain` tactic in standard Lean, but it is slightly different from the one used in this book. If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state. Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`. To enter those brackets, type `\<` and `\>`. +If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state. Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`. To enter those brackets, type `\<` and `\>`. If you have `h : ∃! (x : U), P x`, then `obtain ⟨u, h1, h2⟩ := h` will also introduce `u : U` and `h1 : P u` into the tactic state. In addition, it will introduce `h2` as an identifier for a statement that is equivalent to `∀ (y : U), P y → y = u`. (Unfortunately, the statement introduced is more complicated.) diff --git a/docs/Appendix.html b/docs/Appendix.html index f702c1b..a56817d 100644 --- a/docs/Appendix.html +++ b/docs/Appendix.html @@ -428,7 +428,7 @@

Transitioni -

If you have h : P ∨ Q, then you can break your proof into cases by using the tactic cases' h with hP hQ. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.

+

If you have h : P ∨ Q, then you can break your proof into cases by using the tactic obtain hP | hQ := h. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.

@@ -480,7 +480,7 @@

Transitioni -

There is an obtain tactic in standard Lean, but it is slightly different from the one used in this book. If you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \< and \>.

+

If you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \< and \>.

If you have h : ∃! (x : U), P x, then obtain ⟨u, h1, h2⟩ := h will also introduce u : U and h1 : P u into the tactic state. In addition, it will introduce h2 as an identifier for a statement that is equivalent to ∀ (y : U), P y → y = u. (Unfortunately, the statement introduced is more complicated.)

You may also find the theorems ExistsUnique.exists and ExistsUnique.unique useful:

diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf index 5216efe..c957fb9 100644 Binary files a/docs/How-To-Prove-It-With-Lean.pdf and b/docs/How-To-Prove-It-With-Lean.pdf differ diff --git a/docs/search.json b/docs/search.json index 7a1bea3..aa46713 100644 --- a/docs/search.json +++ b/docs/search.json @@ -375,7 +375,7 @@ "href": "Appendix.html#transitioning-to-standard-lean", "title": "Appendix", "section": "Transitioning to Standard Lean", - "text": "Transitioning to Standard Lean\nIf you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean. A good place to start is the Lean Community website. The resources there use “standard” Lean, which is somewhat different from the Lean in this book.\nIn a few cases we have used notation in this book that differs from standard Lean notation. For example, if h is a proof of P ↔︎ Q, then we have used h.ltr and h.rtl to denote proofs of the left-to-right and right-to-left directions of the biconditional. The standard Lean notation for these is h.mp and h.mpr, respectively (“mp” and “mpr” stand for “modus ponens” and “modus ponens reverse”). As explained at the end of Section 5.4, the notations Pred U and Rel A B denote the types U → Prop and A → B → Prop, respectively. Although Rel is standard notation (defined in Lean’s math library mathlib), Pred is not; the notation BinRel A is also not standard Lean. In place of Pred U you should use U → Prop, and in place of BinRel A you should use Rel A A.\nHowever, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean. If you want to learn to write proofs in standard Lean, you’ll need to learn replacements for those tactics. We discuss some such replacements below. Some of these replacements are built into Lean, and some are defined in mathlib.\n\nassume, fix\n\nIf you are proving P → Q and you want to begin by assuming h : P, in standard Lean you would begin your proof by writing intro h. You don’t need to specify that h is an identifier for the assumption P; Lean will figure that out on its own.\nIf you are proving ∀ (x : U), P x and you want to begin by introducing the variable x to stand for an arbitrary object of type U, in standard Lean you would begin your proof by writing intro x. Again, you don’t need to specify the type of x, because Lean will figure it out.\nThus, the tactic intro does the job of both assume and fix. Furthermore, you can introduce multiple assumptions or objects with a single use of the intro tactic: intro a b c is equivalent to intro a; intro b; intro c.\n\nbicond_neg, demorgan, double_neg, quant_neg\n\nWe have mostly used these tactics to reexpress negative statements as more useful positive statements. The tactic push_neg can be used for this purpose.\n\nby_cases on\n\nIf you have h : P ∨ Q, then you can break your proof into cases by using the tactic cases' h with hP hQ. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.\n\nby_induc, by_strong_induc\n\nWe saw in Section 7.2 that if you are proving a statement of the form ∀ (l : List U), ..., then you can begin a proof by induction on the length of l by using the tactic apply List.rec. Similarly, if you are proving ∀ (n : Nat), ..., you can begin a proof by induction by using the tactic apply Nat.recAux. For strong induction, you can use apply Nat.strongRec.\nThere are also tactics induction and induction' that you may want to learn about.\n\nconditional\n\nThe commands #check @imp_iff_not_or and #check @not_imp produce the results\n\n@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b\n@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b\n\nThus, rewrite [imp_iff_not_or] will convert a statement of the form P → Q into ¬P ∨ Q, and rewrite [←imp_iff_not_or] will go in the other direction. Similarly, rewrite [not_imp] will convert a statement of the form ¬(P → Q) into P ∧ ¬Q, and rewrite [←not_imp] will go in the other direction.\n\ncontradict\n\nSuppose your goal is False (as it would be if you are doing a proof by contradiction), and you have h : ¬P. Recall that Lean treats ¬P as meaning the same thing as P → False, and therefore h _ will prove the goal, if the blank is filled in which a proof of P. It follows that apply h will set P as the goal. In other words, in this situation apply h has the same effect as contradict h.\nYou could also get the same effect with the tactic suffices hP : P from h hP. Think of this as meaning “it would suffice now to prove P, because if hP were a proof of P, then h hP would prove the goal.” Lean therefore sets P to be the goal.\nSimilarly, in a proof by contradiction, if you have h : P, then suffices hnP : ¬P from hnP h will set ¬P as the goal.\nYet another possibility is contrapose! h. (This is a variant on the contrapose! tactic, discussed in the next section.)\n\ncontrapos\n\nIf your goal is a conditional statement, then the tactics contrapose and contrapose! will replace the goal with its contrapositive (contrapose! also uses push_neg to try to simplify the negated statements that arise when forming a contrapositive). You may also find the theorem not_imp_not useful:\n\n@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a\n\n\ndefine\n\nThe tactic whnf (which stands for “weak head normal form”) is similar to define, although it sometimes produces results that are a little confusing.\nAnother way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the rewrite tactic. See, for example, the use of the theorem inv_def in Section 4.2.\n\ndisj_syll\n\nThe following theorems can be useful:\n\n@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b\n@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a\n@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b\n@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a\n\nFor example, if you have h1 : P ∨ Q and h2 : ¬P, then Or.resolve_left h1 h2 is a proof of Q.\n\nexists_unique\n\nIf your goal is ∃! (x : U), P x and you think that a is the unique value of x that makes P x true, then you can use the tactic apply ExistsUnique.intro a. This will leave you with two goals to prove, P a and ∀ (y : U), P y → y = a.\n\nobtain\n\nThere is an obtain tactic in standard Lean, but it is slightly different from the one used in this book. If you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \\< and \\>.\nIf you have h : ∃! (x : U), P x, then obtain ⟨u, h1, h2⟩ := h will also introduce u : U and h1 : P u into the tactic state. In addition, it will introduce h2 as an identifier for a statement that is equivalent to ∀ (y : U), P y → y = u. (Unfortunately, the statement introduced is more complicated.)\nYou may also find the theorems ExistsUnique.exists and ExistsUnique.unique useful:\n\n@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},\n (∃! (x : α), p x) → ∃ (x : α), p x\n@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},\n (∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂\n\n\nor_left, or_right\n\nIf your goal is P ∨ Q, then the tactics or_left and or_right let you assume that one of P and Q is false and prove the other. Perhaps the easiest way to do that in standard Lean is to use proof by cases. For example, to assume P is false and prove Q you might proceed as follows:\n -- Goal is P ∨ Q\n by_cases hP : P\n · -- Case 1. hP : P\n exact Or.inl hP\n done\n · -- Case 2. hP : ¬P\n apply Or.inr\n --We now have hP : ¬P, and goal is Q\n **done::\n\nshow\n\nThere is a show tactic in standard Lean, but it works a little differently from the show tactic we have used in this book. When our goal was a statement P and we had an expression t that was a proof of P, we usually completed the proof by writing show P from t. In standard Lean you can complete the proof by writing exact t, as explained near the end of Section 3.6." + "text": "Transitioning to Standard Lean\nIf you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean. A good place to start is the Lean Community website. The resources there use “standard” Lean, which is somewhat different from the Lean in this book.\nIn a few cases we have used notation in this book that differs from standard Lean notation. For example, if h is a proof of P ↔︎ Q, then we have used h.ltr and h.rtl to denote proofs of the left-to-right and right-to-left directions of the biconditional. The standard Lean notation for these is h.mp and h.mpr, respectively (“mp” and “mpr” stand for “modus ponens” and “modus ponens reverse”). As explained at the end of Section 5.4, the notations Pred U and Rel A B denote the types U → Prop and A → B → Prop, respectively. Although Rel is standard notation (defined in Lean’s math library mathlib), Pred is not; the notation BinRel A is also not standard Lean. In place of Pred U you should use U → Prop, and in place of BinRel A you should use Rel A A.\nHowever, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean. If you want to learn to write proofs in standard Lean, you’ll need to learn replacements for those tactics. We discuss some such replacements below. Some of these replacements are built into Lean, and some are defined in mathlib.\n\nassume, fix\n\nIf you are proving P → Q and you want to begin by assuming h : P, in standard Lean you would begin your proof by writing intro h. You don’t need to specify that h is an identifier for the assumption P; Lean will figure that out on its own.\nIf you are proving ∀ (x : U), P x and you want to begin by introducing the variable x to stand for an arbitrary object of type U, in standard Lean you would begin your proof by writing intro x. Again, you don’t need to specify the type of x, because Lean will figure it out.\nThus, the tactic intro does the job of both assume and fix. Furthermore, you can introduce multiple assumptions or objects with a single use of the intro tactic: intro a b c is equivalent to intro a; intro b; intro c.\n\nbicond_neg, demorgan, double_neg, quant_neg\n\nWe have mostly used these tactics to reexpress negative statements as more useful positive statements. The tactic push_neg can be used for this purpose.\n\nby_cases on\n\nIf you have h : P ∨ Q, then you can break your proof into cases by using the tactic obtain hP | hQ := h. In case 1, h : P ∨ Q will be replaced by hP : P, and in case 2 it will be replaced by hQ : Q. In both cases, you have to prove the original goal. You may also want to learn about the tactics cases and rcases.\n\nby_induc, by_strong_induc\n\nWe saw in Section 7.2 that if you are proving a statement of the form ∀ (l : List U), ..., then you can begin a proof by induction on the length of l by using the tactic apply List.rec. Similarly, if you are proving ∀ (n : Nat), ..., you can begin a proof by induction by using the tactic apply Nat.recAux. For strong induction, you can use apply Nat.strongRec.\nThere are also tactics induction and induction' that you may want to learn about.\n\nconditional\n\nThe commands #check @imp_iff_not_or and #check @not_imp produce the results\n\n@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b\n@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b\n\nThus, rewrite [imp_iff_not_or] will convert a statement of the form P → Q into ¬P ∨ Q, and rewrite [←imp_iff_not_or] will go in the other direction. Similarly, rewrite [not_imp] will convert a statement of the form ¬(P → Q) into P ∧ ¬Q, and rewrite [←not_imp] will go in the other direction.\n\ncontradict\n\nSuppose your goal is False (as it would be if you are doing a proof by contradiction), and you have h : ¬P. Recall that Lean treats ¬P as meaning the same thing as P → False, and therefore h _ will prove the goal, if the blank is filled in which a proof of P. It follows that apply h will set P as the goal. In other words, in this situation apply h has the same effect as contradict h.\nYou could also get the same effect with the tactic suffices hP : P from h hP. Think of this as meaning “it would suffice now to prove P, because if hP were a proof of P, then h hP would prove the goal.” Lean therefore sets P to be the goal.\nSimilarly, in a proof by contradiction, if you have h : P, then suffices hnP : ¬P from hnP h will set ¬P as the goal.\nYet another possibility is contrapose! h. (This is a variant on the contrapose! tactic, discussed in the next section.)\n\ncontrapos\n\nIf your goal is a conditional statement, then the tactics contrapose and contrapose! will replace the goal with its contrapositive (contrapose! also uses push_neg to try to simplify the negated statements that arise when forming a contrapositive). You may also find the theorem not_imp_not useful:\n\n@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a\n\n\ndefine\n\nThe tactic whnf (which stands for “weak head normal form”) is similar to define, although it sometimes produces results that are a little confusing.\nAnother way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the rewrite tactic. See, for example, the use of the theorem inv_def in Section 4.2.\n\ndisj_syll\n\nThe following theorems can be useful:\n\n@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b\n@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a\n@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b\n@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a\n\nFor example, if you have h1 : P ∨ Q and h2 : ¬P, then Or.resolve_left h1 h2 is a proof of Q.\n\nexists_unique\n\nIf your goal is ∃! (x : U), P x and you think that a is the unique value of x that makes P x true, then you can use the tactic apply ExistsUnique.intro a. This will leave you with two goals to prove, P a and ∀ (y : U), P y → y = a.\n\nobtain\n\nIf you have h : ∃ (x : U), P x, then the tactic obtain ⟨u, h1⟩ := h will introduce both u : U and h1 : P u into the tactic state. Note that u and h1 must be enclosed in angle brackets, ⟨ ⟩. To enter those brackets, type \\< and \\>.\nIf you have h : ∃! (x : U), P x, then obtain ⟨u, h1, h2⟩ := h will also introduce u : U and h1 : P u into the tactic state. In addition, it will introduce h2 as an identifier for a statement that is equivalent to ∀ (y : U), P y → y = u. (Unfortunately, the statement introduced is more complicated.)\nYou may also find the theorems ExistsUnique.exists and ExistsUnique.unique useful:\n\n@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},\n (∃! (x : α), p x) → ∃ (x : α), p x\n@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},\n (∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂\n\n\nor_left, or_right\n\nIf your goal is P ∨ Q, then the tactics or_left and or_right let you assume that one of P and Q is false and prove the other. Perhaps the easiest way to do that in standard Lean is to use proof by cases. For example, to assume P is false and prove Q you might proceed as follows:\n -- Goal is P ∨ Q\n by_cases hP : P\n · -- Case 1. hP : P\n exact Or.inl hP\n done\n · -- Case 2. hP : ¬P\n apply Or.inr\n --We now have hP : ¬P, and goal is Q\n **done::\n\nshow\n\nThere is a show tactic in standard Lean, but it works a little differently from the show tactic we have used in this book. When our goal was a statement P and we had an expression t that was a proof of P, we usually completed the proof by writing show P from t. In standard Lean you can complete the proof by writing exact t, as explained near the end of Section 3.6." }, { "objectID": "Appendix.html#typing-symbols",