Zulip Chat Archive

Stream: new members

Topic: permutation


view this post on Zulip Nam (Apr 22 2020 at 06:18):

this lemma about permutation reads very simple, but i have a hard time proving it. could someone give me a hint?

inductive permuted : list  -> list  -> Prop
| nil {} : permuted [] []
| skip {x : } {l l' : list } : permuted l l' -> permuted (x::l) (x::l')
| swap {x y : } {l : list } : permuted (y::x::l) (x::y::l)
| trans {l l' l'' : list } : permuted l l' -> permuted l' l'' -> permuted l l''

lemma cons_to_a_permutation
    {pre suf tail : list } {head : }
    (h : permuted tail (pre ++ suf))
    : permuted (head :: tail) (pre ++ head :: suf) :=
begin
  sorry
end

view this post on Zulip Mario Carneiro (Apr 22 2020 at 06:34):

Have you looked at data.list.perm?

view this post on Zulip Mario Carneiro (Apr 22 2020 at 06:37):

Try this:

view this post on Zulip Mario Carneiro (Apr 22 2020 at 06:37):

lemma permuted_middle
    {pre suf : list } {head : }
    : permuted (head :: pre ++ suf) (pre ++ head :: suf) :=
begin
  induction pre,
  { sorry },
  { sorry },
end

lemma cons_to_a_permutation
    {pre suf tail : list } {head : }
    (h : permuted tail (pre ++ suf))
    : permuted (head :: tail) (pre ++ head :: suf) :=
permuted.trans (permuted.skip h) permuted_middle

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 08:16):

Mario worked all this stuff out already. It's more delicate than you think

view this post on Zulip Nam (Apr 22 2020 at 18:25):

Mario Carneiro said:

Have you looked at data.list.perm?

I did not. Thanks a lot, Mario! perm_cons_app_cons looks like what I need.


Last updated: May 10 2021 at 18:22 UTC