list (list bool) --> list bool

Stream: new members

[Damiano Testa]

Dear All,

I would like to convert a list (list bool) to a single list bool, by taking the "componentwise or of the entries". (I happen to know that all the inner lists of bools have the same length). I found that list.map₂ (∨) does the right thing, with input two separate lists. I would like to iterate this on the whole list. I could probably write it myself, but I also imagine that this already exists!

Thanks!

[Eric Wieser]

by library_search?

[Eric Wieser]

I think this is docs#list.join

[Damiano Testa]

with library_search, I find:

example (ll : list (list bool)) : list bool := list.nil

[Eric Wieser]

Does it behave any better with ll on the right of the colon?

[Damiano Testa]

What I want is some iteration of currying and list.map₂ (∨).

[Damiano Testa]

example : list (list bool) →  list bool := list.join

!

[Damiano Testa]

Ok, maybe it just is not there. It is easy enough to instruct lean what to do anyway. Thanks!

[Eric Wieser]

What output do you want for nil?

[Damiano Testa]

I am not sure that I care...

[Damiano Testa]

probably tt.

[Damiano Testa]

or rather, [tt]

[Johan Commelin]

@Damiano Testa So you want to docs#list.foldr list.map\2, I guess?

[Eric Wieser]

I think the behavior might be easier to reason about if your type was list (vector n X), then the output for nil would be obvious (repeat ff n)

[Damiano Testa]

actually, I think that I want [ff]. But I really do not care: I want to scan the output for tt. Also [] woudl work for me.

[Damiano Testa]

Ah, Johan, this looks promising!! Thanks!

[Johan Commelin]

Another option is to transpose the list of lists first, and then use docs#list.any [edit: was docs#bool.any]

[Johan Commelin]

I think you can use the fact that lists is a docs#traversable

[Eric Wieser]

(it doesn't exist)

[Eric Wieser]

Also, transposing nil : list (list X) is ill-defined (it's a 0 × n list, but n is unknown)

[Johan Commelin]

docs#list.any does!

[Yaël Dillies]

list.map list.any

[Yaël Dillies]

The idea is that you're doing a component-wise operation, so start with list.map. Then you want to take a bunch of or, so list.any.

[Yaël Dillies]

Oh, do you want to take the ors across the lists rather than within each list?

[Kyle Miller]

Why were we against transposing?

def zip_or (ll : list (list bool)) : list bool := ll.transpose.map list.bor

[Yaël Dillies]

No idea, that got me confused too.

[Kyle Miller]

zip_or [] evaluates to [], which is sensible.

[Kyle Miller]

"zip" isn't quite the right name. I was thinking about the Python zip(*ll) idiom for taking transposes, where zip(l1, l2, l3, ..., ln) creates a list of length-n tuples using the entries of the lists, and star notation means "take all the entries of ll as arguments to zip".

[Johan Commelin]

Kyle Miller said:

Why were we against transposing?

I don't think anybody was against transposing. I think @Eric Wieser's :thumbs_down: was indicating that a docs#foobar didn't give a result.

[Yaël Dillies]

Eric Wieser said:

Also, transposing nil : list (list X) is ill-defined (it's a 0 × n list, but n is unknown)

This looked like being against :point_up:

[Damiano Testa]

Sorry, I had a small emergency with my cat, now resolved! Let me get up to speed!

[Patrick Johnson]

Kyle Miller said:

zip_or [] evaluates to [], which is sensible.

If we know what the length of each inner list is supposed to be, we can handle the nil case in a special way:

def f : Π (n : ℕ) (s : list (list bool))
  (h : ∀ (e : list bool), e ∈ s → e.length = n), list bool
| n [] _ := list.repeat ff n
| _ s _ := s.transpose.map list.bor

[Patrick Johnson]

Assumption h is redundant, it's there for safety.

def f : Π (n : ℕ) (s : list (list bool)), list bool
| n [] := list.repeat ff n
| _ s := s.transpose.map list.bor

[Damiano Testa]

Thank you all! I'll go with Kyle's

def zip_or (ll : list (list bool)) : list bool := ll.transpose.map list.bor

but I won't need to actually make the definition. This is for reporting errors and I simply want to make sure that every input is being used. Thus, I just want to know whether an entry is tt, standing for "is unused", or ff, standing for "is not unused".

[Eric Wieser]

Yaël Dillies said:

Eric Wieser said:

Also, transposing nil : list (list X) is ill-defined (it's a 0 × n list, but n is unknown)

This looked like being against :point_up:

This is more an objection against the phrasing of the question in general, not the solution to it. Transposing list (list X) has tripped me up multiple times in python on the empty list; usually it's an indication that your datatype is wrong. I assume docs#list.transpose sends it to the empty list?