Skip to content

Commit

Permalink
Clean up
Browse files Browse the repository at this point in the history
  • Loading branch information
@pi8027
pi8027 committed Nov 3, 2023
1 parent e01cb81 commit c1cea60
Showing 1 changed file with 65 additions and 71 deletions.
136 changes: 65 additions & 71 deletions theories/stablesort.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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).

Expand Down Expand Up @@ -501,24 +494,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 -[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 :
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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.
Expand Down

0 comments on commit c1cea60

Please sign in to comment.