diff --git a/Make b/Make index d80a76b..1211cbc 100644 --- a/Make +++ b/Make @@ -1,3 +1,4 @@ +theories/mathcomp_ext.v theories/param.v theories/stablesort.v diff --git a/Make.misc b/Make.misc index 413c93c..6335e09 100644 --- a/Make.misc +++ b/Make.misc @@ -1,4 +1,5 @@ misc/topdown_tailrec.v +misc/usual_stable.v -R theories stablesort -R misc stablesort.misc diff --git a/misc/usual_stable.v b/misc/usual_stable.v new file mode 100644 index 0000000..1cc0e18 --- /dev/null +++ b/misc/usual_stable.v @@ -0,0 +1,164 @@ +From stablesort Require Import mathcomp_ext. +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. + +Lemma total_refl {T} (r : rel T) : total r -> reflexive r. +Proof. by move=> rt x; have /orP[] := rt x x. Qed. + +Definition eqr {T} (r : rel T) : rel T := [rel x y | r x y && r y x]. + +Lemma eqr_sym {T} (r : rel T) : symmetric (eqr r). +Proof. by move=> x y; apply/andP/andP => -[]. Qed. +#[local] Hint Resolve eqr_sym : core. + +Lemma eqrW {T} (r : rel T) : subrel (eqr r) r. +Proof. by move=> x y /andP[]. Qed. + +Lemma eqr_trans {T} (r : rel T) : transitive r -> transitive (eqr r). +Proof. +by move=> tr y x z /andP[? ?] /andP[? ?]; apply/andP; split; apply: (tr y). +Qed. +Arguments eqr_trans {T r}. + +Lemma eqr_refl {T} (r : rel T) : reflexive r -> reflexive (eqr r). +Proof. by move=> rr x; rewrite /eqr/= rr. Qed. + +Fact sort_usual_stable (sort : stableSort) (T : Type) (leT : rel T) : + total leT -> transitive leT -> + forall s x, filter (eqr leT x) (sort _ leT s) = filter (eqr leT x) s. +Proof. +move=> leT_total leT_tr s x; rewrite sorted_filter_sort// sorted_pairwise//. +apply/(pairwiseP x) => i j ilt jlt _; rewrite eqrW//. +by rewrite (eqr_trans _ x)// ?[eqr _ _ x]eqr_sym (all_nthP _ _)// filter_all. +Qed. + +Section UsualStableSortTheory. + +Section extract. +Context {T : Type} (x0 : T). +Implicit Types (P : {pred T}) (s : seq T). + +Local Definition egraph P s := filter (preim (nth x0 s) P) (iota 0 (size s)). +Arguments egraph : simpl never. +Definition extract P s := nth (size s) (egraph P s). +Definition unextract P s i := index i (egraph P s). + +Local Lemma size_egraph P s : size (egraph P s) = count P s. +Proof. by rewrite size_filter -count_map map_nth_iota0 ?take_size. Qed. + +Lemma extractK P s : + {in gtn (count P s), cancel (extract P s) (unextract P s)}. +Proof. +rewrite /extract /unextract => i iPs. +by rewrite index_uniq ?size_egraph// filter_uniq ?iota_uniq. +Qed. + +Definition extract_codom P s := + [predI (gtn (size s)) & preim (nth x0 s) P]. + +Lemma unextractK P s : + {in extract_codom P s, cancel (unextract P s) (extract P s)}. +Proof. +rewrite /extract /unextract => i /[!inE] /andP[ilts Pi]. +by rewrite nth_index// mem_filter /= Pi mem_iota. +Qed. + +Definition extract_inj P s := can_in_inj (@extractK P s). + +Local Lemma egraph_cons P s x : egraph P (x :: s) = + if P x then 0 :: map S (egraph P s) else map S (egraph P s). +Proof. +by rewrite /egraph/=; case: ifPn => ?; rewrite (iotaDl 1) filter_map. +Qed. + +Lemma extract_out P s i : i >= count P s -> extract P s i = size s. +Proof. by move=> igt; rewrite /extract nth_default// size_egraph. Qed. + +Lemma extract_lt P s i : i < count P s -> extract P s i < size s. +Proof. +move=> ilt; apply/(@all_nthP _ (gtn (size s))); rewrite ?size_egraph//=. +by apply/allP => j /=; rewrite mem_filter inE mem_iota => /and3P[]. +Qed. + +Lemma unextract_lt P s i : i \in extract_codom P s -> + unextract P s i < count P s. +Proof. +move=> /[!inE] /andP[ilt iPs]; rewrite /unextract -size_egraph index_mem. +by rewrite mem_filter/= mem_iota ilt iPs. +Qed. + +Lemma nth_filter P s i : nth x0 (filter P s) i = nth x0 s (extract P s i). +Proof. +have [ismall|ilarge] := ltnP i (count P s); last first. + by rewrite !nth_default// ?size_filter// /extract nth_default// size_egraph. +rewrite /extract; elim: s => [|x s IHs]//= in i ismall *. +rewrite egraph_cons; case: ifPn => [Px|PNx]/= in ismall *; last first. + by rewrite IHs//= (nth_map (size s)) ?size_egraph. +case: i ismall => // i; rewrite ltnS => ismall /=. +by rewrite IHs// (nth_map (size s))//= size_egraph. +Qed. + +Lemma nth_unextract P s i : i \in extract_codom P s -> + nth x0 (filter P s) (unextract P s i) = nth x0 s i. +Proof. by move=> iPs; rewrite nth_filter ?unextractK. Qed. + +Lemma extractP P s i : i < count P s -> P (nth x0 s (extract P s i)). +Proof. +move=> iPs; rewrite -nth_filter. +by apply/all_nthP; rewrite ?filter_all// size_filter. +Qed. + +Lemma le_extract P s : + {in gtn (count P s) &, {mono extract P s : i j / i <= j}}. +Proof. +apply: leq_mono_in => i j /[!inE] ilt jlt ij. +have ltn_trans := ltn_trans. +apply: (@sorted_ltn_nth _ ltn); rewrite -?topredE ?size_egraph//. +by rewrite sorted_filter// iota_ltn_sorted. +Qed. +Definition lt_extract P s := leqW_mono_in (@le_extract P s). + +Lemma le_unextract P s : + {in extract_codom P s &, {mono unextract P s : i j / i <= j}}. +Proof. +apply: can_mono_in (@le_extract P s); first exact/onW_can_in/unextractK. +by move=> i idom; rewrite inE unextract_lt. +Qed. +Definition lt_unextract P s := leqW_mono_in (@le_unextract P s). + +End extract. + +Context {T : Type} (sort : seq T -> seq T) (leT : rel T). +Hypothesis sort_nil : sort [::] = [::]. +Hypothesis sort_sorted : forall s : seq T, sorted leT (sort s). +Hypothesis sort_usual_stable : + forall s x, filter (eqr leT x) (sort s) = filter (eqr leT x) s. + +Lemma usual_stable_sort_stable leT' : total leT -> transitive leT' -> + forall s : seq T, sorted leT' s -> sorted (lexord leT leT') (sort s). +Proof. +move=> leT_total leT'_tr s. +wlog x0 : / T by case: s => [|x s']; [rewrite sort_nil//|apply]. +move=> s_sorted; apply/(sortedP x0) => i; set s':= sort s => iSlt /=. +set u := nth x0 _; pose P := eqr leT (u i). +have lui : leT (u i) (u i.+1) by rewrite (sortedP _ _) ?sort_sorted. +rewrite lui/=; apply/implyP => gui. +have iPs : i \in extract_codom x0 P s'. + by rewrite !inE ltnW//; apply/eqr_refl/total_refl. +have iSPs : i.+1 \in extract_codom x0 P s'. + by rewrite !inE iSlt//=; apply/andP. +pose v := nth x0 (filter P s). +suff: exists j k, [/\ j < k < size (filter P s), u i = v j & u i.+1 = v k]. + move=> [j [k [/andP[jk klt] -> ->]]]. + apply: pairwiseP => //; last by rewrite inE (ltn_trans _ klt). + by rewrite -sorted_pairwise// sorted_filter. +exists (unextract x0 P s' i), (unextract x0 P s' i.+1). +rewrite /v -sort_usual_stable// lt_unextract//= ?nth_unextract//. +by split=> //; rewrite leqnn/= size_filter unextract_lt. +Qed. + +End UsualStableSortTheory. diff --git a/theories/mathcomp_ext.v b/theories/mathcomp_ext.v new file mode 100644 index 0000000..4417f61 --- /dev/null +++ b/theories/mathcomp_ext.v @@ -0,0 +1,60 @@ +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Definition lexord (T : Type) (leT leT' : rel T) := + [rel x y | leT x y && (leT y x ==> leT' x y)]. + +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 /=. +by move: (leT_total x y) (leT'_total x y) => /orP[->|->] /orP[->|->]; + rewrite /= ?implybE ?orbT ?andbT //= (orbAC, orbA) (orNb, orbN). +Qed. + +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]. +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. + +Lemma lexord_irr (T : Type) (leT leT' : rel T) : + irreflexive leT' -> irreflexive (lexord leT leT'). +Proof. by move=> irr x /=; rewrite irr implybF andbN. Qed. + +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. + +Definition condrev (T : Type) (r : bool) (xs : seq T) : seq T := + if r then rev xs else xs. + +Lemma condrev_nilp (T : Type) (r : bool) (xs : seq T) : + nilp (condrev r xs) = nilp xs. +Proof. by case: r; rewrite /= ?rev_nilp. Qed. + +Lemma relpre_trans {T' T} {leT : rel T} {f : T' -> T} : + transitive leT -> transitive (relpre f leT). +Proof. by move=> + y x z; apply. Qed. + +Lemma allrel_rev2 {T S} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) : + allrel r (rev s1) (rev s2) = allrel r s1 s2. +Proof. by rewrite [LHS]all_rev [LHS]allrelC [RHS]allrelC [LHS]all_rev. Qed. + +Lemma count_merge (T : Type) (leT : rel T) (p : pred T) (s1 s2 : seq T) : + count p (merge leT s1 s2) = count p (s1 ++ s2). +Proof. +rewrite count_cat; elim: s1 s2 => // x s1 IH1. +elim=> //= [|y s2 IH2]; first by rewrite addn0. +by case: (leT x); rewrite /= ?IH1 ?IH2 ?[p y + _]addnCA addnA. +Qed. + +Lemma sortedP {T : Type} {e : rel T} {s : seq T} (x : T) : + reflect (forall i, i.+1 < size s -> e (nth x s i) (nth x s i.+1)) + (sorted e s). +Proof. by case: s => *; [constructor|apply: pathP]. Qed. diff --git a/theories/stablesort.v b/theories/stablesort.v index 380d0ef..af72fc0 100644 --- a/theories/stablesort.v +++ b/theories/stablesort.v @@ -1,3 +1,4 @@ +From stablesort Require Import mathcomp_ext. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. From stablesort Require Import param. @@ -5,28 +6,7 @@ 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. - -Local Lemma relpre_trans {T' T} {leT : rel T} {f : T' -> T} : - transitive leT -> transitive (relpre f leT). -Proof. by move=> + y x z; apply. Qed. - -Local Lemma allrel_rev2 {T S} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) : - allrel r (rev s1) (rev s2) = allrel r s1 s2. -Proof. by rewrite [LHS]all_rev [LHS]allrelC [RHS]allrelC [LHS]all_rev. Qed. - -Local Lemma count_merge (T : Type) (leT : rel T) (p : pred T) (s1 s2 : seq T) : - count p (merge leT s1 s2) = count p (s1 ++ s2). -Proof. -rewrite count_cat; elim: s1 s2 => // x s1 IH1. -elim=> //= [|y s2 IH2]; first by rewrite addn0. -by case: (leT x); rewrite /= ?IH1 ?IH2 ?[p y + _]addnCA addnA. -Qed. +Local Notation count_merge := mathcomp_ext.count_merge. (******************************************************************************) (* The abstract interface for stable (merge)sort algorithms *) @@ -964,33 +944,6 @@ Canonical CBVAcc.sortN_stable. Section StableSortTheory. -Let lexord (T : Type) (leT leT' : rel T) := - [rel x y | leT x y && (leT y x ==> leT' x y)]. - -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 /=. -by move: (leT_total x y) (leT'_total x y) => /orP[->|->] /orP[->|->]; - rewrite /= ?implybE ?orbT ?andbT //= (orbAC, orbA) (orNb, orbN). -Qed. - -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]. -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. - -Local Lemma lexord_irr (T : Type) (leT leT' : rel T) : - irreflexive leT' -> irreflexive (lexord leT leT'). -Proof. by move=> irr x /=; rewrite irr implybF andbN. Qed. - -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. - Section StableSortTheory_Part1. Context (sort : stableSort).