From c1cea60650517d05af7b0c96ca45e74a85243b4b Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 3 Nov 2023 01:55:09 +0100 Subject: [PATCH] Clean up --- theories/stablesort.v | 136 ++++++++++++++++++++---------------------- 1 file changed, 65 insertions(+), 71 deletions(-) diff --git a/theories/stablesort.v b/theories/stablesort.v index 03b9c15..11c7a88 100644 --- a/theories/stablesort.v +++ b/theories/stablesort.v @@ -339,28 +339,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 := - 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 := + 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 - 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 := @@ -447,6 +434,12 @@ Definition sortN (xs : seq T) : seq T := (* Proofs *) Let geT x y := leT y x. + +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. + Let astack_of_stack : seq (seq T) -> seq (option (seq T)) := map (fun xs => if xs is [::] then None else Some xs). @@ -501,6 +494,11 @@ 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 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). +Proof. by case: ifP; rewrite /= ?revK /geT /= => ->. Qed. + Lemma asortN_mergeE : Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. @@ -508,17 +506,16 @@ 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 Hx: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same. +pose rs := Nil T; rewrite {}[in LHS]Hx -/(x :: rs). +move: xs Hxs x y 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 +559,15 @@ 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)). +rewrite eqbE if_same IHn // apush_catE -cats1 -!catA. +by case: eqVneq => // -> ->. Qed. End CBN. @@ -678,28 +676,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 := +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 + 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 -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. + pop false accu' stack. #[using="All"] Definition sortN (xs : seq T) : R := @@ -871,22 +858,28 @@ 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 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). +Proof. by case: ifP; rewrite /= ?revK /geT /= => ->. Qed. + Lemma asortN_mergeE : Abstract.sortN leT merge merge' (fun x => [:: x]) [::] =1 sortN. Proof. 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 Hx: [:: x] = condrev (leT x y) [:: x] by rewrite [RHS]if_same. +pose rs := Nil T; rewrite {}[in LHS]Hx -/(x :: rs). +move: xs Hxs x y 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 +930,15 @@ 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)). +rewrite eqbE if_same IHn // apush_catE -cats1 -!catA. +by case: eqVneq => // -> ->. Qed. End CBV.