Diana Kalinichenko

Stream: new members

[Diana Kalinichenko]

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]

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]

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

[Diana Kalinichenko]

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]

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]

docs#array.to_list_foldl

[Diana Kalinichenko]

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]

Does tactic#generalize work?

[Diana Kalinichenko]

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]

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

[Diana Kalinichenko]

Managed to rewrite everything using conv

[Mario Carneiro]

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

[Mario Carneiro]

docs#array.read_write