--- tags: chapman university --- # CPSC-298 Logic in Software Engineering (Lean) ![image](https://hackmd.io/_uploads/BkqF2Wi5a.png) This course is taught by Alexander Kurz ([email](mailto:akurz@chapman.edu)) in Spring 2024 and, while independent of, complements Jeff Turner's course [Using Large Language Models for Coding Assistance](https://github.com/jeffrey-l-turner/CPSC_298). On the surface, it may not be evident how these two courses play together, but Jeff and I designed both courses with common future developments in mind. Roughly speaking, the connection is that neural AI and symbolic AI are coming together in an emerging field called [neuro-symblic AI](https://en.wikipedia.org/wiki/Neuro-symbolic_AI). This is a one-unit course open to all students and has no prerequisites. In this course we will use the interactive theorem prover ***Lean*** to learn about logic in general and applications to software engineering in particular. The focus is on hands-on programming in Lean, but we will be able to glimpse at many advanced topics[^advanced] such as algebraic data types, $\lambda$-calculus, type systems, parsing, functional programming, higher-order functions, recursion (dynamic programming), specification vs implementation, proofs by induction, ... [^advanced]: See the Epilogue below for some links. Make sure to join the Discord if you want to follow the course. (This course ended now.) ## Summary In this course we will focus on learning from the online games available at the [Lean Game Server](https://adam.math.hhu.de/#/), in particular: - [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) - [A Lean Intro to Logic](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic) See the appendices below if you want to study Lean beyond of what is required for this introductory course. Under [Propositional Intutionistic Logic](https://hackmd.io/@alexhkurz/rkgaquGrR), I link the full formal summary of what we are going to learn in terms of rules of logical reasoning. ## Lecture 1 (Introduction) - Introduction to Interactive Theorem Proving. Neural and symbolic AI. <!--Example: [Baldur](https://arxiv.org/pdf/2303.04910.pdf). [^jeff]--> - [Natural Number Game (NNG)](https://adam.math.hhu.de/#/g/leanprover-community/NNG4) <!--[^hints]--> - Why successor numbers (no carrying, unbounded, induction, efficient for proofs, ...). - Getting started is a bit like learning assembly. [^assembly] - While working on the NNG make a list of all theorems. They will come in handy as the puzzles get more challenging. - **Homework:** How far in the Natural Number Game can everybody get? Make a list of what you learned. <!--https://hackmd.io/@alexhkurz/S12MmLiva--> - **Discord Rules for Homework**: - Announce when you complete a "world". - If you get stuck ask an interesting question. - Post interesting answers to interesting questions. Dont post spoilers. - (If you are unsure what is meant by "interesting", dont worry, we will figure this out as we go along.) - I dont have to give you a grade, but for getting a pass I expect you to participate actively. <!--[^hints]: I have some hints that I keep hidden for now. https://hackmd.io/@alexhkurz/HJ-LHqcDa--> [^assembly]: Btw, learning some assembly gives a much deeper understanding of how computers work. Similarly, learning low-level theorem proving teaches a lot about proofs. And, don't worry, we will be working our way up to higher levels. [^jeff]: This paper was recommended to me by Jeff Turner who teaches another CPSC 298 on the use of AI and large language models (LLMs) for coding. While not the focus of our independent courses, the intersection of the two courses (Logic and LLMs, symbolic AI and machine learning) is very interesting for future work. In fact, it is not a coincidence that we are teaching the two courses in the same semester. ## Lecture 2 (Natural Number Game) ### Why Theorem Proving Theorem proving can help answering the question "Is my program correct?" Take the following Python program that squares a number: ```python def square_number(x): return x * x ``` You will maybe test it for one or two inputs but not spend much time worrying about its correctness because you know that it must be correct. It is worth asking the question: How do you know that this program is correct? Because you have a proof of its correctness: The equation $x^2=x\cdot x$ is true. One aim of this course is to convince you that the idea of proving programs correct scales to much more complicated programs that are not obviously correct. ### Theorem Proving as a Search Problem Many common problems in programming can be understood as search problems. Think of finding your path out of a maze. You have a start state and a goal and you have to find a path from start to goal. You search your way out by guessing the next step and, possibly, backtracking if you feel like ending in a cul-de-sac. (Btw, what is a good way to do this in an actual maze? Have you heard of [Ariadne's thread](https://en.wikipedia.org/wiki/Ariadne%27s_thread_(logic))?) Refinements of this basic idea are at the heart of many algorithms, including those for theorem proving. ### Playing the NNG (Tutorial World) In theorem proving, guessing the next step that brings you closer to the goal is guessing the so-called "tactic" you want to use. When you work through the examples below, watch out how each time you apply a tactic the goal changes. **On the first level**, you only have to make one step by choosing the tactic ``` rfl ``` **On the second level**, you first substitute `y` by `x+7` using the tactic ``` rw [h] ``` where `rw` stands for "rewrite" and `h` is (a proof of) `y=x+7`. **On the third level** you use ``` rw [two_eq_succ_one] rw [one_eq_succ_zero] ``` to rewrite `2` as `succ 1` and then to rewrite `1` as `succ 0`. **On the fourth level** (which we didnt do in class) you learn how to rewrite an equation `X=Y` from right-to-left instead of from left-to-right (as we have done on the previous levels). ### Natural Numbers Going back to Level 3, to understand how natural numbers work, we should be asking the following question. What *are* natural numbers? We can find this out by clicking on the "N" symbol in ![image](https://hackmd.io/_uploads/H1qk75Wip.png =300x) which leads us to ![image](https://hackmd.io/_uploads/r1muz5-ia.png =300x) In English the bullet points tell us - `0` is a number - If `n` is a number then `succ n` is a number. Note that in some sense this is more powerful than the data type of numbers you have in a programming language. For example, in C, the datatype `int` has only finitely many elements whereas the datatype $\mathbb N$ has infinitely many elements since the rule of the second bullet point can be applied arbitrarily often. However big your number, you can always to $+1$ to get a bigger one. ### What About Negative Numbers? Good question. We can add negative numbers. Let us postpone this for now, though. ### Homework Continue with the NNG. ## Lecture 3 (Tutorial World, cont'd) The aim of this lecture was to get everybody to finish the Tutorial World. Next lecture we will finally get to induction in more detail. If you are still on the Tutorial World, finish it this week and do not hesitate to use the Discord to get you unstuck. In class, we talked in some detail about level 1/8 which asks you to prove ![image](https://hackmd.io/_uploads/HyLan55s6.png =200x) I write the proof out in mathematics style. Your task is then to figure out how to do this in Lean. \begin{align} 2+2 &= SSO + SSO & \text{ def of } 2\\ &= S(SSO + SO) & \text{ def of } + \\ &= SS(SSO + O) & \text{ def of } + \\ &= SSSSO & \text{ def of } + \\ &= SSS1 & \text{ def of } 1 \\ &= SS2 & \text{ def of } 2 \\ &= S3 & \text{ def of } 3 \\ &= 4 & \text{ def of } 4 \\ \end{align} In Lean, you program the proof above by using so-called tactics that name the steps in the right-hand column above. For example, to find the Lean syntax for the definitions of the numbers 1,2,3,4 use ![image](https://hackmd.io/_uploads/BkVQkjcip.png =200x) and for the definition of $+$ click on the "+" in ![image](https://hackmd.io/_uploads/SJov1sqop.png =200x) **Question:** This is a long proof for 2+2=4. What do we do if the numbers get larger? **Answer:** Induction. **Homework:** For next lecture: - Try to get as far as possible with the Addition World. - Ask an interesting question on Discord in the channel "w3-question" by the end of next Tuesday. Here are the rules: - An interesting question consists of two parts. The first part (typically one or two sentences) sets the scene. The second part (typically one sentence) asks the question. - An interesting question ideally both has some technical content and is open-ended. - An interesting question doesnt have a yes/no answer.  - A purely technical question that only aims to get you unstuck on a proof does not count as interesting[^interesting]. But you can take a technical problem as a lead towards an interesting question. This should be an open ended question on the topic of the class. Purely technical questions to help you get unstuck should go in the "general" channel. - All other questions are of course also welcome, but they should go on the channel "general". [^interesting]: Maybe I need to invent another term than "interesting" for what I want to express. ## Lecture 4 (Addition World) The aim of the lecture was to learn how to use mathematics as an intermediate language to go from English to Lean Tactics. ### Introduction I argued that the essence of programming is to describe infinitely many things by finitely many rules.[^geb] [^geb]: The technical term for this is *recursion*. If you want to learn more, I recommend the book [Goedel, Escher, Bach](https://www.physixfan.com/wp-content/files/GEBen.pdf). For example, a program that sorts lists of numbers is finite, but it can sort any list in the infinite set of all lists of numbers. Similarly, addition is finite but it allows us to add arbitrarily large numbers. In fact, addition is defined by two rules ``` add a 0 = a add a (S b) = S(add a b) ``` **Remark:** The aim of the course is to "teach" *machines* how to reason. Whatever the *model of computation* we use to define "machine", all a machine is able to do is to push symbols around. It is therefore worth looking at the two equations (rules) above from the point of view of symbol pushing: - The first rule says that `0` can be removed. - The second rule says that an "inner" `S` can be moved to the "outside". Note how powerful the second equation is. If you wanted to implement it via a symbol pushing model of computation it could get quite complicated. For example, given $SS0+SSSS0$, we might first need a for-loop to process the string from left to right in order to find the relevant $S$ in $SS0+{\bf S}SSS0$ and then we need another for-loop to move it out so that we end up with $\mathbf S(SS0+SSS0)$.[^ast] [^ast]: If you wonder what role the parentheses play in symbol pushing, the answer is that I think of symbol pushing as manipulating trees, not strings. This is called "abstract syntax" in programming. Ask me if you want to know more. ### Mathematics as a Programming Language I started with some general remarks on the stack of abstractions in computer science, mathematics and science more generally. The purpose of this lecture was to introduce an intermediary level of abstraction between a theorem and its implementation in Lean. In our example [(Level 1/5)](https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Addition/level/1), the question was how to go from ![image](https://hackmd.io/_uploads/SyLB8R7na.png =500x) to ```lean= induction n rw [add_zero] rfl rw [add_succ] rw [n_ih] rfl ``` The answer to the question is to write down the proof in mathematics first as follows. *Proof:* We prove $0+n=n$ for all $n\in\mathbb N$ by induction on $n$. Case $n=0$: \begin{align} 0+0 &= 0 & \text{add_zero} \end{align} Case $n=S\,k$: \begin{align} 0+ Sk &= S(0+k) & \text{add_succ}\\ &= Sk & \text{induction hypothesis}\\ \end{align} **Remark:** - The proof comes in two columns. On the left, we have a sequence of equation. On the right, we have a justification for each equation. - Writing math, you first write the equations and then the justification. - Translating the math to Lean, you use the right-hand column to name the tactics and Lean will construct the equations. **Homework:** - Go through the Lean proof and line it up against the math proof line by line. The Lean proof has more detail, but the same structure. - ***Choose a proof by induction on a level greater than 1/5 and post your math proof on Discord `w4-question` together with a question related to the topic of today.*** **Remark:** If you want to use my method for typesetting a math proof in [markdown](https://daringfireball.net/projects/markdown/) and [latex](https://www.latex-project.org/) make a (free afaik) account with https://hackmd.io . You can use the code for my math proof above as a template: ``` *Proof:* We prove $0+n=n$ for all $n\in\mathbb N$ by induction on $n$. Case $n=0$: \begin{align} 0+0 &= 0 & \text{add_zero} \end{align} Case $n=S\,k$: \begin{align} 0+ Sk &= S(0+k) & \text{add_succ}\\ &= Sk & \text{induction hypothesis}\\ \end{align} ``` The best way to learn how to adapt the above markdown/latex code for your own purposes is to experiment and talk to your favourite LLM. (Also ask on our Discord.) Here are some hints: - Markdown: `*` for italics, `**` for bold, backquotes for `code`. - Latex: - `$...$` for math - `$$...$$` for displayed math - `align` for equations, `&` for separating columns - `\in` for $\in$, `\mathbb N` for $\mathbb N$ Finally, you can take a screenshot of the proof in view mode and post it on Discord. ### Further Reading [Goedel, Escher, Bach](https://www.physixfan.com/wp-content/files/GEBen.pdf). ## Lecture 5 (Addition, cont'd) <!--[Answers to Week 4 Questions](https://hackmd.io/@alexhkurz/Hyjx2An2T)--> ## Lecture 6 (Logic) Guest lecture by Dr Jonathan Weiberger. The topic was the "$\wedge$ Tutorial" of [A Lean Intro to Logic](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic). ## Lecture 7 (Conjunction) In the lecture I gave some more general background connecting what we have done so far with what Jonathan had done in the last lecture. I spent some time on answering a question about what it means for a programming language to be [Turing complete](https://en.wikipedia.org/wiki/Turing_completeness). I also made a remark connecting while loops with induction. Another question we discussed was how to apply theorem proving to programming languages such as C which do not come equipped with a proof assistant. Finally, we went over Answers to Week 5 Questions <!--(https://hackmd.io/@alexhkurz/rkZojL1CT)-->, paying close attention to the idea of literate programming and to writing programs simultaneously in code and in math. ## Lecture 8 (Implication) We started the lecture by discussing the `w7-question`s on Discord. Then we started on the ["$\to$ Tutorial"](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/ImpIntro/level/0) in the logic game: ### Recap on the logic of "and" From the ["$\wedge$ Tutorial"](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic). The logic of and is about lists. If you have names for all elements of a list then a proof is just a nested list (the elements of which can again be lists) as in ![image](https://hackmd.io/_uploads/B1gldAWJA.png =500x) --- If you dont have names already, you can make them using `have` as in ![image](https://hackmd.io/_uploads/SJ8wdRWk0.png =500x) ### The logic of "and" and "implication" The ["$\to$ Tutorial"](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/ImpIntro/level/0) in the logic game. In class we completed Level 1<!--, see [here](https://hackmd.io/@alexhkurz/HkuitCZ1R) for solutions for the first three levels-->. We also talked about the so-called *Howard-Curry correspondence*: |Type Theory|Logic| |:---:|:---:| |Data Type | Proposition| |Program | Proof | **Homework:** (See also on Canvas) - Complete the implication world. - Post a proof in Lean and an interesting conceptual question on Discord. - Additional background material for an interesting question could be (but feel free to research your own) - Wikipedia: [Curry–Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) - Wikibooks: Haskell: [The Curry–Howard isomorphism](https://en.wikibooks.org/wiki/Haskell/The_Curry%E2%80%93Howard_isomorphism) - Richard Zach: [The Significance of the Curry-Howard Isomorphism](https://richardzach.org/wp-content/uploads/2019/11/Zach-2019-The-Significance-of-the-Curry-Howard-Isomorphism.pdf) - Stanford Encyclopedia of Philosophy: [The Development of Proof Theory](https://plato.stanford.edu/entries/proof-theory-development/) - Stanford Encyclopedia of Philosophy: [Type Theory](https://plato.stanford.edu/entries/type-theory/) ## Lecture 9 (Implication, cont'd) We continued with ["$\to$ Tutorial"](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/ImpIntro/level/0) in the logic game Recall the following about how to typeset math | math | source | |:---:|:---:| | $\lambda$ | `\lambda` | | $\mapsto$ | `\mapsto` | | $\langle$ | `\langle` | | $\rangle$ | `\rangle` | | $\wedge$ | `\and` or `\wedge`| Also note that applying a function `f` to an argument `x` is written `f x` with a space between `f` and `x`. <!--I added the solutions for the exercises we did in class [here](https://hackmd.io/@alexhkurz/HkuitCZ1R).--> ## Lecture 10 (Disjunction) We reviewed introduction and elimination rules for $\wedge$ and $\to$. ### Writing a Math Proof Here is a template how to write out ![image](https://hackmd.io/_uploads/HysrBwNeR.png =300x) in math style: > (1) Assume $(S\to C)\wedge(S\to D)$ > (2) $S\to C$ > (3) $S\to D$ > > (4) Assume $S$ > > (5) $C$ > > (6) $D$ > > (7) $C\wedge D$ > > (8) $S\to C\wedge D$ **Exercise:** Annotate each line in the proof above by the rule that is used to derive it. For example, line (5) is derived from lines (2) and (4) using $\to$-elimination (modus ponens). ### Or-Tutorial Then we started on the $\vee$-tutorial. Essentially, all you need to know are how to do the first three levels. --- ![image](https://hackmd.io/_uploads/BJ81ABVe0.png =300x) --- ![image](https://hackmd.io/_uploads/Hydb0r4gR.png =300x) --- ![image](https://hackmd.io/_uploads/r18KCSVg0.png =300x) --- From now on, everything in the $\vee$-tutorial is a combination of things we have seen before. See whether you can get through the rest of the $\vee$-tutorial now ... level 4 we did in class: ![image](https://hackmd.io/_uploads/S12RyUVe0.png =300x) Here is Level 4 in mathematics: > (1) Assume $C\vee O$ > > (2) Case $C$ > > (3) $O\vee C$ > >> (4) Case $O$ >> (5) $O\vee C$ > (6) $O\vee C$ For short proofs this notation looks a bit heavy (too much bureaucracy). But as proofs gets longer this way of structuring proofs becomes a powerful method. **Remark:** In the proof above, I write "Case" to label an assumption that arises from a disjunction ($C\vee O$ in this example). ## Lecture 11 (Parsing and Type Inference) In this lecture we took another look at the Level 4 proof above, both from a programming and from a math point of view. Specifically, we learned how Lean uses an algorithm for Type Inference to compute the math proof from the program. I go through this in detail again below. We start from the Lean program ```{haskell} exact or_elim h (λ c ↦ or_inr c) (λ o ↦ or_inl o) ``` **Exercise:** [Paste](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/OrIntro/level/4) this into Lean. This program doesn't show any types. We can put in all the types, if we want: ```{haskell} exact ( ( or_elim (h : C∨O) (λ c:C ↦ ((or_inr (c:C)):O∨C) : C→O∨C) (λ o:O ↦ ((or_inl (o:O)):O∨C) : O→O∨C) ) : O∨C ) ``` **Exercise:** [Paste](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/OrIntro/level/4) this into Lean. Remove the types and see whether you can put them back in again. **Remark:** We understand now why type inference is important. If we had to always write and read the types, both writing and reading would be too cumbersome. **Exercise:** (This requires some time and patience.) Now we have the Lean program annotated with all the types, can you match the Lean proof with the math proof? By now you should have some idea of how to obtain the math proof from Lean proof once the Lean proof has been annotated with all the types. But how does Lean compute the types? Short answer: Lean has a type inference algorithm. For the longer answer, it is worth making a quick detour and explain how to translate the string ```{haskell} or_elim h (λ c ↦ or_inr c) (λ o ↦ or_inl o) ``` into a tree (the so-called abstract syntax tree (AST)). The type inference algorithm does not work directly on the string, but rather on the AST. ### Excursion on Parsing In class we started with the example `1+2*3`. Does this compute to 7 or 9? Why? How many ways are there to put parentheses into the expression? One way to think about parsing is to put the parentheses back into an expression or program. A better way to think about parsing is as translating strings into trees. For example, the string ```{haskell} or_elim h (λ c ↦ or_inr c) (λ o ↦ or_inl o) ``` can be turned into a tree (where I indicate the tree structure using indentation) ```{haskell} or_elim h λ c or_inr c λ o or_inl o ``` **Exercise:** Write this [tree](https://en.wikipedia.org/wiki/Tree_(data_structure)) out using pen-and-paper connecting each parent to its children by drawing lines as in [this picture](https://en.wikipedia.org/wiki/Tree_(data_structure)#/media/File:Tree_(computer_science).svg). ### Type Inference We want to understand how to compute ```{haskell} exact ( ( or_elim (h : C∨O) (λ c:C ↦ ((or_inr (c:C)):O∨C) : C→O∨C) (λ o:O ↦ ((or_inl (o:O)):O∨C) : O→O∨C) ) : O∨C ) ``` from ```{haskell} or_elim h (λ c ↦ or_inr c) (λ o ↦ or_inl o) ``` using the AST ```{haskell} or_elim h λ c or_inr c λ o or_inl o ``` as the intermediate data structure. The information we have is the first line of the program 1. ![image](https://hackmd.io/_uploads/r1Vssi6lR.png =300x) and the type of `or_elim` (available by finding the button ![image](https://hackmd.io/_uploads/BJ--CpClA.png =50x) in the logic game) which is given as 2. ![image](https://hackmd.io/_uploads/HJyvZh6x0.png =400x) **Exercise:** - From 1. read off the type of `or_elim` at the root of the AST. - From 2. read off the type of `h` in the next line of the AST. - From 1. compute the type of `(λ c ↦ or_inr c)`. - From the previous item, compute the type of `c`. - From the previous item and the type of `or_inr` given by ![image](https://hackmd.io/_uploads/Bke7UhpeR.png =200x) compute the type of `or_inr c`. - Etc In class we went in detail through this and ended up with the following AST. Blue annotations refer to the symbols in 1. and green annotations refer to the symbols in 2. (I admit it takes some time and patience to puzzle this out.) ![image](https://hackmd.io/_uploads/HJ6Uwh6eA.png =400x) **Exercise:** Fill in the remaining question marks in the lower right of the picture. ## Lecture 12 (Intuitionistic Propositional Logic) Most of the lecture consisted in discussing parsing and type inference, but we also returned to proofs in the $\vee$-Tutorial. ### Parsing and Type Checking We discussed the questions on Discord on Parsing and Type Checking/Inference. I wrote a [note on parsing](https://hackmd.io/@alexhkurz/B1SazaUWA) on the example how parse trees explain the ambiguity of certain natural language sentences. ### Proofs in the $\vee$-Tutorial We did [Level 7 of the $\vee$-Tutorial](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/OrIntro/level/7): ![image](https://hackmd.io/_uploads/SkGSXzgfA.png =500x) Or, in math notation: **Theorem:** If $G\wedge (H\vee U)$ then $(G\wedge H)\vee (G\wedge U)$. Here is the math proof (let me know if that doesnt help to find the Lean proof): We assume that $G\wedge (H\vee U)$. > (2) $G$ > (3) $H\vee U$ > (4) Assume: $H$ >> (5) $G\wedge H$ >> > (6) $H\to G\wedge H$ > (7) $H\to (G\wedge H)\vee (G\wedge U)$ > > (8) Assume: $U$ > >> (9) $G\wedge U$ > > (10) $U\to G\wedge U$ > (11) $U\to (G\wedge H)\vee (G\wedge U)$ > (12) $(G\wedge H)\vee (G\wedge U)$ We have proved $(G\wedge H)\vee (G\wedge U)$ as required. **Exercise:** For each numbered line in the proof above, explain which rule was used to derive it. Here are some examples: >(2) follows by applying $\wedge$-elimination to $(G\wedge H)\vee (G\wedge U)$ >(6) follows from (4) and (5) using $\to$-introduction >(11) follows from (10) using $\vee$-introduction The complete list of rules available for the exercise is: ### Intuitionistic Propositional Logic #### $\wedge$-introduction $$ \frac{A\quad\quad B}{A\wedge B} $$ #### $\wedge$-elimination $$ \frac{A\wedge B}{A} \quad\quad\quad\quad \frac{A\wedge B}{B} $$ #### $\to$-introduction $$ \frac{\text{Assume $A$, prove $B$}}{A\to B} $$ #### $\to$-elimination $$ \frac{A \quad\quad A\to B}{B} $$ #### $\vee$-introduction $$ \frac{A}{A\vee B} \quad\quad\quad\quad \frac{B}{A\vee B} $$ #### $\vee$-elimination $$ \frac{A\vee B \quad\quad A\to C \quad\quad B\to C}{C} $$ ## Lecture 13 (Negation) We started with a general discussion about the difference of classical propositional logic, or Boolean logic as given by truth tables and the intuitionistic logic implemented in Lean and summarized by the introduction and elimination rules above. Then we started on the $\neg$-Tutorial, which adds negation to our logic. We write $\neg A$ as the formal notation for "not A". In the logic of Lean (intuitionistic logic), negation is defined via implication. $\neg A$ is $A\to \bot$ in math notation and `A -> False` in Lean notation. $\bot$ or `False` is a proposition that does not have a proof. In terms of the rules for Inutitionstic Propositional Logic from the previous section (Lecture 12), this simply means that there is no introduction rule for $\bot$ or `False`. The elimination rule is sometimes known as *[ex falso quod libet](https://en.wikipedia.org/wiki/Principle_of_explosion)*, that is, `False` implies any formula. #### $\neg$-elimination $$ \frac{\bot}{A} s$$ **Exercise/Activity:** Match up the rule of ex falso quodlibet with the truth table of implication. Here are the proofs we did in class for the first to levels of the $\neg$-Tutorial: ![image](https://hackmd.io/_uploads/B1IwJAWG0.png =400x) ![image](https://hackmd.io/_uploads/rybYyRZzR.png =400x) If you are wondering how to find the proofs, rewrite $\neg$ by $\to$ and use the knowledge from the previous tutorials: - For Level 1, `¬False` becomes `False → False`, which, like any $A\to A$ has `λ f ↦ f` as a proof (see [$\to$-Tutorial, Level 2](https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic/world/ImpIntro/level/2)). - For Level 2, the assumption `h` is of type `S → False`. We also have an element `s` of type `S`. Hence we can apply `h` to `s` writing `h s`. From checking the types we know that `h s` is of type `False`, so we can use `false_elim` to cast `h s` to type `B`. Now give levels 3 and 4 a try. I know negation is the most confusing connective, but if you remember to translate negation into implication you can get it to work. ## Lecture 14 (Negation, cont'd) In this lecture we look first again at negation. Then we connect what we have done this semester with related topics in computer science and software engineering (see the epilogue). ## Epilogue Looking back, this semester we have done a lot of "low level" coding. But how does this hang together with abstract and high level concepts in computer science and software engineering? Thanks to the Natural Number Game and the Lean Intro to Logic, we got some hands-on experience with a wide variety of important topics in theoretical computer science and software engineering. Each of this topics is a worthy topic of study in its own right. But if you come across these topics in the future, you will be able to use your knowledge of Lean to get yourself a good understanding. In the last lecture, I will briefly go throught the topics and links below and explain how they tie in what we have done in class this semester. - [algebraic data types](https://en.wikipedia.org/wiki/Algebraic_data_type#Programming_languages_with_algebraic_data_types) - [recursion (dynamic programming)](https://www.youtube.com/watch?v=oBt53YbR9Kk) - [$\lambda$-calculus](https://softwareengineering.stackexchange.com/a/260344) - [type systems](https://en.wikipedia.org/wiki/Type_system#Specialized_type_systems), [parsing](https://hackmd.io/@alexhkurz/B1SazaUWA) - [functional programming](https://www.turing.com/kb/introduction-to-functional-programming) - [higher-order functions](https://www.freecodecamp.org/news/higher-order-functions-in-javascript-explained/) - [specification vs implementation](https://www.youtube.com/watch?v=m8Icp_Cid5o) - [proofs by induction](https://web.stanford.edu/class/archive/cs/cs103/cs103.1246/lectures/12/), ... - [dependently typed programming](https://stackoverflow.com/a/9374698) - [Curry-Howard correspondence](https://cs.stackexchange.com/a/162116) - intuitionistic logic - proposition as types, proofs as programs - Martin-Lof type theory There are a lot of links on the WWW but I is not easy to find ones that discuss the big ideas in non-technical but interesting and precise way. **If you find links that help you understand these concepts better, please send them to me.** ## Appendix A: Running Lean Locally If you want to work more seriously with Lean, you should install Lean on your computer and program Lean using an editor. Here are the instructions in case you use VSCode as your editor. 1. In Vscode install the `lean4` extension. 2. Following https://lean-lang.org/lean4/doc/quickstart.html , in Vscode, clicking on the $\forall$-symbol, create a new standalone project: Click `New Project`, then `Project: Create Standalone Project`. 3. I am curious about [LeanDojo](https://leandojo.org/). I followed [steps 1 and 2](https://github.com/lean-dojo/LeanCopilot?tab=readme-ov-file#adding-lean-copilot-as-a-dependency) and then ``` lean --version # update lakefile.lean lake update LeanCopilot lake exe LeanCopilot/download lake build ``` but this is not needed for the NNG.[^infact] 4. You can have a look at [`Lean-Games`](https://codeberg.org/alexhkurz/Lean-Games#readme) to see how I implemented the beginnings of the natural number game. 5. Once you start working on a Lean-file in VSCode, do not forget `Infoview: Toggle Infoview` to view the messages of the interactive proof assistant. ## Appendix B: General Lean Resources Further Lean Resources: - Code and links to other resources: [Github](https://github.com/leanprover/lean4/blob/master/README.md) - Commmunity: [Zulip Chat](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members) - Search in the [mathlib](https://leanprover-community.github.io/mathlib4_docs/) library. Books: - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) - [The Mechanics of Proof](https://hrmacbeth.github.io/math2001/) - [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) - [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) - [Hitchhikers Guide to Logical Verification](https://github.com/blanchette/logical_verification_2021/raw/main/hitchhikers_guide.pdf), 2021 (Lean 3) [^infact]: In fact, LeanDojo didn't work for me. Maybe the reason is that for the NNG we define the natural numbers from scratch instead of using the Lean built-in numbers. Without LeanDojo, you can work with the `lakefile.lean` you get from 2. and bypass 3. See [this video](https://www.youtube.com/watch?v=qvaR_VXB4fA) for an introduction to LeanDojo. More info on the [homepage of Kaiyu Yang](https://yangky11.github.io/).