Skip to content

Commit

Permalink
add missing mathlib demo files
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Apr 26, 2024
1 parent b68db8f commit ef7a037
Show file tree
Hide file tree
Showing 9 changed files with 192 additions and 0 deletions.
8 changes: 8 additions & 0 deletions Projects/mathlib-demo/MathlibLatest.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
import Webeditor
import Mathlib
import ProofWidgets

import MathlibLatest.Bijection
import MathlibLatest.Logic
import MathlibLatest.Rational
import MathlibLatest.Ring
25 changes: 25 additions & 0 deletions Projects/mathlib-demo/MathlibLatest/Bijection.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
import Mathlib.Logic.Equiv.Basic -- import the theory
-- of bijections as functions with two-sided inverses

-- Let X, Y and Z be sets
variable (X Y Z : Type)

-- Then there's a bijection between functions `X × Y → Z`
-- and functions from `X` to (the space of functions from `Y` to `Z`).

example : (X × Y → Z) ≃ (X → (Y → Z)) :=
{ -- to go from f : X × Y → Z to a function X → (Y → Z),
-- send x and y to f(x,y)
toFun := fun f ↦ (fun x y ↦ f (x,y))
-- to go from g : X → (Y → Z) to a function X × Y → Z,
-- send a pair p=(x,y) to (g p.1) (p.2) where p.i is the i'th element of p
invFun := fun g ↦ (fun p ↦ g p.1 p.2)
-- Here we prove that if f ↦ g ↦ f' then f' = f
left_inv := by
intro f -- let f : X × Y → Z be arbitrary.
rfl -- turns out f' = f by definition
-- here we prove that if g ↦ f ↦ g' then g' = g
right_inv := by
intro g -- let f : X → (Y → Z) by arbitrary
rfl -- turns out that g' = g by definition
}
15 changes: 15 additions & 0 deletions Projects/mathlib-demo/MathlibLatest/Logic.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
import Mathlib.Logic.Basic -- basic facts in logic
-- theorems in Lean's mathematics library

-- Let P and Q be true-false statements
variable (P Q : Prop)

-- The following is a basic result in logic
example : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q := by
-- its proof is already in Lean's mathematics library
exact not_and_or

-- Here is another basic result in logic
example : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by
apply? -- we can search for the proof in the library
-- we can also replace `apply?` with its output
16 changes: 16 additions & 0 deletions Projects/mathlib-demo/MathlibLatest/Rational.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
import Mathlib.Data.Rat.Order -- import the rationals
import Mathlib.Data.Rat.Init -- import notation ℚ for rationals
import Mathlib.Tactic.Linarith -- a linear arithmetic tactic
import Mathlib.Tactic.Ring -- import the `ring` tactic

-- let `x`, `y` and `z` be rationals
variable (x y z : ℚ)

-- let's prove that if `x < y` and `y + 3 < z + 10` then `x + 37 < z + 44`
example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by
linarith -- the `linarith` tactic can do this automatically

-- let's prove that (x+y)^2=x^2+2*x*y+y^2

example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
ring -- the `ring` tactic can do this automatically
13 changes: 13 additions & 0 deletions Projects/mathlib-demo/MathlibLatest/Ring.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import Mathlib.Tactic.Ring -- import the `ring` tactic

-- let R be a commutative ring (for example the real numbers)
variable (R : Type) [CommRing R]

-- let x and y be elements of R
variable (x y : R)

-- then (x+y)*(x+2y)=x^2+3xy+2y^2

example : (x+y)*(x+2*y)=x^2+3*x*y+2*y^2 := by
-- the `ring` tactic solves this goal automatically
ring
20 changes: 20 additions & 0 deletions Projects/mathlib-demo/build.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
#!/usr/bin/env bash

# Operate in the directory where this file is located
cd $(dirname $0)

# Updating Mathlib: We follow the instructions at
# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

# Note: we had once problems with the `lake-manifest` when a new dependency got added
# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem.

# currently the mathlib post-update-hook is not good enough to update the lean-toolchain.
# things break if the new lakefile is not valid in the old lean version
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

# note: mathlib has now a post-update hook that modifies the `lean-toolchain`
# and calls `lake exe cache get`.

lake update -R
lake build
77 changes: 77 additions & 0 deletions Projects/mathlib-demo/lake-manifest.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
{"version": 7,
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
"rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.30",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4",
"type": "git",
"subDir": null,
"rev": "61ad21e8d0386579b09dc2ecc8f34dc46877d02a",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/hhu-adam/lean4web-tools.git",
"type": "git",
"subDir": null,
"rev": "9e6468e250c05450eedf4aff6e30290fb409af2b",
"name": "webeditor",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "mathlibLatest",
"lakeDir": ".lake"}
17 changes: 17 additions & 0 deletions Projects/mathlib-demo/lakefile.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
import Lake
open Lake DSL

require mathlib from git
"https://github.com/leanprover-community/mathlib4"@"master"

require webeditor from git
"https://github.com/hhu-adam/lean4web-tools.git" @ "main"

package mathlibLatest {
-- add package configuration options here
}

@[default_target]
lean_lib MathlibLatest {
-- add library configuration options here
}
1 change: 1 addition & 0 deletions Projects/mathlib-demo/lean-toolchain
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
leanprover/lean4:v4.7.0

0 comments on commit ef7a037

Please sign in to comment.