## Stream: new members

### Topic: arrays

#### Miroslav Olšák (Apr 05 2020 at 12:02):

Is it just my impression, or the theory around arrays is not much developed yet? Or is there some modern replacement of arrays? I wanted to prove that array.foldl has certain value by exact description of the values during the folding process. I concluded that I would need a lemma like foldl_inits_eq in the following code

def array.simple_take (a : array n α) (m : nat) (h : m ≤ n) : array m α :=
⟨λ i : fin m, a.read ⟨i.val, lt_of_lt_of_le i.is_lt h⟩⟩
def foldl_inits (a : array n α) (b : β) (f : α → β → β) (k : ℕ) (h : k ≤ n) : β
:= (a.simple_take k h).foldl b f
lemma foldl_inits_eq
(a : array n α) (b : β) (f : α → β → β) (f2 : Π (k : ℕ), k ≤ n → β)
: f2 0 bot_le = b →
(∀ i : fin n,
f2 i.val.succ i.is_lt = f (a.read i) (f2 i.val (le_of_lt i.is_lt))) →
f2 = foldl_inits a b f


(note I use my own array.simple_take instead of array.take just because it is easier to handle in proofs).
I almost managed to prove it up to a lemma

lemma fold_step (a1 : array n α) (a2 : array n.succ α) (b : β) (f : α → β → β)
: (∀ i : fin n, a1.read i = a2.read ⟨i, nat.lt.step i.is_lt⟩) →
a2.foldl b f = f (a2.read ⟨n, lt_add_one n⟩) (a1.foldl b f)
:=
begin
intros,
sorry
end


I guess I need to analyze the cases of d_array.iterate_aux, but I am not sure how to do that. Or would it be easier to prove foldl_inits_eq through lists?

#### Mario Carneiro (Apr 05 2020 at 12:03):

what are you trying to prove?

#### Mario Carneiro (Apr 05 2020 at 12:04):

working with arrays is somewhat painful due to all the dependencies and mutable state. If you can recast the theorem in terms of lists it will be easier to prove

#### Miroslav Olšák (Apr 05 2020 at 12:06):

From the higher perspective, still the IMO problem about lamps, C4 in http://imo-official.org/problems/IMO2008SL.pdf

#### Mario Carneiro (Apr 05 2020 at 12:06):

there is no way that IMO said anything about arrays

#### Miroslav Olšák (Apr 05 2020 at 12:07):

Well, it counts sequences of certain lengths that satisfy certain properties.

#### Miroslav Olšák (Apr 05 2020 at 12:08):

So I interpretted them as arrays and counted them with fintype.card

#### Miroslav Olšák (Apr 05 2020 at 12:09):

Which is harder with lists where proving finiteness would be more challenging, I guess.

#### Mario Carneiro (Apr 05 2020 at 12:10):

finiteness of lists is trivial

#### Miroslav Olšák (Apr 05 2020 at 12:10):

What do you mean?

#### Mario Carneiro (Apr 05 2020 at 12:10):

lists are finite. done

#### Miroslav Olšák (Apr 05 2020 at 12:11):

I mean that the number of all lists of certain length is finite (if the original type is also finite)

#### Mario Carneiro (Apr 05 2020 at 12:11):

There is a theorem about that

#### Miroslav Olšák (Apr 05 2020 at 12:12):

But why would I use lists anyway, when the problem discusses only sequences of fixed length?

#### Miroslav Olšák (Apr 05 2020 at 12:12):

It is much more array-like.

#### Mario Carneiro (Apr 05 2020 at 12:12):

array is just a wrapper around fin n -> A

I know.

#### Mario Carneiro (Apr 05 2020 at 12:13):

What representation is best depends on what you need to prove about them

#### Miroslav Olšák (Apr 05 2020 at 12:14):

Well, the sequences describe a certain process.

#### Kevin Buzzard (Apr 05 2020 at 12:15):

Why don't you trust the list API?

#### Miroslav Olšák (Apr 05 2020 at 12:15):

What do you mean by trusting list API?

#### Mario Carneiro (Apr 05 2020 at 12:16):

there are theorems about all the things you are talking about

#### Mario Carneiro (Apr 05 2020 at 12:16):

