permutation

Stream: new members

[Nam]

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

[Mario Carneiro]

Have you looked at data.list.perm?

[Mario Carneiro]

Try this:

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Nam]

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.