From 8423c3c139aae2114d65c9d2407964d3b4714c39 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 1 Oct 2025 07:34:21 +0200 Subject: [PATCH] New result: `List.sorted_range` Proves that `range` is sorted for `(<)` --- theories/datatypes/List.ec | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec index cecd10e893..de13d83a45 100644 --- a/theories/datatypes/List.ec +++ b/theories/datatypes/List.ec @@ -3822,6 +3822,17 @@ rewrite -(perm_cat2l [x]) perm_eq_sym perm_catCl perm_catAC -catA /=. by rewrite -eqss (@perm_eq_trans s) // perm_sort. qed. +lemma sorted_range m n : sorted (<) (range m n). +proof. +case: (n <= m); first by move=> ?; rewrite range_geq. +move/ltzNge => lt_mn; rewrite range_ltn //=. +suff: forall m, 0 <= m => forall b n, b < n => path (<) b (range n (n + m)). +- by move=> /(_ (n - (m + 1)) _ m (m+1) _) /#. +move=> {m n lt_mn}; elim=> /= [|m ge0_m ih] b n ?. +- by rewrite range_geq. +by rewrite addrA range_ltn 1:/# /= addrAC; split=> //#. +qed. + (* -------------------------------------------------------------------- *) (* retrieving a maximal element *) (* -------------------------------------------------------------------- *)