Require Import List.
Require Import ZArith.

Section refleksja.

Variable A:Type.

Inductive lexpr : Set :=
| Cons : N -> lexpr -> lexpr
| Atom : N -> lexpr
| Append : lexpr -> lexpr -> lexpr
| Nil : lexpr.

Variable map : list (list A).

Fixpoint interp (le : lexpr) : list A :=
match le with
| Cons n l => List.nth (Nnat.nat_of_N n) map nil ++ interp l
| Atom n => List.nth (Nnat.nat_of_N n) map nil
| Append l1 l2 => interp l1 ++ interp l2
| Nil => nil
end.

Definition listexpr := list N.

Fixpoint interp' (le : listexpr) : list A :=
match le with
| n :: le => List.nth (Nnat.nat_of_N n) map nil ++ interp' le
| nil => nil
end.

Fixpoint to_list (l: lexpr) : listexpr :=
match l with
| Cons n l => n::to_list l
| Atom n => n::nil
| Append l1 l2 => to_list l1 ++ to_list l2
| Nil => nil
end.

Lemma interp'_app : forall l l', interp' (l ++ l') = interp' l ++ interp' l'.
induction l.
simpl; trivial.
simpl.
intro.
rewrite IHl.
apply ass_app.
Qed.

Lemma to_list_correct : forall l, interp l = interp' (to_list l).
induction l; simpl.
rewrite <- IHl; trivial.
rewrite <- app_nil_end; trivial.
rewrite interp'_app.
rewrite IHl1.
rewrite IHl2.
trivial.
trivial.
Qed.

Hint Constructors Permutation.
Hint Resolve Permutation_refl Permutation_sym.
Hint Resolve Permutation_app Permutation_app_swap.

Lemma Permutation_swap_app:
forall A (l1 l2 l3 : List.list A),
Permutation (l1 ++ l2 ++ l3) (l2 ++ l1 ++ l3).
Proof.
  intros.
  rewrite <- app_ass.
  rewrite <- app_ass.
  auto.
Qed.

Hint Resolve Permutation_swap_app.

Lemma Permutation_interp : 
forall l l', Permutation l l' -> Permutation (interp' l) (interp' l').
induction 1; simpl; eauto.
Qed.

Require Import insertsort.

Lemma Permutation_interp_sort:
forall l, Permutation (interp' l) (interp' (sort l)).
intros.
apply Permutation_interp.
apply sort_Permutation.
Qed.

Lemma Permutation_simpl : forall l l', 
  Permutation (interp' (sort l)) (interp' (sort l')) -> 
    Permutation (interp' l) (interp' l').
eauto using Permutation_interp_sort.
Qed.

End refleksja.

Require Import ListTactics.


Ltac mapuj map expr := 
match expr with
| nil => map
| cons ?x ?exp => 
  let lx := constr:(cons x nil) in
  let map' := AddFvTail lx map in
  mapuj map' exp
| app ?l1 ?l2 => 
  let map' := mapuj map l1 in
  mapuj map' l2
| ?l => AddFvTail l map
end.

Ltac qqquote map expr :=
match expr with
| nil => Nil
| cons ?x ?exp => 
  let lx := constr:(cons x nil) in
  let p1 := Find_at lx map in 
  let p := eval compute in (Npred (Npos (p1))) in
  let l := qqquote map exp in
  constr: (Cons p l)
| app ?l1 ?l2 => 
  let l1' := qqquote map l1 in
  let l2' := qqquote map l2 in
  constr: (Append l1' l2')
| ?l => 
  let p1 := Find_at l map in 
  let p := eval compute in (Npred (Npos (p1))) in
  constr: (Atom p)
end.

Ltac ppquote := 
match goal with
| |- Permutation ?l1 ?l2 => 
  let listA:= type of l1 in
  let empty := constr:(@nil listA) in 
  let map := mapuj empty l1 in 
  idtac "pierwszy mapuj wrocil";
  let map := mapuj map l2 in
  idtac "drugi mapuj wrocil";
  let l1' := qqquote map l1 in
  idtac "pierwszy quote wrocil";
  let l2' := qqquote map l2 in
  idtac "drugi quote wrocil";
  change (let m := map in 
    Permutation (interp _ m l1') (interp _ m l2'))
| _ => fail 1 "This tactic applies to a goal of the form Permutation l1 l2"
end.


Open Scope Z_scope.
Check 18.

Goal Permutation (18::17::nil) (17::18::nil).
ppquote.
intro.
repeat rewrite to_list_correct.
simpl to_list.
apply Permutation_simpl.
simpl sort.
apply Permutation_refl.
Save.

Goal forall l1 l2, Permutation ((18::l1)++l2) (l2++(18::nil)++l1).
intros.
(*Set Ltac Debug.*)
ppquote.
intro.
repeat rewrite to_list_correct.
simpl to_list.
apply Permutation_simpl.
apply Permutation_refl.
Save.

Ltac perm_auto :=
  ppquote;
  intro;
  repeat rewrite to_list_correct;
  simpl to_list;
  apply Permutation_simpl;
  simpl sort;
  apply Permutation_refl.


Require Import String.
Open Scope string_scope.

Goal forall b c l1 l2 l3 l4, l1 = "a"::"ba"::l3 -> l2 = "ba"::"a"::l4 ->
Permutation (l1++c::l1++b::l2)%list (b::c::l1++l2++l1)%list.
intros.
subst.
Show Proof.
perm_auto.
Show Proof.

Qed.