first commit

.devcontainer/Dockerfile

@@ -0,0 +1,8 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -0,0 +1,15 @@
+{
+  "name": "LeanInRome dev container",
+
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+
+  "onCreateCommand": "echo \"Downloading the Lean 4 mathematical library...\" && lake exe cache get && lake build +LeanInRome.Common && echo \"Finished setup! Open a file using the Explorer in the top-left of your screen.\"",
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [ "leanprover.lean4" ]
+    }
+  }
+}

.docker/gitpod/Dockerfile

@@ -0,0 +1,37 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM ubuntu:jammy
+
+USER root
+
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.gitignore

@@ -0,0 +1,11 @@
+/build
+/lake-packages
+/.lake
+/.cache
+.DS_Store
+/lakefile.olean
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.synctex.gz

.gitpod.yml

@@ -0,0 +1,9 @@
+image:
+  file: .docker/gitpod/Dockerfile
+
+vscode:
+  extensions:
+    - leanprover.lean4
+
+tasks:
+  - init: lake exe cache get && lake build +LeanInRome.Common

.vscode/extensions.json

@@ -0,0 +1,13 @@
+{
+	// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
+	// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
+
+	// List of extensions which should be recommended for users of this workspace.
+	"recommendations": [
+		"leanprover.lean4"
+	],
+	// List of extensions recommended by VS Code that should not be recommended for users of this workspace.
+	"unwantedRecommendations": [
+		"ms-vscode-remote.remote-containers"
+	]
+}

.vscode/settings.json

@@ -0,0 +1,38 @@
+{
+    "files.exclude": {
+        "**/.git": true,
+        // "**/.DS_Store": true,
+        // "**/*.olean": true,
+        // "**/.DS_yml": true,
+        // "**/.gitpod.yml": true,
+        // "**/.vscode": true,
+	// ".docker": true,
+	// "build": true,
+	// "html": true,
+	// "lake-packages": true,
+	// ".gitignore": true,
+	// "lake-manifest.json": true,
+	// "lakefile.lean": true,
+    // "LeanInRome.lean": true,
+	// "lean-toolchain": true,
+	// "mathematics_in_lean.pdf": true,
+	// "MIL.lean": true,
+    // "LICENSE":true,
+    // ".devcontainer":true,
+    // "lean-tactics.tex":true,
+    },
+    "editor.minimap.enabled": false,
+    "editor.acceptSuggestionOnEnter": "off",
+    "scm.diffDecorationsGutterVisibility": "hover",
+    "editor.semanticHighlighting.enabled": true,
+    "editor.semanticTokenColorCustomizations": {
+        "[Default Light+]": {"rules": {"variable": "#1a31da"}}
+    },
+    "editor.unicodeHighlight.nonBasicASCII": false,
+    "editor.unicodeHighlight.ambiguousCharacters": false,
+    "editor.fontLigatures": true,
+    "files.trimTrailingWhitespace": true,
+    "files.trimFinalNewlines": true,
+    "lean4.infoview.emphasizeFirstGoal": true,
+    "lean4.infoview.showExpectedType": false
+}

LeanInRome.lean

@@ -0,0 +1 @@
+import LeanInRome.Test

LeanInRome/Common.lean

