{-# OPTIONS --allow-unsolved-metas #-}
module session05 where

{-
  Possible topics for today:

  0. Random questions and comments
  1. More on program verification
  2. Numbers beyond infinity
-}

module Random where
  data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ
  
  Nat : Set
  Nat = ℕ
  
  -- parametric style (the parameter X will be fixed throughout the declaration)
  data _≡_ {X : Set} : X → X → Set where
    refl : {x : X} → x ≡ x
  
  -- indexed style (the value of X can vary)
  data _≡'_ : {X : Set} → X → X → Set₁ where
    refl : {X : Set} → {x : X} → x ≡' x   -- this is a new freshly-minted inhabitant of _≡'_ {X} x x
    foo : zero ≡' succ zero               -- this is a new freshly-minted inhabitant of _≡'_ {ℕ} zero (succ zero)

-- More on verified algorithms. Case study: insertion sort
-- 1. Implement insertion sort
-- 2. Verify that the implementation is correct
-- 3. Reimplement insertion sort in a correct-by-construction manner

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

open import Padova2025.ProvingBasics.Connectives.Disjunction

-- import: loading a module defined in a different file
-- open: open a module (whether it's from the same file or from an already imported file), i.e.
--       bringing the module's definition into the current scope

-- Let's fix a type A; for any elements x, y : A, a type x ≤ y of witnesses that x is at most y;
-- a decision function which inputs two elements x, y : A and outputs either a witness that x ≤ y
-- or a witness that y ≤ x.
module Implementation (A : Set) (_≤_ : A → A → Set) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where
  -- The task of the `insert` function is to behave as `_∷_`, but ensuring that the output list
  -- will be sorted if the input list was.
  --
  -- Input: a new element x and a sorted list ys
  -- Output: a sorted containing all the elements of ys, and the new element x, and none others
  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)

  cheatsort : List A → List A
  cheatsort xs = []

module Verification (A : Set) (_≤_ : A → A → Set) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where
  -- For every list `xs`, let's introduce the type `IsOrdered xs` of witnesses that the list `xs` is (ascendingly) ordered.
  data IsOrdered : List A → Set where
    empty     : IsOrdered []
    singleton : {x : A} → IsOrdered (x ∷ [])
    cons      : {x y : A} {ys : List A} → x ≤ y → IsOrdered (y ∷ ys) → IsOrdered (x ∷ (y ∷ ys))

  -- Include the definitions of the Implementation module, instantiated with the same three parameters as this module
  -- is instantiated with
  open Implementation A _≤_ cmp? using (sort; insert; cheatsort)

  lemma₀ : (x y : A) (ys : List A) → y ≤ x → IsOrdered (y ∷ ys) → IsOrdered (y ∷ insert x ys)
  lemma₀ = {!!}

  lemma : (x : A) (ys : List A) → IsOrdered ys → IsOrdered (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 = lemma₀ x y ys y≤x p

  -- Logical reading: For every list xs, it is the case that sort xs is ordered.
  -- Computational reading: `theorem` is a function which inputs a list `xs` and outputs a witness that `sort xs` is ordered.
  theorem : (xs : List A) → IsOrdered (sort xs)
  theorem []       = empty
  theorem (x ∷ xs) = lemma x (sort xs) (theorem xs)

  cheattheorem : (xs : List A) → IsOrdered (cheatsort xs)
  cheattheorem xs = empty

module CorrectByConstruction (A : Set) (_≤_ : A → A → Set) (-∞ : A) (min! : {x : A} → -∞ ≤ x) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where
  -- `OList l` is the type of ordered lists of elements of A bounded from below by `l`
  -- (i.e. all entries should be ≥ l).
  data OList (l : A) : Set where
    nil  : OList l  -- the empty ordered list
    cons : (x : A) → l ≤ x → OList x → OList l
    -- `cons` is a function which inputs an element x and an ordered list all of whose elements are ≥ x
    -- and which outputs a freshly-minted ordered list all of whose elements are ≥ l
    -- for instance, `cons 6 (cons 2 (cons 4 nil))` should be forbidden

  insert : {l : A} (x : A) → l ≤ x → OList l → OList l
  insert x l≤x nil             = cons x l≤x nil
  insert x l≤x (cons y l≤y ys) with cmp? x y
  ... | left  x≤y = cons x l≤x (cons y x≤y ys)
  ... | right y≤x = cons y l≤y (insert x y≤x ys)

  sort : List A → OList -∞
  sort []       = nil
  sort (x ∷ xs) = insert x min! (sort xs)

-- Ordinal numbers beyond infinity \o/
-- 0, 1, 2, ..., ω, ω + 1, ω + 2, ..., ω·2, ω·2 + 1, ..., ω·ω = ω², ..., ω³, ...
--
-- ω = the smallest infinite number
module Ordinal where
  open import Padova2025.ProgrammingBasics.Naturals.Base

  data O : Set
  Monotonic : (ℕ → O) → Set
  _<_ : O → O → Set
  data _≤_ : O → O → Set

  Monotonic f = ((n : ℕ) → f n < f (succ n))
  -- So for a monotonic function, we will have f 0 < f 1 < f 2 < ...

  data O where
    -- There should be a first ordinal number, called "zero".
    zer : O

    -- Every ordinal number should have a successor.
    -- For instance, ω + 1 is the successor of ω.
    -- For instance, ω + 2 is the successor of ω + 1.
    suc : O → O

    -- Every monotonic infinite sequence of ordinals should have a limit.
    -- For instance, ω     is the limit of the sequence 0, 1, 2, ...
    -- For instance, ω · 2 is the limit of the sequence ω, ω+1, ω+2, ...
    -- By "monotonic", we mean strictly increasing.
    lim : (f : ℕ → O) → Monotonic f → O
    -- Not *every* sequence should have a limit, for instance we don't expect a limit for 0, 1, 0, 1, ...

  x < y = suc x ≤ y

  -- For any ordinal numbers x and y, `x ≤ y` will be the type of witnesses that `x` is at most `y`.
  data _≤_ where
    ≤-zer      : {x : O} → zer ≤ x
    ≤-suc-mon  : {x y : O} → x ≤ y → suc x ≤ suc y

    -- Together, the following two constructors expresses that `lim f fmon` is the smallest number which is ≥ than all terms of f.
    ≤-cocone   : {x : O} {n : ℕ} {f : ℕ → O} {fmon : Monotonic f} → x ≤ f n → x ≤ lim f fmon
    ≤-limiting : {f : ℕ → O} {fmon : Monotonic f} {x : O} → ((n : ℕ) → f n ≤ x) → lim f fmon ≤ x

  uno : O
  uno = suc zer

  fromℕ : ℕ → O
  fromℕ zero     = zer
  fromℕ (succ x) = suc (fromℕ x)
  -- For instance, fromℕ (succ zero) is uno.

  ω : O
  ω = lim fromℕ {!!}

  ω+1 : O
  ω+1 = suc ω

  -- ω + 1 is strictly larger than ω, whereas 1 + ω is just ω again.