code audition

Stream: general

[Egbert Rijke]

I'm trying out lean, and I think it would be helpful if I can have some comments on my code. It compiles with lean 3.11.0. I'm mainly looking for advise on how to make things better. For example, I'm not really sure that I like my definition of fold, and I certainly don't like my definition of assoc_concat.

What I don't like about fold is that I refer to weird variables that are generated by lean. What I don't like about assoc_concat is that I have to do this calculation with a few reflexivity paths. I would have assumed that lean can calculate those automatically, but I wasn't able to make it do a direct rewrite.

Thank you in advance for your advice.

namespace hidden

inductive list (A : Type) : Type
| nil : list
| cons : A → list → list

namespace list

definition unit {A : Type} : A → list A :=
begin
intro a,
exact cons a nil,
end

definition fold {A B : Type} (b : B) (μ : A → B → B) : list A → B :=
begin
intro x,
induction x,
{ exact b},
{ exact μ x_a x_ih}
end

definition length {A : Type} : list A → ℕ :=
begin
refine fold 0 _,
intros a n,
exact n + 1,
end

definition sum_list_ℕ : list ℕ → ℕ :=
begin
refine fold 0 _,
intros m n,
exact m + n,
end

definition concat {A : Type} : list A → list A → list A :=
begin
refine fold id _,
intros a f l,
exact cons a (f l),
end

definition flatten {A : Type} : list (list A) → list A :=
begin
exact fold nil concat,
end

definition reverse {A : Type} : list A → list A :=
begin
intro x,
induction x,
{ exact nil},
{ exact concat x_ih (unit x_a)}
end

definition assoc_concat {A : Type} (x y z : list A) :
  concat (concat x y) z = concat x (concat y z) :=
begin
induction x,
{ reflexivity},
{ calc
    concat (concat (cons x_a x_a_1) y) z = cons x_a (concat (concat x_a_1 y) z) : by reflexivity
    ... = cons x_a (concat x_a_1 (concat y z)) : by rw x_ih
    ... = concat (cons x_a x_a_1) (concat y z) : by reflexivity},
end

#reduce concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

#reduce sum_list_ℕ (concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil)))

end list

end hidden

[Johan Commelin]

@Egbert Rijke You can typically name new variables using with foo bar. So induction x with x ih.

[Egbert Rijke]

Ah, that's helpful! Thanks!

[Johan Commelin]

I think concat_assoc would typically be written using the equation compiler. I think the syntax is actually quite similar to Agda?

[Johan Commelin]

So

statement blabla
| case 1 :=
| case 2 :=

[Johan Commelin]

But it means you'll have to move x y z to the right of the :.

[Johan Commelin]

@Egbert Rijke Also... minor point, it seems that our naming conventions are slightly different. In mathlib it would be concat_assoc instead of assoc_concat.

[Rob Lewis]

Here's a quick attempt to make things a little more "canonical Lean." I didn't go through all the declarations but tried to leave some comments.

namespace list

/- we generally don't write definitions in tactic mode.
it's not a problem using tactics like intro and exact,
but more complicated tactics can produce terms that are hard to work with. -/
def unit {A : Type} (a : A) : list A :=
cons a nil

-- or:
/-
def unit {A : Type} : A → list A :=
λ a, cons a nil
-/

/- we usually write recursive definitions using pattern matching -/
def fold {A B : Type} (b : B) (μ : A → B → B) : list A → B
| nil := b
| (cons a l) := μ a (fold l)