if you want fixed length, just assert length l = n

#### Miroslav Olšák (Apr 05 2020 at 12:16):

Do I understand correctly that you would recommend using lists because they are more developed, even for fixed-size sequences?

#### Kevin Buzzard (Apr 05 2020 at 12:16):

Or maybe you could make a better array API. Remember though that this is different to programming. It doesn't matter if the implementation is inefficient from the point of view of computer science because you're reasoning about the code, not running it

#### Mario Carneiro (Apr 05 2020 at 12:17):

you know that vector A n is just a pair of a list and a proof that it has length n

#### Mario Carneiro (Apr 05 2020 at 12:18):

array is really geared towards efficient algorithms, so many of the functions are unnaturally limited like map : (A -> A) -> array A n -> array A n

#### Kevin Buzzard (Apr 05 2020 at 12:43):

Miroslav Olšák said:

What do you mean by trusting list API?

I mean that data.list.basic contains 1000 theorems about lists including probably everything you want.

#### Miroslav Olšák (Apr 05 2020 at 12:57):

Uff, the foldl parameters are completely reordered.

#### Kevin Buzzard (Apr 05 2020 at 12:58):

I've done a ton of mathematics in Lean and I've never once looked at foldl. What are you doing?

#### Miroslav Olšák (Apr 05 2020 at 13:01):

Applying a sequence of steps to a state of lamps.

#### Miroslav Olšák (Apr 05 2020 at 13:01):

Look at the lamp problem (just the statement).

#### Miroslav Olšák (Apr 05 2020 at 13:04):

Now, I am trying to rewrite arrays to vectors.

#### Miroslav Olšák (Apr 05 2020 at 13:09):

It seems that vectors does not support has_mem, which is inconvenient.

#### Mario Carneiro (Apr 05 2020 at 13:11):

you can write a \in v.1, but what do you need it for?

#### Mario Carneiro (Apr 05 2020 at 13:11):

use list.count to find out how many lights are on

#### Kevin Buzzard (Apr 05 2020 at 13:12):

One can formalise this question entirely in terms of lists.

#### Miroslav Olšák (Apr 05 2020 at 13:17):

I used ∈ for a condition on the M-sequences that every switch is below n.

def is_M_seq {n k : ℕ} (seq : lamp_switch_seq n k) : Prop
:= is_N_seq seq ∧ ∀ l ∈ seq, (l : ℕ) < n


#### Miroslav Olšák (Apr 05 2020 at 13:18):

I defined it as

instance (n k : ℕ) : has_mem (fin (n+n)) (lamp_switch_seq n k)
:= ⟨λ (i : fin (n+n)) (seq : lamp_switch_seq n k), i ∈ seq.val⟩


but the inconvience is that such cross-type manipulations are usually not so well supported by the library.

#### Miroslav Olšák (Apr 05 2020 at 13:22):

For example, with arrays, I could define the sequence by a function, and then immediatelly deduce ∃ si, seq.read si = l from l ∈ seq. Now I can similarly create a vector from a function using vector.of_fn but the same deduction will take me some time.

#### Kevin Buzzard (Apr 05 2020 at 13:22):

Why don't you post your full formalisation of the question?

#### Miroslav Olšák (Apr 05 2020 at 13:23):

Now it is complicated, I am in the middle of rewriting arrays to vectors.

#### Miroslav Olšák (Apr 05 2020 at 13:23):

I guess I will just send you the array version.

#### Miroslav Olšák (Apr 05 2020 at 13:28):

The partial formalisation using arrays: https://github.com/mirefek/my-lean-experiments/blob/master/lamps_array.lean
Attempt to prove something about array.foldl: https://github.com/mirefek/my-lean-experiments/blob/master/array_fold.lean

#### Kevin Buzzard (Apr 05 2020 at 13:31):

Yeah this is going to be hard to do with array I suspect. array is a type written for computer scientists, it seems to me -- it shows up a bunch in meta code. You need a type which is optimised for proving, not computing.

#### Miroslav Olšák (Apr 05 2020 at 13:34):

Well, interpretting a fixed-size sequence as a function is in my opinion mathematical enough.

