Sort by insertion for lists
Content created by Fredrik Bakke, Egbert Rijke, Louis Wasserman and Victor Blanchi.
Created on 2023-05-22.
Last modified on 2025-05-14.
module lists.sort-by-insertion-lists where
Imports
open import finite-group-theory.permutations-standard-finite-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import lists.arrays open import lists.lists open import lists.permutation-lists open import lists.sort-by-insertion-tuples open import lists.sorted-lists open import lists.sorting-algorithms-lists open import order-theory.decidable-total-orders
Idea
We use the definition of sort by insertion for tuples
(lists.sort-by-insertion-tuples
) and we
adapt it for lists.
Definition
module _ {l1 l2 : Level} (X : Decidable-Total-Order l1 l2) where insertion-sort-list : list (type-Decidable-Total-Order X) → list (type-Decidable-Total-Order X) insertion-sort-list l = list-tuple (length-list l) (insertion-sort-tuple X (tuple-list l))
Properties
Sort by insertion is a sort
is-sort-insertion-sort-list : is-sort-list X insertion-sort-list is-sort-insertion-sort-list = is-sort-list-is-sort-tuple ( X) ( insertion-sort-tuple X) ( is-sort-insertion-sort-tuple X) is-permutation-insertion-sort-list : is-permutation-list insertion-sort-list is-permutation-insertion-sort-list = pr1 (is-sort-insertion-sort-list) permutation-insertion-sort-list : (l : list (type-Decidable-Total-Order X)) → Permutation (length-list l) permutation-insertion-sort-list = permutation-list-is-sort-list X insertion-sort-list is-sort-insertion-sort-list eq-permute-list-permutation-insertion-sort-list : (l : list (type-Decidable-Total-Order X)) → insertion-sort-list l = permute-list l (permutation-insertion-sort-list l) eq-permute-list-permutation-insertion-sort-list = eq-permute-list-permutation-is-sort-list X insertion-sort-list is-sort-insertion-sort-list is-sorting-insertion-sort-list : (l : list (type-Decidable-Total-Order X)) → is-sorted-list X (insertion-sort-list l) is-sorting-insertion-sort-list = pr2 (is-sort-insertion-sort-list)
Recent changes
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).
- 2023-06-09. Fredrik Bakke. Remove unused imports (#648).
- 2023-05-23. Egbert Rijke. fix broken links (#629).
- 2023-05-22. Victor Blanchi and Fredrik Bakke. Cycle prime decomposition is closed under cartesian product (#624).