A : Type
x : A
l1 : list A
l2 : list A
l3 : list A

Permutation ((rev l1 ++ nil) ++ (l2 ++ x::l3)) (rev (l3 ++ l2) ++ l1 ++ x::nil)

1. Dla wygody zdefiniuj wygodną notację dla relacji Permutation, np:

   Require Import Permutation.
   
   Infix "==" := (Permutation) (at level 70) : type_scope.
   

2. Relacja Permutation jest zadeklarowana jako klasa Equivalence, co umożliwia jej wygodne stosowanie w komendzie rewrite, co przyda się w pracy nad taktyką. Aby stosowanie to było możliwe w interesujących nas kontekstach należy funkcje tworzące te konteksty zadeklarować jako dopuszczalne konteksty dla przepisywania przy pomocy tej relacji. Np. dla funkcji app deklaracja ta będzie wyglądać tak (zakładamy, że w kontekście jest A:Type):

   Require Import Morphisms Setoid.
         
   Notation permutation := (@Permutation _) (only parsing).
   
   Global Instance appPermutationProper : Proper (permutation ==> permutation ==> permutation) (@app A).
   

   Polecenie to każe nam udowodnić odpowiednią własność funkcji (o czym można się przekonać na własne oczy po kilkukrotnym użyciu taktyki red), a sama potrzebna własność jest już udowodniona w bibliotece standardowej (występujące powyżej znaki @ każą Coq'owi ignorować argumenty implicite stałych).
   
   
3. Należy zaprogramować taktykę reify, na wzór taktyki zdefiniowanej w rozdz. 15.4.1 CPDT, która będzie przekształcać cel oznaczający permutację dwóch wyrażeń listowych (np. rev l1 ++ l2 == rev l2 ++ l1) na interp xs e1 == interp xs e2, gdzie e1 i e2, to abstrakcyjne drzewa składni tych wyrażeń zawierające w liściach numery atomów w słowniku xs. Te atomy to np. zmienne, ale też inne termy, które nie są złożone z rozpatrywanych przez nas symboli funkcyjnych. Funkcja interp to funkcja tłumacząca abstrakcyjne drzewo składni na wyrażenia listowe.
   Do samej zmiany celu służy taktyka change - w naszym przypadku będzie to wywołanie

   change (interp xs e1 == interp xs e2)
   

   które sprawdzi, że obliczone xs, e1 i e2 rzeczywiście tłumaczą się do (wyrażeń konwertowalnych do) początkowych wyrażeń listowych.
   
   Podpowiedź: Do przechowywania słownika atomów zamiast uzywanych w CPDT "list" zbudowanych z zagnieżdżonych par, lepiej jest użyć prawdziwego typu listowego. W szczególności oznacza to zastąpienie Ltac'owych definicji inList i addToList następującymi definicjami:

     Ltac inEnv x xs :=
     match xs with
     | nil => false
     | (x :: _) => true
     | (_ :: ?xs') => inEnv x xs'
     end.
   
     Ltac addToEnv x xs :=
     let b := inEnv x xs in
     match b with
     | true => xs
     | false => constr:(cons x xs)
     end.
   

   Aby poprawnie zainicjować taki pusty słownik-listę, można zrobić tak:

     let typ := type of E1 in
     let emptyEnv := constr:(@nil typ) in
   

   gdzie E1 to dowolne "przechwycone" wyrażenie listowe dobrego typu (takiego jak atomy, które będą przechowywane w słowniku).
   
   Podpowiedź 2: Zamiast rozważać dwóch rodzajów atomów - reprezentujących listy oraz elementy listy - można traktować cons x l jako app lx l, gdzie lx jest "atomową" listą jednoelementową cons x nil. Innymi słowy, w słowniku atomów będą "prawdziwe" atomy reprezentujące listy oraz "sztuczne" atomy reprezentujące jednoelementowe listy stworzone przez nas przy "reifikacji" wyrażeń cons x l.
   Można też w pierwszym podejściu rozważać wyłacznie wyrażenia listowe bez funkcji cons, a następnie dodać jej obsługę np. według powyższej podpowiedzi.
   
   
4. Dalsza część taktyki będzie realizowana po stronie Coqa. Należy zrobić funkcję kanonik, która będzie przekształcać drzewa składni tak, aby drzewa odpowiadające dwóm wyrażeniom reprezentującym listy, które są swoimi permutacjami, były przekształcone do tej samej (identycznej) postaci. Na przykład funkcja taka powinna ignorować odwracanie (rev), rozpłaszczać rozdrzewione struktury złożone z funkcji app, usuwać nil'e, a następnie otrzymany ciąg sortować np. wg kolejności numerów atomów.
   
   
5. Do sortowania można użyć funkcji z pliku Coq.Sorting.Mergesort. Aby ją wykorzystać należy wprowadzić dodatkową reprezentację dla wstępnie wyczyszczonych i rozpłaszczonych wyrażeń listowych - w postaci ciągu atomów, który następnie można posortować.
   
   
6. Aby zapewnić poprawność tego procesu (bez której Coq odmówi i tak wykonania go), należy udowodnić lemat postaci:

     Lemma kanonik_ok : forall ..., interp xs (kanonik l) == interp xs l
   

   a następnie drugi (wynikający z niego) postaci:

     Lemma two_kanonik : forall ...,
     interp xs (kanonik e1) == interp xs (kanonik e2) ->
     interp xs e1 == interp xs e2
   

7. Teraz całość należy zebrać do kupy w taktykę:

   Ltac solve_perm :=
     reify;
     apply two_kanonik;
     reflexivity.
   

   Ta ostatnia taktyka powiedzie się po pierwsze dlatego, że relacja == została zadeklarowana jako Equivalence, a po drugie dlatego, że nasze wyrażenia kanonik e1 i kanonik e2 będą obliczać się do identycznych (literalnie) postaci.
   
   
8. Na zakończenie należy przeprowadzić próbę działania taktyki, np. w postaci dowodu że wynik jakiegoś prostego algorytmu sortującego (np. insertion sort) jest permutacją listy wejściowej (właściwą kolejnością elementów na liście wyjściowej możemy się w tym ćwiczeniu nie przejmować).