Zulip Chat Archive

Stream: LftCM22

Topic: slides and materials from talks

Heather Macbeth (Jul 11 2022 at 14:34):

Link for the Natural Number Game:
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

Jeremy Avigad (Jul 11 2022 at 14:38):

Here's the lean file that I used for my introductory presentation:
introduction.lean
If you have a Lean project installed (for example, the Mathematics in Lean repository), you can just drop it in the src folder and then open it in VS Code.

Heather Macbeth (Jul 11 2022 at 15:00):

After Kevin's talk, we’ll arrange Zoom breakout rooms for any virtual participants who would like to work on the Natural Number Game with a partner and/or tutor. Let me know if you would like to be put in a breakout room.

Jake Levinson (Jul 11 2022 at 15:45):

Oops, the Zoom room closed. If anyone is watching, it will be back shortly!

Heather Macbeth (Jul 11 2022 at 15:45):

Sorry everyone, the Zoom meeting was briefly cut off, bringing it back!

Jake Levinson (Jul 11 2022 at 15:45):

(for breakout rooms)

Heather Macbeth (Jul 11 2022 at 15:47):

Zoom meeting is live again but you'll need to log in.

Alba Marina MÁLAGA SABOGAL (Jul 12 2022 at 13:05):

Somebody can explain how to get the demos 02_Basics that Johan is using on screen on his talk right now ?

Patrick Massot (Jul 12 2022 at 13:07):

The file we see now will be put here later. But you should definitely get the Mathematics in Lean book.

Patrick Massot (Jul 12 2022 at 13:08):

see https://leanprover.zulipchat.com/#narrow/stream/330515-LftCM22/topic/Installation/near/289244517

Ryan McCorvie (Jul 12 2022 at 15:30):

(deleted)

Johan Commelin (Jul 12 2022 at 15:31):

@Alba Marina MÁLAGA SABOGAL I pushed it here: https://leanprover.zulipchat.com/#narrow/stream/330515-LftCM22/topic/Basics.20Demo

Jeremy Avigad (Jul 12 2022 at 15:33):

Here are the slides from the logic session:
logic.lean

Kevin Buzzard (Jul 12 2022 at 16:00):

Oh sorry! Here are my slides from yesterday. Sorry not to post them earlier. talk.pdf

and here are the files I used in the demo:

-- import all the tactics
import tactic
-- import the definition of the degree of a polynomial
import data.polynomial.degree

-- use the usual notation `k[X]` for polynomials over `k`
open_locale polynomial

-- want to type `degree` not `polynomial.degree`
open polynomial

example (n : ℕ) : degree ((X : ℤ[X])^n) = n :=
begin
  library_search,
end

import tactic

variables (x y z : ℕ)

-- comment out the below lines to see various other ways that lean can display info

--set_option pp.notation false

--set_option pp.parens true

example (h1 : x = z)
(h2 : x + y + z = x ^ 2 + y ↔ 2 + 2 = 5)
(h3 : y + z = x + y)
(h4 : x ^ 2 + y = z → x + y = z) :
x + y + z = x ^ 2 + y :=
begin
  -- you can experiment with rewrites here
  sorry
end

import tactic

-- composite of injective functions is injective

variables (X Y Z : Type)
  (f : X → Y) (g : Y → Z)

open function

-- example to show that `apply` is like arguing backwards.
example (hf : injective f)
  (hg : injective g) :
  injective (g ∘ f) :=
begin
  -- What's the maths proof?
  -- x₁ and x₂ in X
  -- know g(f(x₁))=g(f(x₂))
  -- injectivity of g implies f(x₁)=f(x₂)
  -- injectivity of f says x₁ = x₂
  -- so done
  -- Mathematicians move a hypothesis towards the goal.
  intros x₁ x₂ h,
  apply hf, -- apply injectivity of f first??
  apply hg,
  exact h, -- We moved the goal towards the hypothesis with `apply`
end

import tactic
import data.real.basic

example (x : ℕ) :
  x + 0 = x :=
begin
  refl,
end

example (x : ℕ) :
  0 + x = x :=
begin
  -- refl, -- fails because it's not definitional this way around!
  sorry,
end

example (x y z : ℕ)
  (h : x + 0 = y) : x = z :=
begin
--  rw h, -- fails because rw works up to syntactic equality
  change x = y at h, -- change works up to definitional equality