/- but if you really want to do this, you should name the variables from `induction` -/
def fold' {A B : Type} (b : B) (μ : A → B → B) : list A → B :=
begin
intro x,
induction x with a _ b',
{ exact b },
{ exact μ a b' }
end

/- the $ lets us avoid parentheses around the last argument -/
def length {A : Type} : list A → ℕ :=
fold 0 $ λ _ n, n + 1

def sum_list_ℕ : list ℕ → ℕ :=
begin
refine fold 0 _,
intros m n,
exact m + n,
end

def concat {A : Type} : list A → list A → list A :=
begin
refine fold id _,
intros a f l,
exact cons a (f l),
end

/- if your proof / definition is just a term, there's definitely no reason for tactic mode -/
def flatten {A : Type} : list (list A) → list A :=
--begin
--exact
fold nil concat
--end

def reverse {A : Type} : list A → list A :=
begin
intro x,
induction x,
{ exact nil},
{ exact concat x_ih (unit x_a)}
end

/- declarations whose type is a Prop are usually declared with `theorem` instead of `def` -/
theorem assoc_concat {A : Type} (x y z : list A) :
  concat (concat x y) z = concat x (concat y z) :=
begin
induction x,
{ refl},
{ calc
    concat (concat (cons x_a x_a_1) y) z = cons x_a (concat (concat x_a_1 y) z) : rfl
    ... = cons x_a (concat x_a_1 (concat y z)) : by rw x_ih
    ... = concat (cons x_a x_a_1) (concat y z) : rfl},
end


#reduce concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

#reduce sum_list_ℕ (concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil)))

end list

end hidden

[Johan Commelin]

Also, do you want to do everything in tactic mode? Things like

statement :=
begin
  exact foobar
end

can just be turned into

statement :=
foobar

[Johan Commelin]

If you like type classes

def sum_list_ℕ : list ℕ → ℕ :=
begin
refine fold 0 _,
intros m n,
exact m + n,
end

could become

def sum {M : Type*} [add_monoid M] : list M → M :=
begin
refine fold 0 _,
intros m n,
exact m + n,
end

[Rob Lewis]

Here's an equation compiler version of assoc_concat, although whether this is canonical or not depends on who you ask.

theorem assoc_concat' {A : Type} : ∀ (x y z : list A),
  concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z :=
  calc
    concat (concat (cons a l) y) z = cons a (concat (concat l y) z) : rfl
    ... = cons a (concat l (concat y z)) : by rw assoc_concat'
    ... = concat (cons a l) (concat y z) : rfl

[Johan Commelin]

@Egbert Rijke Note that Lean has "poor man's holes" compared to Agda.
If you write

def sum {M : Type*} [add_monoid M] : list M → M :=
fold 0 _ -- <- put cursor before the _

then the editor will tell you the expected type.

[Egbert Rijke]

That is super useful, thank you both!

I especially like the definitions by pattern matching. Makes me feel more at home :)

[Johan Commelin]

That's great (-;

[Johan Commelin]

We like it when people feel at home

[Rob Lewis]

And a slightly less verbose assoc_concat, keeping the same idea as your proof:

theorem assoc_concat' {A : Type} : ∀ (x y z : list A),
  concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z :=
  show cons _ (concat (concat _ _) _) = cons _ (concat _ (concat _ _)),
  by rw assoc_concat'

[Egbert Rijke]

So in HoTT, I would write something like "the action on paths of the function (cons a) to assoc_concat x y z". But in Lean you never apply a function to an equality, do you?

[Reid Barton]

There's congr_arg

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/core/init/logic.html#congr_arg

[Reid Barton]

Indeed you should be able to use it in place of rw.

[Rob Lewis]

You can, but you need to give a little bit to help the HO unification.

theorem assoc_concat' {A : Type} : ∀ (x y z : list A),
  concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z := congr_arg (cons _) $ assoc_concat' _ _ _

[Gabriel Ebner]

Another point that I didn't see mentioned yet: we typically try to write universe-polymorphic declarations and avoid unnecessary restriction to Type (Type is short for Type 0).

namespace hidden

universes u

/-- Linked list with elements of type `A`.  -/
inductive list (A : Type u) : Type u
| nil : list
| cons : A → list → list

namespace list

/-- List containing just the single element `a`. -/
def unit {A : Type u} (a : A) : list A :=
cons a nil

-- ...

end list

end hidden

[Egbert Rijke]

What is precisely the advantage of a $ over parentheses?

[Moses Schönfinkel]

Clarity.

[Rob Lewis]

It saves a character; sometimes it's easier to see "everything that follows is the last argument" than to count/match parens. It's mostly personal preference.

[Egbert Rijke]

Rob Lewis said:

And a slightly less verbose assoc_concat, keeping the same idea as your proof:

theorem assoc_concat' {A : Type} : ∀ (x y z : list A),
  concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z :=
  show cons _ (concat (concat _ _) _) = cons _ (concat _ (concat _ _)),
  by rw assoc_concat'

Another question :) Why does this work, but the following doesn't.

theorem assoc_concat' {A : Type} : ∀ (x y z : list A),
  concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z := by rw assoc_concat'

[Rob Lewis]

The rw tactic doesn't really do definitional unfolding. It will look for a subterm that syntactically matches the LHS of assoc_concat.