#### Miroslav Olšák (Apr 05 2020 at 13:35):

I like it more than some inductive construction of it :-).

#### Kevin Buzzard (Apr 05 2020 at 13:35):

Right but there is a non-mathematical issue as well, which is whether you should use a type optimised for computing or one optimised for proving, if you are going to write a proof.

#### Kevin Buzzard (Apr 05 2020 at 13:35):

This is an implementation issue which mathematicians do not normally have to deal with.

#### Kevin Buzzard (Apr 05 2020 at 13:36):

If you want to prove stuff by induction you should use nat. But if you want to prove 100000+200000=300000 then nat is a disaster because internally it's represented as some super-inefficient linked list or something.

#### Kevin Buzzard (Apr 05 2020 at 13:37):

Conversely binary nats, namely pos_num (check out the definition) are super-efficient for doing arithmetic, but the moment you try and prove something by induction on them you find that your induction principle is "if it's true for n then you need to prove it for 2n and 2n+1"

#### Kevin Buzzard (Apr 05 2020 at 13:37):

However as a mathematician you can't tell the difference between pos_num and pnat because they're both $\{1,2,3,4,\ldots\}$

#### Kevin Buzzard (Apr 05 2020 at 13:39):

If you are proving theorems then you should not be thinking at all about the definition of the structure, you should be thinking about what API is available, and the API will depend on (a) how much people have worked on it and (b) how easy it is to prove things about the object.

#### Kevin Buzzard (Apr 05 2020 at 13:40):

The fact that you don't like some inductive construction of something should be irrelevant. What matters is not the definition of the thing, what matters is the API for the thing. If you formalise the question in terms of arrays for some spurious reason then you are in trouble when you realise that there are no theorems in the API for arrays because they weren't designed to prove theorems.

#### Miroslav Olšák (Apr 05 2020 at 13:41):

I get it, the inside obviously does not matter.

but

#### Kevin Buzzard (Apr 05 2020 at 13:42):

@Floris van Doorn how would you formalise these statements? There's this thread and there's this one. Miroslav might have an easier time formalising the proofs if a Lean expert formalised the statements.

#### Miroslav Olšák (Apr 05 2020 at 13:44):

but it makes sense to have the size inside the type in my case (so rather vector that list)

#### Miroslav Olšák (Apr 05 2020 at 13:45):

In one case, I wanted to quantify over all elements of the vector, but vector does not support has_mem

#### Miroslav Olšák (Apr 05 2020 at 13:46):

it is convenient to give a description of the sequence using function (there is vector.of_fn, that is fine)

#### Kevin Buzzard (Apr 05 2020 at 13:49):

I know you are focussed on the fact that these lists all have the same size, but the size of the list is k which is a variable. So you can formalise a statement about a variable k and then a vector v whose length is k. Or you can just formalise a statement about a list. If the vectors all had length 3 I would understand your point of view.

#### Miroslav Olšák (Apr 05 2020 at 13:50):

It feels to me that each of the structures lacks a bit of the interface for proving.

#### Miroslav Olšák (Apr 05 2020 at 13:53):

So you would have lamp_state as vectors, and lamp_switch_seq primarily as a list?

#### Kevin Buzzard (Apr 05 2020 at 13:54):

I would have everything as lists.

uff

#### Kevin Buzzard (Apr 05 2020 at 13:55):

because data.list.basic is 5000 lines long

#### Miroslav Olšák (Apr 05 2020 at 13:56):

Yes, it is highly a developed structure, just not the one suitable for the task :-D.

#### Kevin Buzzard (Apr 05 2020 at 13:57):

I think you don't have a good understanding of what being suitable for the task means in the context of theorem proving. But I might be wrong. That's why I'd be interested in Floris' opinion.

#### Miroslav Olšák (Apr 05 2020 at 13:58):

I accept that vectors might be better. Alright, let's see what an expert thinks about it.

#### Reid Barton (Apr 05 2020 at 13:58):

This conversation reminds me of when I was at a cryptography talk and the speaker said something like "so what's another group with $p$ elements besides $\mathbb{Z}/p\mathbb{Z}$?"

#### Kevin Buzzard (Apr 05 2020 at 13:59):

$E(k)$

