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