@@ -0,0 +1,116 @@
+import Mathlib.Tactic
+
+-- don't edit this file!
+
+set_option warningAsError false
+
+section
+open Lean Parser Tactic
+
+macro (name := ring) "ring" : tactic =>
+  `(tactic| first | ring1 | ring_nf)
+
+macro (name := ring_at) "ring" cfg:config ? loc:location : tactic =>
+  `(tactic| ring_nf $cfg ? $loc)
+
+end
+
+section delab
+
+section existential
+open Lean Parser Term PrettyPrinter Delaborator
+
+/-- Delaborator for existential quantifier, including extended binders. -/
+-- TODO: reduce the duplication in this code
+@[delab app.Exists]
+def exists_delab' : Delab := whenPPOption Lean.getPPNotation do
+  let #[ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(∃ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(∃ ($x:ident : $dom), $body)
+      else
+        `(∃ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(∃ $i:ident, $j:ident ∈ $s ∧ $body)
+    | `(∃ ($i:ident : $_), $j:ident ∈ $s ∧ $body) =>
+      if i == j then `(∃ $i:ident ∈ $s, $body) else pure stx
+    | `(∃ $x:ident, $y:ident > $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident > $z ∧ $body) =>
+      if x == y then `(∃ $x:ident > $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident < $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident < $z ∧ $body) =>
+      if x == y then `(∃ $x:ident < $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ≥ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ≥ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ≥ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ≤ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ≤ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ≤ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ∉ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ∉ $z ∧ $body) => do
+      if x == y then `(∃ $x:ident ∉ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊆ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊆ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊆ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊂ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊂ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊂ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊇ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊇ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊇ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊃ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊃ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊃ $z, $body) else pure stx
+    | _ => pure stx
+  match stx with
+  | `(∃ $group:bracketedExplicitBinders, ∃ $[$groups:bracketedExplicitBinders]*, $body) =>
+    `(∃ $group $groups*, $body)
+  | `(∃ $b:binderIdent, ∃ $[$bs:binderIdent]*, $body) => `(∃ $b:binderIdent $[$bs]*, $body)
+  | _ => pure stx
+end existential
+
+end delab
+
+namespace Nat
+open Lean Elab Term Meta
+
+def elabIdentFactorial : TermElab := fun stx expectedType? =>
+  match stx with
+  | `($name:ident) => do
+    let name := name.getId
+    if name.hasMacroScopes then
+      -- I think this would mean the name appears from within a quote.
+      -- I'm not sure how to properly deal with this, and it seems ok to just not.
+      throwUnsupportedSyntax
+    else
+      try
+        elabIdent stx expectedType?
+      catch e =>
+        match name with
+        | .str n s =>
+          if s.endsWith "!" then
+            let name' := Name.str n (s.dropRight 1)
+            try
+              elabTerm (← `(Nat.factorial $(mkIdent name'))) expectedType?
+            catch _ =>
+              throw e
+          else
+            throw e
+        | _ => throw e
+  | _ => throwUnsupportedSyntax
+
+attribute [scoped term_elab ident] elabIdentFactorial
+
+end Nat

LeanInRome/Test.lean

@@ -0,0 +1,7 @@
+import Mathlib.Tactic
+
+/- This is a test file. Lean is configured correctly if you see the output "32" when
+  mousing over or clicking on the next line, and you see no other errors in this file. -/
+#eval 2 ^ 5
+
+example (x : ℝ) : x - x = 0 := by simp

README.md

@@ -0,0 +1,83 @@
+# Computer-verified proofs: 48 hours in Rome
+
+24-26 January 2024
+
+## In this repository
+
+You will find the Lean files in the `LeanInRome` directory:
+* The `Lectures` folder contains all lectures
+* The `Assignments` folder contains the assignments that you have to hand in via eCampus
+* The `MIL` folder contains the exercises from the book Mathematics in Lean (so that you don't have to separately clone the `mathematics_in_lean` repository). You can find the textbook online here:
+[Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/)
+(or as a
+[pdf document](https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf)).
+
+## Installation
+
+Note: To get this repository, you will need to download Lean's mathematical library, which takes about 5 GB of storage space.
+
+* You have to install Lean, and two supporting programs: Git and VSCode. Follow these [instructions](https://leanprover-community.github.io/get_started.html) to do this. You do not have to follow the last step (creating Lean projects). Instead, we follow the next steps to set up this repository.
+
+* Open a terminal (I recommend `git bash` on Windows, which was installed as part of git in the first step).
+
+* Use `cd` to navigate to a directory where you would like to create the `LeanInRome` folder.
+
+* Run `git clone https://github.com/fpvandoorn/LeanInRome.git`.
+
+* Run `cd LeanInRome`
+
+* Run `lake exe cache get!`
+  * On Windows, if you get an error that starts with `curl: (35) schannel: next InitializeSecurityContext failed` it is probably your antivirus program that doesn't like that we're downloading many files. The easiest solution is to temporarily disable your antivirus program.
+
+* Launch VS Code, either through your application menu or by typing
+  `code .` (note the dot!). (MacOS users need to take a one-off
+  [extra step](https://code.visualstudio.com/docs/setup/mac#_launching-from-the-command-line)
+   to be able to launch VS Code from the command line.)
+
+* If you launched VS Code from a menu, on the main screen, or in the File menu,
+  click "Open folder" (just "Open" on a Mac), and choose the folder
+  `LeanInRome` (*not* one of its subfolders).
+
+* Test that everything is working by opening `LeanInRome/Test.lean`.
+  It is normal if it takes 10-40 seconds for Lean to start up.
+
+* More files will be added to this repository during the tutorial. The first exercises are in `LeanInRome/MIL/C02_Basics/S01_Calculating.lean`.
+
+### Update the repository
+
+If you have already followed the steps above, and want to update the repository, open a terminal in your local copy of this repository (e.g. `cd LeanInRome`) and then run `git pull`. This gives you the new exercises.
+
+## Altenative ways to use Lean
+
+You can use Codespaces or Gitpod if you have trouble installing Lean locally. These work fine, but not as well as a locally installed copy of Lean.
+
+### Using Codespaces
+
+You can temporarily play with Lean using Github codespaces. This requires a Github account, and you can only use it for a limited amount of time each month. If you are signed in to Github, click here:
+
+<a href='https://codespaces.new/fpvandoorn/LeanInRome' target="_blank" rel="noreferrer noopener"><img src='https://github.com/codespaces/badge.svg' alt='Open in GitHub Codespaces' style='max-width: 100%;'></a>
+
+* Make sure the Machine type is `4-core`, and then press `Create codespace`
+* After 1-2 minutes you see a VSCode window in your browser. However, it is still busily downloading mathlib in the background, so give it another few minutes (5 to be safe) and then open a `.lean` file to start.
+
+### Using Gitpod
+
+Gitpod is an alternative to codespaces that is slightly inconvenient, since it requires you to verify your phone number.
+
+Click this button to get started:
+
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/fpvandoorn/LeanInRome)
+
+This creates a virtual machine in the cloud,
+and installs Lean and Mathlib.
+It then presents you with a VS Code window, running in a virtual
+copy of the repository.
+You can update the repository by opening a terminal in the browser
+and typing `git pull` followed by `lake exe cache get!` as above.
+
+Gitpod gives you 50 free hours every month.
+When you are done working, choose `Stop workspace` from the menu on the left.
+The workspace should also stop automatically
+30 minutes after the last interaction or 3 minutes after closing the tab.
+
+To restart a previous workspace, go to [https://gitpod.io/workspaces/](https://gitpod.io/workspaces/).