From a8d9db97b5deef824c0c79fe3cc15c4a81371e9f Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 2 Nov 2023 22:10:46 +0100 Subject: [PATCH 1/2] Get rid of traces --- .github/workflows/docker-action.yml | 15 +- Make | 1 - README.md | 21 +- coq-stablesort.opam | 21 +- meta.yml | 49 +- theories/param.v | 5 +- theories/stablesort.v | 1224 +++++++++++++++------------ theories/top_down.v | 116 --- 8 files changed, 762 insertions(+), 690 deletions(-) delete mode 100644 theories/top_down.v diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index c6a1d9a..24c4e8c 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,13 +17,9 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.13.0-coq-8.11' - - 'mathcomp/mathcomp:1.13.0-coq-8.12' - 'mathcomp/mathcomp:1.13.0-coq-8.13' - 'mathcomp/mathcomp:1.13.0-coq-8.14' - 'mathcomp/mathcomp:1.13.0-coq-8.15' - - 'mathcomp/mathcomp:1.14.0-coq-8.11' - - 'mathcomp/mathcomp:1.14.0-coq-8.12' - 'mathcomp/mathcomp:1.14.0-coq-8.13' - 'mathcomp/mathcomp:1.14.0-coq-8.14' - 'mathcomp/mathcomp:1.14.0-coq-8.15' @@ -37,16 +33,21 @@ jobs: - 'mathcomp/mathcomp:1.16.0-coq-8.16' - 'mathcomp/mathcomp:1.16.0-coq-8.17' - 'mathcomp/mathcomp:1.16.0-coq-8.18' - - 'mathcomp/mathcomp:1.16.0-coq-dev' - 'mathcomp/mathcomp:1.17.0-coq-8.15' - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' - 'mathcomp/mathcomp:1.17.0-coq-8.18' - - 'mathcomp/mathcomp:1.17.0-coq-dev' + - 'mathcomp/mathcomp:1.18.0-coq-8.16' + - 'mathcomp/mathcomp:1.18.0-coq-8.17' + - 'mathcomp/mathcomp:1.18.0-coq-8.18' + - 'mathcomp/mathcomp:1.18.0-coq-dev' - 'mathcomp/mathcomp:2.0.0-coq-8.16' - 'mathcomp/mathcomp:2.0.0-coq-8.17' - 'mathcomp/mathcomp:2.0.0-coq-8.18' - - 'mathcomp/mathcomp:2.0.0-coq-dev' + - 'mathcomp/mathcomp:2.1.0-coq-8.16' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.1.0-coq-dev' - 'mathcomp/mathcomp-dev:coq-8.16' - 'mathcomp/mathcomp-dev:coq-8.17' - 'mathcomp/mathcomp-dev:coq-8.18' diff --git a/Make b/Make index d65e60b..1211cbc 100644 --- a/Make +++ b/Make @@ -1,7 +1,6 @@ theories/mathcomp_ext.v theories/param.v theories/stablesort.v -theories/top_down.v -R theories stablesort diff --git a/README.md b/README.md index 656145a..8c0d1dd 100644 --- a/README.md +++ b/README.md @@ -28,21 +28,24 @@ The point is that the best mergesort function for lists depends on the situation, in particular, the evaluation strategy and whether it should be incremental or not. -To prove the correctness (including stability) of these mergesort functions, -this library also provides a generic way to prove these properties. The -correctness lemmas provided in this library are overloaded using a canonical -structure (`StableSort.function`). Stable sort functions are characterized in -this interface by the parametricity axiom and binary trees representing the -divide-and-conquer structure of sort. Thus, one may prove the stability of a -new sorting function by using the parametricity translation (Paramcoq) and -by providing a lemma corresponding to the binary tree construction. +This library also provides a generic way to prove the correctness (including +stability) of these mergesort functions. The correctness lemmas in this +library are overloaded using a canonical structure (`StableSort.function`). +This structure characterizes stable sort functions, say `sort`, by an abstract +version of the sort function `asort` parameterized over the type of sorted +lists and its operators such as merge, the parametricity of `asort`, two +equational properties that `asort` instantiated with merge and concatenation +are `sort` and the identity function, respectively. Thus, one may prove the +stability of a new sorting function by defining its abstract version, using +the parametricity translation (Paramcoq), and manually providing the +equational properties. ## Meta - Author(s): - Kazuhiko Sakaguchi (initial) - License: [CeCILL-B Free Software License Agreement](CeCILL-B) -- Compatible Coq versions: 8.11 or later +- Compatible Coq versions: 8.13 or later - Additional dependencies: - [MathComp](https://math-comp.github.io) 1.13.0 or later - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later diff --git a/coq-stablesort.opam b/coq-stablesort.opam index 45067a5..d2ad695 100644 --- a/coq-stablesort.opam +++ b/coq-stablesort.opam @@ -28,19 +28,22 @@ The point is that the best mergesort function for lists depends on the situation, in particular, the evaluation strategy and whether it should be incremental or not. -To prove the correctness (including stability) of these mergesort functions, -this library also provides a generic way to prove these properties. The -correctness lemmas provided in this library are overloaded using a canonical -structure (`StableSort.function`). Stable sort functions are characterized in -this interface by the parametricity axiom and binary trees representing the -divide-and-conquer structure of sort. Thus, one may prove the stability of a -new sorting function by using the parametricity translation (Paramcoq) and -by providing a lemma corresponding to the binary tree construction.""" +This library also provides a generic way to prove the correctness (including +stability) of these mergesort functions. The correctness lemmas in this +library are overloaded using a canonical structure (`StableSort.function`). +This structure characterizes stable sort functions, say `sort`, by an abstract +version of the sort function `asort` parameterized over the type of sorted +lists and its operators such as merge, the parametricity of `asort`, two +equational properties that `asort` instantiated with merge and concatenation +are `sort` and the identity function, respectively. Thus, one may prove the +stability of a new sorting function by defining its abstract version, using +the parametricity translation (Paramcoq), and manually providing the +equational properties.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {>= "8.11"} + "coq" {>= "8.13"} "coq-mathcomp-ssreflect" {>= "1.13.0"} "coq-paramcoq" {>= "1.1.3"} ] diff --git a/meta.yml b/meta.yml index 4b1ce98..4b63107 100644 --- a/meta.yml +++ b/meta.yml @@ -25,14 +25,17 @@ description: |- situation, in particular, the evaluation strategy and whether it should be incremental or not. - To prove the correctness (including stability) of these mergesort functions, - this library also provides a generic way to prove these properties. The - correctness lemmas provided in this library are overloaded using a canonical - structure (`StableSort.function`). Stable sort functions are characterized in - this interface by the parametricity axiom and binary trees representing the - divide-and-conquer structure of sort. Thus, one may prove the stability of a - new sorting function by using the parametricity translation (Paramcoq) and - by providing a lemma corresponding to the binary tree construction. + This library also provides a generic way to prove the correctness (including + stability) of these mergesort functions. The correctness lemmas in this + library are overloaded using a canonical structure (`StableSort.function`). + This structure characterizes stable sort functions, say `sort`, by an abstract + version of the sort function `asort` parameterized over the type of sorted + lists and its operators such as merge, the parametricity of `asort`, two + equational properties that `asort` instantiated with merge and concatenation + are `sort` and the identity function, respectively. Thus, one may prove the + stability of a new sorting function by defining its abstract version, using + the parametricity translation (Paramcoq), and manually providing the + equational properties. authors: - name: Kazuhiko Sakaguchi @@ -46,26 +49,18 @@ license: file: CeCILL-B supported_coq_versions: - text: 8.11 or later - opam: '{>= "8.11"}' + text: 8.13 or later + opam: '{>= "8.13"}' tested_coq_nix_versions: tested_coq_opam_versions: -- version: '1.13.0-coq-8.11' - repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.12' - repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.13' repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.14' repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.15' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.11' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.12' - repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.13' repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.14' @@ -92,8 +87,6 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.16.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-dev' - repo: 'mathcomp/mathcomp' - version: '1.17.0-coq-8.15' repo: 'mathcomp/mathcomp' - version: '1.17.0-coq-8.16' @@ -102,7 +95,13 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.17.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.17.0-coq-dev' +- version: '1.18.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-dev' repo: 'mathcomp/mathcomp' - version: '2.0.0-coq-8.16' repo: 'mathcomp/mathcomp' @@ -110,7 +109,13 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-dev' +- version: '2.1.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-dev' repo: 'mathcomp/mathcomp' - version: 'coq-8.16' repo: 'mathcomp/mathcomp-dev' diff --git a/theories/param.v b/theories/param.v index 03580da..838f781 100644 --- a/theories/param.v +++ b/theories/param.v @@ -1,4 +1,4 @@ -From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. From Param Require Export Param. Set Implicit Arguments. @@ -17,6 +17,7 @@ Parametricity eq. Parametricity or. Parametricity Acc. Parametricity bool. +Parametricity option. Parametricity prod. Parametricity nat. Parametricity list. @@ -24,6 +25,8 @@ Parametricity pred. Parametricity rel. Parametricity BinNums.positive. Parametricity BinNums.N. +Parametricity merge. +Parametricity rev. Lemma bool_R_refl b1 b2 : b1 = b2 -> bool_R b1 b2. Proof. by case: b1 => <-; constructor. Qed. diff --git a/theories/stablesort.v b/theories/stablesort.v index 6e31201..03b9c15 100644 --- a/theories/stablesort.v +++ b/theories/stablesort.v @@ -12,112 +12,48 @@ Unset Printing Implicit Defensive. Module StableSort. -Section Traces. - -Variables (T : Type) (P : {pred T}) (leT : rel T). - -(* One easy way to prove the correctness of highly optimized stable sort *) -(* algorithms is to prove the equivalence between it and a simpler (but *) -(* unoptimized) algorithm, e.g., insertion sort. However, such equivalence *) -(* proof requires the comparison function [leT : rel T] to be total and *) -(* transitive so that [merge] is associative. These requirements are *) -(* undesirable since some correctness properties hold without them. *) -(* Therefore, we present a type of binary trees [trace] representing the *) -(* divide-and-conquer structure of sort. These trees can also be seen as *) -(* "traces" of sorting algorithms, and have to be balanced in the case of *) -(* O(n log n) mergesort. Nevertheless, these trees can also represent rather *) -(* naive algorithms such as insertion sort, since there is no such formal *) -(* "balanced" restriction. *) -Inductive trace := - | branch_trace : bool -> trace -> trace -> trace - | leaf_trace b s : sorted (fun x y => leT x y == b) s -> trace. - -Definition empty_trace := @leaf_trace false [::] erefl. - -(* By flattening a trace, the input list can be obtained. *) -Fixpoint flatten_trace (t : trace) : seq T := - match t with - | branch_trace _ l r => flatten_trace l ++ flatten_trace r - | leaf_trace _ s _ => s - end. - -(* By sorting a trace, the output list can be obtained. *) -Fixpoint sort_trace (t : trace) : seq T := - match t with - | branch_trace true l r => merge leT (sort_trace l) (sort_trace r) - | branch_trace false l r => - rev (merge (fun x y => leT y x) (rev (sort_trace r)) (rev (sort_trace l))) - | leaf_trace true s _ => s - | leaf_trace false s _ => rev s - end. - -Lemma all_trace (t : trace) : all P (sort_trace t) = all P (flatten_trace t). -Proof. -elim: t => [b l IHl r IHr|[] s] /=; rewrite ?all_rev //. -by case: b; rewrite ?(all_rev, all_merge) all_cat IHl IHr // andbC. -Qed. - -Lemma size_trace (t : trace) : size (sort_trace t) = size (flatten_trace t). -Proof. -elim: t => [b l IHl r IHr|[] s] /=; rewrite ?size_rev //. -by case: b; rewrite ?(size_rev, size_merge, size_cat) IHl IHr // addnC. -Qed. - -Lemma trace_nilp (t : trace) : nilp (sort_trace t) = nilp (flatten_trace t). -Proof. -by move: (sort_trace t) (flatten_trace t) (size_trace t) => [|? ?] []. -Qed. - -Variant trace_nil_spec (t : trace) : seq T -> seq T -> bool -> bool -> Type := - | TraceNil : flatten_trace t = [::] -> sort_trace t = [::] -> - trace_nil_spec t [::] [::] true true - | TraceNotNil : flatten_trace t <> [::] -> sort_trace t <> [::] -> - trace_nil_spec t (flatten_trace t) (sort_trace t) false false. - -Lemma trace_nilP (t : trace) : - trace_nil_spec t (flatten_trace t) (sort_trace t) - (nilp (flatten_trace t)) (nilp (sort_trace t)). -Proof. -case: nilP (trace_nilp t); case: nilP => //; last by constructor. -by move=> /[dup] ? -> /[dup] ? ->; constructor. -Qed. - -Definition trace_sort sort := forall s, - {t : trace | s = flatten_trace t & sort s = sort_trace t}. - -End Traces. - -Lemma perm_trace (T : eqType) (leT : rel T) (t : trace leT) : - perm_eql (sort_trace t) (flatten_trace t). -Proof. -apply/permPl; elim: t => [b l IHl r IHr|[] s _] //=; rewrite ?perm_rev //. -by case: b; rewrite /= ?perm_rev perm_merge -?rev_cat ?perm_rev perm_cat. -Qed. - -Parametricity Translation - (forall T : Type, rel T -> seq T -> seq T) as sort_ty_R. +(* the type of polymorphic sort functions *) +Definition sort_ty := + forall T : Type, (* the type of elements *) + rel T -> (* the comparison function [leT] *) + seq T -> (* input *) + seq T. (* output *) + +(* the type of sort functions abstracted over the type of sorted lists and *) +(* some operations on them, e.g., merge *) +Definition asort_ty := + forall T : Type, (* the type of elements *) + forall R : Type, (* the type of sorted lists *) + rel T -> (* the comparison function [leT] *) + (R -> R -> R) -> (* merge by [leT] *) + (R -> R -> R) -> (* merge by the converse of [leT] *) + (T -> R) -> (* singleton sorted list *) + R -> (* empty sorted list *) + seq T -> (* input *) + R. (* output *) + +Parametricity sort_ty. +Parametricity asort_ty. Structure function := Pack { + (* the sort function *) apply : forall T : Type, rel T -> seq T -> seq T; - (* Binary parametricity *) - (* _ : forall T1 T2 (T_R : T1 -> T2 -> Type) *) - (* (leT1 : rel T1) (leT2 : rel T2), *) - (* (forall (x1 : T1) (y1 : T2), T_R x1 y1 -> *) - (* forall (x2 : T1) (y2 : T2), T_R x2 y2 -> *) - (* bool_R (leT1 x1 x2) (leT2 y1 y2)) -> *) - (* forall (xs : seq T1) (ys : seq T2), *) - (* list_R T_R xs ys -> list_R T_R (apply leT1 xs) (apply leT2 ys); *) - _ : sort_ty_R apply apply; - (* Characterization by traces *) - _ : forall (T : Type) (leT : rel T), trace_sort leT (apply leT); + (* the *abstract* sort function *) + asort : asort_ty; + (* the binary parametricity of [asort] *) + _ : asort_ty_R asort asort; + (* [asort] instantiated with merge is extensionally equal to [apply] *) + _ : forall T (leT : rel T), + let geT x y := leT y x in + asort leT (merge leT) (fun xs ys => rev (merge geT (rev ys) (rev xs))) + (fun x => [:: x]) [::] + =1 apply leT; + (* [asort] instantiated with concatenation is the identity function *) + _ : forall T (leT : rel T), asort leT cat cat (fun x => [:: x]) [::] =1 id; }. Module Exports. -Arguments leaf_trace {T leT} b s _. -Arguments empty_trace {T leT}. -Arguments flatten_trace {T leT} t. -Arguments sort_trace {T leT} t. -Arguments Pack apply _ _ : clear implicits. +Arguments Pack apply asort _ _ _ : clear implicits. Notation stableSort := function. Notation StableSort := Pack. Coercion apply : function >-> Funclass. @@ -126,44 +62,21 @@ End Exports. End StableSort. Export StableSort.Exports. -Notation "[ tr]" := StableSort.empty_trace. -Notation "[ 'tr<=' ]" := (StableSort.leaf_trace true [::] erefl) - (format "[ 'tr<=' ]"). -Notation "[ 'tr<=' x ]" := (StableSort.leaf_trace true [:: x] erefl) - (format "[ 'tr<=' x ]"). - -Lemma trace2_subproof T (leT : rel T) (x y : T) : - sorted (fun x' y' => leT x' y' == leT x y) [:: x; y]. -Proof. by rewrite /= eqxx. Qed. - -Notation "[ 'tr' x1 ; x2 ]" := - (StableSort.leaf_trace _ [:: x1; x2] (trace2_subproof _ x1 x2)) - (format "[ 'tr' x1 ; x2 ]"). - (******************************************************************************) (* Merge functions *) (******************************************************************************) -Module MergeR. -Definition merge_ty := forall (T : Type) (leT : rel T), seq T -> seq T -> seq T. -Parametricity merge_ty. -End MergeR. - (* The [MergeSig] and [RevmergeSig] module types are interfaces for *) (* non-tail-recursive and tail-recursive merge functions, respectively. *) Module Type MergeSig. -Import MergeR. Parameter merge : forall (T : Type) (leT : rel T), seq T -> seq T -> seq T. Parameter mergeE : forall (T : Type) (leT : rel T), merge leT =2 path.merge leT. -Parameter merge_R : merge_ty_R merge merge. End MergeSig. Module Type RevmergeSig. -Import MergeR. Parameter revmerge : forall (T : Type) (leT : rel T), seq T -> seq T -> seq T. Parameter revmergeE : forall (T : Type) (leT : rel T) (xs ys : seq T), revmerge leT xs ys = rev (path.merge leT xs ys). -Parameter revmerge_R : merge_ty_R revmerge revmerge. End RevmergeSig. (* The [Merge] module implements a non-tail-recursive merge function using *) @@ -181,8 +94,6 @@ Fixpoint merge (T : Type) (leT : rel T) (xs ys : seq T) : seq T := Lemma mergeE (T : Type) (leT : rel T) : merge leT =2 path.merge leT. Proof. by elim=> // x xs IHxs; elim=> //= y ys IHys; rewrite IHxs IHys. Qed. -Parametricity merge. - End Merge. (* The [MergeAcc] module implements a non-tail-recursive merge function using *) @@ -201,12 +112,12 @@ Fixpoint wf_mergeord (T : Type) (xs ys : seq T) : Acc mergeord (xs, ys) := (x :: xs', y :: ys') (fun _ H => match H with - | or_introl H0 => - let: erefl in (_ = y1) := H0 return Acc mergeord y1 in - wf_mergeord xs' (y :: ys') - | or_intror H0 => - let: erefl in (_ = y1) := H0 return Acc mergeord y1 in - wf_mergeord' ys' + | or_introl H0 => + let: erefl in (_ = y1) := H0 return Acc mergeord y1 in + wf_mergeord xs' (y :: ys') + | or_intror H0 => + let: erefl in (_ = y1) := H0 return Acc mergeord y1 in + wf_mergeord' ys' end) else Acc_intro (x :: xs', [::]) (fun _ => False_ind _)) ys @@ -216,22 +127,22 @@ Fixpoint wf_mergeord (T : Type) (xs ys : seq T) : Acc mergeord (xs, ys) := Fixpoint merge_rec (T : Type) (leT : rel T) (xs ys : seq T) (fuel : Acc mergeord (xs, ys)) : seq T := match fuel, xs, ys return xs = _ -> ys = _ -> _ with - | _, [::], ys => fun _ _ => ys - | _, xs, [::] => fun _ _ => xs - | Acc_intro fuel, x :: xs', y :: ys' => - fun (xsE : x :: xs' = xs) (ysE : y :: ys' = ys) => - if leT x y then - x :: @merge_rec T leT xs' ys - (fuel _ match xsE in _ = xs0, ysE in _ = ys0 - return mergeord (xs', ys0) (xs0, ys0) with - erefl, erefl => or_introl erefl - end) - else - y :: @merge_rec T leT xs ys' - (fuel _ match xsE in _ = xs0, ysE in _ = ys0 - return mergeord (xs0, ys') (xs0, ys0) with - erefl, erefl => or_intror erefl - end) + | _, [::], ys => fun _ _ => ys + | _, xs, [::] => fun _ _ => xs + | Acc_intro fuel, x :: xs', y :: ys' => + fun (xsE : x :: xs' = xs) (ysE : y :: ys' = ys) => + if leT x y then + x :: @merge_rec T leT xs' ys + (fuel _ match xsE in _ = xs0, ysE in _ = ys0 + return mergeord (xs', ys0) (xs0, ys0) with + erefl, erefl => or_introl erefl + end) + else + y :: @merge_rec T leT xs ys' + (fuel _ match xsE in _ = xs0, ysE in _ = ys0 + return mergeord (xs0, ys') (xs0, ys0) with + erefl, erefl => or_intror erefl + end) end erefl erefl. Definition merge (T : Type) (leT : rel T) (xs ys : seq T) : seq T := @@ -243,10 +154,6 @@ rewrite /merge => xs ys; move: xs ys (wf_mergeord xs ys). by elim=> [|x xs IHxs]; elim=> [|y ys IHys] [acc] //=; rewrite IHxs IHys. Qed. -Parametricity mergeord. -Parametricity wf_mergeord. -Parametricity merge. - End MergeAcc. (* The [Revmerge] module implements a tail-recursive merge function using *) @@ -275,8 +182,6 @@ elim: xs ys [::] => [|x xs IHxs]; elim=> [|y ys IHys] accu //=; by case: ifP => _; rewrite rev_cons cat_rcons. Qed. -Parametricity revmerge. - End Revmerge. (* The [RevmergeAcc] module implements a tail-recursive merge function using *) @@ -288,22 +193,22 @@ Import MergeAcc. Fixpoint merge_rec (T : Type) (leT : rel T) (xs ys accu : seq T) (fuel : Acc mergeord (xs, ys)) : seq T := match fuel, xs, ys return xs = _ -> ys = _ -> _ with - | _, [::], ys => fun _ _ => catrev ys accu - | _, xs, [::] => fun _ _ => catrev xs accu - | Acc_intro fuel, x :: xs', y :: ys' => - fun (xsE : x :: xs' = xs) (ysE : y :: ys' = ys) => - if leT x y then - @merge_rec T leT xs' ys (x :: accu) - (fuel _ match xsE in _ = xs0, ysE in _ = ys0 - return mergeord (xs', ys0) (xs0, ys0) with - erefl, erefl => or_introl erefl - end) - else - @merge_rec T leT xs ys' (y :: accu) - (fuel _ match xsE in _ = xs0, ysE in _ = ys0 - return mergeord (xs0, ys') (xs0, ys0) with - erefl, erefl => or_intror erefl - end) + | _, [::], ys => fun _ _ => catrev ys accu + | _, xs, [::] => fun _ _ => catrev xs accu + | Acc_intro fuel, x :: xs', y :: ys' => + fun (xsE : x :: xs' = xs) (ysE : y :: ys' = ys) => + if leT x y then + @merge_rec T leT xs' ys (x :: accu) + (fuel _ match xsE in _ = xs0, ysE in _ = ys0 + return mergeord (xs', ys0) (xs0, ys0) with + erefl, erefl => or_introl erefl + end) + else + @merge_rec T leT xs ys' (y :: accu) + (fuel _ match xsE in _ = xs0, ysE in _ = ys0 + return mergeord (xs0, ys') (xs0, ys0) with + erefl, erefl => or_intror erefl + end) end erefl erefl. Definition revmerge (T : Type) (leT : rel T) (xs ys : seq T) : seq T := @@ -318,8 +223,6 @@ elim=> [|x xs IHxs]; elim=> [|y ys IHys] accu [acc] //=; by case: ifP => _; rewrite rev_cons cat_rcons. Qed. -Parametricity revmerge. - End RevmergeAcc. (******************************************************************************) @@ -327,25 +230,31 @@ End RevmergeAcc. (******************************************************************************) Module Insertion. + +Module Abstract. + +Definition sort (T R : Type) (leT : rel T) + (merge : R -> R -> R) (merge' : R -> R -> R) + (singleton : T -> R) (empty : R) := + foldr (fun x => merge (singleton x)) empty. + +Parametricity sort. + +End Abstract. + Section Insertion. Variables (T : Type) (leT : rel T). -Definition sort := foldr (fun x => merge leT [:: x]) [::]. +Definition sort : seq T -> seq T := foldr (fun x => merge leT [:: x]) [::]. -Import StableSort. - -Lemma sortP : trace_sort leT sort. -Proof. -elim=> [|x _ [t -> /= ->]]; first by exists empty_trace. -by exists (branch_trace true (leaf_trace true [:: x] erefl) t). -Qed. +Lemma asort_catE : Abstract.sort leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. by elim=> //= x xs ->. Qed. End Insertion. -Parametricity sort. - -Definition sort_stable := StableSort.Pack sort sort_R sortP. +Definition sort_stable := + StableSort sort Abstract.sort Abstract.sort_R (fun _ _ _ => erefl) asort_catE. End Insertion. @@ -375,195 +284,304 @@ Canonical Insertion.sort_stable. Module CBN_ (M : MergeSig). +Module Abstract. +Section Abstract. + +Variables (T R : Type) (leT : rel T). +Variables (merge : R -> R -> R) (merge' : R -> R -> R). +Variables (singleton : T -> R) (empty : R). + +Fixpoint push (xs : R) (stack : seq (option R)) : seq (option R) := + match stack with + | None :: stack | [::] as stack => Some xs :: stack + | Some ys :: stack => None :: push (merge ys xs) stack + end. + +Fixpoint pop (xs : R) (stack : seq (option R)) : R := + match stack with + | [::] => xs + | None :: stack => pop xs stack + | Some ys :: stack => pop (merge ys xs) stack + end. + +Fixpoint sort1rec (stack : seq (option R)) (xs : seq T) : R := + if xs is x :: xs then + sort1rec (push (singleton x) stack) xs + else + pop empty stack. + +#[using="All"] +Definition sort1 : seq T -> R := sort1rec [::]. + +Fixpoint sort2rec (stack : seq (option R)) (xs : seq T) : R := + match xs with + | [:: x1, x2 & xs] => + sort2rec (push (merge (singleton x1) (singleton x2)) stack) xs + | [:: x] => pop (singleton x) stack + | [::] => pop empty stack + end. + +#[using="All"] +Definition sort2 : seq T -> R := sort2rec [::]. + +Fixpoint sort3rec (stack : seq (option R)) (xs : seq T) : R := + match xs with + | [:: x1, x2, x3 & xs] => + let t := merge' (merge (singleton x1) (singleton x2)) (singleton x3) in + sort3rec (push t stack) xs + | [:: x1; x2] => pop (merge (singleton x1) (singleton x2)) stack + | [:: x] => pop (singleton x) stack + | [::] => pop empty stack + end. + +#[using="All"] +Definition sort3 : seq T -> R := sort3rec [::]. + +Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R := + if xs is y :: xs then + if leT x y then + incr stack y xs (singleton x) + else + decr stack y xs (singleton x) + else + pop (singleton x) stack +with incr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := + if xs is y :: xs then + if leT x y then + incr stack y xs (merge' accu (singleton x)) + else + sortNrec (push (merge' accu (singleton x)) stack) y xs + else + pop (merge' accu (singleton x)) stack +with decr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := + if xs is y :: xs then + if leT x y then + sortNrec (push (merge accu (singleton x)) stack) y xs + else + decr stack y xs (merge accu (singleton x)) + else + pop (merge accu (singleton x)) stack. + +#[using="All"] +Definition sortN (xs : seq T) : R := + if xs is x :: xs then sortNrec [::] x xs else empty. + +End Abstract. + +Parametricity sort1. +Parametricity sort2. +Parametricity sort3. +Parametricity sortN. + +End Abstract. + Section CBN. Variable (T : Type) (leT : rel T). -Let condrev (r : bool) (s : seq T) : seq T := if r then rev s else s. - -Fixpoint merge_sort_push (s : seq T) (stack : seq (seq T)) : seq (seq T) := +Fixpoint push (xs : seq T) (stack : seq (seq T)) : seq (seq T) := match stack with - | [::] :: stack' | [::] as stack' => s :: stack' - | s' :: stack' => [::] :: merge_sort_push (M.merge leT s' s) stack' + | [::] :: stack | [::] as stack => xs :: stack + | ys :: stack => [::] :: push (M.merge leT ys xs) stack end. -Fixpoint merge_sort_pop (s1 : seq T) (stack : seq (seq T)) : seq T := - if stack is s2 :: stack' then - merge_sort_pop (M.merge leT s2 s1) stack' else s1. +Fixpoint pop (xs : seq T) (stack : seq (seq T)) : seq T := + if stack is ys :: stack then pop (M.merge leT ys xs) stack else xs. -Fixpoint sort1rec (stack : seq (seq T)) (s : seq T) : seq T := - if s is x :: s then sort1rec (merge_sort_push [:: x] stack) s else - merge_sort_pop [::] stack. +Fixpoint sort1rec (stack : seq (seq T)) (xs : seq T) : seq T := + if xs is x :: xs then sort1rec (push [:: x] stack) xs else pop [::] stack. Definition sort1 : seq T -> seq T := sort1rec [::]. -Fixpoint sort2rec (stack : seq (seq T)) (s : seq T) : seq T := - if s is [:: x1, x2 & s'] then - let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in - sort2rec (merge_sort_push s1 stack) s' - else merge_sort_pop s stack. +Fixpoint sort2rec (stack : seq (seq T)) (xs : seq T) : seq T := + if xs is [:: x1, x2 & xs] then + let t := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in + sort2rec (push t stack) xs + else pop xs stack. Definition sort2 : seq T -> seq T := sort2rec [::]. -Fixpoint sort3rec (stack : seq (seq T)) (s : seq T) : seq T := - match s with - | [:: x1, x2, x3 & s'] => - let s1 := - if leT x1 x2 then - if leT x2 x3 then [:: x1; x2; x3] - else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2] - else - if leT x1 x3 then [:: x2; x1; x3] - else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1] - in - sort3rec (merge_sort_push s1 stack) s' - | [:: x1; x2] => - merge_sort_pop (if leT x1 x2 then s else [:: x2; x1]) stack - | _ => merge_sort_pop s stack +Fixpoint sort3rec (stack : seq (seq T)) (xs : seq T) : seq T := + match xs with + | [:: x1, x2, x3 & xs] => + let t := + if leT x1 x2 then + if leT x2 x3 then [:: x1; x2; x3] + else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2] + else + if leT x1 x3 then [:: x2; x1; x3] + else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1] + in + sort3rec (push t stack) xs + | [:: x1; x2] => pop (if leT x1 x2 then xs else [:: x2; x1]) stack + | _ => pop xs stack end. Definition sort3 : seq T -> seq T := sort3rec [::]. -Fixpoint sortNrec (stack : seq (seq T)) (x : T) (s : seq T) : seq T := - if s is y :: s then - if leT x y then incr stack y s [:: x] else decr stack y s [:: x] +Fixpoint sortNrec (stack : seq (seq T)) (x : T) (xs : seq T) : seq T := + if xs is y :: xs then + if leT x y then incr stack y xs [:: x] else decr stack y xs [:: x] else - merge_sort_pop [:: x] stack -with incr (stack : seq (seq T)) (x : T) (s accu : seq T) : seq T := - if s is y :: s then + pop [:: x] stack +with incr (stack : seq (seq T)) (x : T) (xs accu : seq T) : seq T := + if xs is y :: xs then if leT x y then - incr stack y s (x :: accu) + incr stack y xs (x :: accu) else - sortNrec (merge_sort_push (catrev accu [:: x]) stack) y s + sortNrec (push (catrev accu [:: x]) stack) y xs else - merge_sort_pop (catrev accu [:: x]) stack -with decr (stack : seq (seq T)) (x : T) (s accu : seq T) : seq T := - if s is y :: s then + pop (catrev accu [:: x]) stack +with decr (stack : seq (seq T)) (x : T) (xs accu : seq T) : seq T := + if xs is y :: xs then if leT x y then - sortNrec (merge_sort_push (x :: accu) stack) y s + sortNrec (push (x :: accu) stack) y xs else - decr stack y s (x :: accu) + decr stack y xs (x :: accu) else - merge_sort_pop (x :: accu) stack. + pop (x :: accu) stack. -Definition sortN (s : seq T) : seq T := - if s is x :: s then sortNrec [::] x s else [::]. +Definition sortN (xs : seq T) : seq T := + if xs is x :: xs then sortNrec [::] x xs else [::]. (* Proofs *) -Import StableSort. +Let geT x y := leT y x. +Let astack_of_stack : seq (seq T) -> seq (option (seq T)) := + map (fun xs => if xs is [::] then None else Some xs). -Local Notation trace_sort := (trace_sort leT). -Let flatten_stack := foldr (fun x => cat^~ (@flatten_trace _ leT x)) nil. +Notation merge := (path.merge leT) (only parsing). +Notation merge' := + (fun xs ys => rev (path.merge geT (rev ys) (rev xs))) (only parsing). +Notation flatten_stack := + (foldl (fun xs : seq T => oapp (cat^~ xs) xs)) (only parsing). -Definition trace_sort_rec sort_rec := forall s stack, {t : trace leT | - flatten_stack stack ++ s = flatten_trace t & - sort_rec [seq sort_trace i | i <- stack] s = sort_trace t}. +Lemma apop_mergeE xs stack : + Abstract.pop merge xs (astack_of_stack stack) = pop xs stack. +Proof. +by elim: stack xs => [|[|y ys] stack IHstack] xs //=; rewrite M.mergeE IHstack. +Qed. -Lemma trace_sortP sort : trace_sort_rec sort -> trace_sort (sort [::]). -Proof. by move/(_ _ [::]). Qed. +Lemma apush_mergeE xs stack : + ~~ nilp xs -> + Abstract.push merge xs (astack_of_stack stack) + = astack_of_stack (push xs stack). +Proof. +elim: stack xs => [|[|y ys] stack IHstack]; try by case. +by move=> xs Hxs /=; rewrite M.mergeE IHstack // /nilp size_merge. +Qed. -Lemma merge_sort_pushP (t : trace leT) (stack : seq (trace leT)) : - {stack' : seq (trace leT) | - flatten_stack (t :: stack) = flatten_stack stack' & - merge_sort_push (sort_trace t) (map sort_trace stack) = - map sort_trace stack'}. +Lemma asort1_mergeE : + Abstract.sort1 leT merge merge' (fun x => [:: x]) [::] =1 sort1. Proof. -elim: stack t => [|t' stack IHstack] t /=; first by exists [:: t]. -rewrite M.mergeE ifnilE -catA; case: trace_nilP => _ _. - by exists (t :: stack); rewrite //= cats0. -have [/= {IHstack}stack -> ->] := IHstack (branch_trace true t' t). -by exists (empty_trace :: stack); rewrite //= cats0. +rewrite /Abstract.sort1 /sort1 -[Nil (option _)]/(astack_of_stack [::]) => xs. +elim: xs (Nil (seq _)) => /= [|x xs IHxs] stack; first by rewrite apop_mergeE. +by rewrite -IHxs apush_mergeE. Qed. -Lemma merge_sort_popP (t : trace leT) (stack : seq (trace leT)) : - {t' : trace leT | - flatten_stack (t :: stack) = flatten_trace t' & - merge_sort_pop (sort_trace t) (map sort_trace stack) = sort_trace t'}. +Lemma asort2_mergeE : + Abstract.sort2 leT merge merge' (fun x => [:: x]) [::] =1 sort2. Proof. -elim: stack t => [|t' stack IHstack] t; first by exists t; rewrite //= cats0. -rewrite /= M.mergeE -catA. -by have [/= t'' -> ->] := IHstack (branch_trace true t' t); exists t''. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort2 /sort2 -[Nil (option _)]/(astack_of_stack [::]). +elim: n (Nil (seq _)) xs => // n IHn stack [|x [|x' xs /= /ltnW /IHn <-]] /=; + try by rewrite apop_mergeE. +by rewrite apush_mergeE; last case: ifP. Qed. -Lemma sort1P : trace_sort sort1. +Lemma asort3_mergeE : + Abstract.sort3 leT merge merge' (fun x => [:: x]) [::] =1 sort3. Proof. -apply/trace_sortP; elim=> [|x s IHs] stack; first exact: merge_sort_popP [tr] _. -case: (merge_sort_pushP [tr<= x] stack). -by rewrite (catA _ [:: _]) => {}stack /= -> ->; exact: IHs. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort3 /sort3 -[Nil (option _)]/(astack_of_stack [::]). +move: n (Nil (seq _)) xs. +elim=> // n IHn stack [|x [|x' [|x'' xs /= /ltnW /ltnW /IHn <-]]] /=; + try by rewrite apop_mergeE. +rewrite apush_mergeE; last by rewrite /nilp !(size_rev, size_merge). +by rewrite !(fun_if rev, fun_if (path.merge _ _), fun_if (cons _)). Qed. -Lemma sort2P : trace_sort sort2. +Lemma asortN_mergeE : + Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. -apply/trace_sortP => s; have [n] := ubnP (size s); elim: n s => // n IHn. -move=> [|x [|y s]]/=; rewrite ?ltnS => size_s stack. -- exact: merge_sort_popP [tr<=] _. -- exact: merge_sort_popP [tr<= x] _. -case: (merge_sort_pushP [tr x; y] stack). -by rewrite (catA _ [:: _; _]) => /= {}stack -> ->; apply/IHn/ltnW. +case=> // x xs; have [n] := ubnP (size xs). +rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack [::]). +elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs]. + by rewrite [LHS]apop_mergeE. +rewrite /Abstract.sortNrec. +rewrite -/(Abstract.incr _ _ merge' _) -/(Abstract.decr _ _ merge' _). +pose rs := Nil T; rewrite -{1}[[:: x]]/(rcons (rev rs) x) -/(x :: rs). +elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. + rewrite /Abstract.incr /Abstract.decr !apop_mergeE rev_rcons revK /= /geT. + by case: leT. +rewrite /Abstract.incr -/(Abstract.incr _ _ merge' _). +rewrite /Abstract.decr -/(Abstract.decr _ _ merge' _). +rewrite -/(Abstract.sortNrec _ _ merge' _). +move: (IHxs Hxs y z (x :: rs)); rewrite -rev_cons rev_rcons revK /= /geT. +by do 2 case: leT; rewrite // apush_mergeE ?rev_nilp // IHn. Qed. -Lemma sort3P : trace_sort sort3. +Lemma apush_catE (xs ys : seq T) stack : + flatten_stack ys (Abstract.push cat xs stack) + = flatten_stack (xs ++ ys) stack. Proof. -apply/trace_sortP => s; have [n] := ubnP (size s); elim: n s => // n IHn. -move=> [|x [|y [|z s]]]/=; rewrite ?ltnS => size_s stack. -- exact: merge_sort_popP [tr<=] _. -- exact: merge_sort_popP [tr<= x] _. -- exact: merge_sort_popP [tr x; y] _. -rewrite (catA _ [:: _; _; _]). -pose xyz : trace leT := branch_trace false [tr x; y] [tr<= z]. -case: (merge_sort_pushP xyz stack) => /= stack' ->. -set push1 := merge_sort_push _ _; set push2 := merge_sort_push _ _. -have ->: push1 = push2 by congr merge_sort_push; do 3 case: ifP => //=. -by move=> ->; apply/IHn/ltnW/ltnW. +by elim: stack xs => [|[zs|] stack IHstack] xs //=; rewrite IHstack catA. Qed. -Lemma sortNP : trace_sort sortN. +Lemma apop_catE xs stack : Abstract.pop cat xs stack = flatten_stack xs stack. +Proof. by elim: stack xs => [|[]] /=. Qed. + +Lemma asort1_catE : Abstract.sort1 leT cat cat (fun x => [:: x]) [::] =1 id. Proof. -case=> /= [|x s]; first by exists empty_trace. -suff /(_ [::]) : forall stack, {t : trace leT | - flatten_stack stack ++ x :: s = flatten_trace t & - sortNrec [seq sort_trace i | i <- stack] x s = sort_trace t} by []. -have [n] := ubnP (size s); elim: n x s => // n IHn x [|y s]/= sn stack. - exact: merge_sort_popP [tr<= x] _. -set lexy := leT x y. -have: path (fun y x => leT x y == lexy) y [:: x] by rewrite /= eqxx. -have ->: [:: x, y & s] = rev [:: y; x] ++ s by []. -elim: s sn (lexy) (y) [:: x] => {lexy x y} => [|y s IHs' /=] /ltnW sn ord x acc. - rewrite -/(sorted _ (_ :: _)) -rev_sorted cats0 => sorted_acc. - case: (merge_sort_popP (leaf_trace ord _ sorted_acc) stack) => /= t ->. - by rewrite revK; case: ord {sorted_acc} => ->; exists t. -case: ord (boolP (leT x y)) => [] [] lexy. -- move=> path_acc. - have: path (fun y x => leT x y == true) y (x :: acc) by rewrite /= lexy eqxx. - by move=> /(IHs' sn)[t]; rewrite -cat_rcons -rev_cons => -> ->; exists t. -- rewrite -/(sorted _ (_ :: _)) -rev_sorted => sorted_acc. - case: (merge_sort_pushP (leaf_trace true _ sorted_acc) stack) => stack'. - by rewrite /= catA => -> ->; apply/IHn. -- rewrite -/(sorted _ (_ :: _)) -rev_sorted => sorted_acc. - case: (merge_sort_pushP (leaf_trace false _ sorted_acc) stack) => stack'. - by rewrite /= catA revK => -> ->; apply/IHn. -- move=> path_acc. - have: path (fun y x => leT x y == false) y (x :: acc). - by rewrite /= eqbF_neg lexy. - by move=> /(IHs' sn)[t]; rewrite -cat_rcons -rev_cons => -> ->; exists t. +move=> xs; rewrite /Abstract.sort1 -[RHS]/(flatten_stack xs [::]). +elim: xs (Nil (option _)) => /= [|x xs IHxs] stack; first exact: apop_catE. +by rewrite IHxs apush_catE. Qed. -End CBN. +Lemma asort2_catE : Abstract.sort2 leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort2 -[RHS]/(flatten_stack xs [::]). +move: n (Nil (option _)) xs. +by elim=> // n IHn stack [|x [|x' xs /= /ltnW /IHn ->]] /=; + rewrite (apop_catE, apush_catE). +Qed. -Realizer M.merge as merge_R arity 2 := M.merge_R. +Lemma asort3_catE : Abstract.sort3 leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort3 -[RHS]/(flatten_stack xs [::]). +move: n (Nil (option _)) xs. +by elim=> // n IHn stack [|x [|x' [|x'' xs /= /ltnW /ltnW /IHn ->]]] /=; + rewrite (apop_catE, apush_catE). +Qed. -Parametricity merge_sort_push. -Parametricity merge_sort_pop. -Parametricity sort1. -Parametricity sort2. -Parametricity sort3. -Parametricity sortN. +Lemma asortN_catE : Abstract.sortN leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +case=> // x xs; have [n] := ubnP (size xs). +rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]). +elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs]; + first by rewrite [LHS]apop_catE. +rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). +pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _). +elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. + by rewrite if_same [LHS]apop_catE -catA. +rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). +rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +move: (IHxs Hxs y z (rcons rs x)); rewrite IHn // apush_catE -cats1 -!catA /=. +by case: leT => ->; rewrite if_same. +Qed. + +End CBN. -Definition sort1_stable := StableSort.Pack sort1 sort1_R sort1P. -Definition sort2_stable := StableSort.Pack sort2 sort2_R sort2P. -Definition sort3_stable := StableSort.Pack sort3 sort3_R sort3P. -Definition sortN_stable := StableSort.Pack sortN sortN_R sortNP. +Definition sort1_stable := + StableSort sort1 Abstract.sort1 Abstract.sort1_R asort1_mergeE asort1_catE. +Definition sort2_stable := + StableSort sort2 Abstract.sort2 Abstract.sort2_R asort2_mergeE asort2_catE. +Definition sort3_stable := + StableSort sort3 Abstract.sort3 Abstract.sort3_R asort3_mergeE asort3_catE. +Definition sortN_stable := + StableSort sortN Abstract.sortN Abstract.sortN_R asortN_mergeE asortN_catE. End CBN_. @@ -599,231 +617,346 @@ Canonical CBNAcc.sortN_stable. (******************************************************************************) Module CBV_ (M : RevmergeSig). + +Module Abstract. +Section Abstract. + +Variables (T R : Type) (leT : rel T). +Variables (merge : R -> R -> R) (merge' : R -> R -> R). +Variables (singleton : T -> R) (empty : R). + +Fixpoint push (xs : R) (stack : seq (option R)) : seq (option R) := + match stack with + | None :: stack | [::] as stack => Some xs :: stack + | Some ys :: None :: stack | Some ys :: ([::] as stack) => + None :: Some (merge ys xs) :: stack + | Some ys :: Some zs :: stack => + None :: None :: push (merge' zs (merge ys xs)) stack + end. + +Fixpoint pop (mode : bool) (xs : R) (stack : seq (option R)) : R := + match stack with + | [::] => xs + | None :: None :: stack => pop mode xs stack + | None :: stack => pop (~~ mode) xs stack + | (Some ys) :: stack => + pop (~~ mode) (if mode then merge' ys xs else merge ys xs) stack + end. + +Fixpoint sort1rec (stack : seq (option R)) (xs : seq T) : R := + if xs is x :: xs then + sort1rec (push (singleton x) stack) xs + else + pop false empty stack. + +#[using="All"] +Definition sort1 : seq T -> R := sort1rec [::]. + +Fixpoint sort2rec (stack : seq (option R)) (xs : seq T) : R := + match xs with + | [:: x1, x2 & xs] => + sort2rec (push (merge (singleton x1) (singleton x2)) stack) xs + | [:: x] => pop false (singleton x) stack + | [::] => pop false empty stack + end. + +#[using="All"] +Definition sort2 : seq T -> R := sort2rec [::]. + +Fixpoint sort3rec (stack : seq (option R)) (xs : seq T) : R := + match xs with + | [:: x1, x2, x3 & xs] => + let t := merge' (merge (singleton x1) (singleton x2)) (singleton x3) in + sort3rec (push t stack) xs + | [:: x1; x2] => pop false (merge (singleton x1) (singleton x2)) stack + | [:: x] => pop false (singleton x) stack + | [::] => pop false empty stack + end. + +#[using="All"] +Definition sort3 : seq T -> R := sort3rec [::]. + +Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R := + if xs is y :: xs then + if leT x y then + incr stack y xs (singleton x) + else + decr stack y xs (singleton x) + else + pop false (singleton x) stack +with incr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := + if xs is y :: xs then + if leT x y then + incr stack y xs (merge' accu (singleton x)) + else + sortNrec (push (merge' accu (singleton x)) stack) y xs + else + pop false (merge' accu (singleton x)) stack +with decr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := + if xs is y :: xs then + if leT x y then + sortNrec (push (merge accu (singleton x)) stack) y xs + else + decr stack y xs (merge accu (singleton x)) + else + pop false (merge accu (singleton x)) stack. + +#[using="All"] +Definition sortN (xs : seq T) : R := + if xs is x :: xs then sortNrec [::] x xs else empty. + +End Abstract. + +Parametricity sort1. +Parametricity sort2. +Parametricity sort3. +Parametricity sortN. + +End Abstract. + Section CBV. Variables (T : Type) (leT : rel T). Let geT x y := leT y x. -Let condrev (r : bool) (s : seq T) : seq T := if r then rev s else s. - -Fixpoint merge_sort_push (xs : seq T) (stack : seq (seq T)) : seq (seq T) := +Fixpoint push (xs : seq T) (stack : seq (seq T)) : seq (seq T) := match stack with - | [::] :: stack' | [::] as stack' => xs :: stack' - | ys :: [::] :: stack | ys :: ([::] as stack) => - [::] :: M.revmerge leT ys xs :: stack - | ys :: zs :: stack => - [::] :: [::] :: - merge_sort_push (M.revmerge geT (M.revmerge leT ys xs) zs) stack + | [::] :: stack | [::] as stack => xs :: stack + | ys :: [::] :: stack | ys :: ([::] as stack) => + [::] :: M.revmerge leT ys xs :: stack + | ys :: zs :: stack => + [::] :: [::] :: push (M.revmerge geT (M.revmerge leT ys xs) zs) stack end. -Fixpoint merge_sort_pop - (mode : bool) (xs : seq T) (stack : seq (seq T)) : seq T := +Fixpoint pop (mode : bool) (xs : seq T) (stack : seq (seq T)) : seq T := match stack, mode with - | [::], true => rev xs - | [::], false => xs - | [::] :: [::] :: stack, _ => merge_sort_pop mode xs stack - | [::] :: stack, _ => merge_sort_pop (~~ mode) (rev xs) stack - | ys :: stack, true => merge_sort_pop false (M.revmerge geT xs ys) stack - | ys :: stack, false => merge_sort_pop true (M.revmerge leT ys xs) stack + | [::], true => rev xs + | [::], false => xs + | [::] :: [::] :: stack, _ => pop mode xs stack + | [::] :: stack, _ => pop (~~ mode) (rev xs) stack + | ys :: stack, true => pop false (M.revmerge geT xs ys) stack + | ys :: stack, false => pop true (M.revmerge leT ys xs) stack end. -Fixpoint sort1rec (stack : seq (seq T)) (s : seq T) : seq T := - if s is x :: s then sort1rec (merge_sort_push [:: x] stack) s else - merge_sort_pop false [::] stack. +Fixpoint sort1rec (stack : seq (seq T)) (xs : seq T) : seq T := + if xs is x :: xs then + sort1rec (push [:: x] stack) xs + else + pop false [::] stack. Definition sort1 : seq T -> seq T := sort1rec [::]. -Fixpoint sort2rec (stack : seq (seq T)) (s : seq T) : seq T := - if s is [:: x1, x2 & s'] then - let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in - sort2rec (merge_sort_push s1 stack) s' - else merge_sort_pop false s stack. +Fixpoint sort2rec (stack : seq (seq T)) (xs : seq T) : seq T := + if xs is [:: x1, x2 & xs] then + let t := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in + sort2rec (push t stack) xs + else pop false xs stack. Definition sort2 : seq T -> seq T := sort2rec [::]. -Fixpoint sort3rec (stack : seq (seq T)) (s : seq T) : seq T := - match s with - | [:: x1, x2, x3 & s'] => - let s1 := - if leT x1 x2 then - if leT x2 x3 then [:: x1; x2; x3] - else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2] - else - if leT x1 x3 then [:: x2; x1; x3] - else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1] - in - sort3rec (merge_sort_push s1 stack) s' - | [:: x1; x2] => - merge_sort_pop false (if leT x1 x2 then s else [:: x2; x1]) stack - | _ => merge_sort_pop false s stack +Fixpoint sort3rec (stack : seq (seq T)) (xs : seq T) : seq T := + match xs with + | [:: x1, x2, x3 & xs] => + let t := + if leT x1 x2 then + if leT x2 x3 then [:: x1; x2; x3] + else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2] + else + if leT x1 x3 then [:: x2; x1; x3] + else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1] + in + sort3rec (push t stack) xs + | [:: x1; x2] => pop false (if leT x1 x2 then xs else [:: x2; x1]) stack + | _ => pop false xs stack end. Definition sort3 : seq T -> seq T := sort3rec [::]. -Fixpoint sortNrec (stack : seq (seq T)) (x : T) (s : seq T) : seq T := - if s is y :: s then - if leT x y then incr stack y s [:: x] else decr stack y s [:: x] +Fixpoint sortNrec (stack : seq (seq T)) (x : T) (xs : seq T) : seq T := + if xs is y :: xs then + if leT x y then incr stack y xs [:: x] else decr stack y xs [:: x] else - merge_sort_pop false [:: x] stack -with incr (stack : seq (seq T)) (x : T) (s accu : seq T) : seq T := - if s is y :: s then + pop false [:: x] stack +with incr (stack : seq (seq T)) (x : T) (xs accu : seq T) : seq T := + if xs is y :: xs then if leT x y then - incr stack y s (x :: accu) + incr stack y xs (x :: accu) else - sortNrec (merge_sort_push (catrev accu [:: x]) stack) y s + sortNrec (push (catrev accu [:: x]) stack) y xs else - merge_sort_pop false (catrev accu [:: x]) stack -with decr (stack : seq (seq T)) (x : T) (s accu : seq T) : seq T := - if s is y :: s then + pop false (catrev accu [:: x]) stack +with decr (stack : seq (seq T)) (x : T) (xs accu : seq T) : seq T := + if xs is y :: xs then if leT x y then - sortNrec (merge_sort_push (x :: accu) stack) y s + sortNrec (push (x :: accu) stack) y xs else - decr stack y s (x :: accu) + decr stack y xs (x :: accu) else - merge_sort_pop false (x :: accu) stack. + pop false (x :: accu) stack. -Definition sortN (s : seq T) : seq T := - if s is x :: s then sortNrec [::] x s else [::]. +Definition sortN (xs : seq T) : seq T := + if xs is x :: xs then sortNrec [::] x xs else [::]. (* Proofs *) -Import StableSort. +Let condrev (r : bool) (s : seq T) : seq T := if r then rev s else s. -Local Notation trace_sort := (trace_sort leT). -Let flatten_stack := foldr (fun x => cat^~ (@flatten_trace _ leT x)) nil. +Lemma condrev_nilp mode xs : nilp (condrev mode xs) = nilp xs. +Proof. by case: mode; rewrite /= ?rev_nilp. Qed. -Let Fixpoint sort_stack (mode : bool) (stack : seq (trace leT)) : seq (seq T) := - if stack isn't t :: stack then [::] else - condrev mode (sort_trace t) :: sort_stack (~~ mode) stack. +Lemma condrevK mode : involutive (condrev mode). +Proof. by case: mode; first exact: revK. Qed. -Definition trace_sort_rec sort_rec := forall s stack, {t : trace leT | - flatten_stack stack ++ s = flatten_trace t & - sort_rec (sort_stack false stack) s = sort_trace t}. +Let Fixpoint astack_of_stack (mode : bool) (stack : seq (seq T)) := + match stack with + | [::] => [::] + | xs :: stack => + (if nilp xs then None else Some (condrev mode xs)) :: + astack_of_stack (~~ mode) stack + end. -Lemma trace_sortP sort : trace_sort_rec sort -> trace_sort (sort [::]). -Proof. by move/(_ _ [::]). Qed. +Notation merge := (path.merge leT) (only parsing). +Notation merge' := + (fun xs ys => rev (path.merge geT (rev ys) (rev xs))) (only parsing). +Notation flatten_stack := + (foldl (fun xs : seq T => oapp (cat^~ xs) xs)) (only parsing). -Lemma merge_sort_pushP (t : trace leT) (stack : seq (trace leT)) : - {stack' : seq (trace leT) | - flatten_stack (t :: stack) = flatten_stack stack' & - merge_sort_push (sort_trace t) (sort_stack false stack) - = sort_stack false stack'}. +Lemma apop_mergeE mode xs stack : + Abstract.pop merge merge' mode xs (astack_of_stack mode stack) + = pop mode (condrev mode xs) stack. Proof. -move: t stack; fix IHstack 2; move=> t [|t' [|t'' stack]] /=. -- by exists [:: t]. -- rewrite !M.revmergeE ifnilE trace_nilp; have [->|_] := nilP. - by exists [:: t]. - by exists [:: empty_trace; branch_trace true t' t]; rewrite //= cats0. -- rewrite !M.revmergeE !ifnilE rev_nilp !trace_nilp; have [->|_] := nilP. - by exists [:: t, t'' & stack]; rewrite ?cats0. - rewrite -!catA; have [->|_] := nilP. - exists [:: empty_trace, branch_trace true t' t & stack] => //. - by rewrite /= ?cats0. - have [/= {}stack -> ->] := - IHstack (branch_trace false t'' (branch_trace true t' t)) stack. - by exists [:: empty_trace, empty_trace & stack]; rewrite /= ?cats0. +have [n] := ubnP (size stack). +by elim: n mode xs stack => // n IHn [] xs [|[[|[|z zs] stack]|y ys stack]] /=; + rewrite ?M.revmergeE ?revK //; try move/(@ltnW _.+2); move=> /IHn ->. Qed. -Let nilp_condrev (r : bool) (s : seq T) : nilp (condrev r s) = nilp s. -Proof. by case: r; rewrite ?rev_nilp. Qed. +Lemma apush_mergeE xs stack : + ~~ nilp xs -> + Abstract.push merge merge' xs (astack_of_stack false stack) + = astack_of_stack false (push xs stack). +Proof. +have [n] := ubnP (size stack). +by elim: n xs stack => // n IHn xs [|[|y ys] [|[|z zs] stack]] //=; + try move=> /(@ltnW _.+2) /IHn ->; try (by case: ifP); + rewrite ?M.revmergeE revK /nilp ?(size_rev, size_merge, size_cat). +Qed. -Lemma merge_sort_popP (mode : bool) (t : trace leT) (stack : seq (trace leT)) : - {t' : trace leT | - flatten_stack (t :: stack) = flatten_trace t' & - merge_sort_pop mode (condrev mode (sort_trace t)) (sort_stack mode stack) - = sort_trace t'}. +Lemma asort1_mergeE : + Abstract.sort1 leT merge merge' (fun x => [:: x]) [::] =1 sort1. Proof. -move: mode t stack; fix IHstack 3; move=> mode t [|t' stack] /=. - by exists t => //; case: mode; rewrite ?revK. -rewrite -catA !M.revmergeE ifnilE nilp_condrev. -case: trace_nilP => _ _; last first. - by case: mode (IHstack (~~ mode) (branch_trace (~~ mode) t' t) stack). -case: stack => [|t'' stack] /=. - by exists t => //; case: mode; rewrite ?revK. -rewrite !M.revmergeE !ifnilE !nilp_condrev !negbK revK. -case: trace_nilP => _ _; first by rewrite cats0; apply: IHstack. -rewrite -catA. -by case: mode (IHstack mode (branch_trace mode t'' t) stack); rewrite //= revK. +rewrite /Abstract.sort1 /sort1 -/(astack_of_stack false [::]) => xs. +elim: xs (Nil (seq _)) => /= [|x xs IHxs] stack; first exact: apop_mergeE. +by rewrite -IHxs apush_mergeE. Qed. -Lemma sort1P : trace_sort sort1. +Lemma asort2_mergeE : + Abstract.sort2 leT merge merge' (fun x => [:: x]) [::] =1 sort2. Proof. -apply/trace_sortP; elim=> [|x s IHs] stack; first exact: merge_sort_popP [tr] _. -case: (merge_sort_pushP [tr<= x] stack). -by rewrite (catA _ [:: _]) => {}stack /= -> ->; exact: IHs. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort2 /sort2 -/(astack_of_stack false [::]). +elim: n (Nil (seq _)) xs => // n IHn stack [|x [|x' xs /= /ltnW /IHn <-]] /=; + try by rewrite apop_mergeE. +by rewrite apush_mergeE; last case: ifP. Qed. -Lemma sort2P : trace_sort sort2. +Lemma asort3_mergeE : + Abstract.sort3 leT merge merge' (fun x => [:: x]) [::] =1 sort3. Proof. -apply/trace_sortP => s; have [n] := ubnP (size s); elim: n s => // n IHn. -move=> [|x [|y s]]/=; rewrite ?ltnS => size_s stack. -- exact: merge_sort_popP [tr<=] _. -- exact: merge_sort_popP [tr<= x] _. -case: (merge_sort_pushP [tr x; y] stack). -by rewrite (catA _ [:: _; _]) => /= {}stack -> ->; apply/IHn/ltnW. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort3 /sort3 -/(astack_of_stack false [::]). +move: n (Nil (seq _)) xs. +elim=> // n IHn stack [|x [|x' [|x'' xs /= /ltnW /ltnW /IHn <-]]] /=; + try by rewrite apop_mergeE. +rewrite apush_mergeE; last by rewrite /nilp !(size_rev, size_merge). +by rewrite !(fun_if rev, fun_if (path.merge _ _), fun_if (cons _)). Qed. -Lemma sort3P : trace_sort sort3. +Lemma asortN_mergeE : + Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. -apply/trace_sortP => s; have [n] := ubnP (size s); elim: n s => // n IHn. -move=> [|x [|y [|z s]]]/=; rewrite ?ltnS => size_s stack. -- exact: merge_sort_popP [tr<=] _. -- exact: merge_sort_popP [tr<= x] _. -- exact: merge_sort_popP [tr x; y] _. -rewrite (catA _ [:: _; _; _]). -pose xyz : trace leT := branch_trace false [tr x; y] [tr<= z]. -case: (merge_sort_pushP xyz stack) => /= stack' ->. -set push1 := merge_sort_push _ _; set push2 := merge_sort_push _ _. -have ->: push1 = push2 by congr merge_sort_push; do 3 case: ifP => //=. -by move=> ->; apply/IHn/ltnW/ltnW. +case=> // x xs; have [n] := ubnP (size xs). +rewrite /Abstract.sortN /sortN -/(astack_of_stack false [::]). +elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs]. + by rewrite [LHS]apop_mergeE. +rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). +pose rs := Nil T; rewrite -{1}[[:: x]]/(rcons (rev rs) x) -/(x :: rs). +elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. + rewrite /Abstract.incr /Abstract.decr !apop_mergeE rev_rcons revK /= /geT. + by case: leT. +rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). +rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +move: (IHxs Hxs y z (x :: rs)); rewrite -rev_cons rev_rcons revK /= /geT. +by do 2 case: leT; rewrite // apush_mergeE ?rev_nilp // IHn. Qed. -Lemma sortNP : trace_sort sortN. +Lemma apush_catE (xs ys : seq T) stack : + flatten_stack ys (Abstract.push cat cat xs stack) + = flatten_stack (xs ++ ys) stack. Proof. -case=> /= [|x s]; first by exists empty_trace. -suff /(_ [::]) : forall stack, {t : trace leT | - flatten_stack stack ++ x :: s = flatten_trace t & - sortNrec (sort_stack false stack) x s = sort_trace t} by []. -have [n] := ubnP (size s); elim: n x s => // n IHn x [|y s]/= sn stack. - exact: merge_sort_popP [tr<= x] _. -set lexy := leT x y. -have: path (fun y x => leT x y == lexy) y [:: x] by rewrite /= eqxx. -have ->: [:: x, y & s] = rev [:: y; x] ++ s by []. -elim: s sn (lexy) (y) [:: x] => {lexy x y} => [|y s IHs' /=] /ltnW sn ord x acc. - rewrite -/(sorted _ (_ :: _)) -rev_sorted cats0 => sorted_acc. - case: (merge_sort_popP false (leaf_trace ord _ sorted_acc) stack) => /= t ->. - by rewrite revK; case: ord {sorted_acc} => ->; exists t. -case: ord (boolP (leT x y)) => [] [] lexy. -- move=> path_acc. - have: path (fun y x => leT x y == true) y (x :: acc) by rewrite /= lexy eqxx. - by move=> /(IHs' sn)[t]; rewrite -cat_rcons -rev_cons => -> ->; exists t. -- rewrite -/(sorted _ (_ :: _)) -rev_sorted => sorted_acc. - case: (merge_sort_pushP (leaf_trace true _ sorted_acc) stack) => stack'. - by rewrite /= catA => -> ->; apply/IHn. -- rewrite -/(sorted _ (_ :: _)) -rev_sorted => sorted_acc. - case: (merge_sort_pushP (leaf_trace false _ sorted_acc) stack) => stack'. - by rewrite /= catA revK => -> ->; apply/IHn. -- move=> path_acc. - have: path (fun y x => leT x y == false) y (x :: acc). - by rewrite /= eqbF_neg lexy. - by move=> /(IHs' sn)[t]; rewrite -cat_rcons -rev_cons => -> ->; exists t. +have [n] := ubnP (size stack). +by elim: n xs stack => // n IHn xs [|[zs [|[zs'|] stack]|stack]] //=; + try move=> /(@ltnW _.+2) /IHn ->; rewrite !catA. Qed. -End CBV. +Lemma apop_catE mode xs stack : + Abstract.pop cat cat mode xs stack = flatten_stack xs stack. +Proof. +have [n] := ubnP (size stack). +by elim: n mode xs stack => // n IHn mode xs [|[ys stack|[|[zs|] stack]]] //=; + try move/(@ltnW _.+2); move=> /IHn ->; rewrite ?if_same. +Qed. -Realizer M.revmerge as revmerge_R arity 2 := M.revmerge_R. +Lemma asort1_catE : Abstract.sort1 leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +move=> xs; rewrite /Abstract.sort1 -[RHS]/(flatten_stack xs [::]). +elim: xs (Nil (option _)) => /= [|x xs IHxs] stack; first exact: apop_catE. +by rewrite IHxs apush_catE. +Qed. -Parametricity merge_sort_push. -Parametricity merge_sort_pop. -Parametricity sort1. -Parametricity sort2. -Parametricity sort3. -Parametricity sortN. +Lemma asort2_catE : Abstract.sort2 leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort2 -[RHS]/(flatten_stack xs [::]). +move: n (Nil (option _)) xs. +by elim=> // n IHn stack [|x [|x' xs /= /ltnW /IHn ->]] /=; + rewrite (apop_catE, apush_catE). +Qed. -Definition sort1_stable := StableSort.Pack sort1 sort1_R sort1P. -Definition sort2_stable := StableSort.Pack sort2 sort2_R sort2P. -Definition sort3_stable := StableSort.Pack sort3 sort3_R sort3P. -Definition sortN_stable := StableSort.Pack sortN sortN_R sortNP. +Lemma asort3_catE : Abstract.sort3 leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +move=> xs; have [n] := ubnP (size xs). +rewrite /Abstract.sort3 -[RHS]/(flatten_stack xs [::]). +move: n (Nil (option _)) xs. +by elim=> // n IHn stack [|x [|x' [|x'' xs /= /ltnW /ltnW /IHn ->]]] /=; + rewrite (apop_catE, apush_catE). +Qed. + +Lemma asortN_catE : Abstract.sortN leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. +case=> // x xs; have [n] := ubnP (size xs). +rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]). +elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs]; + first by rewrite [LHS]apop_catE. +rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). +pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _). +elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. + by rewrite if_same [LHS]apop_catE -catA. +rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). +rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +move: (IHxs Hxs y z (rcons rs x)); rewrite IHn // apush_catE -cats1 -!catA /=. +by case: leT => ->; rewrite if_same. +Qed. + +End CBV. + +Definition sort1_stable := + StableSort sort1 Abstract.sort1 Abstract.sort1_R asort1_mergeE asort1_catE. +Definition sort2_stable := + StableSort sort2 Abstract.sort2 Abstract.sort2_R asort2_mergeE asort2_catE. +Definition sort3_stable := + StableSort sort3 Abstract.sort3 Abstract.sort3_R asort3_mergeE asort3_catE. +Definition sortN_stable := + StableSort sortN Abstract.sortN Abstract.sortN_R asortN_mergeE asortN_catE. End CBV_. @@ -848,7 +981,7 @@ Section StableSortTheory. Let lexord (T : Type) (leT leT' : rel T) := [rel x y | leT x y && (leT y x ==> leT' x y)]. -Let lexord_total (T : Type) (leT leT' : rel T) : +Local Lemma lexord_total (T : Type) (leT leT' : rel T) : total leT -> total leT' -> total (lexord leT leT'). Proof. move=> leT_total leT'_total x y /=. @@ -856,7 +989,7 @@ by move: (leT_total x y) (leT'_total x y) => /orP[->|->] /orP[->|->]; rewrite /= ?implybE ?orbT ?andbT //= (orbAC, orbA) (orNb, orbN). Qed. -Let lexord_trans (T : Type) (leT leT' : rel T) : +Local Lemma lexord_trans (T : Type) (leT leT' : rel T) : transitive leT -> transitive leT' -> transitive (lexord leT leT'). Proof. move=> leT_tr leT'_tr y x z /= /andP[lexy leyx] /andP[leyz lezy]. @@ -864,7 +997,7 @@ rewrite (leT_tr _ _ _ lexy leyz); apply/implyP => lezx; move: leyx lezy. by rewrite (leT_tr _ _ _ leyz lezx) (leT_tr _ _ _ lezx lexy); exact: leT'_tr. Qed. -Let lexordA (T : Type) (leT leT' leT'' : rel T) : +Local Lemma lexordA (T : Type) (leT leT' leT'' : rel T) : lexord leT (lexord leT' leT'') =2 lexord (lexord leT leT') leT''. Proof. by move=> x y /=; case: (leT x y) (leT y x) => [] []. Qed. @@ -872,49 +1005,62 @@ Section StableSortTheory_Part1. Variable (sort : stableSort). -Local Lemma param_sort : StableSort.sort_ty_R sort sort. -Proof. by case: sort => ? param ?; exact: param. Qed. - -Lemma map_sort (T T' : Type) (f : T' -> T) (leT' : rel T') (leT : rel T) : - {mono f : x y / leT' x y >-> leT x y} -> - {morph map f : s1 / sort _ leT' s1 >-> sort _ leT s1}. -Proof. -move=> leT_mono xs; apply/esym/rel_map_map/param_sort/map_rel_map. -by move=> ? ? <- ? ? <-; apply/bool_R_refl/esym/leT_mono. -Qed. - -Lemma sort_map (T T' : Type) (f : T' -> T) (leT : rel T) (s : seq T') : - sort _ leT (map f s) = map f (sort _ (relpre f leT) s). -Proof. exact/esym/map_sort. Qed. +Local Lemma param_asort : + StableSort.asort_ty_R (StableSort.asort sort) (StableSort.asort sort). +Proof. by case: sort. Qed. Section SortSeq. Variable (T : Type) (P : {pred T}) (leT : rel T). +Let geT x y := leT y x. -Variant sort_spec : seq T -> seq T -> Type := - SortSpec (t : StableSort.trace leT) : - sort_spec (StableSort.flatten_trace t) (StableSort.sort_trace t). - -Local Lemma sortP (s : seq T) : sort_spec s (sort _ leT s). +Local Lemma asort_mergeE : + StableSort.asort sort leT (merge leT) + (fun xs ys => rev (merge geT (rev ys) (rev xs))) (fun x => [:: x]) [::] + =1 sort _ leT. +Proof. by case: sort. Qed. + +Local Lemma asort_catE : + StableSort.asort sort leT cat cat (fun x => [:: x]) [::] =1 id. +Proof. by case: sort. Qed. + +Lemma sort_ind (R : seq T -> seq T -> Prop) : + (forall xs xs', R xs xs' -> forall ys ys', R ys ys' -> + R (cat xs ys) (merge leT xs' ys')) -> + (forall xs xs', R xs xs' -> forall ys ys', R ys ys' -> + R (cat xs ys) (rev (merge geT (rev ys') (rev xs')))) -> + (forall x, R [:: x] [:: x]) -> R [::] [::] -> + forall s, R s (sort _ leT s). Proof. -by case: sort => ? ? sortP; have [/= t -> ->] := sortP _ leT s; constructor. +move=> ? ? Hsingleton ? s; rewrite -[s in R s _]asort_catE -asort_mergeE. +apply: (@param_asort _ _ eq _ _ R) => //. +- by move=> ? ? -> ? ? ->; apply: bool_R_refl. +- by move=> ? ? ->; apply: Hsingleton. +by elim: s; constructor. Qed. Lemma all_sort (s : seq T) : all P (sort _ leT s) = all P s. -Proof. by case: sortP; exact: StableSort.all_trace. Qed. +Proof. +by elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys; + rewrite !(all_rev, all_merge) all_cat IHxs IHys // andbC. +Qed. Lemma size_sort (s : seq T) : size (sort _ leT s) = size s. -Proof. case: sortP; exact: StableSort.size_trace. Qed. +Proof. +by elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys; + rewrite ?size_rev size_merge !size_cat ?size_rev IHxs IHys // addnC. +Qed. Lemma sort_nil : sort _ leT [::] = [::]. Proof. by case: (sort _) (size_sort [::]). Qed. Lemma pairwise_sort (s : seq T) : pairwise leT s -> sort _ leT s = s. Proof. -case: {s}sortP; elim=> [b l IHl r IHr|[] [|x [|y s]]] //=; last by case: leT. -rewrite pairwise_cat => /and3P[hlr /IHl -> /IHr ->]. -rewrite !allrel_merge ?rev_cat ?revK //; first by case: b. -by rewrite /allrel all_rev [all _ _]allrelC /allrel all_rev. +elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys. + rewrite pairwise_cat => /and3P[hlr /IHxs -> /IHys ->]. + by rewrite !allrel_merge. +rewrite pairwise_cat => /and3P[hlr /IHxs -> /IHys ->]. +by rewrite allrel_merge 1?allrel_rev2 1?allrelC // rev_cat !revK. Qed. Lemma sorted_sort : transitive leT -> @@ -923,6 +1069,27 @@ Proof. by move=> leT_tr s; rewrite sorted_pairwise //; apply/pairwise_sort. Qed. End SortSeq. +Local Lemma param_sort : StableSort.sort_ty_R sort sort. +Proof. +move=> T T' T_R leT leT' leT_R xs xs' xs_R; rewrite -!asort_mergeE. +apply: (@param_asort _ _ T_R _ _ (list_R T_R) _ _ leT_R _ _ (merge_R leT_R)); + try by do ?constructor. +move=> ys ys' ys_R zs zs' zs_R; apply/rev_R/merge_R/rev_R/ys_R/rev_R/zs_R. +by move=> ? ? ? ? ? ?; apply/leT_R. +Qed. + +Lemma map_sort (T T' : Type) (f : T' -> T) (leT' : rel T') (leT : rel T) : + {mono f : x y / leT' x y >-> leT x y} -> + {morph map f : s1 / sort _ leT' s1 >-> sort _ leT s1}. +Proof. +move=> leT_mono xs; apply/esym/rel_map_map/param_sort/map_rel_map. +by move=> ? ? <- ? ? <-; apply/bool_R_refl/esym/leT_mono. +Qed. + +Lemma sort_map (T T' : Type) (f : T' -> T) (leT : rel T) (s : seq T') : + sort _ leT (map f s) = map f (sort _ (relpre f leT) s). +Proof. exact/esym/map_sort. Qed. + Lemma sorted_sort_in (T : Type) (P : {pred T}) (leT : rel T) : {in P & &, transitive leT} -> forall s : seq T, all P s -> sorted leT s -> sort _ leT s = s. @@ -936,7 +1103,10 @@ Section EqSortSeq. Variables (T : eqType) (leT : rel T). Lemma perm_sort (s : seq T) : perm_eql (sort _ leT s) s. -Proof. by case: sortP; exact: StableSort.perm_trace. Qed. +Proof. +by apply/permPl; elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys; + rewrite 1?perm_rev perm_merge -1?rev_cat 1?perm_rev perm_cat. +Qed. Lemma mem_sort (s : seq T) : sort _ leT s =i s. Proof. exact/perm_mem/permPl/perm_sort. Qed. @@ -950,15 +1120,19 @@ Lemma sort_pairwise_stable (T : Type) (leT leT' : rel T) : total leT -> forall s : seq T, pairwise leT' s -> sorted (lexord leT leT') (sort _ leT s). Proof. -move=> leT_total s; case: {s}sortP; elim=> [b l IHl r IHr|b s] /=. - rewrite pairwise_cat => /and3P[hlr /IHl ? /IHr ?]. - rewrite fun_if ?(rev_sorted, merge_stable_sorted) ?if_same ?allrel_rev2//; - do 2 rewrite /allrel ?all_rev StableSort.all_trace [all _ _]allrelC //. - by rewrite allrelC. -move=> sorted_s1 /pairwise_sorted /(conj sorted_s1) /andP. -case: (b); rewrite -sorted_relI ?rev_sorted; - apply: sub_sorted => x y /= /andP[/eqP xy xy']; rewrite ?xy ?xy' ?implybT //. -by case: (leT _ _) xy (leT_total x y) => //= _ ->. +move=> leT_total s. +suff: (forall P, all P s -> all P (sort T leT s)) /\ + (pairwise leT' s -> sorted (lexord leT leT') (sort T leT s)). + by case. +elim/sort_ind: (sort _ leT s) => // xs xs' [IHxs IHxs'] ys ys' [IHys IHys']; + rewrite pairwise_cat; split => [P|/and3P[hlr /IHxs' ? /IHys' ?]]. +- by rewrite all_cat all_merge => /andP[/IHxs -> /IHys ->]. +- apply/merge_stable_sorted => //=. + by apply/IHxs; apply/sub_all: hlr => ?; apply/IHys. +- by rewrite all_cat all_rev all_merge !all_rev => /andP[/IHxs -> /IHys ->]. +- rewrite rev_sorted; apply/merge_stable_sorted; rewrite ?rev_sorted //. + rewrite allrel_rev2 allrelC. + by apply/IHxs; apply/sub_all: hlr => ?; apply/IHys. Qed. Lemma sort_pairwise_stable_in (T : Type) (P : {pred T}) (leT leT' : rel T) : @@ -1188,7 +1362,7 @@ by move=> subseq_ts /(sorted_sort sort leT_tr) <-; exact: subseq_sort. Qed. Lemma mem2_sort (s : seq T) (x y : T) : - leT x y -> mem2 s x y -> mem2 (sort _ leT s) x y. + leT x y -> mem2 s x y -> mem2 (sort _ leT s) x y. Proof. move=> lexy; rewrite !mem2E => /subseq_sort; rewrite !eq_sort_insert //. by case: (_ == _); rewrite //= lexy. @@ -1232,13 +1406,13 @@ End StableSortTheory_Part2. End StableSortTheory. -Arguments map_sort sort {T T' f leT' leT} _ _. -Arguments sort_map sort {T T' f leT} s. Arguments all_sort sort {T} P leT s. Arguments size_sort sort {T} leT s. Arguments sort_nil sort {T} leT. Arguments pairwise_sort sort {T leT s} _. Arguments sorted_sort sort {T leT} leT_tr {s} _. +Arguments map_sort sort {T T' f leT' leT} _ _. +Arguments sort_map sort {T T' f leT} s. Arguments sorted_sort_in sort {T P leT} leT_tr {s} _ _. Arguments perm_sort sort {T} leT s _. Arguments mem_sort sort {T} leT s _. diff --git a/theories/top_down.v b/theories/top_down.v deleted file mode 100644 index 080f392..0000000 --- a/theories/top_down.v +++ /dev/null @@ -1,116 +0,0 @@ -Require Export PArith. -From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. -From stablesort Require Import param stablesort. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Module CBN_ (M : MergeSig). - -Section CBN. - -Variable (T : Type) (leT : rel T). - -Fixpoint sort2_rec (c : bool) (n : positive) (s : seq T) : seq T * seq T := - let rec c1 c2 n s := - let (s1, s') := sort2_rec c1 n s in - let (s2, s'') := sort2_rec c2 n s' in (M.merge leT s1 s2, s'') - in - match n, c, s with - | 1%positive, _, [::] | 2%positive, _, [::] => ([::], s) - | 1%positive, false, x :: s - | 1%positive, true, x :: [::] as s - | 2%positive, _, x :: [::] as s => ([:: x], s) - | 1%positive, true, x :: y :: s | 2%positive, false, x :: y :: s => - ((if leT x y then [:: x; y] else [:: y; x]), s) - | xO n, _, s => rec false c n s - | xI n, _, s => rec c true n s - end. - -Definition sort2 (s : seq T) := - if bin_of_nat (size s) is Npos n then (sort2_rec false n s).1 else [::]. - -Import StableSort. - -Lemma sort2_recP (c : bool) (n : positive) (s : seq T) : - let n' := c + nat_of_pos n in - {t : trace leT | - take n' s = flatten_trace t & sort2_rec c n s = (sort_trace t, drop n' s) }. -Proof. -elim: n c s => /= [n IHn c s|[n|n|] IHn c s|]. -- case: sort2_rec (IHn c s) => [_ s'] [t1 Ht1 [-> s'E]]. - case: sort2_rec (IHn true s') => [_ s''] [t2 Ht2 [-> s''E]]. - rewrite NatTrec.doubleE; exists (branch_trace true t1 t2). - + rewrite /= -Ht1 -Ht2 s'E take_drop addnACA addnn addSnnS. - rewrite -[LHS](cat_take_drop (c + nat_of_pos n)) take_take //. - by rewrite leq_add2l leqW // -addnn leq_addr. - + by rewrite s''E s'E drop_drop addnACA addnn add1n addSnnS M.mergeE. -- case: sort2_rec (IHn false s) => [_ s'] [t1 Ht1 [-> s'E]]. - case: sort2_rec (IHn c s') => [_ s''] [t2 Ht2 [-> s''E]]. - rewrite NatTrec.doubleE; exists (branch_trace true t1 t2). - + rewrite /= -Ht1 -Ht2 s'E take_drop addnACA addnn add0n addn0. - rewrite -[LHS](cat_take_drop (nat_of_pos (xI n))) take_take //. - by rewrite -addnn addnA leq_addl. - + by rewrite s''E s'E drop_drop addnACA addnn addn0 M.mergeE. -- case: sort2_rec (IHn false s) => [_ s'] [t1 Ht1 [-> s'E]]. - case: sort2_rec (IHn c s') => [_ s''] [t2 Ht2 [-> s''E]]. - rewrite NatTrec.doubleE; exists (branch_trace true t1 t2). - + rewrite /= -Ht1 -Ht2 s'E take_drop addnACA addnn add0n addn0. - rewrite -[LHS](cat_take_drop (nat_of_pos (xO n))) take_take //. - by rewrite -addnn addnA leq_addl. - + by rewrite s''E s'E drop_drop addnACA addnn addn0 M.mergeE. -- case: c s => [] [|x [|y s]]. - + by exists (leaf_trace true [::] isT). - + by exists (leaf_trace true [:: x] isT). - + case: sort2_rec (IHn false [:: x, y & s]) => [_ s'] [t1 Ht1 [-> s'E]]. - case: sort2_rec (IHn true s') => [_ s''] [t2 Ht2 [-> s''E]]. - rewrite NatTrec.doubleE; exists (branch_trace true t1 t2). - * by rewrite /= -Ht1 -Ht2 s'E. - * by rewrite s''E s'E M.mergeE. - + by exists (leaf_trace true [::] isT). - + by exists (leaf_trace true [:: x] isT). - + have sorted_xy: sorted (fun x0 y0 => leT x0 y0 == leT x y) [:: x; y]. - by rewrite /= eqxx. - exists (leaf_trace (leT x y) [:: x; y] sorted_xy). - by rewrite /= take0. - by rewrite /= drop0. -- case=> [[|x [|y s]] | [|x s]] //=. - + by exists (leaf_trace true [::] isT). - + by exists (leaf_trace true [:: x] isT). - + have sorted_xy: sorted (fun x0 y0 => leT x0 y0 == leT x y) [:: x; y]. - by rewrite /= eqxx. - exists (leaf_trace (leT x y) [:: x; y] sorted_xy). - by rewrite take0. - by rewrite drop0. - + by exists (leaf_trace true [::] isT). - + exists (leaf_trace true [:: x] isT). - by rewrite take0. - by rewrite drop0. -Qed. - -Lemma sort2P (s : seq T) : - {t : trace leT | s = flatten_trace t & sort2 s = sort_trace t}. -Proof. -rewrite /sort2. -case: (bin_of_nat _) (bin_of_natK (size s)) => [|n] //=. -- by move=> /esym /size0nil ->; exists (leaf_trace true [::] isT). -- move=> nE; case: (sort2_recP false n s) => t /=. - by rewrite add0n nE take_oversize // drop_oversize // => -> -> /=; exists t. -Qed. - -End CBN. - -Realizer M.merge as merge_R arity 2 := M.merge_R. - -Parametricity sort2. - -Definition sort2_stable := StableSort.Pack sort2 sort2_R sort2P. - -End CBN_. - -Module CBN := CBN_(Merge). -Module CBNAcc := CBN_(MergeAcc). - -Canonical CBN.sort2_stable. -Canonical CBNAcc.sort2_stable. From dc96c30eaaf0ff62e8c652eb60f405d202e687bc Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 3 Nov 2023 01:55:09 +0100 Subject: [PATCH 2/2] Clean up --- theories/stablesort.v | 194 ++++++++++++++++++------------------------ 1 file changed, 84 insertions(+), 110 deletions(-) diff --git a/theories/stablesort.v b/theories/stablesort.v index 03b9c15..bf71fa4 100644 --- a/theories/stablesort.v +++ b/theories/stablesort.v @@ -6,6 +6,13 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Local Definition condrev (T : Type) (r : bool) (xs : seq T) : seq T := + if r then rev xs else xs. + +Local Lemma condrev_nilp (T : Type) (r : bool) (xs : seq T) : + nilp (condrev r xs) = nilp xs. +Proof. by case: r; rewrite /= ?rev_nilp. Qed. + (******************************************************************************) (* The abstract interface for stable (merge)sort algorithms *) (******************************************************************************) @@ -234,25 +241,20 @@ Module Insertion. Module Abstract. Definition sort (T R : Type) (leT : rel T) - (merge : R -> R -> R) (merge' : R -> R -> R) - (singleton : T -> R) (empty : R) := + (merge merge' : R -> R -> R) (singleton : T -> R) (empty : R) := foldr (fun x => merge (singleton x)) empty. Parametricity sort. End Abstract. -Section Insertion. - -Variables (T : Type) (leT : rel T). - -Definition sort : seq T -> seq T := foldr (fun x => merge leT [:: x]) [::]. +Definition sort (T : Type) (leT : rel T) : seq T -> seq T := + foldr (fun x => merge leT [:: x]) [::]. -Lemma asort_catE : Abstract.sort leT cat cat (fun x => [:: x]) [::] =1 id. +Lemma asort_catE (T : Type) (leT : rel T) : + Abstract.sort leT cat cat (fun x => [:: x]) [::] =1 id. Proof. by elim=> //= x xs ->. Qed. -End Insertion. - Definition sort_stable := StableSort sort Abstract.sort Abstract.sort_R (fun _ _ _ => erefl) asort_catE. @@ -287,9 +289,8 @@ Module CBN_ (M : MergeSig). Module Abstract. Section Abstract. -Variables (T R : Type) (leT : rel T). -Variables (merge : R -> R -> R) (merge' : R -> R -> R). -Variables (singleton : T -> R) (empty : R). +Context (T R : Type) (leT : rel T). +Context (merge merge' : R -> R -> R) (singleton : T -> R) (empty : R). Fixpoint push (xs : R) (stack : seq (option R)) : seq (option R) := match stack with @@ -339,28 +340,15 @@ Definition sort3 : seq T -> R := sort3rec [::]. Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R := if xs is y :: xs then - if leT x y then - incr stack y xs (singleton x) - else - decr stack y xs (singleton x) - else - pop (singleton x) stack -with incr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := + sortNrec' (leT x y) stack y xs (singleton x) else pop (singleton x) stack +with sortNrec' (incr : bool) (stack : seq (option R)) + (x : T) (xs : seq T) (accu : R) : R := + let accu' := (if incr then merge' else merge) accu (singleton x) in if xs is y :: xs then - if leT x y then - incr stack y xs (merge' accu (singleton x)) - else - sortNrec (push (merge' accu (singleton x)) stack) y xs - else - pop (merge' accu (singleton x)) stack -with decr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := - if xs is y :: xs then - if leT x y then - sortNrec (push (merge accu (singleton x)) stack) y xs - else - decr stack y xs (merge accu (singleton x)) + if eqb incr (leT x y) then + sortNrec' incr stack y xs accu' else sortNrec (push accu' stack) y xs else - pop (merge accu (singleton x)) stack. + pop accu' stack. #[using="All"] Definition sortN (xs : seq T) : R := @@ -377,7 +365,7 @@ End Abstract. Section CBN. -Variable (T : Type) (leT : rel T). +Context (T : Type) (leT : rel T). Fixpoint push (xs : seq T) (stack : seq (seq T)) : seq (seq T) := match stack with @@ -447,6 +435,7 @@ Definition sortN (xs : seq T) : seq T := (* Proofs *) Let geT x y := leT y x. + Let astack_of_stack : seq (seq T) -> seq (option (seq T)) := map (fun xs => if xs is [::] then None else Some xs). @@ -504,21 +493,23 @@ Qed. Lemma asortN_mergeE : Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. +have mergeEcons x y rs : + (if leT x y then merge' else merge) (condrev (leT x y) (x :: rs)) [:: y] + = condrev (leT x y) (y :: x :: rs). + by case: ifP; rewrite /= ?revK /geT /= => ->. case=> // x xs; have [n] := ubnP (size xs). rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack [::]). elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs]. by rewrite [LHS]apop_mergeE. -rewrite /Abstract.sortNrec. -rewrite -/(Abstract.incr _ _ merge' _) -/(Abstract.decr _ _ merge' _). -pose rs := Nil T; rewrite -{1}[[:: x]]/(rcons (rev rs) x) -/(x :: rs). -elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. - rewrite /Abstract.incr /Abstract.decr !apop_mergeE rev_rcons revK /= /geT. - by case: leT. -rewrite /Abstract.incr -/(Abstract.incr _ _ merge' _). -rewrite /Abstract.decr -/(Abstract.decr _ _ merge' _). -rewrite -/(Abstract.sortNrec _ _ merge' _). -move: (IHxs Hxs y z (x :: rs)); rewrite -rev_cons rev_rcons revK /= /geT. -by do 2 case: leT; rewrite // apush_mergeE ?rev_nilp // IHn. +rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _). +have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same. +move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)). +elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE. + by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP. +rewrite /Abstract.sortNrec'. +rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //. +by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP. Qed. Lemma apush_catE (xs ys : seq T) stack : @@ -562,14 +553,14 @@ case=> // x xs; have [n] := ubnP (size xs). rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]). elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs]; first by rewrite [LHS]apop_catE. -rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). +rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _). pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _). elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. - by rewrite if_same [LHS]apop_catE -catA. -rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). -rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). -move: (IHxs Hxs y z (rcons rs x)); rewrite IHn // apush_catE -cats1 -!catA /=. -by case: leT => ->; rewrite if_same. + by rewrite [LHS]apop_catE if_same -catA. +rewrite /Abstract.sortNrec'. +rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +move: (IHxs Hxs y z (rcons rs x)). +by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->. Qed. End CBN. @@ -621,9 +612,8 @@ Module CBV_ (M : RevmergeSig). Module Abstract. Section Abstract. -Variables (T R : Type) (leT : rel T). -Variables (merge : R -> R -> R) (merge' : R -> R -> R). -Variables (singleton : T -> R) (empty : R). +Context (T R : Type) (leT : rel T). +Context (merge merge' : R -> R -> R) (singleton : T -> R) (empty : R). Fixpoint push (xs : R) (stack : seq (option R)) : seq (option R) := match stack with @@ -678,28 +668,17 @@ Definition sort3 : seq T -> R := sort3rec [::]. Fixpoint sortNrec (stack : seq (option R)) (x : T) (xs : seq T) : R := if xs is y :: xs then - if leT x y then - incr stack y xs (singleton x) - else - decr stack y xs (singleton x) + sortNrec' (leT x y) stack y xs (singleton x) else pop false (singleton x) stack -with incr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := - if xs is y :: xs then - if leT x y then - incr stack y xs (merge' accu (singleton x)) - else - sortNrec (push (merge' accu (singleton x)) stack) y xs - else - pop false (merge' accu (singleton x)) stack -with decr (stack : seq (option R)) (x : T) (xs : seq T) (accu : R) : R := +with sortNrec' (incr : bool) (stack : seq (option R)) + (x : T) (xs : seq T) (accu : R) : R := + let accu' := (if incr then merge' else merge) accu (singleton x) in if xs is y :: xs then - if leT x y then - sortNrec (push (merge accu (singleton x)) stack) y xs - else - decr stack y xs (merge accu (singleton x)) + if eqb incr (leT x y) then + sortNrec' incr stack y xs accu' else sortNrec (push accu' stack) y xs else - pop false (merge accu (singleton x)) stack. + pop false accu' stack. #[using="All"] Definition sortN (xs : seq T) : R := @@ -716,7 +695,7 @@ End Abstract. Section CBV. -Variables (T : Type) (leT : rel T). +Context (T : Type) (leT : rel T). Let geT x y := leT y x. Fixpoint push (xs : seq T) (stack : seq (seq T)) : seq (seq T) := @@ -799,15 +778,7 @@ Definition sortN (xs : seq T) : seq T := (* Proofs *) -Let condrev (r : bool) (s : seq T) : seq T := if r then rev s else s. - -Lemma condrev_nilp mode xs : nilp (condrev mode xs) = nilp xs. -Proof. by case: mode; rewrite /= ?rev_nilp. Qed. - -Lemma condrevK mode : involutive (condrev mode). -Proof. by case: mode; first exact: revK. Qed. - -Let Fixpoint astack_of_stack (mode : bool) (stack : seq (seq T)) := +Fixpoint astack_of_stack (mode : bool) (stack : seq (seq T)) := match stack with | [::] => [::] | xs :: stack => @@ -874,19 +845,23 @@ Qed. Lemma asortN_mergeE : Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. +have mergeEcons x y rs : + (if leT x y then merge' else merge) (condrev (leT x y) (x :: rs)) [:: y] + = condrev (leT x y) (y :: x :: rs). + by case: ifP; rewrite /= ?revK /geT /= => ->. case=> // x xs; have [n] := ubnP (size xs). -rewrite /Abstract.sortN /sortN -/(astack_of_stack false [::]). +rewrite /Abstract.sortN /sortN -[Nil (option _)]/(astack_of_stack false [::]). elim: n (Nil (seq _)) x xs => // n IHn stack x [|y xs /= /ltnSE Hxs]. by rewrite [LHS]apop_mergeE. -rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). -pose rs := Nil T; rewrite -{1}[[:: x]]/(rcons (rev rs) x) -/(x :: rs). -elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. - rewrite /Abstract.incr /Abstract.decr !apop_mergeE rev_rcons revK /= /geT. - by case: leT. -rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). -rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). -move: (IHxs Hxs y z (x :: rs)); rewrite -rev_cons rev_rcons revK /= /geT. -by do 2 case: leT; rewrite // apush_mergeE ?rev_nilp // IHn. +rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _). +have {1}->: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same. +move: xs Hxs x y (RS in x :: RS) {-2}(leT x y) (erefl (leT x y)). +elim=> [_|z xs IHxs /= /ltnW Hxs] x y rs incr incrE. + by rewrite /Abstract.sortNrec' apop_mergeE /= incrE mergeEcons; case: ifP. +rewrite /Abstract.sortNrec'. +rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +rewrite eqbE incrE mergeEcons apush_mergeE ?condrev_nilp // IHn //. +by have [/[dup] /IHxs -> // ->|] := eqVneq; do 2?case: ifP. Qed. Lemma apush_catE (xs ys : seq T) stack : @@ -937,14 +912,14 @@ case=> // x xs; have [n] := ubnP (size xs). rewrite /Abstract.sortN -[RHS]/(flatten_stack (x :: xs) [::]). elim: n x (Nil (option _)) xs => // n IHn x stack [|y xs /= /ltnSE Hxs]; first by rewrite [LHS]apop_catE. -rewrite /Abstract.sortNrec -/(Abstract.incr _ _ _ _) -/(Abstract.decr _ _ _ _). +rewrite /Abstract.sortNrec -/(Abstract.sortNrec' _ _ _ _). pose rs := Nil T; rewrite -[x :: y :: _]/(rs ++ _) -[[:: x]]/(rs ++ _). elim: xs Hxs x y rs => [_|z xs IHxs /= /ltnW Hxs] x y rs. - by rewrite if_same [LHS]apop_catE -catA. -rewrite /Abstract.incr -/(Abstract.incr _ _ _ _). -rewrite /Abstract.decr -/(Abstract.decr _ _ _ _) -/(Abstract.sortNrec _ _ _ _). -move: (IHxs Hxs y z (rcons rs x)); rewrite IHn // apush_catE -cats1 -!catA /=. -by case: leT => ->; rewrite if_same. + by rewrite [LHS]apop_catE if_same -catA. +rewrite /Abstract.sortNrec'. +rewrite -/(Abstract.sortNrec' _ _ _ _) -/(Abstract.sortNrec _ _ _ _). +move: (IHxs Hxs y z (rcons rs x)). +by rewrite eqbE if_same IHn // apush_catE -cats1 -!catA; case: eqVneq => // ->. Qed. End CBV. @@ -1003,7 +978,7 @@ Proof. by move=> x y /=; case: (leT x y) (leT y x) => [] []. Qed. Section StableSortTheory_Part1. -Variable (sort : stableSort). +Context (sort : stableSort). Local Lemma param_asort : StableSort.asort_ty_R (StableSort.asort sort) (StableSort.asort sort). @@ -1011,7 +986,7 @@ Proof. by case: sort. Qed. Section SortSeq. -Variable (T : Type) (P : {pred T}) (leT : rel T). +Context (T : Type) (P : {pred T}) (leT : rel T). Let geT x y := leT y x. Local Lemma asort_mergeE : @@ -1100,7 +1075,7 @@ Qed. Section EqSortSeq. -Variables (T : eqType) (leT : rel T). +Context (T : eqType) (leT : rel T). Lemma perm_sort (s : seq T) : perm_eql (sort _ leT s) s. Proof. @@ -1275,12 +1250,12 @@ Qed. Section StableSortTheory_Part2. -Variable (sort : stableSort). +Context (sort : stableSort). Section Stability. -Variables (T : Type) (leT : rel T). -Variables (leT_total : total leT) (leT_tr : transitive leT). +Context (T : Type) (leT : rel T). +Context (leT_total : total leT) (leT_tr : transitive leT). Lemma eq_sort_insert : sort _ leT =1 Insertion.sort leT. Proof. exact: eq_sort. Qed. @@ -1308,9 +1283,8 @@ End Stability. Section Stability_in. -Variables (T : Type) (P : {pred T}) (leT : rel T). -Hypothesis leT_total : {in P &, total leT}. -Hypothesis leT_tr : {in P & &, transitive leT}. +Context (T : Type) (P : {pred T}) (leT : rel T). +Context (leT_total : {in P &, total leT}) (leT_tr : {in P & &, transitive leT}). Let le_sT := relpre (val : sig P -> _) leT. Let le_sT_total : total le_sT := in2_sig leT_total. @@ -1346,8 +1320,8 @@ End Stability_in. Section Stability_subseq. -Variables (T : eqType) (leT : rel T). -Variables (leT_total : total leT) (leT_tr : transitive leT). +Context (T : eqType) (leT : rel T). +Context (leT_total : total leT) (leT_tr : transitive leT). Lemma subseq_sort : {homo sort _ leT : t s / subseq t s}. Proof. @@ -1372,7 +1346,7 @@ End Stability_subseq. Section Stability_subseq_in. -Variables (T : eqType) (leT : rel T). +Context (T : eqType) (leT : rel T). Lemma subseq_sort_in (t s : seq T) : {in s &, total leT} -> {in s & &, transitive leT} ->