--  rw add_zero at h, -- would also work; note that the proof of `add_zero` is `refl`.
  rw h, -- now it works
  sorry,
end

Jeremy Avigad (Jul 12 2022 at 16:13):

I had actually prepared a few more examples for my talk, including some power-user moves. I added the examples to the file logic.lean attached here, as well as cut-and-pasted here.
logic.lean

/-
More examples.
-/

section
variables p q : Prop
variables r s : ℕ → Prop

example : p ∧ q → q ∧ p :=
begin
  intro h,
  cases h with h1 h2,
  split,
  apply h2,
  apply h1
end

example : p ∧ q → q ∧ p :=
begin
  intro h,
  exact ⟨h.right, h.left⟩
end

example : p ∧ q → q ∧ p :=
begin
  intro h,
  exact and.intro h.right h.left
end

example : p ∧ q → q ∧ p :=
begin
  rintros ⟨h1, h2⟩,
  exact ⟨h2, h1⟩
end

example : p ∧ q → q ∧ p :=
λ ⟨h1, h2⟩, ⟨h2, h1⟩

example : p ∧ q → q ∧ p :=
begin
  intro h,
  rwa and_comm
end

example : p ∧ q → q ∧ p :=
by tauto

example : p ∧ q → q ∧ p :=
by finish

example : p ∨ q → q ∨ p :=
begin
  intro h,
  cases h with hp hq,
  { right, apply hp },
  { left, apply hq }
end

example : (∃ x, r x ∧ s x) → (∃ x, r x) ∧ (∃ x, s x) :=
begin
  intro h,
  cases h with x hx,
  split,
  { use [x, hx.left] },
  { use [x, hx.right] }
end

example : (∃ x, r x ∧ s x) → (∃ x, r x) ∧ (∃ x, s x) :=
begin
  rintros ⟨x, hx1, hx2⟩,
  use [x, hx1, x, hx2]
end

example : (∃ x, r x ∧ s x) → (∃ x, r x) ∧ (∃ x, s x) :=
by finish

example : ∀ z, (∃ x y, r x ∧ s y ∧ y = z) → ∃ x, r x ∧ s z :=
begin
  rintros z ⟨x, y, rx, sy, heq⟩,
  use [x, rx],
  rwa ←heq
  -- or:
  -- rw ←heq
  -- exact sy
end

example : ∀ z, (∃ x y, r x ∧ s y ∧ y = z) → ∃ x, r x ∧ s z :=
begin
  rintros z ⟨x, y, rx, sy, rfl⟩,
  use [x, rx, sy]
end

example : ∀ z, (∃ x y, r x ∧ s y ∧ y = z) → ∃ x, r x ∧ s z :=
by finish

end

Rob Lewis (Jul 13 2022 at 12:48):

I'm talking about structures and classes in 12 minutes. My goal is to keep the talk short and let you work on exercises, so here's a problem sheet! I'll post my finished demo code after the talk -- most of it will be filled in as I go. structures_exercises.lean

Rob Lewis (Jul 13 2022 at 12:49):

import data.rat.defs
import data.nat.parity
import tactic.basic

/-!

Most of these exercises are adapted from the LftCM 2020 exercises:
<https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/structures.lean>


-/

open nat

noncomputable theory -- definitions are allowed to not compute in this file
open_locale classical -- use classical logic in this file

/-!
## Structures and Classes

In this session we will discuss structures together,
and then you can solve the exercises yourself.


### Declaring a Structure
-/



/-!
  ### Exercise: a simple structure
  * Define a structure of eventually constant sequences `ℕ → ℕ`. The first field will be
    `seq : ℕ → ℕ`, and the second field will be the statement that `seq` is eventually constant.
  * Define a structure of a type with 2 points that are unequal.
    (hint: omit the type of the structure, Lean might complain if you give it explicitly)

  Lean will not tell you if you got the right definition, but it will complain if you make a syntax
  error. If you are unsure, ask a mentor to check whether your solution is correct.
-/


/-!
  ### Exercise: manipulating structure elements

Here we give the upper bounds for a function `f`. We can omit the type of the structure. -/
structure bounds (f : ℕ → ℕ) :=
  (bound : ℕ)
  (le_bound : ∀ (n : ℕ), f n ≤ bound)

/-! You can use `#print` to print the type and all fields of a structure. -/

#print bounds

/-!
  * Define `bounds` (given above) again, but now using a the subtype notation `{ _ : _ // _ }`.
  * Define functions back and forth from the structure `bounds` given above and `bounds` given here.
    Try different variations using the anonymous constructor and the projection notation.
