{-# OPTIONS --cubical --safe --exact-split -WnoUnsupportedIndexedMatch #-} module Cubical.Structures.Set.CMon.SList.Sort.Sort where open import Cubical.Foundations.Everything open import Cubical.Data.Sigma open import Cubical.Data.Nat open import Cubical.Data.Nat.Order renaming (_≤_ to _≤ℕ_; _<_ to _<ℕ_) open import Cubical.Data.Sum as ⊎ open import Cubical.Data.Maybe as Maybe open import Cubical.Data.Empty as ⊥ open import Cubical.Induction.WellFounded open import Cubical.Relation.Binary open import Cubical.Relation.Binary.Order open import Cubical.Relation.Nullary open import Cubical.Relation.Nullary.HLevels open import Cubical.Data.List open import Cubical.HITs.PropositionalTruncation as P import Cubical.Data.List as L open import Cubical.Functions.Logic as L hiding (¬_; ⊥) import Cubical.Structures.Set.Mon.Desc as M import Cubical.Structures.Set.CMon.Desc as M import Cubical.Structures.Free as F open import Cubical.Structures.Sig open import Cubical.Structures.Str public open import Cubical.Structures.Tree open import Cubical.Structures.Eq open import Cubical.Structures.Arity open import Cubical.Structures.Set.Mon.List open import Cubical.Structures.Set.CMon.SList.Base renaming (_∷_ to _∷*_; [] to []*; [_] to [_]*; _++_ to _++*_) import Cubical.Structures.Set.CMon.SList.Base as S open import Cubical.Structures.Set.CMon.SList.Length as S open import Cubical.Structures.Set.CMon.SList.Membership as S open import Cubical.Structures.Set.CMon.SList.Sort.Base open Iso private variable ℓ : Level A : Type ℓ module Sort→Order (isSetA : isSet A) (sort : SList A -> List A) (sort≡ : ∀ xs -> list→slist (sort xs) ≡ xs) where isSetMaybeA : isSet (Maybe A) isSetMaybeA = isOfHLevelMaybe 0 isSetA isSetListA : isSet (List A) isSetListA = isOfHLevelList 0 isSetA private module 𝔖 = M.CMonSEq < SList A , slist-α > slist-sat open Membership isSetA open Membership* isSetA open Sort isSetA sort open Sort.Section isSetA sort sort≡ least : SList A -> Maybe A least xs = head-maybe (sort xs) least-nothing : ∀ xs -> least xs ≡ nothing -> xs ≡ []* least-nothing xs p with sort xs | inspect sort xs ... | [] | [ q ]ᵢ = sort-[] xs q ... | y ∷ ys | [ q ]ᵢ = ⊥.rec (¬just≡nothing p) least-Σ : ∀ x xs -> least xs ≡ just x -> Σ[ ys ∈ List A ] (sort xs ≡ x ∷ ys) least-Σ x xs p with sort xs ... | [] = ⊥.rec (¬nothing≡just p) ... | y ∷ ys = ys , congS (_∷ ys) (just-inj y x p) least-in : ∀ x xs -> least xs ≡ just x -> x ∈* xs least-in x xs p = let (ys , q) = least-Σ x xs p x∷ys≡xs = congS list→slist (sym q) ∙ sort≡ xs in subst (x ∈*_) x∷ys≡xs (x∈*xs x (list→slist ys)) least-choice : ∀ x y -> (least (x ∷* [ y ]*) ≡ just x) ⊔′ (least (x ∷* [ y ]*) ≡ just y) least-choice x y = P.rec squash₁ (⊎.rec (L.inl ∘ congS head-maybe) (L.inr ∘ congS head-maybe)) (sort-choice x y) _≤_ : A -> A -> Type _ x ≤ y = least (x ∷* y ∷* []*) ≡ just x isProp-≤ : ∀ {a} {b} -> isProp (a ≤ b) isProp-≤ = isSetMaybeA _ _ ≤-Prop : ∀ x y -> hProp _ ≤-Prop x y = (x ≤ y) , isProp-≤ refl-≤ : ∀ x -> x ≤ x refl-≤ x = P.rec isProp-≤ (⊎.rec (idfun _) (idfun _)) (least-choice x x) antisym-≤ : ∀ x y -> x ≤ y -> y ≤ x -> x ≡ y antisym-≤ x y p q = P.rec (isSetA x y) (⊎.rec (λ xy -> just-inj x y $ just x ≡⟨ sym xy ⟩ least (x ∷* y ∷* []*) ≡⟨ congS least (swap x y []*) ⟩ least (y ∷* x ∷* []*) ≡⟨ q ⟩ just y ∎) (λ yx -> just-inj x y $ just x ≡⟨ sym p ⟩ least (x ∷* [ y ]*) ≡⟨ yx ⟩ just y ∎)) (least-choice x y) total-≤ : ∀ x y -> (x ≤ y) ⊔′ (y ≤ x) total-≤ x y = P.rec squash₁ (⊎.rec L.inl (λ p -> L.inr $ least (y ∷* [ x ]*) ≡⟨ congS least (swap y x []*) ⟩ least (x ∷* [ y ]*) ≡⟨ p ⟩ just y ∎)) (least-choice x y) dec-≤ : (discA : Discrete A) -> ∀ x y -> Dec (x ≤ y) dec-≤ discA x y = discreteMaybe discA _ _ is-sorted→≤ : ∀ x y -> is-sorted (x ∷ y ∷ []) -> x ≤ y is-sorted→≤ x y = P.rec (isSetMaybeA _ _) λ (xs , p) -> congS head-maybe (congS sort (sym (sym (sort≡ xs) ∙ congS list→slist p)) ∙ p) module _ (sort-is-sort : is-head-least) where trans-≤ : ∀ x y z -> x ≤ y -> y ≤ z -> x ≤ z trans-≤ x y z x≤y y≤z with least (x ∷* y ∷* z ∷* []*) | inspect least (x ∷* y ∷* z ∷* []*) ... | nothing | [ p ]ᵢ = ⊥.rec (snotz (congS S.length (least-nothing _ p))) ... | just u | [ p ]ᵢ = P.rec (isSetMaybeA _ _) (⊎.rec case1 (P.rec (isSetMaybeA _ _) (⊎.rec case2 (case3 ∘ x∈[y]→x≡y _ _)) ) ) (least-in u (x ∷* y ∷* z ∷* []*) p) where tail' : Σ[ xs ∈ List A ] u ∷ xs ≡ sort (x ∷* y ∷* z ∷* []*) tail' with sort (x ∷* y ∷* z ∷* []*) ... | [] = ⊥.rec (¬nothing≡just p) ... | v ∷ xs = xs , congS (_∷ xs) (just-inj _ _ (sym p)) tail : List A tail = tail' .fst tail-proof : u ∷ tail ≡ sort (x ∷* y ∷* z ∷* []*) tail-proof = tail' .snd u∷tail-is-sorted : is-sorted (u ∷ tail) u∷tail-is-sorted = ∣ ((x ∷* y ∷* z ∷* []*) , sym tail-proof) ∣₁ u-is-smallest : ∀ v -> v ∈* (x ∷* y ∷* z ∷* []*) -> u ≤ v u-is-smallest v q = is-sorted→≤ u v (sort-is-sort u v tail u∷tail-is-sorted (subst (v ∈_) (sym tail-proof) (sort-∈ v _ q))) case1 : u ≡ x -> x ≤ z case1 u≡x = subst (_≤ z) u≡x (u-is-smallest z (L.inr (L.inr (L.inl refl)))) case2 : u ≡ y -> x ≤ z case2 u≡y = subst (_≤ z) (antisym-≤ y x y≤x x≤y) y≤z where y≤x : y ≤ x y≤x = subst (_≤ x) u≡y (u-is-smallest x (L.inl refl)) case3 : u ≡ z -> x ≤ z case3 u≡z = subst (x ≤_) (antisym-≤ y z y≤z z≤y) x≤y where z≤y : z ≤ y z≤y = subst (_≤ y) u≡z (u-is-smallest y (L.inr (L.inl refl))) ≤-isToset : IsToset _≤_ IsToset.is-set ≤-isToset = isSetA IsToset.is-prop-valued ≤-isToset x y = isOfHLevelMaybe 0 isSetA _ _ IsToset.is-refl ≤-isToset = refl-≤ IsToset.is-trans ≤-isToset = trans-≤ IsToset.is-antisym ≤-isToset = antisym-≤ IsToset.is-strongly-connected ≤-isToset = total-≤