Skip to content

Instantly share code, notes, and snippets.

View PatrickMassot's full-sized avatar

Patrick Massot PatrickMassot

View GitHub Profile
@PatrickMassot
PatrickMassot / extends_product.lean
Created April 27, 2018 08:45
Class extension example
/- The goal of this file is to explain why it's important that using extends in
command `class foo extends bar` creates a `foo.to_bar` function with an
instance implicit parameter.
We will define magmas with law denoted by ◆ and a commutative version.
Then we want products of such things. The goal is to reuse the work on product
magmas when defining product commutative magmas, and do so in a completely
transparent way. -/
-- Defining magmas with some notation is already covered in TPIL
@PatrickMassot
PatrickMassot / simplicial_set.lean
Created May 28, 2018 14:56
Johan's simplicial set cleanup
import order.basic .simplex_category data.finset data.finsupp algebra.group
local notation ` [`n`] ` := fin (n+1)
/-- Simplicial set -/
class simplicial_set :=
(objs : Π n : ℕ, Type*)
(maps {m n : ℕ} {f : [m] → [n]} (hf : monotone f) : objs n → objs m)
(comp {l m n : ℕ} {f : [l] → [m]} {g : [m] → [n]} (hf : monotone f) (hg : monotone g) :
(maps hf) ∘ (maps hg) = (maps (monotone_comp hf hg)))
@PatrickMassot
PatrickMassot / subtypes.lean
Created July 19, 2018 09:55
refine_struct for subtypes
import algebra.ring
import group_theory.submonoid
import tactic.interactive
namespace tactic
open tactic.interactive
meta def derive_field_subtype : tactic unit :=
do b ← target >>= is_prop,
@PatrickMassot
PatrickMassot / quotient_top_grop.lean
Last active October 4, 2018 07:06
Quotient additive commutative topological group
import analysis.topology.topological_structures
import group_theory.quotient_group
open function set
variables {α : Type*} [topological_space α] {β : Type*} [topological_space β]
variables {γ : Type*} [topological_space γ] {δ : Type*} [topological_space δ]
def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)
/-
This file defines the I-adic topology on a commutative ring R with ideal I.
The ring is wrapped in `adic_ring I := R`, which then receive all relevant type classes.
The end-product is `instance : topological_ring (adic_ring I)`.
-/
import tactic.ring
import data.pnat
import ring_theory.ideal_operations
@PatrickMassot
PatrickMassot / tasks.py
Last active January 25, 2019 10:25
Debian package builder for Lean
import tempfile
from pathlib import Path
from invoke import task
LEAN_CONTROL="""Package: lean
Version: {}
Section: math
Priority: optional
Architecture: amd64
Depends: git (>= 1.2)
@PatrickMassot
PatrickMassot / pratt.lean
Created January 25, 2019 09:42
Logic puzzle from John P. Pratt in Lean (starts at line 38)
import tactic.interactive
import tactic.linarith
@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith
constant only_child : people → Prop
constant salary : people → ℕ
@[derive decidable_eq]
@PatrickMassot
PatrickMassot / lean.json
Created February 12, 2019 13:13
VScode user code snippets for Lean
{
"Type*": {
"prefix": "Type*",
"body": [
"{$1 : Type*}$0"
],
"description": "Type* variable",
},
"Variables": {
"prefix": "var",
@PatrickMassot
PatrickMassot / push_neg.lean
Last active March 25, 2019 23:11
A tactic pushing negations inwards while keeping names
import tactic.interactive
import algebra.order
open tactic expr
namespace push_neg
section
@PatrickMassot
PatrickMassot / proof_tutorial.lean
Last active November 16, 2023 01:13
First proofs in Lean
/-
This file is intended for Lean beginners. The goal is to demonstrate what it feels like to prove
things using Lean and mathlib. Complicated definitions and theory building are not covered.
-/
-- We want real numbers and their basic properties
import data.real.basic
-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable