Zulip Chat Archive

Stream: new members

Topic: arrays


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:03):

what are you trying to prove?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:06):

there is no way that IMO said anything about arrays

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:07):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:08):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:09):

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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:10):

finiteness of lists is trivial

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:10):

What do you mean?

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:10):

lists are finite. done

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:11):

There is a theorem about that

view this post on Zulip 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?

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:12):

It is much more array-like.

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:12):

array is just a wrapper around fin n -> A

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:12):

I know.

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:13):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:14):

Well, the sequences describe a certain process.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 12:15):

Why don't you trust the list API?

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:15):

What do you mean by trusting list API?

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:16):

there are theorems about all the things you are talking about

view this post on Zulip Mario Carneiro (Apr 05 2020 at 12:16):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 12:57):

Uff, the foldl parameters are completely reordered.

view this post on Zulip 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?

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:01):

Applying a sequence of steps to a state of lamps.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:01):

Look at the lamp problem (just the statement).

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:02):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:04):

Now, I am trying to rewrite arrays to vectors.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:09):

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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 13:11):

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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 13:11):

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:12):

One can formalise this question entirely in terms of lists.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:22):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:23):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:23):

I guess I will just send you the array version.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:34):

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

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:35):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:35):

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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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,}\{1,2,3,4,\ldots\}

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:41):

I get it, the inside obviously does not matter.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:41):

but

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:54):

I would have everything as lists.

view this post on Zulip Miroslav Olšák (Apr 05 2020 at 13:55):

uff

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:55):

because data.list.basic is 5000 lines long

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 pp elements besides Z/pZ\mathbb{Z}/p\mathbb{Z}?"

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:59):

E(k)E(k)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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