From c5b4e866303ec63f7fbee7c7f9aad0d9c4f9dee8 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 16 Feb 2024 18:04:01 +0100 Subject: [PATCH] Remove workaround for coq/coq#3488 --- theories/stablesort.v | 6 ------ 1 file changed, 6 deletions(-) diff --git a/theories/stablesort.v b/theories/stablesort.v index e56d0ee..fb5001c 100644 --- a/theories/stablesort.v +++ b/theories/stablesort.v @@ -508,13 +508,10 @@ 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 -/(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. @@ -560,12 +557,9 @@ 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.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 [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.