{-# OPTIONS --allow-unsolved-metas #-}
{-

    Can abstract mathematical proofs be run as programs?

    Theoretical Computer Science Seminar
    University of Antwerp


    Agda is:

    ‍💻 a programming language
        - purely functional
        - similar to Haskell
        - statically typed
        - familiar types: integers, lists, trees, ...
        - type inference

    📝 a proof language
        - facilitated by types of witnesses, e.g.
            - type of witnesses that a sorting function works correctly
            - type of witnesses that there are infinitely many prime numbers
            - type of witnesses that the continuum hypothesis holds


    Agda helps us in ...
    
    🧮 implementing algorithms which are
        - correct by post-hoc verification or
        - correct by construction

    ✅ verifying the correctness of proofs

    💭 structuring and communicating mathematical thoughts

    ⚙️ appreciating mathematics from a new computational angle

    🚀 collaboratively engineering mathematical libraries

-}


data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

-- In Haskell, Either A B
data _⊎_ (A : Set) (B : Set) : Set where
  left  : A → A ⊎ B
  right : B → A ⊎ B

module _ (A : Set) (_≤_ : A → A → Set) (cmp : (x : A) → (y : A) → (x ≤ y) ⊎ (y ≤ x)) where
  -- Contract: "insert x ys" is ascendingly ordered, if "ys" is ascendingly ordered.
  insert : A → List A → List A
  insert x []       = x ∷ []
  insert x (y ∷ ys) with cmp x y
  ... | left  x≤y = x ∷ (y ∷ ys)
  ... | right y≤x = y ∷ insert x ys

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

  data IsSorted : List A → Set where
    empty     : IsSorted []
    singleton : {x : A} → IsSorted (x ∷ [])
    cons      : {x y : A} {ys : List A} → x ≤ y → IsSorted (y ∷ ys) → IsSorted (x ∷ (y ∷ ys))

  lemma : (x : A) → (ys : List A) → IsSorted ys → IsSorted (insert x ys)
  lemma x []       p = singleton
  lemma x (y ∷ ys) p with cmp x y
  ... | left  x≤y = cons x≤y p
  ... | right y≤x = {!!}

  -- Claim: The sort function works correctly.
  -- Logical reading: For every list "xs", the list "sort xs" is ascendingly ordered.
  -- Computational reading: "theorem" is a function which inputs a list "xs"
  -- and outputs a value of type "IsSorted (sort xs)". The values of this type
  -- are witnesses of the claim that "sort xs" is ascendingly ordered.
  theorem : (xs : List A) → IsSorted (sort xs)
  theorem []       = empty
  theorem (x ∷ xs) = lemma x (sort xs) (theorem xs)

--euclid : (n : ℕ) → ...type of witnesses that there are larger prime numbers than n...