diff --git a/README.md b/README.md index 5f17d7b..4e4f0e6 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,15 @@ -# bookshelf-lean +# bookshelf -A collection of proofs and answers to exercises to books I'm studying. +A collection on the study of the books listed below. I aim to use [Lean](https://leanprover.github.io/) +when possible (with respect to my current level of ability) and fallback to +LaTeX when not. -## Updates - -Lean's tooling is a fickle beast. If looking to update e.g. `Mathlib`, pin a new -version to the `lake-manifest.json` file and start a new build from scratch: - -```bash -> lake update -> lake clean -> lake build -``` +- [ ] Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991. +- [ ] Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +- [ ] Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015. +- [ ] Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009. +- [ ] Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001. +- [ ] Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +- [ ] Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020. +- [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d. +- [ ] Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000. diff --git a/bookshelf/Bookshelf.lean b/bookshelf/Bookshelf.lean deleted file mode 100644 index f4bb429..0000000 --- a/bookshelf/Bookshelf.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Bookshelf.Sequence.Arithmetic -import Bookshelf.Sequence.Geometric -import Bookshelf.Tuple -import Bookshelf.Vector diff --git a/bookshelf/Bookshelf/Vector.lean b/bookshelf/Bookshelf/Vector.lean deleted file mode 100644 index 8c9b34d..0000000 --- a/bookshelf/Bookshelf/Vector.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Mathlib.Tactic.Ring - -/-- -A list-like structure with its size encoded in the type. - -For a `Vector`-like type with opposite "endian", refer to `Tuple`. --/ -inductive Vector (α : Type u) : (size : Nat) → Type u where - | nil : Vector α 0 - | cons : α → Vector α n → Vector α (n + 1) - -syntax (priority := high) "v[" term,* "]" : term - -macro_rules - | `(v[]) => `(Vector.nil) - | `(v[$x]) => `(Vector.cons $x v[]) - | `(v[$x, $xs:term,*]) => `(Vector.cons $x v[$xs,*]) - -namespace Vector - -/-- -Returns the number of entries in the `Vector`. --/ -def size (_ : Vector α n) : Nat := n - -/-- -Returns the first entry of the `Vector`. --/ -def head : Vector α (n + 1) → α - | cons v _ => v - -/-- -Returns the last entry of the `Vector`. --/ -def last : Vector α (n + 1) → α - | cons v vs => if _ : n = 0 then v else - match n with - | _ + 1 => vs.last - -/-- -Returns all but the `head` of the `Vector`. --/ -def tail : Vector α (n + 1) → Vector α n - | cons _ vs => vs - -/-- -Appends an entry to the end of the `Vector`. --/ -def snoc : Vector α n → α → Vector α (n + 1) - | nil, a => v[a] - | cons v vs, a => cons v (snoc vs a) - -end Vector diff --git a/common/Common.lean b/common/Common.lean new file mode 100644 index 0000000..e9ccfee --- /dev/null +++ b/common/Common.lean @@ -0,0 +1,3 @@ +import Common.Sequence.Arithmetic +import Common.Sequence.Geometric +import Common.Tuple diff --git a/bookshelf/Bookshelf/Sequence/Arithmetic.lean b/common/Common/Sequence/Arithmetic.lean similarity index 92% rename from bookshelf/Bookshelf/Sequence/Arithmetic.lean rename to common/Common/Sequence/Arithmetic.lean index c732265..16d4166 100644 --- a/bookshelf/Bookshelf/Sequence/Arithmetic.lean +++ b/common/Common/Sequence/Arithmetic.lean @@ -1,10 +1,3 @@ -/- -# References - -1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d. - https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf. --/ - import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring @@ -70,4 +63,4 @@ theorem sum_closed_formula (seq : Arithmetic) (n : Nat) -- TODO: To continue, need to find how to deal with division. _ = ↑(n + 1) / 2 * (seq.a₀ + seq.termClosed n) := by sorry) -end Arithmetic \ No newline at end of file +end Arithmetic diff --git a/bookshelf/Bookshelf/Sequence/Geometric.lean b/common/Common/Sequence/Geometric.lean similarity index 87% rename from bookshelf/Bookshelf/Sequence/Geometric.lean rename to common/Common/Sequence/Geometric.lean index fa3f033..81797c2 100644 --- a/bookshelf/Bookshelf/Sequence/Geometric.lean +++ b/common/Common/Sequence/Geometric.lean @@ -1,10 +1,3 @@ -/- -# References - -1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d. - https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf. --/ - import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring @@ -53,4 +46,4 @@ def sum : Geometric → Nat → Int | _, 0 => 0 | seq, (n + 1) => seq.termClosed n + seq.sum n -end Geometric \ No newline at end of file +end Geometric diff --git a/bookshelf/Bookshelf/Tuple.lean b/common/Common/Tuple.lean similarity index 91% rename from bookshelf/Bookshelf/Tuple.lean rename to common/Common/Tuple.lean index 6f45ee5..52c8865 100644 --- a/bookshelf/Bookshelf/Tuple.lean +++ b/common/Common/Tuple.lean @@ -1,10 +1,3 @@ -/- -# References - -1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: - Harcourt/Academic Press, 2001. --/ - import Mathlib.Tactic.Ring /-- @@ -29,9 +22,9 @@ macro_rules namespace Tuple -/- ------------------------------------- - - Coercions - - -------------------------------------/ +-- ======================================== +-- Coercions +-- ======================================== scoped instance : CoeOut (Tuple α (min (m + n) m)) (Tuple α m) where coe := cast (by simp) @@ -54,9 +47,9 @@ scoped instance : Coe (Tuple α (min m n + 1)) (Tuple α (min (m + 1) (n + 1))) scoped instance : Coe (Tuple α m) (Tuple α (min (m + n) m)) where coe := cast (by simp) -/- ------------------------------------- - - Equality - - -------------------------------------/ +-- ======================================== +-- Equality +-- ======================================== theorem eq_nil : @Tuple.nil α = t[] := rfl @@ -90,9 +83,9 @@ protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) : Decidable (Eq instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq -/- ------------------------------------- - - Basic API - - -------------------------------------/ +-- ======================================== +-- Basic API +-- ======================================== /-- Returns the number of entries of the `Tuple`. @@ -118,9 +111,9 @@ def cons : Tuple α n → α → Tuple α (n + 1) | t[], a => t[a] | snoc ts t, a => snoc (cons ts a) t -/- ------------------------------------- - - Concatenation - - -------------------------------------/ +-- ======================================== +-- Concatenation +-- ======================================== /-- Join two `Tuple`s together end to end. @@ -179,9 +172,9 @@ theorem snoc_eq_init_concat_last (as : Tuple α m) : snoc as a = concat as t[a] rfl (fun _ _ => by simp; unfold concat concat; rfl) -/- ------------------------------------- - - Initial sequences - - -------------------------------------/ +-- ======================================== +-- Initial sequences +-- ======================================== /-- Take the first `k` entries from the `Tuple` to form a new `Tuple`, or the entire diff --git a/bookshelf/lake-manifest.json b/common/lake-manifest.json similarity index 100% rename from bookshelf/lake-manifest.json rename to common/lake-manifest.json diff --git a/bookshelf/lakefile.lean b/common/lakefile.lean similarity index 65% rename from bookshelf/lakefile.lean rename to common/lakefile.lean index d21af3d..41fc850 100644 --- a/bookshelf/lakefile.lean +++ b/common/lakefile.lean @@ -1,13 +1,11 @@ import Lake open Lake DSL -package «Bookshelf» +package «Common» require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" @[default_target] -lean_lib «Bookshelf» { - -- add library configuration options here -} +lean_lib «Common» diff --git a/bookshelf/lean-toolchain b/common/lean-toolchain similarity index 100% rename from bookshelf/lean-toolchain rename to common/lean-toolchain diff --git a/first-course-abstract-algebra/lake-manifest.json b/first-course-abstract-algebra/lake-manifest.json index 123a66f..59662d6 100644 --- a/first-course-abstract-algebra/lake-manifest.json +++ b/first-course-abstract-algebra/lake-manifest.json @@ -1,8 +1,7 @@ {"version": 4, "packagesDir": "lake-packages", "packages": - [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}}, - {"git": + [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", @@ -25,4 +24,5 @@ "subDir?": null, "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", - "inputRev?": "main"}}]} + "inputRev?": "main"}}, + {"path": {"name": "Common", "dir": "./../common"}}]} diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean index 847a260..6ace49d 100644 --- a/first-course-abstract-algebra/lakefile.lean +++ b/first-course-abstract-algebra/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «first-course-abstract-algebra» -require Bookshelf from "../bookshelf" +require Common from "../common" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" diff --git a/mathematical-introduction-logic/Enderton/Chapter0.lean b/mathematical-introduction-logic/Enderton/Chapter0.lean index f0e95e2..6189b37 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.lean +++ b/mathematical-introduction-logic/Enderton/Chapter0.lean @@ -4,15 +4,15 @@ Chapter 0 Useful Facts About Sets -/ -import Bookshelf.Tuple +import Common.Tuple /-- -The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`, -an `n`-tuple is defined recursively like so: +The following describes a so-called "generic" tuple. Like in `Common.Tuple`, an +`n`-tuple is defined recursively like so: `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` -Unlike `Bookshelf.Tuple`, a "generic" tuple bends the syntax above further. For +Unlike `Common.Tuple`, a "generic" tuple bends the syntax above further. For example, both tuples above are equivalent to: `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩` @@ -20,7 +20,7 @@ example, both tuples above are equivalent to: for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to prove certain theorems found in [1] (e.g. `lemma_0a`). -In general, prefer `Bookshelf.Tuple`. +In general, prefer `Common.Tuple`. -/ inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where | nil : XTuple α (0, 0) @@ -38,9 +38,9 @@ namespace XTuple open scoped Tuple -/- ------------------------------------- - - Normalization - - -------------------------------------/ +-- ======================================== +-- Normalization +-- ======================================== /-- Converts an `XTuple` into "normal form". @@ -97,9 +97,9 @@ theorem norm_snoc_eq_concat {t₁ : XTuple α (p, q)} {t₂ : Tuple α n} : norm (snoc t₁ t₂) = Tuple.concat t₁.norm t₂ := by conv => lhs; unfold norm -/- ------------------------------------- - - Equality - - -------------------------------------/ +-- ======================================== +-- Equality +-- ======================================== /-- Implements Boolean equality for `XTuple α n` provided `α` has decidable @@ -108,9 +108,9 @@ equality. instance BEq [DecidableEq α] : BEq (XTuple α n) where beq t₁ t₂ := t₁.norm == t₂.norm -/- ------------------------------------- - - Basic API - - -------------------------------------/ +-- ======================================== +-- Basic API +-- ======================================== /-- Returns the number of entries in the `XTuple`. @@ -163,9 +163,9 @@ def snd : XTuple α (m, n) → Tuple α n | x[] => t[] | snoc _ ts => ts -/- ------------------------------------- - - Lemma 0A - - -------------------------------------/ +-- ======================================== +-- Lemma 0A +-- ======================================== section @@ -188,13 +188,13 @@ lemma n_eq_succ_k : n = k + 1 := _ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm] _ = 1 + k := by simp _ = k + 1 := by rw [Nat.add_comm] - + lemma n_pred_eq_k : n - 1 = k := by have h : k + 1 - 1 = k + 1 - 1 := rfl conv at h => lhs; rw [←n_eq_succ_k p q] simp at h exact h - + lemma n_geq_one : 1 ≤ n := by rw [n_eq_succ_k p q] simp @@ -221,7 +221,7 @@ def cast_norm : XTuple α (n, m - 1) → Tuple α (m + k) def cast_fst : XTuple α (n, m - 1) → Tuple α (k + 1) | xs => cast (by rw [n_eq_succ_k p q]) xs.fst - + def cast_take (ys : Tuple α (m + k)) := cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1)) diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json index 123a66f..59662d6 100644 --- a/mathematical-introduction-logic/lake-manifest.json +++ b/mathematical-introduction-logic/lake-manifest.json @@ -1,8 +1,7 @@ {"version": 4, "packagesDir": "lake-packages", "packages": - [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}}, - {"git": + [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", @@ -25,4 +24,5 @@ "subDir?": null, "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", - "inputRev?": "main"}}]} + "inputRev?": "main"}}, + {"path": {"name": "Common", "dir": "./../common"}}]} diff --git a/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean index 6ead34c..338c3cc 100644 --- a/mathematical-introduction-logic/lakefile.lean +++ b/mathematical-introduction-logic/lakefile.lean @@ -3,9 +3,7 @@ open Lake DSL package «mathematical-introduction-logic» -require Bookshelf from "../bookshelf" +require Common from "../common" @[default_target] -lean_lib «enderton» { - -- add library configuration options here -} +lean_lib «enderton» diff --git a/theorem-proving-in-lean/Avigad/Chapter2.lean b/theorem-proving-in-lean/Avigad/Chapter2.lean index 37066f8..bfa62a3 100644 --- a/theorem-proving-in-lean/Avigad/Chapter2.lean +++ b/theorem-proving-in-lean/Avigad/Chapter2.lean @@ -4,9 +4,11 @@ Chapter 2 Dependent Type Theory -/ +-- ======================================== -- Exercise 1 -- -- Define the function `Do_Twice`, as described in Section 2.4. +-- ======================================== namespace ex1 def double (x : Nat) := x + x @@ -17,9 +19,11 @@ def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f end ex1 +-- ======================================== -- Exercise 2 -- -- Define the functions `curry` and `uncurry`, as described in Section 2.4. +-- ======================================== namespace ex2 def curry (f : α × β → γ) : (α → β → γ) := @@ -30,6 +34,7 @@ def uncurry (f : α → β → γ) : (α × β → γ) := end ex2 +-- ======================================== -- Exercise 3 -- -- Above, we used the example `vec α n` for vectors of elements of type `α` of @@ -39,6 +44,8 @@ end ex2 -- implicit arguments for parameters that can be inferred. Declare some -- variables and check some expressions involving the constants that you have -- declared. +-- ======================================== + namespace ex3 universe u @@ -64,6 +71,7 @@ variable (c d : vec Prop 2) end ex3 +-- ======================================== -- Exercise 4 -- -- Similarly, declare a constant `matrix` so that `matrix α m n` could represent @@ -72,6 +80,8 @@ end ex3 -- (using vec) multiplication of a matrix by a vector. Once again, declare some -- variables and check some expressions involving the constants that you have -- declared. +-- ======================================== + namespace ex4 universe u diff --git a/theorem-proving-in-lean/Avigad/Chapter3.lean b/theorem-proving-in-lean/Avigad/Chapter3.lean index 47b465d..51856c6 100644 --- a/theorem-proving-in-lean/Avigad/Chapter3.lean +++ b/theorem-proving-in-lean/Avigad/Chapter3.lean @@ -4,10 +4,13 @@ Chapter 3 Propositions and Proofs -/ +-- ======================================== -- Exercise 1 -- -- Prove the following identities, replacing the "sorry" placeholders with -- actual proofs. +-- ======================================== + namespace ex1 open or @@ -102,10 +105,13 @@ example : (p → q) → (¬q → ¬p) := end ex1 --- Example 2 +-- ======================================== +-- Exercise 2 -- -- Prove the following identities, replacing the “sorry” placeholders with -- actual proofs. These require classical reasoning. +-- ======================================== + namespace ex2 open Classical @@ -147,9 +153,12 @@ example : (((p → q) → p) → p) := end ex2 --- Example 3 +-- ======================================== +-- Exercise 3 -- -- Prove `¬(p ↔ ¬p)` without using classical logic. +-- ======================================== + namespace ex3 variable (p : Prop) diff --git a/theorem-proving-in-lean/Avigad/Chapter4.lean b/theorem-proving-in-lean/Avigad/Chapter4.lean index 6768087..f0223da 100644 --- a/theorem-proving-in-lean/Avigad/Chapter4.lean +++ b/theorem-proving-in-lean/Avigad/Chapter4.lean @@ -4,10 +4,13 @@ Chapter 4 Quantifiers and Equality -/ +-- ======================================== -- Exercise 1 -- -- Prove these equivalences. You should also try to understand why the reverse -- implication is not derivable in the last example. +-- ======================================== + namespace ex1 variable (α : Type _) @@ -34,11 +37,14 @@ example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := end ex1 +-- ======================================== -- Exercise 2 -- -- It is often possible to bring a component of a formula outside a universal -- quantifier, when it does not depend on the quantified variable. Try proving -- these (one direction of the second of these requires classical logic). +-- ======================================== + namespace ex2 variable (α : Type _) @@ -70,11 +76,14 @@ example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := end ex2 +-- ======================================== -- Exercise 3 -- -- Consider the "barber paradox," that is, the claim that in a certain town -- there is a (male) barber that shaves all and only the men who do not shave -- themselves. Prove that this is a contradiction. +-- ======================================== + namespace ex3 open Classical @@ -91,6 +100,7 @@ example (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : False := end ex3 +-- ======================================== -- Exercise 4 -- -- Remember that, without any parameters, an expression of type `Prop` is just @@ -101,6 +111,8 @@ end ex3 -- states that every odd number greater than `5` is the sum of three primes. -- Look up the definition of a Fermat prime or any of the other statements, if -- necessary. +-- ======================================== + namespace ex4 def even (a : Nat) := ∃ b, a = 2 * b @@ -132,9 +144,12 @@ def Fermat'sLastTheorem : Prop := end ex4 +-- ======================================== -- Exercise 5 -- -- Prove as many of the identities listed in Section 4.4 as you can. +-- ======================================== + namespace ex5 open Classical @@ -215,9 +230,12 @@ example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := end ex5 +-- ======================================== -- Exercise 6 -- -- Give a calculational proof of the theorem `log_mul` below. +-- ======================================== + namespace ex6 variable (log exp : Float → Float) diff --git a/theorem-proving-in-lean/Avigad/Chapter5.lean b/theorem-proving-in-lean/Avigad/Chapter5.lean index 1698e11..f34fb4b 100644 --- a/theorem-proving-in-lean/Avigad/Chapter5.lean +++ b/theorem-proving-in-lean/Avigad/Chapter5.lean @@ -4,13 +4,18 @@ Chapter 5 Tactics -/ +-- ======================================== -- Exercise 1 -- -- Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you -- can now with tactic proofs, using also `rw` and `simp` as appropriate. +-- ======================================== + namespace ex1 +-- ---------------------------------------- -- Exercises 3.1 +-- ---------------------------------------- section ex3_1 @@ -151,7 +156,9 @@ example : (p → q) → (¬q → ¬p) := by end ex3_1 +-- ---------------------------------------- -- Exercises 3.2 +-- ---------------------------------------- section ex3_2 @@ -220,7 +227,9 @@ example : (((p → q) → p) → p) := by end ex3_2 +-- ---------------------------------------- -- Exercises 3.3 +-- ---------------------------------------- section ex3_3 @@ -232,7 +241,9 @@ example (hp : p) : ¬(p ↔ ¬p) := by end ex3_3 +-- ---------------------------------------- -- Exercises 4.1 +-- ---------------------------------------- section ex4_1 @@ -261,7 +272,9 @@ example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := by end ex4_1 +-- ---------------------------------------- -- Exercises 4.2 +-- ---------------------------------------- section ex4_2 @@ -313,7 +326,9 @@ example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by end ex4_2 +-- ---------------------------------------- -- Exercises 4.3 +-- ---------------------------------------- section ex4_3 @@ -332,7 +347,9 @@ example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by end ex4_3 +-- ---------------------------------------- -- Exercises 4.5 +-- ---------------------------------------- section ex4_5 @@ -443,9 +460,12 @@ end ex4_5 end ex1 +-- ======================================== -- Exercise 2 -- -- Use tactic combinators to obtain a one line proof of the following: +-- ======================================== + namespace ex2 example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := diff --git a/theorem-proving-in-lean/Avigad/Chapter7.lean b/theorem-proving-in-lean/Avigad/Chapter7.lean index 032e5f9..c556ec7 100644 --- a/theorem-proving-in-lean/Avigad/Chapter7.lean +++ b/theorem-proving-in-lean/Avigad/Chapter7.lean @@ -4,6 +4,7 @@ Chapter 7 Inductive Types -/ +-- ======================================== -- Exercise 1 -- -- Try defining other operations on the natural numbers, such as multiplication, @@ -15,6 +16,8 @@ Inductive Types -- Since many of these are already defined in Lean’s core library, you should -- work within a namespace named hide, or something like that, in order to avoid -- name clashes. +-- ======================================== + namespace ex1 -- As defined in the book. @@ -74,6 +77,7 @@ end Nat end ex1 +-- ======================================== -- Exercise 2 -- -- Define some operations on lists, like a `length` function or the `reverse` @@ -82,6 +86,8 @@ end ex1 -- a. `length (s ++ t) = length s + length t` -- b. `length (reverse t) = length t` -- c. `reverse (reverse t) = t` +-- ======================================== + namespace ex2 variable {α : Type _} @@ -171,6 +177,7 @@ theorem reverse_reverse (t : List α) end ex2 +-- ======================================== -- Exercise 3 -- -- Define an inductive data type consisting of terms built up from the following @@ -183,6 +190,8 @@ end ex2 -- -- Recursively define a function that evaluates any such term with respect to an -- assignment of values to the variables. +-- ======================================== + namespace ex3 inductive Foo : Type _ diff --git a/theorem-proving-in-lean/Avigad/Chapter8.lean b/theorem-proving-in-lean/Avigad/Chapter8.lean index 0ae3c31..5c3e731 100644 --- a/theorem-proving-in-lean/Avigad/Chapter8.lean +++ b/theorem-proving-in-lean/Avigad/Chapter8.lean @@ -4,12 +4,15 @@ Chapter 8 Induction and Recursion -/ +-- ======================================== -- Exercise 1 -- -- Open a namespace `Hidden` to avoid naming conflicts, and use the equation -- compiler to define addition, multiplication, and exponentiation on the -- natural numbers. Then use the equation compiler to derive some of their basic -- properties. +-- ======================================== + namespace ex1 def add : Nat → Nat → Nat @@ -26,11 +29,14 @@ def exp : Nat → Nat → Nat end ex1 +-- ======================================== -- Exercise 2 -- -- Similarly, use the equation compiler to define some basic operations on lists -- (like the reverse function) and prove theorems about lists by induction (such -- as the fact that `reverse (reverse xs) = xs` for any list `xs`). +-- ======================================== + namespace ex2 variable {α : Type _} @@ -43,11 +49,14 @@ def reverse : List α → List α end ex2 +-- ======================================== -- Exercise 3 -- -- Define your own function to carry out course-of-value recursion on the -- natural numbers. Similarly, see if you can figure out how to define -- `WellFounded.fix` on your own. +-- ======================================== + namespace ex3 def below {motive : Nat → Type} : Nat → Type @@ -58,11 +67,14 @@ def below {motive : Nat → Type} : Nat → Type end ex3 +-- ======================================== -- Exercise 4 -- -- Following the examples in Section Dependent Pattern Matching, define a -- function that will append two vectors. This is tricky; you will have to -- define an auxiliary function. +-- ======================================== + namespace ex4 inductive Vector (α : Type u) : Nat → Type u @@ -77,11 +89,14 @@ end Vector end ex4 +-- ======================================== -- Exercise 5 -- -- Consider the following type of arithmetic expressions. The idea is that -- `var n` is a variable, `vₙ`, and `const n` is the constant whose value is -- `n`. +-- ======================================== + namespace ex5 inductive Expr where @@ -113,10 +128,12 @@ def sampleVal : Nat → Nat -- Try it out. You should get 47 here. -- #eval eval sampleVal sampleExpr +-- ---------------------------------------- -- Implement "constant fusion," a procedure that simplifies subterms like -- `5 + 7` to `12`. Using the auxiliary function `simpConst`, define a function -- "fuse": to simplify a plus or a times, first simplify the arguments -- recursively, and then apply `simpConst` to try to simplify the result. +-- ---------------------------------------- def simpConst : Expr → Expr | plus (const n₁) (const n₂) => const (n₁ + n₂)