Add Properties of List actions on Bools

[Taneb]

I'm not sure of the name for and-locate and or-locate, but they're the whole reason I ended up making this PR...

[jamesmckinna]

It looks as though I added a note to Data.Bool.ListAction suggesting it be refactored to make use of https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Effectful/Foldable.agda but I no longer entirely remember what I had had in mind!

Would it be better to refactor this PR to make use of the properties defined there? And perhaps to do that prior refactoring?

[JacquesCarette]

I'm okay with and-locate and or-locate. But definitely most of these properties are true more generally (of [commutative] monoid folds), with the locate property being of monoids with a 'zero' element.

I would probably be fine with adding these as-is, and refactoring later when more general proofs exist.

[jamesmckinna]

I'm okay with and-locate and or-locate. But definitely most of these properties are true more generally (of [commutative] monoid folds), with the locate property being of monoids with a 'zero' element.

I would probably be fine with adding these as-is, and refactoring later when more general proofs exist.

Fine by me.

FTR, I think that the converse directions to the locate lemmas follow from having a zero element, but these lemmas further require that the monoid operation be Conical wrt that zero?

[Taneb]

Yes, it requires there are no "zero divisors" in the monoid, which is not the case in, for example, the monoid of integers modulo 6 under multiplication, where 2 * 3 = 0

[jamesmckinna]

Add a CHANGELOG and you'll be good to go.

[jamesmckinna]

OK, so I experimented with my proposed refactoring, and surprise surprise not all was plain sailing...

• Data.Bool.Properties doesn't export any (obvious!) definitions of ∧-monoid, ∨-monoid, so the ++-homo theorem isn't directly applicable... (groan)
• there is some more plumbing to do to ensure that foldr and foldMap id are appropriately correctly identified, so that the theorem, even if applicable, actually returns the correct result definitionally... (sigh)
• I must at some point have run of steam refactoring Permutation with the result that the appeal to foldr-commMonoid itself requires so much extraneous additional plumbing to apply... (bewilderment)

So I'll write a cut-down review, and then let's merge this as-is, and figure out the mess afterwards!

[jamesmckinna]

All but the CHANGELOG typo are optional.

But my general meta-comment for the library going forward ought perhaps to be that we try to 'take the high road', ie. reuse all the abstraction machinery we have developed, rather than taking the 'low' road of proving things directly by pattern-matching, which otherwise is too 'easy'/'tempting' in cases like these?

[jamesmckinna]

This (morally) should have the proof and-++ bs cs = ++-homo ∧-monoid id bs {cs} but doesn't, for reasons given.

[jamesmckinna]

These two however, should be rewritten in terms of Data.List.Properties.foldr-map, given the definition of all as a foldr (and) followed by a map? Or is the ergonomics of doing such similarly too tortured to be worth the effort?

[Taneb]

This was my best effort:

∨-distribˡ-and : ∀ b cs → b ∨ and cs ≡ all (b ∨_) cs
∨-distribˡ-and b cs = begin
  b ∨ foldr _∧_ true cs                ≡⟨ foldr-fusion (b ∨_) true (∨-distribˡ-∧ b) cs ⟩
  foldr (b ∨_ -⟨ _∧_ ∣) (b ∨ true) cs  ≡⟨ foldr-map _∧_ (b ∨_) (b ∨ true) cs ⟨
  foldr _∧_ (b ∨ true) (map (b ∨_) cs) ≡⟨ cong (λ e → foldr _∧_ e (map (b ∨_) cs)) (∨-zeroʳ b) ⟩
  foldr _∧_ true (map (b ∨_) cs)       ∎
  where open ≡-Reasoning

I personally don't think it's worth it, but maybe I'm missing a trick

[jamesmckinna]

Maybe you're right... I managed

∨-distribˡ-and b cs = begin
  b ∨ and cs            ≡⟨ foldr-fusion (b ∨_) true (∨-distribˡ-∧ b) cs ⟩
  foldr g (b ∨ true) cs ≡⟨ foldr-cong (λ _ _ → refl) (∨-zeroʳ b) cs ⟩
  foldr g true cs       ≡⟨ foldr-map _∧_  (b ∨_) true cs ⟨
  all (b ∨_) cs         ∎
  where
  open ≡-Reasoning
  g : Bool → Bool → Bool
  g z = (b ∨ z) ∧_

which isn't much better, but is more 'abstract'?

I won't fight you for this though!

[jamesmckinna]

Ditto. or-++ bs cs = ++-homo ∨-monoid id bs {cs}, or... should be, modulo blah blah blah.

[jamesmckinna]

Ditto. foldr-map instances?

[Taneb]

Data.Bool.Properties doesn't export any (obvious!) definitions of ∧-monoid, ∨-monoid, so the ++-homo theorem isn't directly applicable... (groan)

That's a serious omission that should definitely be fixed!

Requested changes have now been made, so I can approve.

[jamesmckinna]

All fine by me now, and I think the one approval should suffice!

[jamesmckinna]

A last thought here, but one which should perhaps be revisited: we define all resp. any in terms of and resp. or, but what if we did it the other way round?