diff options
| author | Cyril Cohen | 2020-11-17 22:45:49 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-18 01:33:41 +0100 |
| commit | 8eb486ad82accfb1417be11ecc2889aa09c22081 (patch) | |
| tree | b780572ba74f5d464d7adb440de6c9c66f628625 | |
| parent | 068284d23c4a05c7ffeb4db8e277d24ed561369f (diff) | |
Adding size_merge_sort_push
This documents the fact that `merge_sort_push` preserves an invariant on its second argument.
Importing a statement and proof by Georges Gonthier, inspired by one of Karl Palmskog's contribution.
Co-Authored-By: Karl Palmskog <palmskog@kth.se>
Co-Authored-By: Georges Gonthier <georges.gonthier@inria.fr>
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 13 |
2 files changed, 16 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dbe49c7..a36eab8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -286,6 +286,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `fullrowsub_free`, `mxrank_fullrowsub`, `eq_fullrowsub`, and `fullrankfun_inj`. +- in `path.v`, added `size_merge_sort_push`, which documents an + invariant of `merge_sort_push`. + ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 93521d7..4fe56b7 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -691,6 +691,19 @@ move=> leT_tr; elim: s => //= y [//|z s] ihs /andP[xy yz]; rewrite xy {}ihs//. by move: yz => /= /andP [/(leT_tr _ _ _ xy) ->]. Qed. +Remark size_merge_sort_push s1 : + let graded ss := forall i, size (nth [::] ss i) \in pred2 0 (2 ^ (i + 1)) in + size s1 = 2 -> {homo merge_sort_push s1 : ss / graded ss}. +Proof. +set n := {2}1; rewrite -[RHS]/(2 ^ n) => graded sz_s1 ss. +elim: ss => [|s2 ss IHss] in (n) graded s1 sz_s1 * => sz_ss i //=. + by case: i => [|[]] //; rewrite sz_s1 inE eqxx orbT. +case: s2 i => [|x s2] [|i] //= in sz_ss *; first by rewrite sz_s1 inE eqxx orbT. + exact: (sz_ss i.+1). +rewrite addSnnS; apply: IHss i => [|i]; last by rewrite -addSnnS (sz_ss i.+1). +by rewrite size_merge size_cat sz_s1 (eqnP (sz_ss 0)) addnn expnS mul2n. +Qed. + Hypothesis leT_tr : transitive leT. Lemma path_sortedE x s : path x s = all (leT x) s && sorted s. |