チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

稼働中の Docker コンテナ内にファイルを転送するツール Docker Inject を作ってみました

ホスト側から run 中の Docker コンテナ内へ、ディレクトリごとコピーします。

github.com

背景

Docker を運用している上で、動いているコンテナの中にファイルを送り込みたくなったことはないでしょうか。ないですか? 残念ながらあるところにはあるのです。とりあえず今回はあるということにして進みます。

docker cp コマンドを使用すれば「コンテナからホストへ」のファイル転送は可能ですが、逆に「ホストからコンテナへ」の転送手段は公式では提供されていないはずです。docker run 時に -v オプションを付けておいて、マウントされたディレクトリをファイルの受け渡し場所として使用することも不可能ではないですが、ご存知の通りすでに稼働しているコンテナに後から -v を設定することはできません。

無論、コンテナにファイルを送り込むと Dockerfile とコンテナの状態とが乖離することになるため、いわゆる immutable infrastructure の観点からは邪道です。公式で提供されていない理由もそのあたりにあるのでしょう。理想を言えばそういう状況は発生しないに越したことはないのですが、現実というやつはいとも簡単に我々を裏切るわけで、まあそういう経緯でこのツールは制作されました。

インストール

今回は Go のクロスコンパイル機能を使ってバイナリ配布にしてみました。解凍して出てきた実行ファイルを PATH が通っている場所に置けばそのまま使えます。

Releases · y-taka-23/docker-inject · GitHub

あるいは Go の処理系が手元にあるなら go get でも使用可能になります。

$ go get https://github.com/y-taka-23/docker-inject

使い方

docker-inject <コピー元> <コンテナ名>:<コピー先> で動作します。

asciicast

ちなみに Windows の場合、<コピー元> のパスは \ 区切りですが、<コピー先>Linux なので / 区切りで指定する必要があるのでご注意を。

動作原理

基本的には以下のようなコマンドを実行しているだけです。

$ docker exec -i <コンテナ名> bash -c 'cat > <コピー先ファイル>' < <コピー元ファイル>

これを実行すると

  • docker exec でコンテナ内でコマンドを実行
  • その際 -i オプションによりホスト側の標準入力がコンテナ内の標準入力に接続される
  • ホスト側ではコピー元ファイルを標準入力に流し込む
  • コンテナ内では cat が標準入力の内容をコピー先ファイルに書き出す

という過程を経て、ホスト側のファイルがコンテナ内に書き出されます。

直したいところ

現状の問題点として、以下がすぐに思いつきます。

  • ファイルごとに毎回 docker exec を実行しているため動作が遅い
  • コピー先のファイルは上書きされる。-f とか -u オプションがない。

可能ならばいずれこの辺も対応したいところではありますが、それはまた別の話。

Dockerfile をパラメータ化するツール VoicePipe を作ってみました

ひとつの Dockerfile から複数の Docker イメージをビルドすることができます。

github.com

背景

インフラ環境まわりを Docker 化している場合、しばしば複数の Docker イメージを同時並行的に管理する必要が生じます。例えばミドルウェアのバージョンの組み合わせをいろいろ試したいとか、開発環境と本番環境とで設定を変えたいとか。

一方、一般的にイメージとしてビルドされる情報はすべて Dockerfile に記述されており、docker build コマンドの際にはパラメータを渡すことができないため、いきおい、一部分だけ異なる Dockerfile を複数管理する状況に陥ったりします。

これは面倒だし、Dockerfile に変更を入れるときに漏れが出ないとも限らない。できれば一元化したい。

VoicePipe はこのような状況に対応し、単独の Dockerfile にパラメータを導入して、そこから相異なる複数の Docker イメージをビルドするためのツールです。

インストール

$ go get https://github.com/y-taka-23/voicepipe

使い方

例として、開発環境用と本番環境用に、index.html の内容がそれぞれ異なるふたつの Nginx の Docker イメージを作成する必要があるとしましょう。

