# Zulip Chat Archive

## Stream: general

### Topic: code audition

#### Egbert Rijke (May 14 2020 at 11:10):

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 (May 14 2020 at 11:20):

@Egbert Rijke You can typically name new variables using `with foo bar`

. So `induction x with x ih`

.

#### Egbert Rijke (May 14 2020 at 11:21):

Ah, that's helpful! Thanks!

#### Johan Commelin (May 14 2020 at 11:27):

I think `concat_assoc`

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

#### Johan Commelin (May 14 2020 at 11:27):

So

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

#### Johan Commelin (May 14 2020 at 11:28):

But it means you'll have to move `x y z`

to the right of the `:`

.

#### Johan Commelin (May 14 2020 at 11:29):

@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 (May 14 2020 at 11:30):

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 (May 14 2020 at 11:30):

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 (May 14 2020 at 11:32):

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 (May 14 2020 at 11:34):

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 (May 14 2020 at 11:37):

@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 (May 14 2020 at 11:39):

That is super useful, thank you both!

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

#### Johan Commelin (May 14 2020 at 11:41):

That's great (-;

#### Johan Commelin (May 14 2020 at 11:41):

We like it when people feel at home

#### Rob Lewis (May 14 2020 at 11:43):

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 (May 14 2020 at 11:45):

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 (May 14 2020 at 12:06):

There's `congr_arg`

#### Reid Barton (May 14 2020 at 12:06):

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

#### Reid Barton (May 14 2020 at 12:06):

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

.

#### Rob Lewis (May 14 2020 at 12:15):

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 (May 14 2020 at 12:30):

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 (May 14 2020 at 12:55):

What is precisely the advantage of a `$`

over parentheses?

#### Moses Schönfinkel (May 14 2020 at 12:55):

Clarity.

#### Rob Lewis (May 14 2020 at 12:58):

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 (May 14 2020 at 13:01):

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 (May 14 2020 at 13:24):

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 (May 14 2020 at 13:24):

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 (May 14 2020 at 13:41):

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 (May 14 2020 at 13:44):

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 (May 14 2020 at 13:45):

in tactic mode, `symmetry`

will change the goal and `symmetry at h`

will change the hypothesis

#### Jalex Stark (May 14 2020 at 13:46):

```
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 (May 14 2020 at 13:47):

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 (May 14 2020 at 13:47):

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 (May 14 2020 at 13:48):

or just `: h1.symm`

#### Jalex Stark (May 14 2020 at 13:48):

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 (May 14 2020 at 16:42):

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 (May 14 2020 at 16:48):

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 (May 14 2020 at 16:48):

You'll need the `functor`

and `monad`

type classes.

#### Johan Commelin (May 14 2020 at 16:48):

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

#### Reid Barton (May 14 2020 at 16:49):

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 (May 14 2020 at 16:49):

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

#### Egbert Rijke (May 14 2020 at 16:50):

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

#### Johan Commelin (May 14 2020 at 16:51):

@Egbert Rijke Things like `<$>`

and `>>=`

#### Johan Commelin (May 14 2020 at 16:52):

Aren't those standard? I dunno...

#### Bhavik Mehta (May 14 2020 at 16:52):

they're the same as the haskell ones

#### Egbert Rijke (May 14 2020 at 16:52):

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

#### Reid Barton (May 14 2020 at 16:52):

More importantly it has `do`

notation... ah.

#### Egbert Rijke (May 14 2020 at 16:53):

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

#### Johan Commelin (May 14 2020 at 16:59):

No, but it gives you nice notation

#### Johan Commelin (May 14 2020 at 16:59):

Doesn't Agda have that?

#### Egbert Rijke (May 14 2020 at 17:00):

Not that I know of

#### Johan Commelin (May 14 2020 at 17:00):

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

#### Johan Commelin (May 14 2020 at 17:00):

Also uses that notation

#### Kevin Buzzard (May 14 2020 at 19:54):

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`

.

Last updated: Dec 20 2023 at 11:08 UTC