[Rob Lewis]

If you use show, you tell Lean to convert the goal to something definitionally equal, where the LHS of assoc_concat does appear syntactically. So then you can rewrite.

[Egbert Rijke]

Another newbie question. What do I have to do in a calc if my equation holds, but it goes the other way (i.e. I need the inverse of the equality)?

[Jalex Stark]

Do you mean that you have a goal a=b and a proof of b=a and you want to stitch them together?

[Jalex Stark]

in tactic mode, symmetry will change the goal and symmetry at h will change the hypothesis

[Jalex Stark]

import tactic
example {α : Type} {a b c : α}
(h1 : b = a)
(h2 : b = c) :
a = c :=
calc a = b : by {symmetry, exact h1,}
... = c : h2

[Egbert Rijke]

Yeah, that's what I wanted. I have a proof p:b=a and I need a=b somewhere in my calculation. Actually... lean just accepts by rw p. It is quite amazing!

[Egbert Rijke]

Oh, that's good to know too, that you can say by {stuff, more stuff} in a calc part of the proof. Thanks!

[Reid Barton]

or just : h1.symm

[Jalex Stark]

in my head I pretend that rw applies a depth-limited version of refl afterward. I don't know how far from literally true that is

[Egbert Rijke]

Thanks to everyone here it wasn't much effort to prove a few basic things about lists :thank_you:

Now the next thing to worry about... will it compile with lean 3.12.0 :upside_down:

/- This is a short tutorial on lean for the Logic in Computer Science course at the university
of Ljubljana. -/

namespace logika_v_racunalnistvu

/- We typically want to be universe polymorphic in lean, so we introduce a universe variable u. -/

universes u v w

/- Definitions of inductive types are made using the inductive keyword. Different constructors
   are separated by |. -/

inductive list (A : Type u) : Type u
| nil : list
| cons : A → list → list

/- We open the namespace list, so that we can use nil and cons directly. -/

namespace list

/- We will now define some basic operations on lists. -/

/- Direct definitions are made using the definition keyword, followed by := -/

definition unit {A : Type u} (a : A) : list A :=
cons a nil

/- A shorthand for definition is def, which may also be used. -/

/- Since the type of lists is an inductive type, we can make inductive definitions on list
using pattern matching. The syntax is analogous to the syntax of the inductive type itself.
Note that in pattern matching definitions, we don't use := at the end of the specification. -/

def fold {A : Type u} {B : Type v} (b : B) (μ : A → B → B) : list A → B
| nil := b
| (cons a l) := μ a (fold l)

def functor_list {A : Type u} {B : Type v} (f : A → B) : list A → list B
| nil := nil
| (cons a x) := cons (f a) (functor_list x)

def length {A : Type u} : list A → ℕ :=
fold 0 (λ _ n, n + 1)

def sum_list_ℕ : list ℕ → ℕ :=
fold 0 (λ m n, m + n)

def concat {A : Type u} : list A → list A → list A :=
fold id (λ a f l, cons a (f l))

def flatten {A : Type u} : list (list A) → list A :=
fold nil concat

def reverse {A : Type u} : list A → list A
| nil := nil
| (cons a l) := concat (reverse l) (unit a)

/- We have now finished defining our basic operations on lists. Let us check by some examples
   that the operations indeed do what they are supposed to do. With your mouse, hover over the
   #reduce keyword to see what each term reduces to. -/

#reduce concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

#reduce sum_list_ℕ (concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil)))

#reduce reverse (concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil)))

/- Of course, if you really want to know that your operations behave as expected, you should
   prove the relevant properties about them. This is what we will do next. -/

theorem identity_law_functor_list {A : Type u} :
    ∀ (x : list A), functor_list id x = x
| nil := rfl
| (cons a x) :=
    calc
    functor_list id (cons a x)
        = cons a (functor_list id x) : rfl
    ... = cons a x : by rw identity_law_functor_list

theorem composition_law_functor_list {A : Type u} {B : Type v} {C : Type w} (f : A → B) (g : B → C) :
    ∀ (x : list A), functor_list (g ∘ f) x = functor_list g (functor_list f x)
| nil := rfl
| (cons a x) :=
    calc
    functor_list (g ∘ f) (cons a x)
        = cons (g (f a)) (functor_list (g ∘ f) x) : rfl
    ... = cons (g (f a)) (functor_list g (functor_list f x)) : by rw composition_law_functor_list
    ... = functor_list g (functor_list f (cons a x)) : rfl