最終的な作業用ディレクトリの中身は次のようになります。ちなみに同じものが GitHub リポジトリexample 以下に作成してあります。

+--- Dockerfile
+--- index
|    +--- index_develop.html
|    +--- index_latest.html
|    `--- index_production.html
`--- voicepipe.yml

まず、Dockerfile の中身は次のようにしましょう。差し替える予定のパラメータとなる部分が、ENV コマンドによって環境変数 INDEX_HTML として定義されていることに注意します。

FROM nginx
ENV INDEX_HTML index_latest.html
COPY index/${INDEX_HTML} /usr/share/nginx/html/index.html

次に、必要なイメージのパラメータを voicepipe.yml に記述します。

repository: user/nginx
images:
  - tag: develop
    description: "for the development environment"
    parameters:
      - name: INDEX_HTML
        value: index_develop.html
  - tag: production
    description: "for the production environment"
    parameters:
      - name: INDEX_HTML
        value: index_production.html

最後に voicepipe.yml と同じディレクトリ内で

$ voicepipe build

を実行すると、ふたつの Docker イメージ user/nginx:developuser/nginx:production がビルドされるはずです。もちろん、各々のイメージ内の index.html にはそれぞれ対応するものが COPY されています。

動作原理

ls -a などを実行するとわかりますが、ビルドしたあとの作業ディレクトリには次のような隠しディレクトリ .voicepipe が生成されています。

