Zulip Chat Archive

Stream: new members

Topic: Diana Kalinichenko


view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 13:51):

Hi, I am Diana Kalinichenko, a CS undergrad from HSE Moscow interested in formal verification, type theory and related areas. I've done some simple stuff in Lean (natural numbers game and some tutorials) and I'm joining here to ask questions about more complicated stuff. I'm mainly interested in the "verified programming" aspect of Lean, but I think formalization of mathematics is also a cool thing. Also, I'd like to contribute to mathlib some day if there's anything that I can do!

view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 14:16):

So, I'm having trouble proving a lemma. I've decided to implement a grow-only counter CRDT in Lean 3:

def GCounter (n: ) : Type := array n 

def inc {n: } (g: GCounter n) (index: fin n) (value: ) : GCounter n :=
  g.write index $ g.read index + value

def merge {n: } (g₁: GCounter n) (g₂: GCounter n) : GCounter n :=
  array.map₂ max g₁ g₂

def value {n: } (g: GCounter n) :  :=
  array.foldl g 0 (+)

Proving that (GCounter, merge) is a semilattice was easy, however I'm stuck on the following seemingly simple property:

lemma inc_value_increasing
  {n: } (v: ) (i: fin n) (g: GCounter n) :
  value (inc g i v) = value g + v := _

When I try to rewrite everything by definition and then go on, I run into complicated expressions involving d_array.iterate_aux and other stuff. Could someone suggest a way to proceed here?

I could also change the representation of GCounter to a vector and prove everything by induction, but then it would be a less computationally efficient, so I'd like to try keeping it an array.

view this post on Zulip Johan Commelin (Feb 03 2021 at 14:42):

We don't have many lemmas about array, so you might have to develop some API to prove things about them.

view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 15:01):

Looking at list, it has a bunch of lemmas about foldl, particularly list.foldl_nil and list.foldl_cons. Perhaps I should try proving analogous lemmas for array with respect to push_back.

view this post on Zulip Yakov Pechersky (Feb 03 2021 at 15:03):

Since the lemmas aren't being used for computation, I would try to convert any g.write or g.read to the equivalent list op. Then you can use the oodles of list API we have

view this post on Zulip Yakov Pechersky (Feb 03 2021 at 15:07):

docs#array.to_list_foldl

view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 15:15):

Thanks! Also, is there a tactic in Lean that could introduce (array.to_list g) as a separate variable so goals would be nicer?

view this post on Zulip Anne Baanen (Feb 03 2021 at 15:19):

Does tactic#generalize work?

view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 15:25):

It introduces the variable, but it doesn't replace the expression with the new variable and rw fails with rewrite tactic failed, motive is not type correct

view this post on Zulip Yakov Pechersky (Feb 03 2021 at 15:54):

There are some annoyances here about heq: docs#array.to_list_to_array

view this post on Zulip Diana Kalinichenko (Feb 03 2021 at 16:32):

Managed to rewrite everything using conv

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:21):

There should be theorems about read-of-write on array

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:22):

docs#array.read_write


Last updated: May 14 2021 at 07:19 UTC