-/


def bounds' (f : ℕ → ℕ) : Type :=
sorry

example (f : ℕ → ℕ) : bounds f → bounds' f :=
sorry

/- In the example below, replace the `sorry` by an underscore `_`.
  A small yellow lightbulb will appear. Click it, and then select
  `Generate skeleton for the structure under construction`.
  This will automatically give an outline of the structure for you. -/
example (f : ℕ → ℕ) : bounds' f → bounds f :=
λ n, sorry




/-! ### Exercise: Bijections and equivalences -/

section bijections

open function

variables {α β : Type*}

/-
An important structure is the type of equivalences, which gives an equivalence (bijection)
between two types:

structure equiv (α β : Type*) :=
(to_fun : α → β)
(inv_fun : β → α)
(left_inv : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

In this section we show that this is the same as the bijections from `α` to `β`.
-/
#print equiv

structure bijection (α β : Type*) :=
  (to_fun : α → β)
  (injective : injective to_fun)
  (surjective : surjective to_fun)

/- We declare a *coercion*. This allows us to treat `f` as a function if `f : bijection α β`. -/
instance : has_coe_to_fun (bijection α β) (λ _, α → β) :=
⟨λ f, f.to_fun⟩

/-! To show that two bijections are equal, it is sufficient that the underlying functions are
  equal on all inputs. We mark it as `@[ext]` so that we can later use the tactic `ext` to show that
  two bijections are equal. -/
@[ext] def bijection.ext {f g : bijection α β} (hfg : ∀ x, f x = g x) : f = g :=
by { cases f, cases g, congr, ext, exact hfg x }

/-! This lemma allows `simp` to reduce the application of a bijection to an argument. -/
@[simp] lemma coe_mk {f : α → β} {h1f : injective f} {h2f : surjective f} {x : α} :
  { bijection . to_fun := f, injective := h1f, surjective := h2f } x = f x := rfl

/- There is a lemma in the library that almost states this.
  You can use the tactic `suggest` to get suggested lemmas from Lean
  (the one you want has `bijective` in the name). -/
def equiv_of_bijection (f : bijection α β) : α ≃ β :=
begin
  sorry
end

def bijection_of_equiv (f : α ≃ β) : bijection α β :=
sorry

/-! Show that bijections are the same (i.e. equivalent) to equivalences. -/
def bijection_equiv_equiv : bijection α β ≃ (α ≃ β) :=
sorry

end bijections



/-! ### Exercise: Bundled groups -/

/-! Below is a possible definition of a group in Lean.
  It's not the definition we use use in mathlib. The actual definition uses classes. -/

structure Group :=
  (G : Type*)
  (op : G → G → G)
  (infix * := op) -- temporary notation `*` for `op`, just inside this structure declaration
  (op_assoc' : ∀ (x y z : G), (x * y) * z = x * (y * z))
  (id : G)
  (notation 1 := id) -- temporary notation `1` for `id`, just inside this structure declaration
  (id_op' : ∀ (x : G), 1 * x = x)
  (inv : G → G)
  (postfix ⁻¹ := inv) -- temporary notation `⁻¹` for `inv`, just inside this structure declaration
  (op_left_inv' : ∀ (x : G), x⁻¹ * x = 1)

/-! You can use the `extend` command to define a structure that adds fields
  to one or more existing structures. -/
structure CommGroup extends Group :=
  (infix * := op)
  (op_comm : ∀ (x y : G), x * y = y * x)

/- Here is an example: the rationals form a group under addition. -/
def rat_Group : Group :=
{ G := ℚ,
  op := (+), -- you can put parentheses around an infix operation to talk about the operation itself.
  op_assoc' := add_assoc,
  id := 0,
  id_op' := zero_add,
  inv := λ x, -x,
  op_left_inv' := neg_add_self }

/-- You can extend an object of a structure by using the structure notation and using
  `..<existing object>`. -/
def rat_CommGroup : CommGroup :=
{ G := ℚ, op_comm := add_comm, ..rat_Group }

namespace Group

variables {G : Group} /- Let `G` be a group -/

/- The following line declares that if `G : Group`, then we can also view `G` as a type. -/
instance : has_coe_to_sort Group (Type*) := ⟨Group.G⟩
/- The following lines declare the notation `*`, `⁻¹` and `1` for the fields of `Group`. -/
instance : has_mul G := ⟨G.op⟩
instance : has_inv G := ⟨G.inv⟩
instance : has_one G := ⟨G.id⟩

/- the axioms for groups are satisfied -/
lemma op_assoc (x y z : G) : (x * y) * z = x * (y * z) := G.op_assoc' x y z

lemma id_op (x : G) : 1 * x = x := G.id_op' x

lemma op_left_inv (x : G) : x⁻¹ * x = 1 := G.op_left_inv' x

/- Use the axioms `op_assoc`, `id_op` and `op_left_inv` to prove the following lemma.
  The fields `op_assoc'`, `id_op'` and `op_left_inv'` should not be used directly, nor can you use
  any lemmas from the library about `mul`. -/
lemma eq_id_of_op_eq_self {G : Group} {x : G} : x * x = x → x = 1 :=
begin
  sorry
end

/- Apply the previous lemma to show that `⁻¹` is also a right-sided inverse. -/
lemma op_right_inv {G : Group} (x : G) : x * x⁻¹ = 1 :=
begin
  sorry
end

/- we can prove that `1` is also a right identity. -/
lemma op_id {G : Group} (x : G) : x * 1 = x :=
begin
  sorry
end

/-!
  However, it is inconvenient to use this group instance directly.
  One reason is that to use these group operations we now have to write
  `(x y : rat_Group)` instead of `(x y : ℚ)`.
  That's why in Lean we use classes for algebraic structures.
-/

/- show that the cartesian product of two groups is a group. The underlying type will be `G × H`. -/

def prod_Group (G H : Group) : Group :=
sorry

end Group


/-!

### Exercise: type classes

We'll see the true power of type classes in later lectures today.
Remember that, normally, a type class has the appearance
```lean
class new_structure {α : Type} {β : Type} :=
(data_name : data_type)
(property_name : property_type)

That is, it is a structure with one or more type parameters,
zero or more data fields,
and zero or more property fields.

We think of an instance new_structure A B as saying "A and B have a canonical new_structure structure."
For instance, int.add_group : add_group ℤ says that the integers have a canonical group structure.

What other examples of "structured sets" can you think of that could be represented as type classes?
Can you write them down in Lean, in real or mock-up syntax?
-/

/-!

Exercise: a finite group

We're going to show that the two-element type {z, o} has a group structure.

-- First we define this type, and call it two. Its elements are z and o.
inductive two
| z | o

open two

#check z
#check o

-- Now we define addition on the type two, by cases.
def two.add : two → two → two
| o o := z
| z z := z
| _ _ := o

-- Do this one yourself! Define negation on the type two.
def two.neg : two → two
| o := sorry
| z := sorry

-- Once you fill in two.neg, most proofs about o and z are by definition!
example : two.add o (two.neg z) = o :=
rfl

-- With our addition and negation operators, two should form an additive group.
-- Fill in the missing fields.
-- Hint: if you have a : two, the tactic cases a might be useful.
instance : add_group two :=
{ add := two.add,
neg := two.neg,
add_assoc := sorry,
zero := sorry,
zero_add := sorry,
add_zero := sorry,
add_left_neg := sorry }

-- And with this instance, you can use familiar group operations (and lemmas) on two.

example : o + -z = o :=
rfl

Rob Lewis (Jul 13 2022 at 15:01):

And here's the result of my talk (belated, sorry):

import data.real.basic

/-

# Structures and type classes

References:
* Mathematics in Lean section 6.1
* Theorem Proving in Lean chapters 9--10
* [Hitchhiker's Guide to Logical Verification](https://cs.brown.edu/courses/cs1951x/static_files/main.pdf)
  sections 4.5--4.6

You've seen a bunch of talks about tools to prove things about objects that are
  already defined.

How do we define our own new things?

A thought, especially if you've done some programming:
  data types are often a *conjunction* of fields or a *disjunction* of constructors.

Conjunction: a complex number is a pair of a real and imaginary part, both real
  numbers.
Disjunction: a propositional formula is either a variable p,
  or an application of a binary connective ∧ ∨ → to two formulas,
  or an application of ¬ to one formula

Heuristic claim: mathematicians use the conjunction pattern much more often.
-/

structure R3 :=
(x : ℝ)
(y : ℝ)
(z : ℝ)

/- What is the type of `R3`? -/

#check R3

/- How do you create a `R3`? -/

#check R3.mk 1 2 3

#check ({x := 1, y := 2, z := 3} : R3)

#check (⟨1, 2, 3⟩ : R3)
.

/- When are two `R3`s equal? -/

example (a b : R3) : a = b :=
begin
  cases a, cases b, simp,
end


/- If you have a `R3`, how do you extract the coordinates? -/

def v : R3 := ⟨1, 2, 3⟩

#check v.z

#check R3.x

/-
You can do this in most programming languages. What's special in Lean:
  we can add *propositional* fields to our structures.
-/

structure R3_plus :=
(x y z : ℝ)
(x_pos : x > 0)
(y_pos : y > 0)
(z_pos : z > 0)

#check R3_plus.mk

/- When are two `R3_plus`es equal? -/

example (a b : R3_plus) : a = b :=
begin
  cases a, cases b, simp only,
end

/-
Structures can take *parameters*.
It feels kind of like adding another field, but there are practical and moral
  differences.
There's an art to choosing which to use.
-/

structure Rn_plus (n : ℕ) :=
(coeff : fin n → ℝ)
(coeff_pos : ∀ k, coeff k > 0)

structure Rn_plus' :=
(n : ℕ)
(coeff : fin n → ℝ)


#check Rn_plus

#check @Rn_plus.mk

-- #check (⟨![0,0,0,0,0]⟩ : Rn_plus 5)


#check Rn_plus'.mk 5 (λ k, 0)

example (x : Rn_plus 2) (y : Rn_plus 3) : x ≠ y :=
sorry



/- So: let's define a group. -/




structure Group (G : Type) :=
(one : G)
(mul : G → G → G)
(inv : G → G)
(one_mul : ∀ x : G, mul one x = x)
-- ...

#check Group ℤ















/-
To bundle, or not to bundle? How are we going to use them?
These algebraic structures are a bit of a special situation.
Sometimes we think of a group as an object itself. (Category of groups, ...)
Other times we work *within* a particular group.
  (A particular type has a single familiar group structure.)
-/

example (x : ℤ) : -x + x = 0 :=
add_left_neg x

/-
`add_left_neg` is a generic theorem about (additive) groups.
-/

#check @add_left_neg
.
/-
Read this as: "for any type `G` with an additive group structure, for every `a : G`, `-a + a = 0`."

What are those `+`, `-`, `0`? They come from that group structure on `G`.

There's some magic going on here when we write our example.
Lean has automatically found a group structure on `ℤ`.
This is done with a process called *type class inference*.
-/

#print add_group
#print int.add_group
.
/-
Ignore the actual definitions here, but notice some information at the beginnings.

* `add_group` is a *type class*. This is a special kind of structure:
  approximately, "this structure bundles additional features into a type."
* `int.add_group` is an *instance* of this type class.
  It shows that `ℤ` has the extra features described by `add_group`.
  Furthermore, it registers this fact for *type class inference*.
* `add_left_neg` takes an argument `[inst_1 : add_group G]`.
  The square brackets tell Lean to fill in this argument automatically using the
  registered instances.


Type class inference is more than a lookup table: it's recursive.
-/


example (G : Type) [add_group G] (a : G × G) : -a + a = 0 :=
add_left_neg _

#check @prod.add_group
.

/-
Type classes are used *everywhere* in Lean to do all the bookkeeping you don't
  want to think about.
You'll see examples from topology, algebra, analysis, ... over the next few days.
But let's do a very basic example together as practice: nonempty types.
-/

class my_nonempty (A : Type) : Prop :=
(has_val : ∃ x : A, true)

instance : my_nonempty ℤ :=
{ has_val := ⟨0, trivial⟩ }

instance whatever {A B : Type} [ha : my_nonempty A] [hb : my_nonempty B] :
  my_nonempty (A × B) :=
begin
  cases ha.has_val with a _,
  cases hb.has_val with b _,
  apply my_nonempty.mk,
  use (a, b),
end

set_option pp.implicit true
def k : my_nonempty (ℤ × ℤ × ℤ × ℕ × ℤ × ℤ × ℤ × ℤ) := --
begin
  apply @whatever _ _ _ _,
  apply_instance,
  apply @whatever _ _ _ _,
  apply_instance,
  apply @whatever _ _ _ _,
  apply_instance,
  apply @whatever _ _ _ _,
  use ⟨⟨0, trivial⟩⟩,
  apply_instance
end
--by apply_instance
#print k