/- We begin with the properties concatenation. Concatenation of lists is an associative
   operation, and it satisfies the left and right unit laws.universe

   In order to prove associativity, we note that since concatenation is defined by induction
   on the left argument, we will again use induction on the left argument to prove this
   propoerty. The proof is presented by pattern matching.

   In the proof we will use the built-in equation compiler. We just calculate as if we were
   working on a sheet of paper, and each time we mention the reason why the equality holds. -/

theorem assoc_concat {A : Type u} :
    ∀ (x y z : list A), concat (concat x y) z = concat x (concat y z)
| nil _ _ := rfl
| (cons a l) y z :=
    calc
    concat (concat (cons a l) y) z
        = cons a (concat (concat l y) z) : by reflexivity
    ... = cons a (concat l (concat y z)) : by rw assoc_concat
    ... = concat (cons a l) (concat y z) : by reflexivity

theorem left_unit_law_concat {A : Type u} :
    ∀ (x : list A), concat nil x = x :=
    eq.refl

theorem right_unit_law_concat {A : Type u} :
    ∀ (x : list A), concat x nil = x
| nil := rfl
| (cons a x) :=
    show cons a (concat x nil) = cons a x,
    by rw right_unit_law_concat

/- Next, we prove the elementary properties of the length function. -/

theorem length_nil {A : Type u} :
    length (@nil A) = 0 := rfl

theorem length_unit {A : Type u} (a : A) :
    length (unit a) = 1 :=
    rfl

theorem length_concat {A : Type u} :
    ∀ (x y : list A), length (concat x y) = length x + length y
| nil y :=
    calc
    length (concat nil y)
        = length y : rfl
    ... = 0 + length y : by rw zero_add
    ... = length nil + length y : by rw length_nil
| (cons a x) y :=
    calc
    length (concat (cons a x) y)
        = length (concat x y) + 1 : rfl
    ... = (length x + length y) + 1 : by rw length_concat
    ... = (length x + 1) + length y : by rw nat.succ_add
    ... = (length (cons a x)) + length y : rfl

/- Next, we prove the elemenatary properties of the flatten function. -/

theorem flatten_unit {A : Type u} :
    ∀ (x : list A), flatten (unit x) = x :=
    right_unit_law_concat

theorem length_flatten {A : Type u} :
    ∀ (x : list (list A)), length (flatten x) = sum_list_ℕ (functor_list length x)
| nil := rfl
| (cons a x) :=
    calc
    length (flatten (cons a x))
        = length (concat a (flatten x)) : rfl
    ... = length a + length (flatten x) : by rw length_concat
    ... = length a + sum_list_ℕ (functor_list length x) : by rw length_flatten
    ... = sum_list_ℕ (functor_list length (cons a x)) : rfl

theorem flatten_concat {A : Type u} :
    ∀ (x y : list (list A)), flatten (concat x y) = concat (flatten x) (flatten y)
| nil y := rfl
| (cons a x) y :=
    calc
    flatten (concat (cons a x) y)
        = concat a (flatten (concat x y)) : rfl
    ... = concat a (concat (flatten x) (flatten y)) : by rw flatten_concat
    ... = concat (concat a (flatten x)) (flatten y) : by rw assoc_concat
    ... = concat (flatten (cons a x)) (flatten y) : rfl

theorem flatten_flatten {A : Type u} :
    ∀ (x : list (list (list A))), flatten (flatten x) = flatten (functor_list flatten x)
| nil := rfl
| (cons a x) :=
    calc
    flatten (flatten (cons a x))
        = flatten (concat a (flatten x)) : rfl
    ... = concat (flatten a) (flatten (flatten x)) : by rw flatten_concat
    ... = concat (flatten a) (flatten (functor_list flatten x)) : by rw flatten_flatten
    ... = flatten (functor_list flatten (cons a x)) : rfl

/- Next, we prove the elementary properties of list reversal. -/

theorem unit_reverse {A : Type u} (a : A) :
    reverse (unit a) = unit a := rfl

theorem length_reverse {A : Type u} :
    ∀ (x : list A), length (reverse x) = length x
