A simpler proof of all_sort

pi8027 · Feb 23, 2024 · f63908e · f63908e
1 parent 7f8650d
commit f63908e
Showing 1 changed file with 10 additions and 13 deletions.
diff --git a/theories/stablesort.v b/theories/stablesort.v
@@ -1029,12 +1029,6 @@ apply: (@param_asort _ _ eq _ _ R) => //.
 by elim: s; constructor.
 Qed.
 
-Lemma all_sort (s : seq T) : all P (sort _ leT s) = all P s.
-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 count_sort (a : pred T) (s : seq T) : count a (sort _ leT s) = count a s.
 Proof.
 by elim/sort_ind: (sort _ leT s) => // xs xs' IHxs ys ys' IHys;
@@ -1044,16 +1038,18 @@ Qed.
 Lemma size_sort (s : seq T) : size (sort _ leT s) = size s.
 Proof. exact: (count_sort predT). Qed.
 
+Lemma all_sort (s : seq T) : all P (sort _ leT s) = all P s.
+Proof. by rewrite !all_count count_sort size_sort. 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.
 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.
+  by rewrite pairwise_cat => /and3P[/allrel_merge <- /IHxs -> /IHys ->].
+rewrite pairwise_cat allrelC -allrel_rev2 => /and3P[hlr /IHxs -> /IHys ->].
+by rewrite allrel_merge // rev_cat !revK.
 Qed.
 
 Lemma sorted_sort : transitive leT ->
@@ -1341,7 +1337,7 @@ Context (leT_total : total leT) (leT_tr : transitive leT).
 Lemma subseq_sort : {homo sort _ leT : t s / subseq t s}.
 Proof.
 move=> _ s /subseqP [m _ ->].
-have [m' <-] := mask_sort leT_total leT_tr s m; exact: mask_subseq.
+by have [m' <-] := mask_sort leT_total leT_tr s m; exact: mask_subseq.
 Qed.
 
 Lemma sorted_subseq_sort (t s : seq T) :
@@ -1368,7 +1364,8 @@ Lemma subseq_sort_in (t s : seq T) :
   subseq t s -> subseq (sort _ leT t) (sort _ leT s).
 Proof.
 move=> leT_total leT_tr /subseqP [m _ ->].
-have [m' <-] := mask_sort_in leT_total leT_tr m (allss _); exact: mask_subseq.
+have [m' <-] := mask_sort_in leT_total leT_tr m (allss _).
+exact: mask_subseq.
 Qed.
 
 Lemma sorted_subseq_sort_in (t s : seq T) :
@@ -1395,9 +1392,9 @@ End StableSortTheory_Part2.
 
 End StableSortTheory.
 
-Arguments all_sort                sort {T} P leT s.
 Arguments count_sort              sort {T} leT a s.
 Arguments size_sort               sort {T} leT s.
+Arguments all_sort                sort {T} P leT s.
 Arguments sort_nil                sort {T} leT.
 Arguments pairwise_sort           sort {T leT s} _.
 Arguments sorted_sort             sort {T leT} leT_tr {s} _.