arrays

Stream: new members

[Miroslav Olšák]

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]

what are you trying to prove?

[Mario Carneiro]

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]

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

[Mario Carneiro]

there is no way that IMO said anything about arrays

[Miroslav Olšák]

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

[Miroslav Olšák]

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

[Miroslav Olšák]

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

[Mario Carneiro]

finiteness of lists is trivial

[Miroslav Olšák]

What do you mean?

[Mario Carneiro]

lists are finite. done

[Miroslav Olšák]

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

[Mario Carneiro]

There is a theorem about that

[Miroslav Olšák]

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

[Miroslav Olšák]

It is much more array-like.

[Mario Carneiro]

array is just a wrapper around fin n -> A

[Miroslav Olšák]

I know.

[Mario Carneiro]

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

[Miroslav Olšák]

Well, the sequences describe a certain process.

[Kevin Buzzard]

Why don't you trust the list API?

[Miroslav Olšák]

What do you mean by trusting list API?

[Mario Carneiro]

there are theorems about all the things you are talking about

[Mario Carneiro]

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

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

Uff, the foldl parameters are completely reordered.

[Kevin Buzzard]

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

[Miroslav Olšák]

Applying a sequence of steps to a state of lamps.

[Miroslav Olšák]

Look at the lamp problem (just the statement).

[Miroslav Olšák]

C4 in http://imo-official.org/problems/IMO2008SL.pdf

[Miroslav Olšák]

Now, I am trying to rewrite arrays to vectors.

[Miroslav Olšák]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

One can formalise this question entirely in terms of lists.

[Miroslav Olšák]

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]

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]

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]

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

[Miroslav Olšák]

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

[Miroslav Olšák]

I guess I will just send you the array version.

[Miroslav Olšák]

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]

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]

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

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

I get it, the inside obviously does not matter.

[Miroslav Olšák]

but

[Kevin Buzzard]

@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]

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

[Miroslav Olšák]

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

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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

[Miroslav Olšák]

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

[Kevin Buzzard]

I would have everything as lists.

[Miroslav Olšák]

uff

[Kevin Buzzard]

because data.list.basic is 5000 lines long

[Miroslav Olšák]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

$E(k)$

[Mario Carneiro]

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]

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]

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)