| nil := rfl
| (cons a x) :=
    calc
    length (reverse (cons a x))
        = length (concat (reverse x) (unit a)) : rfl
    ... = length (reverse x) + length (unit a) : by rw length_concat
    ... = length (reverse x) + 1 : by rw length_unit
    ... = length x + 1 : by rw length_reverse
    ... = length (cons a x) : rfl

theorem reverse_concat {A : Type u} :
    ∀ (x y : list A), reverse (concat x y) = concat (reverse y) (reverse x)
| nil y :=
    calc
    reverse (concat nil y) = reverse y : by reflexivity
    ... = concat (reverse y) nil : by rw right_unit_law_concat
| (cons a x) y :=
    calc
    reverse (concat (cons a x) y)
        = concat (reverse (concat x y)) (unit a) : rfl
    ... = concat (concat (reverse y) (reverse x)) (unit a) : by rw reverse_concat
    ... = concat (reverse y) (concat (reverse x) (unit a)) : by rw assoc_concat
    ... = concat (reverse y) (reverse (cons a x)) : rfl

theorem reverse_flatten {A : Type u} :
    ∀ (x : list (list A)), reverse (flatten x) = flatten (reverse (functor_list reverse x))
| nil := rfl
| (cons a x) :=
    calc
    reverse (flatten (cons a x))
        = reverse (concat a (flatten x)) : rfl
    ... = concat (reverse (flatten x)) (reverse a) : by rw reverse_concat
    ... = concat (flatten (reverse (functor_list reverse x))) (reverse a) : by rw reverse_flatten
    ... = concat (flatten (reverse (functor_list reverse x))) (flatten (unit (reverse a))) : by rw flatten_unit
    ... = flatten (concat (reverse (functor_list reverse x)) (unit (reverse a))) : by rw flatten_concat
    ... = flatten (reverse (cons (reverse a) (functor_list reverse x))) : rfl
    ... = flatten (reverse (functor_list reverse (cons a x))) : rfl

theorem reverse_reverse {A : Type u} :
    ∀ (x : list A), reverse (reverse x) = x
| nil := rfl
| (cons a x) :=
    calc
    reverse (reverse (cons a x))
        = reverse (concat (reverse x) (unit a)) : rfl
    ... = concat (reverse (unit a)) (reverse (reverse x)) : by rw reverse_concat
    ... = concat (unit a) (reverse (reverse x)) : by rw unit_reverse
    ... = concat (unit a) x : by rw reverse_reverse
    ... = cons a x : rfl

end list

end logika_v_racunalnistvu

[Johan Commelin]

Nice! Note that lean has all the nice functional programming trigraphs for functors and monads... I don't know if you like those (-;

[Johan Commelin]

You'll need the functor and monad type classes.

[Johan Commelin]

(But I don't know if you want to mention and/or use type classes in this tutorial.)

[Reid Barton]

Looks nice! You might also want to mention explicitly that in recursive definitions, arguments to the left of the colon are fixed and not written at the recursive calls.

[Egbert Rijke]

Cool, I don't know what trigraphs are, but I know what a monad is :)

[Egbert Rijke]

@Reid Barton That's a good thing to mention to the students. Thanks!

[Johan Commelin]

@Egbert Rijke Things like <$> and >>=

[Johan Commelin]

Aren't those standard? I dunno...

[Bhavik Mehta]

they're the same as the haskell ones

[Egbert Rijke]

Maybe, but I don't know these either. I'm not a programmer :)

[Reid Barton]

More importantly it has do notation... ah.

[Egbert Rijke]

But are you saying that lean can automatically handle the functoriality of the list operator?

[Johan Commelin]

No, but it gives you nice notation

[Johan Commelin]

Doesn't Agda have that?

[Egbert Rijke]

Not that I know of

[Johan Commelin]

https://en.wikipedia.org/wiki/Monad_(functional_programming)#Definition

[Johan Commelin]

Also uses that notation

[Kevin Buzzard]

Egbert Rijke said:

Yeah, that's what I wanted. I have a proof p:b=a and I need a=b somewhere in my calculation. Actually... lean just accepts by rw p. It is quite amazing!

In the middle of a calc block you see things like ... = b : sorry and at the sorry the goal is a = b. If you have p : b = a then replacing the sorry with by rw p will work because the goal a = b will be rewritten to a = a which will then be closed with refl because rw tries refl after every invocation. But you can't just replace sorry with p, although you could replace it with eq.symm p; moreover, because the type of p is eq a b, you could also replace it with p.symm.