list.perm.trans

Stream: new members

[Marcus Rossel]

I have a question about induction over list.perm that extends a previous one.

How can I prove that a specific list-fold is commutative if that only holds for certain lists?
As a MWE, consider the following:

import data.list.perm

variables {α β : Type*}

def list.is_green : list α → Prop := sorry

def consume (b : β) (a : α) : β := sorry
def consume_list (l : list α) (b : β) : β := list.foldl consume b l

The consume_list function folds over consume and list.is_green property is some property over lists.
The consume function is proven to be commutative given some other condition called its_raining:

def its_raining : Prop := sorry

lemma consume_comm (b : β) (a a' : α) :
its_raining → consume (consume b a) a' = consume (consume b a') a :=
sorry

I would like to show the following:

theorem consume_list_comm (b : β) (l l' : list α) (h_p : l ~ l') :
l.is_green → l'.is_green → consume_list l b = consume_list l' b :=
begin
induction h_p generalizing b,
  case list.perm.nil { sorry }, -- ok
  case list.perm.cons { sorry }, -- ok
  case list.perm.swap { sorry }, -- ok & uses `consume_comm`
  case list.perm.trans {
    -- missing `h_p_l₂.is_green`

  },

That is, given two lists that are green (and permutations of each other), the consume_list function is commutative.
I started by induction on the permutation, which splits into the four cases shown above. I was able to solve the first three, but I have a problem in list.perm.trans.

In order to use induction hypotheses in that case, the intermediate list has to be green. But since the intermediate list is "generated" by the induction tactic, it isn't green.

Is the approach I'm trying (by induction over the permutation) not suitable in this case, or is there some way to have the intermediate list also be green?

Thanks :pray:🏻

[Yakov Pechersky]

Can you prove the following? Does it make sense for your definitions?

theorem green_trans {la lb lc : list α} (ha : la.is_green) (hb : lb.is_green) (hp : la ~ lb) (hp': lb ~ lc) : lc.is_green := sorry

[Marcus Rossel]

Yakov Pechersky said:

Can you prove the following? Does it make sense for your definitions?

theorem green_trans {la lb lc : list α} (ha : la.is_green) (hb : lb.is_green) (hp : la ~ lb) (hp': lb ~ lc) : lc.is_green := sorry

I don't think I can. The is_green property is actually the proposition that a list is topologically sorted.

[Marcus Rossel]

And consume_list_comm should therefore actually be a proof that consume_list behaves the same for all topologically sorted lists.
So the its_raining property actually means that for the two elements a and a' neither a ≤ a' nor a' ≤ a.

[Yakov Pechersky]

Have you tried induction on one of the 'l' generalizing the other?

[Marcus Rossel]

Yakov Pechersky said:

Have you tried induction on one of the 'l' generalizing the other?

I have now, and it seems to be the better path.
Thanks :)

[Yakov Pechersky]

I'll explain how I came to that thought -- you need to somehow show that is_green is the limiting factor in making the commuting work, and that it is some property that is transferred across some permutations. So in your case, you need to abstract out the _other_ l' there, which is a bit more obvious if you had a statement like so:

theorem consume_list_comm (b : β) (l : list α) (hg : is_green l) :
Π (l' : list α), is_green l' → l ~ l' → consume_list l b = consume_list l' b :=
begin
  induction l with hd tl hl,
  sorry,
  sorry
end

[Yakov Pechersky]

Because you don't care about _which_ other l' you're considering. But when you're inducting on the perm, you're making a claim that the way they are related by a permutation is how the theorem is true. Which isn't really the case. The crucial thing to prove here is that is_green (hd :: tl) -> is_green tl