Commutativity of Recursive Application

Stream: new members

[Marcus Rossel]

I have a function that recursively applies a commutative operation and would like to show that this recursive application is also commutative.
Here's an analogous example:

structure bucket := (content : ℕ)

def pour (c : ℕ) (b : bucket) : bucket := {content := b.content + c}

lemma pour_comm (c c' : ℕ) (b : bucket) :
pour c (pour c' b) = pour c' (pour c b) :=
sorry

def pour_list : list ℕ → bucket → bucket
| [] b := b
| (hd :: tl) b := pour_list tl (pour hd b)

theorem pour_list_comm (cs cs' : list ℕ) (b : bucket) :
pour_list cs (pour_list cs' b) = pour_list cs' (pour_list cs b) :=
begin
  --?
end

The target of the operation is a bucket. Doing a single pour is proven to be commutative. I would like to show that pour_list is also commutative.
Is there a neat way of proving this?
Thanks

[Yakov Pechersky]

structure bucket := (content : ℕ)

def pour (c : ℕ) (b : bucket) : bucket := {content := b.content + c}

lemma pour_comm (c c' : ℕ) (b : bucket) :
  pour c (pour c' b) = pour c' (pour c b) :=
sorry

def pour_list : list ℕ → bucket → bucket
| [] b := b
| (hd :: tl) b := pour_list tl (pour hd b)

lemma pour_list_comm_singleton (cs : list ℕ) (c : ℕ) (b : bucket) :
  pour_list cs (pour c b) = pour c (pour_list cs b) :=
begin
  induction cs with hd tl hl generalizing b,
  { simp [pour_list] },
  { simp [pour_list, hl, pour_comm] }
end

theorem pour_list_comm (cs cs' : list ℕ) (b : bucket) :
  pour_list cs (pour_list cs' b) = pour_list cs' (pour_list cs b) :=
begin
  induction cs' with hd tl hl generalizing cs b,
  { simp [pour_list] },
  { simp [pour_list, pour_list_comm_singleton, hl] }
end

[Yakov Pechersky]

I had to prove the simpler pour_list_comm_singleton first.

[Yakov Pechersky]

You might like the is_commutative Prop

[Yakov Pechersky]

Although that operation is limited to things that are all in the same type. I think Kevin remarked on this at some point (or for is_associative).

[Marcus Rossel]

Thanks for your feedback @Yakov Pechersky! Unfortunately I noticed that the example I gave above was actually a bit weaker than what I'm trying to prove. What I actually want to prove is that if I pass two lists to pour_list where one is just a permutation of the other, the results stay the same. So:

import data.list.perm

structure bucket := (content : ℕ)

def pour (c : ℕ) (b : bucket) : bucket := {content := b.content + c}

lemma pour_comm (c c' : ℕ) (b : bucket) :
pour c (pour c' b) = pour c' (pour c b) :=
sorry

def pour_list : list ℕ → bucket → bucket
| [] b := b
| (hd :: tl) b := pour_list tl (pour hd b)

theorem pour_list_comm (cs cs' : list ℕ) (h : cs ~ cs') (b : bucket) :
pour_list cs b = pour_list cs' b :=
begin
  --?
end

[Yakov Pechersky]

Do you know that your pour is associative too?

[Marcus Rossel]

Yakov Pechersky said:

Although that operation is limited to things that are all in the same type. I think Kevin remarked on this at some point (or for is_associative).

Yeah, there's right_commutative and left_commutative to work around that.

[Marcus Rossel]

Yakov Pechersky said:

Do you know that your pour is associative too?

Yes it is :)

[Yakov Pechersky]

Can you show that?

[Marcus Rossel]

Yakov Pechersky said:

Can you show that?

Yeah, I think I could come up with a proof of that.

[Marcus Rossel]

Ok, I guess I got ahead of myself there. How would associativity work for a function whose output type is not the same as its input type?

[Yakov Pechersky]

Right.

[Kyle Miller]

Here's a sort of cheating way to prove pour_list_comm:

import data.list.perm

@[ext]
structure bucket := (content : ℕ)

def pour (c : ℕ) (b : bucket) : bucket := {content := b.content + c}

lemma pour_comm (c c' : ℕ) (b : bucket) :
  pour c (pour c' b) = pour c' (pour c b) :=
bucket.ext _ _ (by { simp [pour, add_comm, add_left_comm] })

def pour_list : list ℕ → bucket → bucket
| [] b := b
| (hd :: tl) b := pour_list tl (pour hd b)

lemma pour_list_eq (cs : list ℕ) (b : bucket) : pour_list cs b = pour cs.sum b :=
begin
  induction cs generalizing b,
  { cases b, simp [pour_list, pour], },
  { dsimp [pour_list], rw cs_ih,
    simp [pour, add_comm, add_left_comm], },
end

theorem pour_list_comm (cs cs' : list ℕ) (h : cs ~ cs') (b : bucket) :
  pour_list cs b = pour_list cs' b :=
by simp [pour_list_eq, list.perm.sum_eq h]

[Marcus Rossel]

I've gotten to the point in the proof where the remaining goal is:

⊢ pour_list (pour b hd) (cs'.erase hd) = pour_list b cs'

(where hd is the head of cs') but I don't know if I took the right path, or how to continue from here.

[Eric Wieser]

Can you just use multiset.foldr directly here?

[Eric Wieser]

If you've proven docs#left_commutative then it will do the rest of the work for you

[Marcus Rossel]

Eric Wieser said:

Can you just use multiset.foldr directly here?

You mean instead of the inductive definition over a list?

[Eric Wieser]

Yes

[Marcus Rossel]

Yeah, I could do that. How would I get the commutativity of foldr then?

[Eric Wieser]

Ah, you want docs#list.perm.foldr_eq

[Eric Wieser]

multiset not needed

[Marcus Rossel]

wow, list has fold too :D

[Eric Wieser]

If you insist on your inductive definition, then you could hopefully prove very easily that it's equal to a fold

[Marcus Rossel]

Nah, fold is perfect.
Thanks everybody! I think I'll be able to get it from here :)

[Yakov Pechersky]

Yeah, pour_list is best defined as a foldr

[Marcus Rossel]

Marcus Rossel said:

Nah, fold is perfect.
Thanks everybody! I think I'll be able to get it from here :)

Well bummer, I'm not able to get it from here ^^
There's a constraint on the commutativity of my pour function, that's giving me a hard time extending the commutativity to pour_list.

Let's say the commutativity of pour depends on a belongs_to property:

import data.list.perm

structure bucket := (content : ℕ)

def pour (c : ℕ) (b : bucket) : bucket := {content := b.content + c}

def belongs_to (c : ℕ) (b : bucket) : Prop := sorry

lemma pour_comm (c c' : ℕ) (b : bucket) (h : belongs_to c b) (h' : belongs_to c' b) :
pour c (pour c' b) = pour c' (pour c b) :=
sorry

def pour_list : bucket → list ℕ → bucket := list.foldr pour

theorem pour_list_comm (cs cs' : list ℕ) (h : cs ~ cs') (b : bucket) (h_b : ∀ x ∈ cs, belongs_to x b) (h_b' : ∀ x' ∈ cs', belongs_to x' b) :
pour_list b cs' = pour_list b cs' :=
begin
  -- Can't just use `list.perm.foldr_eq` here ...
end

Using list.perm.foldr_eq or list.perm.foldr_eq' in the proof of the theorem doesn't work anymore, because the commutativity of pour doesn't hold for all cs. But assuming that all of the elements in cs and cs' do have that property (required by h_b and h_b'), is there a way to show that pour_list is the same for permutations?

[Mario Carneiro]

Do you know belongs_to c (pour c' b)? Otherwise that theorem looks difficult to apply

[Mario Carneiro]

in fact I'm not even sure it's true for three elements

[Mario Carneiro]

import data.list.perm
inductive bucket
| zero
| one
| two
| three (c : ℕ)

def pour (c : ℕ) : bucket → bucket
| bucket.zero := bucket.one
| bucket.one := bucket.two
| _ := bucket.three c

def belongs_to (c : ℕ) (b : bucket) := b = bucket.zero

lemma pour_comm (c c' : ℕ) (b : bucket) (h : belongs_to c b) (h' : belongs_to c' b) :
  pour c (pour c' b) = pour c' (pour c b) :=
by {cases h, cases h', refl}

def pour_list : bucket → list ℕ → bucket := list.foldr pour

theorem pour_list_comm : ¬ ∀ (cs cs' : list ℕ) (h : cs ~ cs') (b : bucket)
  (h_b : ∀ x ∈ cs, belongs_to x b) (h_b' : ∀ x' ∈ cs', belongs_to x' b),
  pour_list b cs = pour_list b cs' :=
begin
  intro H,
  cases H [1, 0, 0] [0, 1, 0] dec_trivial bucket.zero (λ _ _, rfl) (λ _ _, rfl),
end

[Mario Carneiro]

However if you assume that belongs_to is closed under pour then it is true:

import data.list.perm
def bucket : Type := sorry
def pour : ∀ (c : ℕ), bucket → bucket := sorry
def belongs_to : ∀ (c : ℕ) (b : bucket), Prop := sorry
lemma belongs_to.pour {c c' : ℕ} {b : bucket} :
  belongs_to c b → belongs_to c' b → belongs_to c (pour c' b) := sorry

lemma pour_comm {c c' : ℕ} {b : bucket} (h : belongs_to c b) (h' : belongs_to c' b) :
  pour c (pour c' b) = pour c' (pour c b) := sorry

def pour_list : bucket → list ℕ → bucket := list.foldr pour

theorem belongs_to.pour_list {c} {cs : list ℕ} {b : bucket}
  (hc : belongs_to c b) (hcs : ∀ x' ∈ cs, belongs_to x' b) :
  belongs_to c (pour_list b cs) :=
begin
  induction cs generalizing c,
  { exact hc },
  { cases list.forall_mem_cons.1 hcs with h1 h2,
    exact belongs_to.pour (cs_ih h2 hc) (cs_ih h2 h1) }
end

theorem pour_list_comm (cs cs' : list ℕ) (h : cs ~ cs') (b : bucket)
  (h_b : ∀ x ∈ cs, belongs_to x b) (h_b' : ∀ x' ∈ cs', belongs_to x' b) :
  pour_list b cs = pour_list b cs' :=
begin
  simp [pour_list],
  induction h,
  { refl },
  case list.perm.cons : _ _ _ _ IH {
    simp [list.foldr], rw IH (list.forall_mem_cons.1 h_b).2 (list.forall_mem_cons.1 h_b').2 },
  case list.perm.swap {
    simp [list.foldr],
    rw [list.forall_mem_cons, list.forall_mem_cons] at h_b,
    rcases h_b with ⟨h1, h2, h3⟩,
    exact pour_comm (belongs_to.pour_list h1 h3) (belongs_to.pour_list h2 h3) },
  case list.perm.trans : l1 l2 l3 p1 p2 IH1 IH2 {
    have hc := λ x h, h_b x (p1.mem_iff.2 h),
    exact (IH1 h_b hc).trans (IH2 hc h_b') }
end

[Marcus Rossel]

Wow, thanks @Mario Carneiro! The "belongs_to is closed under pour"-part and the special induction for list.perm was what I was missing.