+--- .voicepipe
|    +--- develop
|    |    +--- Dockerfile
|    |    `--- index
|    |         +--- index_develop.html
|    |         +--- index_latest.html
|    |         `--- index_production.html
|    `--- production
|         +--- Dockerfile
|         `--- index
|              +--- index_develop.html
|              +--- index_latest.html
|              `--- index_production.html
+--- Dockerfile
+--- index
|    +--- index_develop.html
|    +--- index_latest.html
|    `--- index_production.html
`--- voicepipe.yml

また .voicepipe/develop.voicepipe/production の中にある Dockerfile を見ると、voicepipe.yml の指定に従って ENV 行が書き変わっているのがわかるはずです。実際にビルドされているのはこれら生成された Dockerfile です。

なお、Dockerfile を Git で管理している場合はこの .voicepipe は邪魔なので、.gitignore で無視させるか、あるいはビルド後に voicepipe clean を実行すると削除してくれます。

その他

ちなみに、voicepipe list を実行するとビルドできるイメージとその説明が一覧で表示されたり、voicepipe build -L とするとついでに元の Dockerfile を latest タグでビルドしたりします。

なお、Docker 1.6 から、Dockerfile 中のLABEL 行でイメージにラベルを付与する機能がつきました。VoicePipe でもこのラベルを設定できるようにしようかと思っているのですが、それはまた別の話。

NGK2014B で SPIN について話してきました

名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。

内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。

当日の動画は Youtube から見ることができます。

ちなみに、発表順は乱数で決められているはずなのですが、なぜか去年の NGK と全く同じ 3 番目でした。

リソース共有問題の Promela モデル

LT の冒頭に登場するリソース共有時のデッドロックについて、Promela で記述したモデルが Gist においてあります。

この Promela モデルは、次のようなシステムを想定したものです。

  • クライアント
    1. スキャナもしくはプリンタのどちらかをロックし、その後もう片方をロック
    2. スキャナもしくはプリンタのどちらかをアンロックし、その後もう片方をアンロック
  • リソース (スキャナ、プリンタ)
    1. ロックするメッセージを待ち、相手のプロセス ID を記憶
    2. アンロックするメッセージを待ち、相手のプロセス ID とロックしたプロセスを照合
    3. ロックとアンロックが同じプロセスからのものならば最初に戻る

すぐわかる通り (LT 内でも述べていますが) このシステムには欠陥があり、デッドロックが発生します。スキャナとプリンタにロックを掛ける順番が指定されていない (そして Promela がそういう非決定的な記述を許す) というところがポイントです。

いずれこのモデルを題材にして Promela/SPIN の入門記事でも書くつもりではありますが、それはまた別の話。

Coq で Quine

Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごとく Gist 上 https://gist.github.com/4700318 にも同じものを置いておきました。

Coq の特性あれこれ

Quine なるものを初めて聞いた人は wikipedia:クワイン_(プログラミング) あたりを見てみましょう。「自分自身のソースコードを標準出力する。ただし空ファイルでなく、入力は受け付けない」というのが一般的な Quine のお作法ですが、Coq で書くにはいくつか考えねばならない点があります。

標準出力……。

最大の問題として、Coq 単体では出力ができません。純粋すぎる相手というのは得てして扱いにくいものです。悩んでどうにかなる問題でもないので、コードの最後を Eval compute in として、ここが評価されたときにコード全体と同じ文字列になることを目指しました。

文字列の扱い

大部分の言語と違い、Coq は文字列を扱うのにいちいちライブラリを読み込む必要があります。使うライブラリは Ascii と String。

ascii 型の方はコンストラクタの引数に bool を 8 個取って、8 ビット ASCII コードとして読むものです。

Inductive ascii : Set :=
    Ascii : bool ->
            bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii

ちなみに実験してみるとわかりますが、引数の順番は下位ビットが先です。

Eval compute in Ascii true  false false false
                      false false true  false.

    = "A"%char
    : ascii

また、string 型の方はリストと同じ構造を持っています。

Inductive string : Set :=
    EmptyString : string | String : ascii -> string -> string

EmptyString が nil、String が cons 相当のコンストラクタですね。string_scope を開いておくと文字列の結合 append が + でシュガーされるので、見やすくするためにこれを使いました。

クォーテーションの扱い

文字列のデリミタは " です。Quine を書く上で、文字列の中に " が出現するためエスケープを考える訳ですが、ここで若干問題が。どうも Coq では (少なくとも CoqIDE の表示上は) 記号 " を単体で表示させることができないようです。実際、ASCII コード 34 を評価すると

Eval compute in ascii_of_nat 34.

     = """"%char
     : ascii

となり、"" で一文字分 (つまり "" が " のエスケープ表現) となっていることがわかります。ここは若干不本意ですが、「表示文字列中の " と "" との差には目をつぶる」として逃げることにしましょう。

Quine の実装

以上のことを踏まえて具体的なコードを作っていきましょうか。

まず大まかな構造として、次のような形を考えます。

Definition Q : string := [空欄 A].
Eval compute in [空欄 A'].

この Eval compute in [空欄 A']. でコード自身が表示されればよいわけです。

ステップその 1

Definition と Eval の二つの文がある以上、[空欄 A'] はこの二つの文をつなげた文字列が入るはずです。そこで、次のような形になることがわかります。

Definition Q : string := [空欄 A].
Eval compute in [空欄 B] ++ "." ++ [空欄 C].

非形式的な言い方をすれば、[空欄 B] が「Q にしかるべき文字列を代入せよ」、[空欄 C] が「「このコードを表示せよ」を表示せよ」を表す部分です。

ステップその 2

次に、[空欄 C] について考えます。意味するところが「〜を表示せよ」なので Eval compute in を入れたいところですが、そうすると堂々巡りになってしまいそうですね。回避策として、前半で定義している Q を参照します。

Definition Q : string := [空欄 A].
Eval compute in [空欄 B] ++ "." ++ Q.

そうすると、Q は「〜を表示せよ」でなくてはならないため、Eval compute in で始まることがわかりました。

Definition Q : string := "Eval compute in [空欄 D]".
Eval compute in [空欄 B] ++ "." ++ Q.
ステップその 3

次に埋めるべきは [空欄 B] です。ここには前半部に対応する「Q に 「Q の中身」を定義せよ」を意味するコード文字列が入るはずですね。「Q の中身」を文字列として表すのに、冒頭に挙げた参照文献では Q に対して Haskell の show を使っています。Coq に show はないので、手動でデリミタ " を付けましょう。文字列「Q の中身」は """" ++ Q ++ """" です。

Definition Q : string := "Eval compute in [空欄 D]".
Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
ステップその 4

これでほとんど完成しました。後は [空欄 D] として、実際に Eval compute in の引数になっている「"Definition Q : string := " ++ """" ++ Q + """" ++ "." ++ Q.」をそのまま持ってきてエスケープすればオッケー。

Definition Q : string := "Eval compute in ""Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
完成!

ライブラリの読み込みなどを追加し、また見やすくなるように適宜改行を入れたりした完成品が以下になります。はてなブログのベタ打ちだと若干見づらいですが、Gist の方を見てもらうと地の文と文字列との境目が分かりやすいかと。

Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "
Eval compute in ""
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.

その他補足

ここで書いた Quine は当然ですが最短ではありません。改行が無駄ですし、型宣言も省略できます。あるいは、今回は構成手順に重きを置いたためこの形になりましたが、もしかしたらもっと本質的にいい書き方があるかもしれません。しかしまあ、そもそも Coq は短く書くことに向いた言語ではありませんし、無理に追求はしないことにしましょう。なお、どうしても短い Quine が書きたい人は wikipedia:HQ9+ あるいは PHP の利用をおすすめします。

ちなみに今回は深入りはしませんが、「自分自身のコード」に言及する上でキモになっているのが [空欄 C] の中身「「このコードを表示せよ」を表示せよ」という部分です。こういう表現の背後には Kleene の再帰定理があり、またかの有名な不完全性定理の証明と関係があったりして面白い部分ではあるのですが、それはまた別の話。

Coq でクイックソート (3)

Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。

  1. アルゴリズムの定義
  2. 仕様の検証その 1
  3. 仕様の検証その 2 (この記事)

今回の目標

今回は、最後に残った qsort の二つ目の仕様

  • 出力が入力の置換 (並び替え) になっていること

を証明します。モジュール Sorting.Permutation を使いましょう。前回の Sorted に比べ、Permutation はリスト操作とそれなりに相性がよく、証明済みの定理も使えそうなヤツが揃っています。

述語 Permutation の中身

Permutation の定義は以下です。

Inductive Permutation (A : Type) : list A -> list A -> Prop :=
    perm_nil : Permutation nil nil
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' -> Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' -> Permutation l' l'' -> Permutation l l''

特に複雑なところはないですね。要するに、空リストから始めて「同じ要素を先頭にくっつける」「先頭から二つを入れ替える」を有限回繰り返して得られるリストは互いに置換である、というわけです。

いざ、最後の証明

示したい定理を改めて掲げておきます。

Theorem qsort_Permutation : forall l : list nat,
                            Permutation (qsort l) l.

証明に使うのは前回と同じく functional induction タクティク。さらに上手いことに、ライブラリを覗いてみるとこんなのがありました。

Permutation_cons_app
     : forall (A : Type) (l l1 l2 : list A) (a : A),
       Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2)

qsort の定義が

Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

だったことを考えれば、使ってくれと言わんばかりです。事実、今回はほとんど自前で示すべき補題はありません。唯一の例外は「filter の結果と antifilter の結果を append したものは、もとのリストの置換」という補題 filter_Permutation ですが、これにしたって単純な場合分けだけですぐに証明できてしまいます。

その他補足

さて、全三回に渡ってお送りしてきましたが、以上によりクイックソート qsort の仕様が証明されました。これで明日から安心してクイックソートが使えますね。めでたしめでたし。ちなみにこのナイーブな実装では遅すぎて実用性が皆無ですが、まあご愛嬌ということで。

今回の「置換であること」の定式化や証明には、この他にも方法が考えられるはずです。すぐに思いつくのは、「任意の要素に関して、二つのリストに含まれる個数が等しければ置換」というものでしょうか。形式的に書けば

Theorem Permutation_count : forall l1 l2 : list nat,
                            Permutation l1 l2 <->
                            (forall n : nat, count_occ eq_nat_dec l1 n =
                                             count_occ eq_nat_dec l2 n).

という感じでしょうかね。ただ、置換であることと述語 In とはあまり相性がよくありません。前回の補足でも述べた通り、In は重複した要素を区別することができないからです。リストが重複要素を含まないときのみ、In を使って Permutation を特徴づける補題 NoDup_Permutation も用意されていますが、使いどころは難しい気がします。

なお、ここに挙げた定理 Permutation_count はそう苦労せずに証明することができるのですが、それはまた別の話。

Coq でクイックソート (2)

Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。

  1. アルゴリズムの定義
  2. 仕様の検証その 1 (この記事)
  3. 仕様の検証その 2

今回の目標

さて、前回の最後にも触れた通り、前回定義したクイックソート qsort について、

  • 出力が昇順になっていること

を保証することが第一の目標です。ここでは、標準ライブラリ Sorting モジュール内にある述語 Sorted を使うことにしました。Sorting.Sorted の中には、「リストが (ある関係 R に対して) 昇順である」ことを意味する述語が三種類用意されています (LocallySorted、Sorted、StronglySorted) が、これらはすべて同値です。

述語 Sorted の中身

Sorted の定義を見ると、次のようになっています。

Inductive Sorted (A : Type) (R : A -> A -> Prop) : list A -> Prop :=
    Sorted_nil : Sorted R nil
  | Sorted_cons : forall (a : A) (l : list A),
                  Sorted R l -> HdRel R a l -> Sorted R (a :: l)

ちなみに、ここで補助的に使われている HdRel の定義は以下です。

Inductive HdRel (A : Type) (R : A -> A -> Prop) (a : A) : list A -> Prop :=
    HdRel_nil : HdRel R a nil
  | HdRel_cons : forall (b : A) (l : list A), R a b -> HdRel R a (b :: l)

自然言語で読み下せば、HdRel R a l は「a とリスト l の先頭要素との間に関係 R が成立」を意味しています。Head Relation の略でしょうね。これを考えると、Sorted は直感的には「既にソートされたリストに対して、現在の先頭要素以下のものを先頭に付け足してもソートされている」と定義されていることがわかります。

さて、ここまで来てちょっと困りました。というのも、qsort は再帰的に定義されていて、最終的な出力の先頭要素がどこから来ているのかわからないからです。こういうときに使えるのが functional induction タクティクです。

Functional Induction による証明

さて改めて確認しておくと、qsort の定義は以下でした。

Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

もし人間が紙の上で「qsort の出力が昇順」を示したいとしたら、自然なのは「qsort lts とqsort ges が昇順だと仮定すると〜」というものでしょう。Coq に対してこれを伝えるタクティクが functional induction で、関数の再帰呼び出しに対して帰納法を適用することができます。実際に今回示したい定理

Theorem qsort_Sorted : forall l : list nat, Sorted le (qsort l).

に対して functional induction (qsort l) を打ち込んでみると、l = n :: l' の場合に使える仮定として「Sorted le (qsort (antifilter (leb n) l'))」および「Sorted le (qsort (filter (leb n) l'))」が追加されるはずです。

これができれば、それ以外はたいした問題はないはず。もちろん、二つの昇順リストを連結したときに結果が再び昇順になるためには、左側に小さい要素、右側に大きい要素が集まっている必要があるので、それさえ示しておけば大丈夫。定式化の方法はいろいろあると思いますが、ここでは次のような補題を使ってあります。

Lemma Sorted_app : forall (l1 l2 : list nat),
                   Sorted le l1 -> Sorted le l2 ->
                   (forall n1 n2 : nat,
                    In n1 l1 -> In n2 l2 -> n1 <= n2) ->
                   Sorted le (l1 ++ l2).

その他補足

さて、これで半分終わりました。次回は残りのもうひとつ、qsort の出力が入力の置換であることを証明する予定です。

ちなみに「置換である」という部分だけ見ると、今回補題として用いた

Lemma qsort_in : forall (l : list nat) (n : nat),
                 In n l <-> In n (qsort l).

がそのまま使えそうな気がします。がしかし、この補題は置換であることを保証しません。というのも、述語 In は「リストの中に一個以上存在する」ことしか保証せず、ダブりを考慮できないからです。置換であるためには個数まで含めて一致する必要がありますからね。

とはいえ、ライブラリを見てもらえればわかる通り、Sorting.Permutation は今回の Sorting.Sorted よりも使えそうな補題が豊富です。次回はこいつらを活用する方針で行きたいと思いますが、それはまた別の話。

Coq でクイックソート (1)

以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。

  1. アルゴリズムの定義 (この記事)
  2. 仕様の検証その 1
  3. 仕様の検証その 2

ちなみに、今回の分のコードは https://gist.github.com/4526374 に置いてあります。使い古されたネタではありますが、もしよろしければしばしお付き合いを。

おなじみのアルゴリズム

今更ですが、アルゴリズムの復習から始めましょう。深く考えずにクイックソートを書き下すと次のようになります。

Fixpoint qsort (l : list nat) : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

前も使いましたが、antifilter は、filter と逆の (つまり false になる要素の) 抽出を行う関数として定義してあります。ここで言えば、ピボット n に対して、lts として n より小さい要素、ges として n 以上の要素が抽出されるわけです。

しかしこのコードを読み込むと、

Error:
Recursive definition of qsort is ill-formed.

と怒られてしまいます。Coq には qsort の再帰呼び出しが有限回で停止することが理解できないからです。

そこで、リストの長さが短くなっていることを明示的に教えてやりましょう。Recdef モジュールをインポートしておいて、Function コマンドで定義します。

Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

これで怒られることはなくなりましたが、その代わりリストの長さが短くなることの証明が必要です。filter 関数の検証の際に使った補題が役に立ちそうですね。

Lemma filter_sublist : forall (f : A -> bool) (l : list A),
                       sublist (filter f l) l.

Lemma antifilter_sublist : forall (f : A -> bool) (l : list A),
                           sublist (antifilter f l) l.

Lemma sublist_length : forall l1 l2 : list A,
                       sublist l1 l2 ->
                       (l1 = l2 \/ length l1 < length l2).

ソートがソートであるために

上で定義した qsort に対して、仕様の検証を行うのが今回のネタの最終目的です。 wikipedia:ソート にも書いてある通り、ソート関数の仕様として次の性質を要求します。

  1. 出力は昇順になっている。
  2. 出力は入力の置換になっている。

準備がよいことに、これらの性質は標準ライブラリ Sorting モジュールに既に準備されています。こいつを使ってやりましょう。

Inductive Sorted (A : Type) (R : A -> A -> Prop) : list A -> Prop :=
    Sorted_nil : Sorted R nil
  | Sorted_cons : forall (a : A) (l : list A),
                  Sorted R l -> HdRel R a l -> Sorted R (a :: l)

Inductive Permutation (A : Type) : list A -> list A -> Prop :=
    perm_nil : Permutation nil nil
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' -> Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' -> Permutation l' l'' -> Permutation l l''

ちなみに有名チュートリアル プログラミング Coq では整列性の定義として、Sorted ではなく LocallySorted の方を採用しています。補題 Sorted_LocallySorted_iff によってこれら二つの性質は同値なので問題は無いはずです。

その他補足

今回は nat 型のリストに対してしか定義していないのであまり関係がありませんが、ここで定義した qsort は安定ソートになっています。「Coq で filter 関数」でも「順序を維持したままマージしたもの」という表現が出てきましたね。その代わりと言ってはなんですが、常に左端の値をピボットとして取るため、入力が整列済みの場合に計算量は最悪 O(n^2) になります。

次回はまず仕様その 1 として qsort の出力が整列していることを証明する予定です。この証明では functional induction が威力を発揮するのですが、それはまた別の話。