QIITExamples

module QIITExamples where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order

module Example1 where

  infixr 20 _∷_

  data FinSet : Type where
    []    : FinSet
    _∷_   : (x : ℕ) (xs : FinSet) → FinSet
    dup   : (x : ℕ) (xs : FinSet) → x ∷ x ∷ xs ≡ x ∷ xs
    comm  : (x y : ℕ) (xs : FinSet) → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
    trunc : isSet FinSet

module Example2 where
  data SortedList : Type
  data _≤ₗ_ : ℕ → SortedList → Type

  infixr 21 cons
  syntax cons x xs p = x ∷⟨ p ⟩ xs

  data SortedList where
    []   : SortedList
    cons : (x : ℕ) (xs : SortedList) (p : x ≤ₗ xs) → SortedList

  data _≤ₗ_ where
    []≤ₗ   : {n : ℕ} → n ≤ₗ []
    cons≤ₗ : {n x : ℕ} {xs : SortedList} {p : x ≤ₗ xs}
           → n ≤ x
           → n ≤ₗ x ∷⟨ p ⟩ xs

  ex1 : SortedList
  ex1 = 0 ∷⟨ cons≤ₗ (≤-suc ≤-refl) ⟩ 1 ∷⟨ []≤ₗ ⟩ []

  ex2 : SortedList
  ex2 = 0 ∷⟨ cons≤ₗ ≤-refl ⟩ 0 ∷⟨ cons≤ₗ (≤-suc ≤-refl) ⟩ 1 ∷⟨ []≤ₗ ⟩ []

module Example3 where
  data SortedList : Type
  data _≤ₗ_ : ℕ → SortedList → Type

  infixr 21 cons
  syntax cons x xs p = x ∷⟨ p ⟩ xs

  data SortedList where
    []    : SortedList
    cons  : (x : ℕ) (xs : SortedList) (p : x ≤ₗ xs) → SortedList
    dup   : (x : ℕ) (xs : SortedList) (p : x ≤ₗ xs) (q : x ≤ₗ x ∷⟨ p ⟩ xs)
          → x ∷⟨ q ⟩ x ∷⟨ p ⟩ xs ≡ x ∷⟨ p ⟩ xs
    trunc : isSet SortedList

  data _≤ₗ_ where
    []≤ₗ   : {n : ℕ} → n ≤ₗ []
    cons≤ₗ : {n x : ℕ} {xs : SortedList} {p : x ≤ₗ xs}
           → n ≤ x
           → n ≤ₗ x ∷⟨ p ⟩ xs

  ex1 : SortedList
  ex1 = 0 ∷⟨ cons≤ₗ (≤-suc ≤-refl) ⟩ 1 ∷⟨ []≤ₗ ⟩ []

  ex2 : SortedList
  ex2 = 0 ∷⟨ cons≤ₗ ≤-refl ⟩ 0 ∷⟨ cons≤ₗ (≤-suc ≤-refl) ⟩ 1 ∷⟨ []≤ₗ ⟩ []

  ex2≡ex1 : ex2 ≡ ex1
  ex2≡ex1 = dup 0 (1 ∷⟨ []≤ₗ ⟩ []) (cons≤ₗ (≤-suc ≤-refl)) (cons≤ₗ ≤-refl)