Suggestions for clarity

conv.md

@@ -14,7 +14,7 @@ As a first example, let us prove example
 (examples in this file are somewhat artificial since
 other tactics could finish them immediately). The naive
 first attempt is to enter tactic mode and try `rw [Nat.mul_comm]`. But this
-transforms the goal into `b * c * a = a * (c * b)`, after commuting the
+transforms the goal into `b * c * a = a * (c * b)`, because it commutes the
 very first multiplication appearing in the term. There are several
 ways to fix this issue, and one way is to use a more precise tool:
 the conversion mode. The following code block shows the current target
@@ -35,7 +35,8 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
 
 The above snippet shows three navigation commands:
 
-- `lhs` navigates to the left hand side of a relation (here equality), there is also a `rhs` navigating to the right hand side.
+- `lhs` navigates to the left-hand side of a relation (here equality).
+There is also a `rhs` to navigate to the right-hand side.
 - `congr` creates as many targets as there are (nondependent and explicit) arguments to the current head function
   (here the head function is multiplication).
 - `rfl` closes target using reflexivity.
@@ -154,8 +155,13 @@ example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by
   exact h₁
 ```
 
+
 - `enter [1, x, 2, y]` iterate `arg` and `intro` with the given arguments. It is just the macro:
 
+<!-- using the specific example [1, x, 2, y] here is confusing.
+For example, the reader might think that only versions this particular form (alternating index, name) can be used.
+Adding, say, [1,2,x] as another example would also be useful. -->
+
 ```
 syntax enterArg := ident <|> group("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv

dependent_type_theory.md

@@ -224,8 +224,8 @@ hierarchy of types:
 Think of ``Type 0`` as a universe of "small" or "ordinary" types.
 ``Type 1`` is then a larger universe of types, which contains ``Type
 0`` as an element, and ``Type 2`` is an even larger universe of types,
-which contains ``Type 1`` as an element. The list is indefinite, so
-that there is a ``Type n`` for every natural number ``n``. ``Type`` is
+which contains ``Type 1`` as an element. The list is infinite:
+there is a ``Type n`` for every natural number ``n``. ``Type`` is
 an abbreviation for ``Type 0``:
 
 ```lean
@@ -256,8 +256,8 @@ type signature of the function ``List``:
 ```
 
 Here ``u`` is a variable ranging over type levels. The output of the
-``#check`` command means that whenever ``α`` has type ``Type n``,
-``List α`` also has type ``Type n``. The function ``Prod`` is
+``#check List`` command means that whenever ``α`` has type ``Type u``,
+``List α`` also has type ``Type u``. The function ``Prod`` is
 similarly polymorphic:
 
 ```lean
@@ -355,11 +355,11 @@ You can also pass types as parameters:
 ```lean
 #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
 ```
-The last expression, for example, denotes the function that takes
+This expression, for example, denotes the function that takes
 three types, ``α``, ``β``, and ``γ``, and two functions, ``g : β → γ``
 and ``f : α → β``, and returns the composition of ``g`` and ``f``.
 (Making sense of the type of this function requires an understanding
-of dependent products, which will be explained below.)
+of *dependent products*, which will be explained below.)
 
 The general form of a lambda expression is ``fun x : α => t``, where
 the variable ``x`` is a "bound variable": it is really a placeholder,
@@ -482,30 +482,33 @@ So `def` can also be used to simply name a value like this:
 def pi := 3.141592654
 ```
 
-`def` can take multiple input parameters.  Let's create one
+`def` can take multiple input parameters.  Let's define a function
 that adds two natural numbers:
 
 ```lean
-def add (x y : Nat) :=
+def add (x Nat) (y : Nat) :=
   x + y
 
 #eval add 3 2               -- 5
 ```
 
-The parameter list can be separated like this:
+For convenience, the parameter list can be abbreviated as follows:
 
 ```lean
 # def double (x : Nat) : Nat :=
 #  x + x
-def add (x : Nat) (y : Nat) :=
+def add (x y : Nat) :=
   x + y
 
 #eval add (double 3) (7 + 9)  -- 22
 ```
+The resulting function will display a different *signature*, but the function itself will have the same type as before.
 
-Notice here we called the `double` function to create the first
+Notice that we used the `double` function to create the first
 parameter to `add`.
 
+<!-- a quick note about currying would be in order here, and perhaps a definition of "signature" -->
+
 You can use other more interesting expressions inside a `def`:
 
 ```lean
@@ -517,7 +520,7 @@ def greater (x y : Nat) :=
 You can probably guess what this one will do.
 
 You can also define a function that takes another function as input.
-The following calls a given function twice passing the output of the
+The following calls a given function twice, passing the output of the
 first invocation to the second:
 
 ```lean
@@ -530,30 +533,30 @@ def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
 ```
 
 Now to get a bit more abstract, you can also specify arguments that
-are like type parameters:
+are like type parameters,
+such as `(α β γ : Type)` here:
 
 ```lean
 def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
   g (f x)
 ```
 
-This means `compose` is a function that takes any two functions as input
-arguments, so long as those functions each take only one input.
-The type algebra `β → γ` and `α → β` means it is a requirement
+This defines `compose` as a function that takes three type arguments (`α β γ : Type`) and two other functions as arguments,
+locally named `f` and `g`. Furthermore,
+the type constraints `β → γ` and `α → β` require
 that the type of the output of the second function must match the
 type of the input to the first function - which makes sense, otherwise
 the two functions would not be composable.
 
-`compose` also takes a 3rd argument of type `α` which
-it uses to invoke the second function (locally named `f`) and it
-passes the result of that function (which is type `β`) as input to the
-first function (locally named `g`).  The first function returns a type
-`γ` so that is also the return type of the `compose` function.
+`compose` also takes one last argument `x` of type `α`, which
+it uses to invoke the second function (`f`).
+The result of that function, of type `β`, is passed as the input to the
+first function (`g`).  The first function returns a result of type
+`γ`, so that is also the return type of the `compose` function.
 
-`compose` is also very general in that it works over any type
-`α β γ`.  This means `compose` can compose just about any 2 functions
-so long as they each take one parameter, and so long as the type of
-output of the second matches the input of the first.  For example:
+`compose` is also very general in that it works over any types
+`α β γ`.  This means `compose` can compose just about any two functions
+as long as the output type of the second matches the input type of the first.  For example:
 
 ```lean
 # def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
@@ -566,6 +569,10 @@ def square (x : Nat) : Nat :=
 #eval compose Nat Nat Nat double square 3  -- 18
 ```
 
+Lean has syntax to make the three type parameters (`α β γ`) implicit,
+so that they don't have to be explicitly included each time that `compose` is called ---
+see the [Implicit Arguments](#Implicit-Arguments) section below.
+
 Local Definitions
 -----------------
 
@@ -733,12 +740,13 @@ open Foo
 #check Foo.fa
 ```
 
-When you declare that you are working in the namespace ``Foo``, every
-identifier you declare has a full name with prefix "``Foo.``". Within
-the namespace, you can refer to identifiers by their shorter names,
-but once you end the namespace, you have to use the longer names.
-Unlike `section`, namespaces require a name. There is only one
-anonymous namespace at the root level.
+Inside the scope of the namespace ``Foo``, every
+identifier you declare is given a full name with prefix "``Foo.``".
+Within the namespace, you can use the shorter names,
+but once you end the namespace, you must use the longer, *fully qualified* names.
+
+Unlike `section`, namespaces require a name. (There is only one
+anonymous namespace: the one at the root level.)
 
 The ``open`` command brings the shorter names into the current
 context. Often, when you import a module, you will want to open one or
@@ -1076,10 +1084,10 @@ used to specify the desired types of the expressions ``id`` and
 ```
 
 Numerals are overloaded in Lean, but when the type of a numeral cannot
-be inferred, Lean assumes, by default, that it is a natural number. So
+be inferred, Lean assumes, by default, that it is a natural number. Thus,
 the expressions in the first two ``#check`` commands below are
-elaborated in the same way, whereas the third ``#check`` command
-interprets ``2`` as an integer.
+both elaborated as `Nat`, whereas the third ``#check`` command
+interprets ``2`` as an `Int`.
 
 ```lean
 #check 2            -- Nat
@@ -1102,6 +1110,8 @@ made explicit.
 #check @id Bool true -- Bool
 ```
 
-Notice that now the first ``#check`` command gives the type of the
-identifier, ``id``, without inserting any placeholders. Moreover, the
-output indicates that the first argument is implicit.
+Notice that the ``#check @id`` command now gives the full type of the
+identifier, ``id``, without any placeholders. Moreover, the
+curly brackets in the
+output indicate that the first argument, `α`, is implicit.
+

interacting_with_lean.md

@@ -17,8 +17,8 @@ Importing Files
 ---------------
 
 The goal of Lean's front end is to interpret user input, construct
-formal expressions, and check that they are well formed and type
-correct. Lean also supports the use of various editors, which provide
+formal expressions, and check that they are well-formed and type-correct.
+Lean also supports the use of various editors, which provide
 continuous checking and feedback. More information can be found on the
 Lean [documentation pages](https://lean-lang.org/documentation/).
 
@@ -290,6 +290,8 @@ theorem List.isPrefix_self (as : List α) : as ≤ as :=
   ⟨[], by simp⟩
 ```
 
+<!-- This example is confusing because the `instance:...` command does not mention ≤ -->
+
 That assignment can also be made local:
 
 ```lean

propositions_and_proofs.md

@@ -13,12 +13,14 @@ One strategy for proving assertions about objects defined in the
 language of dependent type theory is to layer an assertion language
 and a proof language on top of the definition language. But there is
 no reason to multiply languages in this way: dependent type theory is
-flexible and expressive, and there is no reason we cannot represent
+flexible and expressive, and it turns out that we can represent
 assertions and proofs in the same general framework.
 
-For example, we could introduce a new type, ``Prop``, to represent
+<!-- it is not clear if this is meant as an example of layering languages on top or not -->
+
+For example, we can introduce a new type, ``Prop``, to represent
 propositions, and introduce constructors to build new propositions
-from others.
+from others:
 
 ```lean
 # def Implies (p q : Prop) : Prop := p → q
@@ -136,7 +138,7 @@ that even though we can treat proofs ``t : p`` as ordinary objects in
 the language of dependent type theory, they carry no information
 beyond the fact that ``p`` is true.
 
-The two ways we have suggested thinking about the
+The two ways we have suggested for thinking about the
 propositions-as-types paradigm differ in a fundamental way. From the
 constructive point of view, proofs are abstract mathematical objects
 that are *denoted* by suitable expressions in dependent type
@@ -156,7 +158,7 @@ syntax and semantics by saying, at times, that a program "computes" a
 certain function, and at other times speaking as though the program
 "is" the function in question.
 
-In any case, all that really matters is the bottom line. To formally
+In any case, all that really matters is the bottom line: To formally
 express a mathematical assertion in the language of dependent type
 theory, we need to exhibit a term ``p : Prop``. To *prove* that
 assertion, we need to exhibit a term ``t : p``. Lean's task, as a
@@ -191,7 +193,7 @@ true.
 Note that the ``theorem`` command is really a version of the
 ``def`` command: under the propositions and types
 correspondence, proving the theorem ``p → q → p`` is really the same
-as defining an element of the associated type. To the kernel type
+as defining an element of the associated type. To the Lean kernel type
 checker, there is no difference between the two.
 
 There are a few pragmatic differences between definitions and
@@ -202,7 +204,7 @@ theorem is complete, typically we only need to know that the proof
 exists; it doesn't matter what the proof is. In light of that fact,
 Lean tags proofs as *irreducible*, which serves as a hint to the
 parser (more precisely, the *elaborator*) that there is generally no
-need to unfold it when processing a file. In fact, Lean is generally
+need to unfold them when processing a file. In fact, Lean is generally
 able to process and check proofs in parallel, since assessing the
 correctness of one proof does not require knowing the details of
 another.
@@ -260,10 +262,10 @@ axiom hp : p
 theorem t2 : q → p := t1 hp
 ```
 
-Here, the ``axiom`` declaration postulates the existence of an
-element of the given type and may compromise logical consistency. For
-example, we can use it to postulate the empty type `False` has an
-element.
+The ``axiom`` declaration postulates the existence of an
+element of the given type, and may compromise logical consistency. For
+example, we can use it to postulate that the empty type `False` has an
+element:
 
 ```lean
 axiom unsound : False
@@ -321,6 +323,9 @@ be written ``∀ (p q : Prop) (hp : p) (hq : q), p``, since the arrow
 denotes nothing more than an arrow type in which the target does not
 depend on the bound variable.
 
+<!-- Perhaps point out that `variable {p : Prop}` does not mean that `p` is an axiom, but
+     `variable (hp : p)` does, letting us prove `theorem pholds : p := hp` -->
+
 When we generalize ``t1`` in such a way, we can then apply it to
 different pairs of propositions, to obtain different instances of the
 general theorem.