{-
  Today (?):
  1. A riddle in termination
  2. Disjunction (∨), existential quantification (∃), conjunction (∧)
  3. Assisting you with exercises :-)
-}

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Equality.Base

{-
f : ℕ → ℕ
f zero     = zero
f (succ x) = f (f x)
-- Agda complains: "Termination checking failed".
-}

{-
  Motto: Agda is like a calculator, but for logic.
  (Nothing more, nothing less.)
  Agda is very careful, very diligent, but not smart.
-}

-- f one   = f (succ zero) = f (f zero) = f zero = zero
-- f two   = f (succ one)  = f (f one)  = f zero = zero
-- f three = ...                                 = zero
-- ...

{-
  Five ways of dealing with that issue:
  0. Give up, do something else
  1. Promise to Agda that the recursion terminates
  2. Mark the function as non-terminating, so that we can continue,
     but the function will never be unrolled during type checking
  3. Use a brittle kind of gas
  4. Use a more sophisticated kind of gas
  5. Prove termination
-}

-- Option 1 (rejected by Agda if {-# OPTIONS --safe #-} is active)
{-# TERMINATING #-}
f : ℕ → ℕ
f zero     = zero
f (succ x) = f (f x)

-- Option 2 (rejected by Agda if {-# OPTIONS --safe #-} is active)
{-# NON_TERMINATING #-}
g : ℕ → ℕ
g zero     = zero
g (succ x) = g (g x)

g-eq : (x : ℕ) → g (succ x) ≡ g (g x)
g-eq x = {!refl!}

{-# NON_TERMINATING #-}
loop : zero ≡ one
loop = loop
-- In blackboard mathematics, this proof attempt would like this:
-- Result A. 0 = 1.
-- Proof. This follows from Result A. ∎

-- Option 3.
h : ℕ → ℕ
h x = go (succ x) x
  where
  go : ℕ → ℕ → ℕ
  go zero       x        = four  -- fantasy value, hopefully never reached
  go (succ gas) zero     = zero
  go (succ gas) (succ x) = go gas (go gas x)

-- Option 5.
-- Let us introduce a type "Def x" containing witnesses that
-- the funtion is defined on input "x", i.e. that the recursion terminates
-- on input "x".

{-
  fun zero     = zero
  fun (succ x) = fun (fun x)
-}

data Def : ℕ → Set
fun : (x : ℕ) → Def x → ℕ

data Def where
  base : Def zero
  -- "fun terminates on input zero."

  step : {x : ℕ} → (p : Def x) → Def (fun x p) → Def (succ x)
  -- "If 'fun x' terminates and if 'fun (fun x)' terminates, then also
  -- 'fun (succ x)' terminates."
  -- "If fun is defined on input x and if fun is defined on input (fun x);
  -- then fun is also defined on input succ x."

fun zero     base       = zero
fun (succ x) (step p q) = fun (fun x p) q

fun-is-defined-on-input-one : Def one
fun-is-defined-on-input-one = step base base

fun-is-defined-on-input-two : Def two
fun-is-defined-on-input-two = step fun-is-defined-on-input-one base

-- Logical reading: For every number x, the function is defined on input x.
-- Computational reading: "theorem" inputs a number x and outputs a witness
-- that the function is defined on input x.
theorem : (x : ℕ) → Def x
theorem x = {!!}

open import Padova2025.ProvingBasics.EvenOdd
open import Padova2025.ProvingBasics.Negation

-- "A ⊎ B" is the disjoint union of the types "A" and "B".
data _⊎_ (A B : Set) : Set where
  left  : A → A ⊎ B    -- Logical reading: If A, then A or B.
  right : B → A ⊎ B    -- Logical reading: If B, then A or B.
-- The inhabitants of A ⊎ B are:
-- For each x : A, we have "left  x" as an inhabitant of A ⊎ B.
-- For each y : B, we have "right y" as an inhabitant of A ⊎ B.

one-is-even-or-odd : Even one ⊎ Odd one
one-is-even-or-odd = right base-odd

five-is-even-or-odd : Even five ⊎ Odd five
five-is-even-or-odd = right (step-odd (step-odd base-odd))

every-number-is-zero-or-not-zero : (x : ℕ) → (x ≡ zero) ⊎ (¬ (x ≡ zero))
every-number-is-zero-or-not-zero x = {!!}

oracle : {A : Set} → ¬ ¬ (A ⊎ (¬ A))
oracle = λ k → k (right (λ x → k (left x)))

-- "Every number is either even or odd."
-- "Even x ⊎ Odd x" is the type of witnesses that x is even or that x is odd.
even-or-odd : (x : ℕ) → Even x ⊎ Odd x
even-or-odd zero        = left base-even
even-or-odd (succ zero) = right base-odd
even-or-odd (succ (succ x)) with even-or-odd x
... | left  p = left  (step-even p)
... | right q = right (step-odd q)

even-or-odd' : (x : ℕ) → Even x ⊎ Odd x
even-or-odd' zero        = left base-even
even-or-odd' (succ zero) = right base-odd
even-or-odd' (succ (succ x)) = lemma (even-or-odd' x)
  where
  lemma : {a : ℕ} → Even a ⊎ Odd a → Even (succ (succ a)) ⊎ Odd (succ (succ a))
  lemma (left  p) = left  (step-even p)
  lemma (right q) = right (step-odd q)

{-
                              { left (step-even p),   if even-or-odd x is of the form left p
even-or-odd (succ (succ x)) = {
                              { right (step-odd q),   if even-or-odd x is of the form right q
-}

example : ℕ → ℕ
example x with even-or-odd x
... | left  p = four + x
... | right q = three

_ : example five ≡ three
_ = refl

_ : example four ≡ four + four
_ = refl

_ : example four ≡ succ (succ (succ (succ (succ (succ (succ (succ zero)))))))
_ = refl

-- "Beyond every natural number, there is an even number."
-- ∀(x ∈ ℕ). ∃(y ∈ ℕ). (y ≥ x ∧ Even(y))

-- Given a type A and given a predicate P : A → Set (for instance A = ℕ, P = Even),
-- there is a type "Σ A P" of witnesses that there is at least one x : A such that P x holds.
-- These witnesses are dependent pairs (x , p) consisting of a suitable value x : A and a witness p : P x.
-- A nicer syntax for writing this type is:                          "Σ[ x ∈ A ] P x"
-- In case we do not want to specify the type A, an abbreviation is: "∃[ x ] P x"

data Σ (A : Set) (P : A → Set) : Set where
  ⟦_,_⟩ : (x : A) → P x → Σ A P

there-exists-at-least-one-odd-number : Σ ℕ Odd
there-exists-at-least-one-odd-number = ⟦ one , base-odd ⟩

there-exists-at-least-one-odd-number' : Σ ℕ Odd
there-exists-at-least-one-odd-number' = ⟦ three , step-odd base-odd ⟩

beyond-every-natural-number-there-is-an-even-number : (x : ℕ) → Σ ℕ (λ y → {!......... Even y!})
-- beyond-every-natural-number-there-is-an-even-number : (x : ℕ) → ∃[ y ] ...... Even y
beyond-every-natural-number-there-is-an-even-number x = {!!}

-- A witness for a conjunction "A and B" should consist of a witness for A and a witness for B,
-- i.e. a witness for "A and B" should be a pair consisting of a witness for A and a witness for B.
data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B
-- In other words, "A × B" is the type of pairs of elements of A and elements of B.
-- "Cartesian product type".
-- Its inhabitants are of the form (x , y) with x : A and y : B.

four-is-even-and-five-is-odd : Even four × Odd five
four-is-even-and-five-is-odd = step-even (step-even base-even) , step-odd (step-odd base-odd)