add a bunch of conceptual examples to start this great monday (#3)

Author: mia von steinkirch, phd

.github/.keep

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.github/workflows/lean_action_ci.yml

@@ -2,6 +2,7 @@
 /build/
 /.lake/
 /.elan/
+elan-init
 
 # editor and os files
 *.swp

.gitignore

@@ -0,0 +1,4 @@
+import src.Basics
+
+def main : IO Unit :=
+  IO.println s!"gm... testing... btw, double of 5 is {double 5}"

Main.lean

@@ -24,10 +24,22 @@ serve: check-lean
 update: check-lean
 	@lake update
 
+.PHONY: run-main
+run-main: check-lean
+	@lake run
+
 .PHONY: run-basics
 run-basics: check-lean
 	@lake env lean src/Basics.lean
 
 .PHONY: run-simple_proofs_I
 run-simple_proofs_I: check-lean
 	@lake env lean src/SimpleProofs_I.lean
+
+.PHONY: run-bt
+run-bt: check-lean
+	@lake env lean src/BinaryTree.lean
+
+.PHONY: run-tc
+run-tc: check-lean
+	@lake env lean src/TypeClasses.lean

Makefile

@@ -2,7 +2,7 @@
 
 <br>
 
-> *this repository contains examples and explanations as i learn lean 4 (a powerful theorem prover and programming language for the AI age)*
+> *this repository contains examples and explanations as i learn lean4 (a powerful theorem prover and programming language for the AI age)*
 
 <br>
 
@@ -35,166 +35,78 @@ lean --version
 lake --version
 ```
 
----
-
-### project structure
-
-<br>
-
-- `lakefile.lean`: the lean package manager configuration file
-- `src.lean`: the main entry point for the source code
-- `src/Basics.lean`: basic examples and concepts
-- `src/SimpleProofs_*.lean`: more advanced concepts and examples for proofs
-- `Makefile`
-
 <br>
 
 ---
 
-### basic concepts
+### documentation
 
 <br>
 
-#### types and functions
-
-lean has several basic types:
-- natural numbers (`Nat`): whole numbers starting from 0
-- booleans (`Bool`): true or false values
-- strings: text values
+- [basic concepts](docs/basic_concepts.md) - introduction to types, functions, and simple proofs in lean4
 
 <br>
 
-we start with simple examples to check types using `#check` and evaluate expressions using `#eval`:
+---
 
-```lean
-#check 43        -- shows the type of 43
-#eval 43 + 1     -- evaluates to 44
-#check true      -- shows the type of true
-#eval true && false  -- evaluates to false
-```
+### running
 
 <br>
 
-#### function definitions
-
-functions are defined using the `def` keyword. here's a simple example:
-
-```lean
-def double (n : Nat) : Nat := n + n
-```
-
-this defines a function that:
-- takes a natural number `n` as input
-- returns a natural number
-- doubles the input by adding it to itself
+#### project structure
 
 <br>
 
-#### simple proofs
-
-lean is primarily a theorem prover. here's a simple proof:
-
-```lean
-theorem double_add (n m : Nat) : double (n + m) = double n + double m := by
-  -- unfold the definition of double to work with the raw addition
-  unfold double
-
-  -- use Lean's simplifier with three key properties of natural number addition
-  -- 1. Nat.add_assoc: (a + b) + c = a + (b + c)  (associativity)
-  -- 2. Nat.add_comm: a + b = b + a              (commutativity)
-  -- 3. Nat.add_left_comm: a + (b + c) = b + (a + c)  (left commutativity)
-  simp only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
-```
+- `src.lean`: the main entry point for the source code
+- `Main.lean`: the main module file
+- `src/`: source code for examples and concepts
+- `Makefile`
+- `lakefile.lean`: the lean package manager configuration file (TODO: replace with `toml`)
+- `lake-manifest.json`: automatically generated dependency lock file
+- `lean-toolchain`: specifies the Lean version for the project
 
 <br>
 
----
-
-### running
+#### `make build`
 
 <br>
 
-run all `*.lean` files with:
+run all `src/*.lean` files with:
 
 ```shell
 make build
-
-info: src/Basics.lean:8:0: 43 : ℕ
-info: src/Basics.lean:9:0: 44
-info: src/Basics.lean:12:0: Bool.true : Bool
-info: src/Basics.lean:13:0: false
-info: src/Basics.lean:16:0: "gm, anon" : String
-info: src/Basics.lean:17:0: "gm, anon"
-info: src/Basics.lean:27:0: 666
-info: src/Basics.lean:32:0: true
-info: src/Basics.lean:33:0: false
-ℹ [2853/2855] Built src.SimpleProofs_I
-info: src/SimpleProofs_I.lean:21:0: 10
-info: src/SimpleProofs_I.lean:22:0: 0
-info: src/SimpleProofs_I.lean:23:0: 6
-info: src/SimpleProofs_I.lean:26:0: true
-info: src/SimpleProofs_I.lean:27:0: false
-info: src/SimpleProofs_I.lean:28:0: true
-info: src/SimpleProofs_I.lean:31:0: double_add (n m : ℕ) : double (n + m) = double n + double m
-info: src/SimpleProofs_I.lean:34:0: 14
-info: src/SimpleProofs_I.lean:35:0: 14
-Build completed successfully.
 ```
 
 <br>
 
-#### basic types and functions
+#### basic types, theorems, type classes...
 
 <br>
 
-run `Basics.lean` with:
+run any other file inside `src/` following its command inside `Makefile`. for instance, run `src/Basics.lean` with:
 
 ```shell
 make run-basic
-
-43 : ℕ
-44
-Bool.true : Bool
-false
-"gm, anon" : String
-"gm, anon"
-666
-true
-false
 ```
 
 <br>
 
----
-
-#### theorem to prove that doubling the sum of two numbers is the same as adding their double
-
-<br>
-
-run `SimpleProofs_I.lean` with:
 
-```shell
-make run-simple_proofs_I
-
-10
-0
-6
-true
-false
-true
-double_add (n m : Nat) : double (n + m) = double n + double m
-14
-14
-```
+----
 
+### study resources
 
 <br>
 
-----
+#### learning lean
 
-### resources
+- [learn lean](https://lean-lang.org/documentation/0)
+- [lean4 documentation](https://leanprover.github.io/lean4/doc/)
+- [vscode/cursor plugin](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4)
 
 <br>
 
-- [lean 4 documentation](https://leanprover.github.io/lean4/doc/)
-- [lean 4 manual](https://leanprover.github.io/lean4/doc/)
+#### applied examples
+
+- [AI safety via debate, by g. irving et al (2018)](https://arxiv.org/pdf/1805.00899)
+    - *"in the debate game, it is harder to lie than to refute a lie."*

README.md

@@ -0,0 +1,28 @@
+## basic concepts
+
+<br>
+
+---
+
+### types and functions
+
+<br>
+
+* there are two primary concepts in lean: functions and types
+* basic types examples are natural numbers (`Nat`, whole numbers starting from 0), booleans (`Bool`), true or false values, strings
+* check types using `#check`
+* evaluate expressions using `#eval`
+
+<br>
+
+---
+
+### function definitions
+
+<br>
+
+* functions are defined using the `def` keyword:
+
+```lean
+def double (n : Nat) : Nat := n + n
+```

docs/basic_concepts.md

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e6f52a442b52ac7fddcb4ae4818e1751c6efd3c9",
+   "rev": "8744850cc139c0d23086fdabad638f970a983bce",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

elan-init

@@ -11,4 +11,8 @@ require mathlib from git
 @[default_target]
 lean_lib «src» {
   -- add library configuration options here
+}
+
+lean_exe Main {
+  root := `Main
 }