## Stream: new members

### Topic: permutation

#### 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))
begin
sorry
end


#### Mario Carneiro (Apr 22 2020 at 06:34):

Have you looked at data.list.perm?

Try this:

#### 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.trans (permuted.skip h) permuted_middle


#### Kevin Buzzard (Apr 22 2020 at 08:16):

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

#### 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