Zulip Chat Archive

Stream: new members

Topic: Diana Kalinichenko

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!

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.

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.

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.

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

Yakov Pechersky (Feb 03 2021 at 15:07):


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?

Anne Baanen (Feb 03 2021 at 15:19):

Does tactic#generalize work?

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

Yakov Pechersky (Feb 03 2021 at 15:54):

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

Diana Kalinichenko (Feb 03 2021 at 16:32):

Managed to rewrite everything using conv

Mario Carneiro (Feb 03 2021 at 17:21):

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

Mario Carneiro (Feb 03 2021 at 17:22):


Last updated: Dec 20 2023 at 11:08 UTC