#### Mario Carneiro (Apr 05 2020 at 14:25):

Here's one way to state the problem:

import logic.function
import data.fintype.basic

def list.chain'' {α} (R : α → α → Prop) : (α → Prop) → list α → α → Prop
| P [] a := P a
| P (a::l) b := P a ∧ list.chain'' (R a) l b

def flip_one {α} [decidable_eq α] (f : α → bool) (i : α) : α → bool :=
function.update f i (bnot (f i))

def admissible {α} [decidable_eq α] (f g : α → bool) : Prop :=
∃ i, g = flip_one f i

def restricted_admissible {α} [decidable_eq α] (f g : α ⊕ α → bool) : Prop :=
∃ i, g = flip_one f (sum.inl i)

def end_state {α} : α ⊕ α → bool
| (sum.inl _) := tt
| (sum.inr _) := ff

def lamp_seq {α} (R : ∀ (f g : α ⊕ α → bool), Prop) (l : list (α ⊕ α → bool)) : Prop :=
list.chain'' R (λ s, end_state = s) l (λ _, ff)

open_locale classical
theorem C4 {α} [fintype α] [decidable_eq α] (k n : ℕ)
(h1 : 2 ∣ k + n) (h2 : n ≤ k) (h3 : fintype.card α = n) :
fintype.card {f : vector (α ⊕ α → bool) k // lamp_seq admissible f.1} =
2 ^ (k - n) *
fintype.card {f : vector (α ⊕ α → bool) k // lamp_seq restricted_admissible f.1} :=
sorry


#### Miroslav Olšák (Apr 06 2020 at 00:22):

How would you prove something about the list.chain''? For example that if n = k, then there exist an admissible sequence (simply switch n-th lamp in n-th step).

#### Mario Carneiro (Apr 06 2020 at 01:31):

theorem list.chain''_imp₂ {α} {R R' : α → α → Prop}
(h₁ : ∀ a b, R a b → R' a b) :
∀ {P P' : α → Prop}, (∀ a, P a → P' a) →
∀ {l b}, list.chain'' R P l b → list.chain'' R' P' l b
| P P' hP [] a := hP a
| P P' hP (a::l) b := and.imp (hP a) (list.chain''_imp₂ (h₁ a))

theorem admissible_of_restricted {α} [decidable_eq α] (f g : α ⊕ α → bool) :
restricted_admissible f g → admissible f g
| ⟨i, h⟩ := ⟨_, h⟩

theorem exists_admissible_finset {α} [decidable_eq α] (s : finset α) :
∃ l : list (α ⊕ α → bool), l.length = s.card ∧
list.chain'' restricted_admissible
(eq (sum.elim (λ a, a ∈ s) (λ _, ff)))
l (λ _, ff) :=
begin
apply finset.induction_on s; simp,
{ refine ⟨[], rfl, _⟩, funext i, cases i; refl },
{ intros a s hs l e IH,
refine ⟨_::l, _, rfl, list.chain''_imp₂ (λ _ _, id) _ IH⟩,
{ rw [finset.card_insert_of_not_mem hs, ← e], refl },
{ rintro _ rfl, use a,
funext i, cases i; [simp, refl],
rw [flip_one, function.update],
split_ifs; simp at h ⊢; simp [hs, h] } }
end

theorem exists_restricted_admissible {α} [decidable_eq α] [fintype α]
{n} (h : fintype.card α = n) :
∃ f : vector (α ⊕ α → bool) n, lamp_seq restricted_admissible f.1 :=
begin
obtain ⟨l, e, hl⟩ := exists_admissible_finset (@finset.univ α _),
refine ⟨⟨_, e.trans h⟩, list.chain''_imp₂ (λ _ _, id) _ hl⟩,
rintro _ rfl, funext i; cases i; simp [end_state],
end

theorem exists_admissible {α} [decidable_eq α] [fintype α]
{n} (h : fintype.card α = n) :
∃ f : vector (α ⊕ α → bool) n, lamp_seq admissible f.1 :=
(exists_restricted_admissible h).imp \$ λ f,
list.chain''_imp₂ admissible_of_restricted (λ _, id)


Last updated: May 14 2021 at 06:16 UTC