diff --git a/README.md b/README.md index 96bb210..1fe6dbf 100644 --- a/README.md +++ b/README.md @@ -5,13 +5,13 @@ Abstract Mathematics as Semantics Domains for Complex Computations TL;DR ----- -This repo supports the development and delivery of notes for an early graduate course in computer science at the University Virginia. This course is intended to take early graduate students from a point of having no knowledge of formal reasoning through basics of logic and proof using the Lean proof assistant, and into the realm of formalized mathematics. The thesis underlying this work is that CS can now benefit greatly by taking advantage of rapid advances in the formalization of abstract and advanced mathemtics to provide deep semantic foundations for critical application areas, including robotics, cyberphysical systems more generally, and AI. This work is thus meant to start to close a significant gap between mathematics and computer science research to improve software design, productivity, and dependability, but *not* on a path to formal verification. The evolving notes are [here](https://www.computingfoundations.org). We solicit interest and are open to research community engagement. Feel free to reach out: sullivan@virginia.edu. +This repo supports the development and delivery of notes for an early graduate course in computer science at the University Virginia. This course is intended to take early graduate students from a point of having no knowledge of formal reasoning through basics of logic and proof using the Lean proof assistant, and into the realm of formalized mathematics. The thesis underlying this work is that CS can now benefit greatly by taking advantage of rapid advances in the formalization of abstract and advanced mathematics to provide deep semantic foundations for critical application areas, including robotics, cyberphysical systems more generally, and AI. This work is thus meant to start to close a significant gap between mathematics and computer science research to improve software design, productivity, and dependability, but *not* on a path to formal verification. The evolving notes are [here](https://www.computingfoundations.org). We solicit interest and are open to research community engagement. Feel free to reach out: sullivan@virginia.edu. Motivation ---------- -For millenia, to the present day, abstract mathematics +For millennia, to the present day, abstract mathematics has been an analog, paper-and-pencil, pursuit. For most of that time, there was nothing but paper and pencil, of course and that's what it mostly remains. @@ -31,7 +31,7 @@ This work has been funded in part by the National Science Foundation as part of This Repository --------------- -This repository is the course development and delivery platform for CS6501, Special Topics in Software Engineering, Abstract Mathemtical Foundations, being taught in the Spring of 2023. +This repository is the course development and delivery platform for CS6501, Special Topics in Software Engineering, Abstract Mathematical Foundations, being taught in the Spring of 2023. The rest of this document is entirely for my own use. It presents instructions, mostly for myself, on how to use it. @@ -71,7 +71,7 @@ Manual Processes ---------------- The following files are maintained by hand: -- The file `source/index.rst` should have an entry for each chapter/dicrectory. +- The file `source/index.rst` should have an entry for each chapter/directory. - For each chapter/directory, there should be a `.rst` file in `source`. It should include - each of the sections. - For each section, there should be a `.lean` file in the appropriate place in `lean_source`. @@ -100,7 +100,7 @@ From the top-level directory of the cloned repo do this: - deploy.sh (TODO: needs to be fixed) - instead follow instructions in UPLOAD.md -The script `deploy.sh` KS: FIX deploy everythings (textbook +The script `deploy.sh` KS: FIX deploy everything (textbook and user version of the example and solution files) to an arbitrary repository, set up to use the `gh-pages` branch to display the html. Note: Avigad uses the following here: diff --git a/lean_source/A_00_Introduction/A_01_abstract_language_and_thought.lean b/lean_source/A_00_Introduction/A_01_abstract_language_and_thought.lean index 20b35ed..c01d874 100644 --- a/lean_source/A_00_Introduction/A_01_abstract_language_and_thought.lean +++ b/lean_source/A_00_Introduction/A_01_abstract_language_and_thought.lean @@ -54,8 +54,8 @@ Costs of Concreteness This ubiquitous approach to programming physical computations is problematical in multiple dimensions. First, as mentioned, -it substitues concrete representations for abstract, adding -inessesntial complexity to models and computations. Second, +it substitutes concrete representations for abstract, adding +inessential complexity to models and computations. Second, it generally strips away crucial mathematical properties of the abstract representations of objects of interest, making it impossible to check programs for consistency with such @@ -111,7 +111,7 @@ exercise, making it, hard even impossible, to connect code to such mathematics. Now, with rapidly developing work by a still small set of -ressearchers in mathematics, the complete formalization and +researchers in mathematics, the complete formalization and mechanization of advanced abstract mathematics is becoming a reality. As and example Massot and his colleagues in 2022 managed to formalize not only a statement, but a proof, of @@ -133,7 +133,7 @@ The insight driving this class is that this kind of work from the mathematics community is now making it possible to develop *computable abstract mathematics* for purposes of software engineering. Promising application domains for -such work clearly include divere cyber-physical systems and +such work clearly include diverse cyber-physical systems and might be relevant to deep learning as well, with its basic assumption that real-world data have geometric properties, such as lying on high-dimensional manifolds. @@ -160,7 +160,7 @@ TEXT. -/ /- The idea of raising the abstraction level of programming languages and programs is ages old. But these increases -in abstration are usually incremental and ad hoc, moving +in abstraction are usually incremental and ad hoc, moving in small steps from the language of the machine closer to but never really approaching the richness of the abstract mathematics of the domain, using its concepts, notations, @@ -209,7 +209,7 @@ manifolds. Linking such abstract mathematics to code has always been a manual processes. Now, however, with the automation of -abstract mathemtics by parts of the mathematics community +abstract mathematics by parts of the mathematics community using constructive logic proof assistants and type theory, that has become possible. This course will teach you the basic concepts that you will need to start to make such diff --git a/lean_source/A_00_Introduction/A_02_this_class.lean b/lean_source/A_00_Introduction/A_02_this_class.lean index ee25148..2d20fa2 100644 --- a/lean_source/A_00_Introduction/A_02_this_class.lean +++ b/lean_source/A_00_Introduction/A_02_this_class.lean @@ -27,14 +27,14 @@ Here, the adjective, abstract, means *being coordinate-free*. For the opposite of *abstract*, we'll use *parametric*. The idea is that a mathematical object, such as a vector, can be understood simply as such, with no reference to coordinates; or that same abstract -vector can be represented concretely/parametrically as a struture of +vector can be represented concretely/parametrically as a structure of parameter values expressed relative to some given frame of reference. Why *abstract* mathematics? --------------------------- A premise of this class is that domain experts (e.g., in the -physics of terrestrial robotics, or of elemenary particles) speak, +physics of terrestrial robotics, or of elementary particles) speak, model, analyze, and understand the operation of systems in the abstract mathematical language of the domain, and very often not in terms of ultimately arbitrarily selected frames of reference . @@ -73,7 +73,7 @@ of the domain and with very little custom coding needed also to have corresponding verified implementations, even if only used as test oracles for production code. -This is the of abstract specifictions from which concrete +This is the of abstract specifications from which concrete implementations are derived. I will not say refined because in practice most derivations are not refinements but rather toyish models of semantically rich and complex computations @@ -84,7 +84,7 @@ This class The first major part of this class will teach you the fundamentals of programming and reasoning in Lean 3. We will mainly use Lean 3, -nothwithstaning that Lean 4 is garnering real attention and effort. +notwithstanding that Lean 4 is garnering real attention and effort. Student might wish to explore Lean 4 as an optional class activity. The second part of the class will focus on how to formalized abstract diff --git a/lean_source/A_01_Propositional_Logic/A_01_formal_languages.lean b/lean_source/A_01_Propositional_Logic/A_01_formal_languages.lean index a10ac44..9449868 100644 --- a/lean_source/A_01_Propositional_Logic/A_01_formal_languages.lean +++ b/lean_source/A_01_Propositional_Logic/A_01_formal_languages.lean @@ -8,7 +8,7 @@ As a warmup, and to put some basic concepts into play, we'll begin by specifying the syntax and semantics of a simple formal language: the language of strings of balanced parentheses. Before we do that, we'll -better explain wht it all menas. So let's get started. +better explain what it all means. So let's get started. Formal languages ---------------- @@ -34,7 +34,7 @@ natural number, *n*, there is a such a string with nesting depth *n*. We clearly can't specify the set of strings by exhaustively -enumerating them expliciitly. There are too many for that. +enumerating them explicitly. There are too many for that. Rather, we need a concise, precise, finite, and manageable way to specify the set of all such strings. We will do that by defining a small set of *basic rules for building* strings @@ -66,13 +66,13 @@ Paper & Pencil Syntax What we've basically done in this case is to specify the set of strings in our language with a *grammar* or *syntax definition*. Such grammars are often expressed, especially in the programming -worls, using so-called *Backus-Naur Form (BNF)*. +world, using so-called *Backus-Naur Form (BNF)*. Backus first used BNF notation to define the syntax of the Algol 60 programming language. BNF is basically a notation for specifying what the linguist, Noam Chomsky, called *context-free grammars*. -Here's a grammer in BNF for our language of balanced parentheses. +Here's a grammar in BNF for our language of balanced parentheses. We can say that the BNF grammar defines the syntax, or permitted forms, of strings in our language. Be sure you see how this grammar allow larger expressions to be build from smaller ones of the same @@ -232,7 +232,7 @@ data types in Lean that you should now understand. First, they are *disjoint*. Different constructors *never* produce the same value. Second, they are *injective*. A constructor applied to different argument values will always produce different terms. -Finally, they are complete. The langauge they define contains +Finally, they are complete. The language they define contains *all* of the strings constructible by any finite number of applications of the defined constructors *and no other terms*. For example, our *bal* language doesn't contain any *error* or diff --git a/lean_source/A_01_Propositional_Logic/A_02_subset_prop_logic.lean b/lean_source/A_01_Propositional_Logic/A_02_subset_prop_logic.lean index 43036e9..3ec5936 100644 --- a/lean_source/A_01_Propositional_Logic/A_02_subset_prop_logic.lean +++ b/lean_source/A_01_Propositional_Logic/A_02_subset_prop_logic.lean @@ -7,7 +7,7 @@ Simplified Propositional Logic Our next step toward formalizing abstract mathematics for software engineering, we will specify the syntax and semantics of a simple -but important mathatical language, namely *propositional logic*. +but important mathematical language, namely *propositional logic*. Propositional logic is isomorphic to (essentially the same thing as) Boolean algebra. You already know about Boolean algebra from diff --git a/lean_source/A_01_Propositional_Logic/A_06_prop_logic_algebraic_axioms.lean b/lean_source/A_01_Propositional_Logic/A_06_prop_logic_algebraic_axioms.lean index 5649761..354c07b 100644 --- a/lean_source/A_01_Propositional_Logic/A_06_prop_logic_algebraic_axioms.lean +++ b/lean_source/A_01_Propositional_Logic/A_06_prop_logic_algebraic_axioms.lean @@ -114,7 +114,7 @@ Another Notation As we've seen, mathematical theories are often augmented with concrete syntactic notations that make it easier for people to read and write such -mathemantics. We would typically write *3 + 4*, +mathematics. We would typically write *3 + 4*, for example, in lieu of *nat.add 3 4*. For that matter, we write *3* for (succ(succ(succ zero))). Good notations are important. @@ -197,7 +197,7 @@ Specialization of Generalizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Observe: We can *apply* these theorems -to particular objects to specalize the +to particular objects to specialize the generalized statement to the particular objects. TEXT. -/ @@ -358,7 +358,7 @@ developed into a mathematical library component with an emphasis on good design. What does that even mean? Good with respect to -what criteria, deciderata, needs, objectives? +what criteria, desiderata, needs, objectives? - data type definitions - operation definitions diff --git a/lean_source/A_01_Propositional_Logic/A_07_prop_logic_inference_rules.lean b/lean_source/A_01_Propositional_Logic/A_07_prop_logic_inference_rules.lean index 26d39ff..7e8ecbf 100644 --- a/lean_source/A_01_Propositional_Logic/A_07_prop_logic_inference_rules.lean +++ b/lean_source/A_01_Propositional_Logic/A_07_prop_logic_inference_rules.lean @@ -6,7 +6,7 @@ Inference Rules In this chapter we will present another approach to validating our model of propositional logic: by -verifying that it satisifies the *inference rules* +verifying that it satisfies the *inference rules* of this logic. An inference rule is basically a function that takes diff --git a/lean_source/A_01_Propositional_Logic/A_08_prop_logic_inference_rules_validation.lean b/lean_source/A_01_Propositional_Logic/A_08_prop_logic_inference_rules_validation.lean index 3f56507..45affc3 100644 --- a/lean_source/A_01_Propositional_Logic/A_08_prop_logic_inference_rules_validation.lean +++ b/lean_source/A_01_Propositional_Logic/A_08_prop_logic_inference_rules_validation.lean @@ -17,7 +17,7 @@ The first section of this chapter refactors the partial solution we developed in class, grouping definitions of the propositions that represent them, and separately a proof that each rule expresses in our model is valid. -These sections also afford opportunities to intruduce +These sections also afford opportunities to introduce a few more concepts in type theory and Lean. To begin we import some definitions and declare a set @@ -177,7 +177,7 @@ Identify any rules that fail to be provably valid in the presence of the bug we'd injected in bimp. Which rule validation proofs break when you re-activate that bug? -To get you started, the following proof shosws that the +To get you started, the following proof shows that the false elimination inference rule is valid in our logic. TEXT. -/ @@ -196,12 +196,12 @@ theorem false_elim : false_elim_rule X i := begin unfold false_elim_rule pEval, assume h, -cases h, -- contradiction, can't hppen, no cases! +cases h, -- contradiction, can't happen, no cases! -- Lean determines tt = ff is impossible end --- Define the remaning propositions and proofs here: +-- Define the remaining propositions and proofs here: end rule_validation -- section diff --git a/lean_source/A_01_Propositional_Logic/A_99_06_prop_logic_validation.old.lean b/lean_source/A_01_Propositional_Logic/A_99_06_prop_logic_validation.old.lean index ee8ee1e..5eaa06f 100644 --- a/lean_source/A_01_Propositional_Logic/A_99_06_prop_logic_validation.old.lean +++ b/lean_source/A_01_Propositional_Logic/A_99_06_prop_logic_validation.old.lean @@ -51,7 +51,7 @@ Algebraic Properties First, a propositional logic can be understood as an algebra over Boolean-valued terms, variables, and constants. Constants and variables are are terms, but terms can also be constructed from smaller terms using -connectives: ∧, ∨, ¬, and so on. The axioms of propopsitiona logic impose +connectives: ∧, ∨, ¬, and so on. The axioms of propositional logic impose constraints on how these operations behave, on their own and combined. The constraints are algebraic, just as the axioms are algebraic that @@ -91,7 +91,7 @@ and_commutes -- proof from last chapter As we've seen, mathematical theories are often augmented with concrete syntax / notations that make it practical for people to read and write -such mathemantics. +such mathematics. A standard notation for a "meaning-of-expression" operator is a pair of *denotation* or *Scoot* @@ -131,7 +131,7 @@ to be the same as function arguments. /- Observe: We can *apply* these theorems -to particular objects to specalize the +to particular objects to specialize the generalized statement to the particular objects. -/ diff --git a/lean_source/A_01_Propositional_Logic/A_99_ignore_this.lean b/lean_source/A_01_Propositional_Logic/A_99_ignore_this.lean index 4f030dc..1d7dbf5 100644 --- a/lean_source/A_01_Propositional_Logic/A_99_ignore_this.lean +++ b/lean_source/A_01_Propositional_Logic/A_99_ignore_this.lean @@ -45,7 +45,7 @@ which generate all and only the well formed formulae strings of in the language The strings are called the *well formed formulae* (or *wffs, -terms, or expressions*) of the language. The sematics of a +terms, or expressions*) of the language. The semantics of a formal language is as assignment of meanings to expressions. It is possible, in general, that only some expressions in a diff --git a/lean_source/A_02_Constructive_Logic/A_02_Propositions_as_Types.lean b/lean_source/A_02_Constructive_Logic/A_02_Propositions_as_Types.lean index 44a5ef7..bca4afc 100644 --- a/lean_source/A_02_Constructive_Logic/A_02_Propositions_as_Types.lean +++ b/lean_source/A_02_Constructive_Logic/A_02_Propositions_as_Types.lean @@ -17,7 +17,7 @@ propositional logic to provide a way to reason about the truth of given propositions. In this chapter, we will represent propositions as types of a special kind, instead, and proofs as values of these types. We will -then adopt exacty the same inference rules we saw in +then adopt exactly the same inference rules we saw in the last chapter, but generalized to this far more expressive logic. @@ -187,7 +187,7 @@ elements values of type Type 0 is itself a value of type Type 1. As a final comment, Lean allows one to generalize over these type universes. To do so you declare one or more *universe -variable* which you can then use in decaring types. Lean can +variable* which you can then use in declaring types. Lean can also infer universe levels. TEXT. -/ diff --git a/lean_source/A_02_Constructive_Logic/A_04_Inference_Rules.lean b/lean_source/A_02_Constructive_Logic/A_04_Inference_Rules.lean index 6c4c6ea..69e1c12 100644 --- a/lean_source/A_02_Constructive_Logic/A_04_Inference_Rules.lean +++ b/lean_source/A_02_Constructive_Logic/A_04_Inference_Rules.lean @@ -11,7 +11,7 @@ library of mathematical definitions. Your next major task is to know and understand these inference rules. For each connective, learn its related introduction (proof constructing) and elimination (proof -consuming) rules. Grasp the sense of each rule clerly. +consuming) rules. Grasp the sense of each rule clearly. And learn how to to compose them, e.g., in proof scripts, to produce proofs of more complex propositions. @@ -510,7 +510,7 @@ TEXT. -/ -- QUOTE: --- A proof of 0 = 0 by contradition +-- A proof of 0 = 0 by contradiction example : 0 = 0 := begin by_contradiction, -- applies ¬¬P → P @@ -559,7 +559,7 @@ that for any given proposition, P, there is a proof of P ∨ ¬P. This axiom then enables proof by contradiction. That's an easy proof. We need to prove that if *P ∨ ¬ P* then *¬¬P → P*. The -proof is by case analysis on an assumped proof of *P ∨ ¬ P*. +proof is by case analysis on an assumed proof of *P ∨ ¬ P*. In the first case, we assume a proof of P, so the implication is true trivially. In the case where we have a proof of ¬P, we have a contradiction between ¬P and ¬¬P, and so this case can't @@ -746,7 +746,7 @@ In this section you've encountered analogs in higher-order logic of the reasoning principles that you saw (in weaker forms) in propositional logic, but now as rules for and expressed in a -higher-order predicae logic itself embedded in +higher-order predicate logic itself embedded in the higher-order logic of Lean. Just as we ourselves specified an embedding diff --git a/lean_source/A_02_Constructive_Logic/A_99_ingore_this.lean b/lean_source/A_02_Constructive_Logic/A_99_ingore_this.lean index 15aa51c..ce203d2 100644 --- a/lean_source/A_02_Constructive_Logic/A_99_ingore_this.lean +++ b/lean_source/A_02_Constructive_Logic/A_99_ingore_this.lean @@ -18,7 +18,7 @@ You already have a reasonable intuitive grasp of the meanings of the connectives in propositional logic. Predicate logic uses the same connectives to compose given propositions into new ones, with the same basic -meanings. For example, we still have one introdcution +meanings. For example, we still have one introduction (construction) rule for ∧ and two elimination rules. Key differences, already discussed in class, are that @@ -30,7 +30,7 @@ terms of proof/type judgments rather than in terms of For example, instead of *P* and *Q* being of type *prop_expr*, we now have them being of type *Prop*. They are types that encode logical propositions. And -whereas the *and_intro* rule in proposital logic is +whereas the *and_intro* rule in propositional logic is (⟦P⟧ i = tt) → (⟦Q⟧ i = tt) → (⟦P ∧ Q⟧ i = tt), now it is *∀ (P Q : Prop), P → Q → and P Q*. ∧ is notation for *and.* diff --git a/lean_source/A_03_Recursive_Types/A_02_natural_numbers.lean b/lean_source/A_03_Recursive_Types/A_02_natural_numbers.lean index 221388c..302da08 100644 --- a/lean_source/A_03_Recursive_Types/A_02_natural_numbers.lean +++ b/lean_source/A_03_Recursive_Types/A_02_natural_numbers.lean @@ -131,7 +131,7 @@ def plus : nat → nat → nat #eval plus 3 4 -- multiplication adds the second argument --- to itself the first argumen number of times +-- to itself the first argument number of times def times : nat → nat → nat | 0 m := 0 | (n'+1) m := plus m (times n' m) @@ -140,7 +140,7 @@ def times : nat → nat → nat #eval times 1 20 --- substraction illustrates case analysis on +-- subtraction illustrates case analysis on -- multiple (here two) arguments at once def subtract : nat → nat → nat | 0 _ := 0 diff --git a/lean_source/A_03_Recursive_Types/A_03_polymorphic_lists.lean b/lean_source/A_03_Recursive_Types/A_03_polymorphic_lists.lean index 50dc2d1..5e74e5b 100644 --- a/lean_source/A_03_Recursive_Types/A_03_polymorphic_lists.lean +++ b/lean_source/A_03_Recursive_Types/A_03_polymorphic_lists.lean @@ -126,7 +126,7 @@ is empty. When we defined pred, above, we defined pred of zero to be zero (rather than to be undefined). Doing that makes the function total and easily represented as a function (lambda -abstractraction) in Lean. However, in a different application +abstraction) in Lean. However, in a different application we really might want to define pred 0 to be undefined, not 0. A similar set of issues arises when we consider head and @@ -183,7 +183,7 @@ fully to an empty list, in which case (3) no real result has to be specified to "prove the return type" because such a case can't happen. It would be a contradiction if it did, and so it can be dismissed as an impossibility. Magic: It *is* a total -function, but it can never be fully appied to an empty list +function, but it can never be fully applied to an empty list because a required proof argument, for *that* list, can never be given; so one can dismiss this case by false elimination, without having to give an actual proof of the conclusion. diff --git a/lean_source/A_03_Recursive_Types/A_04_higher_order_functions.lean b/lean_source/A_03_Recursive_Types/A_04_higher_order_functions.lean index 453ae52..f36b70f 100644 --- a/lean_source/A_03_Recursive_Types/A_04_higher_order_functions.lean +++ b/lean_source/A_03_Recursive_Types/A_04_higher_order_functions.lean @@ -333,14 +333,14 @@ The key roadblock will be that there's no way to do this using exactly the same code for, say, lists and options. So the kind of parametric polymorphism we've been using will no longer be enough. The answer will be found in a -different kind of polymorphism, *ad hoc* polynorphism, of +different kind of polymorphism, *ad hoc* polymorphism, of which *operator overloading* (as in C++) is an example. For instance, you can write complex number and string classes and overload the + operator in each class to do respective complex number addition and string append, but the implementations of these operations will hardly share the same code. Completely different implementations will -be needed, to be selected (by the compler in C++) based +be needed, to be selected (by the compiler in C++) based on the types of the arguments to which the + operator is applied. More on this topic later. TEXT. -/ @@ -351,7 +351,7 @@ Fold list: α → α → α -------------------- We now turn to a very different higher-order function -appliable to lists. It's called *fold* (or event better, +applicable to lists. It's called *fold* (or event better, *fold_right*) or *reduce*. Overview diff --git a/lean_source/A_03_Recursive_Types/A_05_recursive_proofs.lean b/lean_source/A_03_Recursive_Types/A_05_recursive_proofs.lean index b9a404f..87062f5 100644 --- a/lean_source/A_03_Recursive_Types/A_05_recursive_proofs.lean +++ b/lean_source/A_03_Recursive_Types/A_05_recursive_proofs.lean @@ -21,7 +21,7 @@ for smaller values of *a*, and (2) starting from proofs of The rest of this chapter will: -- provide a concrete and pecific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to *P*); +- provide a concrete and specific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to *P*); - see how the concept of an induction axiom generalizes to any inductively defined type, α; - introduce the concept of *inductive families* with recursive constructors; - introduce the idea of well founded recursion, meaning that a proof for every value of a type can be constructed starting with smallest values of the type. @@ -75,7 +75,7 @@ end -- QUOTE. /- TEXT: -The *simp* tactict tries to find, and if found applies, +The *simp* tactic tries to find, and if found applies, rules/axioms from the definition of the listed functions: here from just nat.add. We could have used *rfl* instead of *simp*, but writing the proof in this way emphasizes @@ -445,7 +445,7 @@ Induction Axiom for ℕ The principle we've developed is available as an axiom generated from the definition of the nat data type. The name of the principle is *nat.rec_on*. Applying it to the -smaller lemmas yeilds a proof of the generalization. +smaller lemmas yields a proof of the generalization. If you prove the lemmas first, in a bottom-up proof style, you can just apply the induction principle to a value, *a*, @@ -784,7 +784,7 @@ def nil_right_ident_append_list' {α : Type} : ∀ (l' : list α), list.append l Induction Axiom for Lists ~~~~~~~~~~~~~~~~~~~~~~~~~ -We see again that there's nothing myseterious about proof by induction. +We see again that there's nothing mysterious about proof by induction. If we have base values/proofs and step functions to build next-bigger ones, and we can have a function that (using recursion on these elements) computes a value/proof for any given input value, and thus for all values @@ -793,7 +793,7 @@ of the input type. Proof by induction is done by functions that compute results using recursion on given base values and step functions. Every inductive axiom can be understood as a proof of universal generalization that -asserts that every value of some input type has a corresponging result +asserts that every value of some input type has a corresponding result value of type. These return values can be proofs of properties or they can be function return values of any type. @@ -918,7 +918,7 @@ TEXT. -/ -- QUOTE: inductive le (n : nat): nat → Prop --- n is an implicit firt argument to each constructor +-- n is an implicit first argument to each constructor | refl : le (n) n | step : ∀ m, le (n) m → le (n) m.succ diff --git a/lean_source/A_03_Recursive_Types/A_99_ignore2.lean b/lean_source/A_03_Recursive_Types/A_99_ignore2.lean index 7ec24bc..a6d94c3 100644 --- a/lean_source/A_03_Recursive_Types/A_99_ignore2.lean +++ b/lean_source/A_03_Recursive_Types/A_99_ignore2.lean @@ -65,7 +65,7 @@ functions given as arguments, a higher-order function can also *return* function values. Suppose, for example, that you apply *apply_comp* to just two function values, without giving the third argument. The result is a new function, -which we can write as (g ∘ f), pronouned as *g after f*, +which we can write as (g ∘ f), pronounced as *g after f*, that takes an argument, *a*, and returns *g(f(a)).* As an exercise, let's write a version, *comp*, of @@ -212,7 +212,7 @@ fold The *fold* function, also often called *reduce*, takes a list, *l*, of values of some type, α, and reduces it to a single value of some type β. It is defined by case analysis on *l*. If *l* is -nil, fold needs to return an approriate result. For now, we will +nil, fold needs to return an appropriate result. For now, we will pass this "value for the base case" as an additional argument to fold. In the second, cases, where *l* is non-empty and thus of the form, *h::t,* fold returns the result obtained by applying diff --git a/lean_source/A_03_Recursive_Types/A_99_ignore3.lean b/lean_source/A_03_Recursive_Types/A_99_ignore3.lean index b15bba3..d9a2f35 100644 --- a/lean_source/A_03_Recursive_Types/A_99_ignore3.lean +++ b/lean_source/A_03_Recursive_Types/A_99_ignore3.lean @@ -28,7 +28,7 @@ is succ (0 + 0). *BE SURE YOU UNDERSTAND THIS STEP.* Now yy the first rule, 0 + 0 = 0, so we can rewrite succ (0 + 0) to just succ 0. With this expression on the left side, all -thatremains to prove is that succ 0 = succ 0, +that remains to prove is that succ 0 = succ 0, and this is true of course by the reflexivity of the equality relation. diff --git a/lean_source/A_03_Recursive_Types/A_99_saves_pbi.lean b/lean_source/A_03_Recursive_Types/A_99_saves_pbi.lean index 18cea6a..06b6158 100644 --- a/lean_source/A_03_Recursive_Types/A_99_saves_pbi.lean +++ b/lean_source/A_03_Recursive_Types/A_99_saves_pbi.lean @@ -5,7 +5,7 @@ define *le a* to the a *property* (one property for each *a*, making a family) of being less than or equal to a second ℕ, *b*. We then define constructors necessary and sufficient to build proofs of *a is less or equal to than b* whenever that -is mathemtically true. A *refl* constructor will produce a +is mathematically true. A *refl* constructor will produce a proof of *a is less than or equal to a* for any *a*, and a *step* constructor given any proof of *a ≤ b* will return a proof of *a ≤ b + 1*. Think about it. It works. @@ -53,7 +53,7 @@ define *le a* to the a *property* (one property for each *a*, making a family) of being less than or equal to a second ℕ, *b*. We then define constructors necessary and sufficient to build proofs of *a is less or equal to than b* whenever that -is mathemtically true. A *refl* constructor will produce a +is mathematically true. A *refl* constructor will produce a proof of *a is less than or equal to a* for any *a*, and a *step* constructor given any proof of *a ≤ b* will return a proof of *a ≤ b + 1*. Think about it. It works. @@ -122,7 +122,7 @@ to natural numbers in particular is often call proof by *mathematical* induction. In the next section of this chapter, we will stick with -the usual approach of introducting the general idea via +the usual approach of introducing the general idea via the special case of mathematical induction. In the next chapter after, we'll see proof by induction generalizes to all inductively defined types. It is a very general @@ -161,7 +161,7 @@ repeat { }, end --- dumb change of notation lema only +-- dumb change of notation lemma only lemma zero_ident_nat_add_notation : ∀ (a : ℕ), (a + 0 = a ∧ 0 + a = a) ↔ diff --git a/lean_source/A_04_Typeclasses/A_00_unit_title.lean b/lean_source/A_04_Typeclasses/A_00_unit_title.lean index 9db9e43..db8ace9 100644 --- a/lean_source/A_04_Typeclasses/A_00_unit_title.lean +++ b/lean_source/A_04_Typeclasses/A_00_unit_title.lean @@ -24,7 +24,7 @@ Key ideas include the following: (1) we will define a safe version of *foldr* that wil works for any monoid; we'll see how to associate monoid data (a binary operation, identity element, property proofs) with types, whose values are taken as monoid elements; (4) how to -tell Lean to automaticall (implicitly) find and pass monoid data +tell Lean to automatically (implicitly) find and pass monoid data structures to functions depending on the types of other arguments; (5) and ways to use this approach in useful ways. TEXT. -/ diff --git a/lean_source/A_04_Typeclasses/A_01_review.lean b/lean_source/A_04_Typeclasses/A_01_review.lean index dae13c3..29fcc75 100644 --- a/lean_source/A_04_Typeclasses/A_01_review.lean +++ b/lean_source/A_04_Typeclasses/A_01_review.lean @@ -43,7 +43,7 @@ Monoids so far We have so far defined one monoid type. It is a product type, which is to say that it has just constructor (mk), -with multiple argments, and can be thought of as defining +with multiple arguments, and can be thought of as defining an ordinary *record* type. We associate such records with element types, such as nat and list α, in order to extend them with additional monoid structure. Such structure is diff --git a/lean_source/A_04_Typeclasses/A_02_monoids.lean b/lean_source/A_04_Typeclasses/A_02_monoids.lean index bb27d59..976e4cc 100644 --- a/lean_source/A_04_Typeclasses/A_02_monoids.lean +++ b/lean_source/A_04_Typeclasses/A_02_monoids.lean @@ -21,7 +21,7 @@ binary operations of monoid objects. We can for example, define *+* as a notation for *op* in an additive monoid, such as ⟨list,++,[]⟩, and *\** as a notation for *op* in a multiplicative monoid, such as ⟨nat, *, 1⟩. We can then use -the *+* and *\** notations to denote whathever operators +the *+* and *\** notations to denote whatever operators are recorded in the *op* field of any given monoid object. For this to work (and for some other reasons) we'' define @@ -39,7 +39,7 @@ Sadly then, we'll also need two definitions of foldr, one that takes any additive monoid as an argument and one that takes a multiplicative monoid. The need to split definitions into additive and multiplicative is counter-intuitive to most -mathematicians but is forced by our type theory. In practce, +mathematicians but is forced by our type theory. In practice, Lean provides mechanisms for writing one definition and then cloning it automatically to produce the code for the other. TEXT. -/ @@ -82,7 +82,7 @@ a list of elements of some type α if and *only if* we have a definition of a monoid for α. For example, given what we've defined above, we can apply fold operation to lists of nat and lists of list, but not to list of bool, because we have -not yet defined a monoid (additive or muliplicative) for the +not yet defined a monoid (additive or multiplicative) for the bool type. In other words, to apply foldr to lists of elements of type, diff --git a/lean_source/A_05_Algebraic_Structures/A_01_monoids.lean b/lean_source/A_05_Algebraic_Structures/A_01_monoids.lean index da12333..8dc7eb0 100644 --- a/lean_source/A_05_Algebraic_Structures/A_01_monoids.lean +++ b/lean_source/A_05_Algebraic_Structures/A_01_monoids.lean @@ -15,10 +15,10 @@ As an exceptionally simple example, we'll define an instance of this concept where the elements of a multiplicative monoid are *rotations* of an equilateral triangle that leave its vertices pointing in the same direction as the original. We call such rotations *symmetries* -of an equilateral triange. +of an equilateral triangle. Think of such a triangle with a black dot marking the top vertex when -the triangle is in an un-rotated state. The symetries are rotations +the triangle is in an un-rotated state. The symmetries are rotations that leave the rotated triangle sitting right on top of where it was in its unrotated state. These are rotations by 0 degrees, which leaves the dot where it is; by 120 degrees, which rotates the dot by one @@ -230,7 +230,7 @@ mul_one_class instance To complete a typeclass instance for monoid, we also need an instance for mul_one_class, and as we'll now see, that in turn requires -instances of has_one and has_mul. We aready have an instance of has_mul, +instances of has_one and has_mul. We already have an instance of has_mul, so all we need to define now is has_one, which identities the identity element in the monoid, which will then be denoted by *1*. TEXT. -/ diff --git a/lean_source/A_05_Algebraic_Structures/A_02_groups.lean b/lean_source/A_05_Algebraic_Structures/A_02_groups.lean index 5785b49..309c0aa 100644 --- a/lean_source/A_05_Algebraic_Structures/A_02_groups.lean +++ b/lean_source/A_05_Algebraic_Structures/A_02_groups.lean @@ -75,7 +75,7 @@ action, of rotations on (representations of) equilateral triangles. A rotation of this kind rotates an equilateral triangle by -an amount that makes the resulting triang sit right on top +an amount that makes the resulting triangle sit right on top of the original equilateral triangle. These are rotations by 0, 120, and 240 degrees. There are no other rotational symmetries of such a triangle. diff --git a/lean_source/A_05_Algebraic_Structures/A_03_group_actions.lean b/lean_source/A_05_Algebraic_Structures/A_03_group_actions.lean index fa84a0e..faf1520 100644 --- a/lean_source/A_05_Algebraic_Structures/A_03_group_actions.lean +++ b/lean_source/A_05_Algebraic_Structures/A_03_group_actions.lean @@ -41,7 +41,7 @@ objects that group elements act on. To make the concept of a group action clearer, we'll develop it in the context of our running example of the rotational symmetries of equilateral triangles. What these actions act -on are equilaterial triangles. We'll overload an operation +on are equilateral triangles. We'll overload an operation called smul, introduced by the group_action typeclass, and denoted g • b to represent the result of applying the action g to the object b, with a result of the same type b has. As @@ -63,7 +63,7 @@ result of g acting on b. Lean provides this notation through instantiation of its group_action typeclass. In addition to this notation, this -typeclass requires verification of the two actioms of group +typeclass requires verification of the two axioms of group actions, namely that 1 • b = b, and that (g₁ \* g₂) • b = g₁ • (g₂ • b). diff --git a/lean_source/A_05_Algebraic_Structures/A_04_torsors.lean b/lean_source/A_05_Algebraic_Structures/A_04_torsors.lean index bf027ea..46284ca 100644 --- a/lean_source/A_05_Algebraic_Structures/A_04_torsors.lean +++ b/lean_source/A_05_Algebraic_Structures/A_04_torsors.lean @@ -244,7 +244,7 @@ instance : add_group rot := /- TEXT: -Next we formulate the action of a rotation on a triange. +Next we formulate the action of a rotation on a triangle. We do it in two steps, first adding a binary operation taking a rot and a tri and yielding a tri, with +ᵥ as notation; then we formally define an add_action and show @@ -519,5 +519,5 @@ To be sure that we've given modules their due, we will cross through them on our way to replacing the rot group in our example so far with a one dimensional vector space over a (coefficient) *field*, K. The corresponding point -torsor will then be the corresonding affine space. +torsor will then be the corresponding affine space. TEXT. -/ \ No newline at end of file diff --git a/lean_source/A_05_Algebraic_Structures/A_05_modules.lean b/lean_source/A_05_Algebraic_Structures/A_05_modules.lean index 78fc24f..792e41d 100644 --- a/lean_source/A_05_Algebraic_Structures/A_05_modules.lean +++ b/lean_source/A_05_Algebraic_Structures/A_05_modules.lean @@ -9,7 +9,7 @@ import data.int.basic Modules ******* -We've now undertood what it means to be a torsor over +We've now understood what it means to be a torsor over a group. A concrete example is our torsor of triangles over a group of rotational symmetries. That fact that rotational symmetries form an additive group lets us @@ -27,7 +27,7 @@ then s • v is scalar multiplication of s and v yielding a new, "scaled" group action. The set of scalars must form at least a *ring*, so you -can add, invert, substract, and multiply scalars by each +can add, invert, subtract, and multiply scalars by each other (+, -, *). For example, the integers for a ring: you can multiply, add, invert, and thus subtract them, but dividing them generally doesn't produce new integers. @@ -38,7 +38,7 @@ set of real numbers minus {0} forms a field. A module with a scalar *field* is called a vector space. The overall picture, then, is one in which, in a module, -you can not only add, invert, and substract actions, but +you can not only add, invert, and subtract actions, but you can also multiply (*scale*) them by scalars. Example: if v₁ and v₂ are group actions and s₁ and s₂ are scalars, then s₁ • (v1 +ᵥ v2) is also an action, s₁ • v₁ + s₁ • v₂; @@ -331,13 +331,13 @@ distrib_mul_action ℤ rot ~~~~~~~~~~~~~~~~~~~~~~~~ First we'll define s • m to mean rot_zpow s m. -In other workds, we'll define scalar multiplication +In other words, we'll define scalar multiplication integer s by rotation r to be: (1) for a non-negative s, the rotation *added* to itself that many times (already implemented by rot_zpow), and for a negative s by the additive inverse (negation) of that sum. The we'll need to prove that scaling a rotation b -by scalar (x * y) is the same as scalaing b first +by scalar (x * y) is the same as scaling b first by y then by x. With that we can define an instance, (mul_action ℤ rot). @@ -371,7 +371,7 @@ instance : mul_action ℤ rot := /- TEXT: With our (mul_action ℤ rot) defined we now put together -the final peices needed for (distrib_mul_action ℤ rot). +the final pieces needed for (distrib_mul_action ℤ rot). With this instance in hand, in the next subsection we instantiate (module ℤ rot), which was our aim: to have not just a group, but a *module*, of rotation actions: @@ -388,7 +388,7 @@ lemma rot_smul_zero : ∀ (a : ℤ), a • (0 : rot) = 0 := simp [rot_zpow], end --- scalaing a sum of rotations is the sum of the scalaed rotations +-- scaling a sum of rotations is the sum of the scaled rotations lemma rot_smul_add : ∀ (a : ℤ) (x y : rot), a • (x + y) = a • x + a • y := begin assume z x y, @@ -525,7 +525,7 @@ open tri -- scalar difference (a scalar) multiplied by rotation then acting on triangle #reduce (((3:ℤ) - (2:ℤ)) • r120) • t120 --- addition of scaled and unscaled vector, acting on a triange +-- addition of scaled and unscaled vector, acting on a triangle #reduce (((3:ℤ) • r120) +ᵥ r240) • t120 -- important: function subtracting points yielding a rot then acting on a triangle diff --git a/lean_source/A_05_Algebraic_Structures/A_06_vector_spaces.lean b/lean_source/A_05_Algebraic_Structures/A_06_vector_spaces.lean index 9b66ca1..6b723e0 100644 --- a/lean_source/A_05_Algebraic_Structures/A_06_vector_spaces.lean +++ b/lean_source/A_05_Algebraic_Structures/A_06_vector_spaces.lean @@ -135,7 +135,7 @@ relation to points (no distinguished origin), another to stand in relation to vectors, and yet a third to stand in relation to the scalars by which vectors can be multiplied. -Formlizing ℚ as a torsor over itself as a vector space is +Formalizing ℚ as a torsor over itself as a vector space is straightforward, requiring only proofs of the two torsor laws, where the values are all rationals. The proofs are in turn by straightforward simplification. @@ -161,7 +161,7 @@ instance : add_torsor ℚ ℚ := /- TEXT: We can now at least signal our abstract intent by using operations that reflect our intended interpretations of -their argment as points, vectors, or scalars. We can in +their argument as points, vectors, or scalars. We can in particular use -ᵥ to computes differences of points; +ᵥ to represent addition of a vector to a point; and • to represent scalar multiplication of a vector. diff --git a/lean_source/A_05_Algebraic_Structures/A_07_affine_spaces.lean b/lean_source/A_05_Algebraic_Structures/A_07_affine_spaces.lean index 756bb55..3e8f2d0 100644 --- a/lean_source/A_05_Algebraic_Structures/A_07_affine_spaces.lean +++ b/lean_source/A_05_Algebraic_Structures/A_07_affine_spaces.lean @@ -43,10 +43,10 @@ TEXT. -/ Generalizing over fields ------------------------ -To begin we'll set up our design to be gneral over scalar +To begin we'll set up our design to be general over scalar fields, from rational affine spaces to spaces over other fields, such as the real or complex numbers. We'll use the -identifer, *K*, to represent the scalar field type. In this +identifier, *K*, to represent the scalar field type. In this chapter we'll define *K := ℚ*, but by writing the rest of our definitions in terms of *K* we'll create the option to change the field type for an entire application by changing @@ -78,7 +78,7 @@ represent the duration (a vector), *2 hours*; the expression will represent the point halfway between *p1* and *p2*. In this design we'll represent points, vectors, and scalars -as rational numbers. To remind us of our intended intepretations +as rational numbers. To remind us of our intended interpretations of such numbers, we'll provide *lightweight abstractions* by defining *pnt*, *vec*, and *scl* as alternative names (type aliases) for the rational number type, ℚ. (Lean uses the name, @@ -115,7 +115,7 @@ to be associated with, and usually represented by (0:ℚ), every other point in the torsor can then be specified as (p +ᵥ v) for some vector, v, in the associated 1-dimensional vector space. -To see what can go wrong, suppose p is a point representedby the +To see what can go wrong, suppose p is a point represented by the rational 1/2 and v is a vector, literally a rational, namely 1/4. The expression v + p represents the point arrived at by translating p *in the direction and by the magnitude* of v. @@ -177,8 +177,7 @@ Points We will represent our 1-d space of points in time by rationals. We do not treat the rational number, 0, as being special. There is no distinguished origin in classical time. We will represent durations -as vector differences betwe -en such points. What can go wrong? +as vector differences between such points. What can go wrong? One approach is to define type, *pnt* (for "point"), as just another name for ℚ. In Lean this can be done using *abbreviation.* In this @@ -268,7 +267,7 @@ Vectors ~~~~~~~ Given that differences between points still have the type -of bare rationals, we can use our vector object whereever +of bare rationals, we can use our vector object wherever any rational is expected, and we can use any rational, no matter what it actually means, as a vector in our physical and geometric computations. That is not good enough. @@ -281,7 +280,7 @@ points. As an aside: Recall that Lean doesn't provide vector_space as a typeclass; rather one uses module with a scalar field -to acheive this result. So we will need to lift the module +to achieve this result. So we will need to lift the module structure from ℚ to our new *vec* (for vector) type. We will also need to lift add_comm_monoid and add_group structures for everything to work. Note how we do this by deriving from diff --git a/lean_source/A_05_Algebraic_Structures/A_08_product_spaces.lean b/lean_source/A_05_Algebraic_Structures/A_08_product_spaces.lean index 78939b3..53fd9c9 100644 --- a/lean_source/A_05_Algebraic_Structures/A_08_product_spaces.lean +++ b/lean_source/A_05_Algebraic_Structures/A_08_product_spaces.lean @@ -220,7 +220,7 @@ points. As an aside: Recall that Lean doesn't provide vector_space as a typeclass; rather one uses module with a scalar field -to acheive this result. So we will need to lift the module +to achieve this result. So we will need to lift the module structure from ℚ to our new *vec* (for vector) type. We will also need to lift add_comm_monoid and add_group structures for everything to work. Note how we do this by deriving from diff --git a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_key_1.lean b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_key_1.lean index 801122c..81ada48 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_key_1.lean +++ b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_key_1.lean @@ -78,7 +78,7 @@ has_inv and has_div An instance of the has_inv typeclass will have one field value, a total function from group elements to other group -elements. In the context of a group, it will be cosntrained +elements. In the context of a group, it will be constrained to behave as a genuine inverse operation must: that given an element, r, it will return an element r⁻¹, such that r⁻¹ * r = 1 (the group identity element). diff --git a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_old.lean b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_old.lean index 90dea8b..6453272 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_old.lean +++ b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_02_groups_old.lean @@ -74,7 +74,7 @@ action, of rotations on (representations of) equilateral triangles. A rotation of this kind rotates an equilateral triangle by -an amount that makes the resulting triang sit right on top +an amount that makes the resulting triangle sit right on top of the original equilateral triangle. These are rotations by 0, 120, and 240 degrees. There are no other rotational symmetries of such a triangle. @@ -95,7 +95,7 @@ typeclass for a new type, with three values, representing the set of symmetry rotations. We'll start top-down, with Lean's group typeclass, see what typeclasses it extends, and then construct the elements needed to instantiate all of these -typeclasses, finally assembing all of these pieces into a +typeclasses, finally assembling all of these pieces into a group typeclass instance for our set of rotation-representing group elements. @@ -179,7 +179,7 @@ in this way. /- TEXT: An instance of the has_inv typeclass will have one field value, a total function from group elements to other group -elements. In the context of a group, it will be cosntrained +elements. In the context of a group, it will be constrained to behave as a genuine inverse operation must: that given an element, r, it will return an element r⁻¹, such that r⁻¹ * r = 1 (the group identity element). @@ -304,7 +304,7 @@ div_inv_monoid Now we can turn to zpow. Its type is reported as ℤ → G → G, where, here, G = rot. If the argument, (z : ℤ), is not negative, we know how to recurse down from z to 0 in order to -iterate some operation; but what do we do with argumentss that +iterate some operation; but what do we do with arguments that are negative integers? More generally, how do we define a function to compute a result for any values of type integer? diff --git a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_05_modules.lean b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_05_modules.lean index 6e296cd..3fbe114 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_05_modules.lean +++ b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_05_modules.lean @@ -225,7 +225,7 @@ addition, subtraction, multiplication, and sometimes division *of pairs of scalars* with scalar multiplication by of scalars by monoid elements. -For exampe, it better be the case that (r₁ + r₂) • v = +For example, it better be the case that (r₁ + r₂) • v = (r₁ • v) + (r₂ • v). Be sure you see that the + on the left is addition of scalars, while the + on the right is addition of monoid elements (each obtained by scalar @@ -241,7 +241,7 @@ are headed here. The monoid structure gives us associative addition and an identity element. We then select a scalar ring or field and define the -scalar muliplication operation taking a scalar and a +scalar multiplication operation taking a scalar and a monoid element to another monoid element (just like multiplying a scalar and a vector yields a scaled vector). diff --git a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_99_cuts.txt b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_99_cuts.txt index 5e10350..79339d0 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_99_cuts.txt +++ b/lean_source/A_05_Algebraic_Structures/A_99_cuts/A_99_cuts.txt @@ -44,7 +44,7 @@ to any group in this way. /- TEXT: An instance of the has_inv typeclass will have one field value, a total function from group elements to other group -elements. In the context of a group, it will be cosntrained +elements. In the context of a group, it will be constrained to behave as a genuine inverse operation must: that given an element, r, it will return an element r⁻¹, such that r⁻¹ * r = 1 (the group identity element). @@ -114,7 +114,7 @@ example :r240 / r240 = 1 := rfl ======= Torsors What this means is we can do arithmetic on transformations -in the group--addition, substraction, and multiplication by +in the group--addition, subtraction, and multiplication by natural number constants (n-iterated addition) separately from the actions then apply the result, or we can apply all the separate transformations, and in either case we'll diff --git a/lean_source/A_05_Algebraic_Structures/A_99_nick.lean b/lean_source/A_05_Algebraic_Structures/A_99_nick.lean index 02c5b98..5f6b38e 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_nick.lean +++ b/lean_source/A_05_Algebraic_Structures/A_99_nick.lean @@ -101,7 +101,7 @@ variables (condition : bool_expr) /- -Here's a model of our app. Dooes it capture it (but for the outer loop)? +Here's a model of our app. Does it capture it (but for the outer loop)? -/ def md : app := seq @@ -123,13 +123,13 @@ Technical claim: ∃ (a : app), P a, where it seems that P could well be of interest to the community. The proof is constructive. That is, we present a witness along with a demonstration that the witness has the stated property. -The challege is to have a P that's new, interesting, and +The challenge is to have a P that's new, interesting, and useful. What is P? What such properties will our apps have that no others to our knowledge do? Explain at a technical but reasonably concise level each of the challenges (including what you need to know about -the particuar stack we used to see the specific problems +the particular stack we used to see the specific problems we found and for which we present a solution). The claim would be interesting only to the extent that the output is significantly novel in conception. The idea of "mere" diff --git a/lean_source/A_05_Algebraic_Structures/A_99_rings.lean b/lean_source/A_05_Algebraic_Structures/A_99_rings.lean index c5cd5fd..0f6997e 100644 --- a/lean_source/A_05_Algebraic_Structures/A_99_rings.lean +++ b/lean_source/A_05_Algebraic_Structures/A_99_rings.lean @@ -25,7 +25,7 @@ semiring is a single type with these additionalstructures. Without inverses, there is no division., but we do now have both (commutative) addition and (not necessarily -commutative) multipication of elements in a way that no +commutative) multiplication of elements in a way that no matter what those elements are obeys the distributive laws, both left and right. So arithmetic with addition and multiplication, identities, and n-times iterated addition diff --git a/lean_source/A_06_Dependent_Types/A_02_Pi_types.lean b/lean_source/A_06_Dependent_Types/A_02_Pi_types.lean index 21470f7..ff38764 100644 --- a/lean_source/A_06_Dependent_Types/A_02_Pi_types.lean +++ b/lean_source/A_06_Dependent_Types/A_02_Pi_types.lean @@ -46,7 +46,7 @@ Indexed Families ~~~~~~~~~~~~~~~~ Note that each *n* to to which one applies -*Q* gives rised to a proposition--a type--that +*Q* gives rise to a proposition--a type--that *is about* (and in this sense, depends on) *n*. Such a types is said to be a *dependent type*.