Zulip Chat Archive

Stream: general

Topic: code audition


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Egbert Rijke (May 14 2020 at 11:21):

Ah, that's helpful! Thanks!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 14 2020 at 11:27):

So

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

view this post on Zulip Johan Commelin (May 14 2020 at 11:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (May 14 2020 at 11:41):

That's great (-;

view this post on Zulip Johan Commelin (May 14 2020 at 11:41):

We like it when people feel at home

view this post on Zulip 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'

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 14 2020 at 12:06):

There's congr_arg

view this post on Zulip Reid Barton (May 14 2020 at 12:06):

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

view this post on Zulip Reid Barton (May 14 2020 at 12:06):

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

view this post on Zulip 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' _ _ _

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 14 2020 at 12:55):

What is precisely the advantage of a $ over parentheses?

view this post on Zulip Moses Schönfinkel (May 14 2020 at 12:55):

Clarity.

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 14 2020 at 13:45):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Reid Barton (May 14 2020 at 13:48):

or just : h1.symm

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (May 14 2020 at 16:48):

You'll need the functor and monad type classes.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Egbert Rijke (May 14 2020 at 16:49):

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

view this post on Zulip Egbert Rijke (May 14 2020 at 16:50):

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

view this post on Zulip Johan Commelin (May 14 2020 at 16:51):

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

view this post on Zulip Johan Commelin (May 14 2020 at 16:52):

Aren't those standard? I dunno...

view this post on Zulip Bhavik Mehta (May 14 2020 at 16:52):

they're the same as the haskell ones

view this post on Zulip Egbert Rijke (May 14 2020 at 16:52):

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

view this post on Zulip Reid Barton (May 14 2020 at 16:52):

More importantly it has do notation... ah.

view this post on Zulip Egbert Rijke (May 14 2020 at 16:53):

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

view this post on Zulip Johan Commelin (May 14 2020 at 16:59):

No, but it gives you nice notation

view this post on Zulip Johan Commelin (May 14 2020 at 16:59):

Doesn't Agda have that?

view this post on Zulip Egbert Rijke (May 14 2020 at 17:00):

Not that I know of

view this post on Zulip Johan Commelin (May 14 2020 at 17:00):

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

view this post on Zulip Johan Commelin (May 14 2020 at 17:00):

Also uses that notation

view this post on Zulip 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: May 11 2021 at 13:22 UTC