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

{-
  Proposal for today:

  -1. Random questions and comments
  0. Upcoming events and conferences
  1. Review of some of the equational reasoning exercises
  2. Logical connectives
     - Review of ¬
     - ∨
     - ∃
     - ∧
  3. Program verification
-}

data ⊥ : Set where
-- empty data type

¬_ : Set → Set
¬ X = (X → ⊥)

-- Logical reading: If A, and if ¬ A, then ⊥. (The "law of non-contradiction".)
-- Computational reading: `foo` is a function which inputs
-- 0. an arbitrary type A (implicitly)
-- 1. a witness of A
-- 2. a witness of ¬ A
-- and which outputs a witness of ⊥.
foo : {A : Set} → A → ¬ A → ⊥
foo x f = f x
-- In English: "Assume A (let's call this assumption "x"). Assume ¬ A
-- (which means that A → ⊥) (let's call this assumption "f"). We want to show ⊥.
-- This follows by using assumption f, applied to the instance x."

-- bar : {A : Set} → "A or ¬ A"  -- the "law of excluded middle"
-- bar = ?

data Weird : Set where
  succ : Weird → Weird
-- This type is empty, but not manifestly empty.

-- Logical reading: "For every inhabitant of type Weird, we have a contradiction."
-- Computational reading: `theorem` is a function which inputs a value of type Weird and which outputs a value of type ⊥.
theorem : Weird → ⊥
theorem (succ x) = theorem x

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

-- For every type A and every type B, there will be a new type `A ⊎ B`,
-- the "tagged union A and B" / "disjoint union of A and B".
data _⊎_ (A B : Set) : Set where
  left  : A → A ⊎ B
  right : B → A ⊎ B
-- The inhabitants of `A ⊎ B` look as follows:
-- Firstly,  an inhabitant can be of the form `left x`,  where `x : A`.
-- Secondly, an inhabitant can be of the form `right y`, where `y : B`.
-- There are no more inhabitants.

data 𝟙 : Set where
  * : 𝟙
-- This type contains exactly one inhabitant, namely *.
-- "The unit type"
-- In set-theoretical notation: 𝟙 = { * }.

-- On a blackboard, we could form 𝟙 ∪ 𝟙 = { *, * } = { * } = 𝟙.
-- In contrast, 𝟙 ⊎ 𝟙 contains two distinct elements, namely `left *` and `right *`.

-- Intuitively, a witness of "A ∨ B" should either be a witness of A or a witness of B.
-- An inhabitant of (two + two ≡ four) ⊎ (two + two ≡ five) is either of the form left p,
-- where p is a witness that two + two equals four, or of the form right q,
-- where q is a witness that two + two equals five.

-- 2 + 2 equals 4 or 2 + 2 equals 5.
observation : (two + two ≡ four) ⊎ (two + two ≡ five)  --- \u+
observation = left refl

data Even : ℕ → Set where
  base-even : Even zero
  step-even : {n : ℕ} → Even n → Even (succ (succ n))

data Odd : ℕ → Set where
  base-odd : Odd one
  step-odd : {n : ℕ} → Odd n → Odd (succ (succ n))

five-is-odd : Odd five
five-is-odd = step-odd (step-odd base-odd)

-- Logical reading: For every number x, x is even or x is odd.
-- Computational reading: `even-or-odd` is a function which inputs a number `x`
-- and which outputs either `left p`, where `p` is a witness that `x` is even,
-- or `right q`, where `q` is a witness 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)

-- In mainstream programming languages which don't have dependent types, we could only
-- write a function of type "even-or-odd : ℕ → Bool" which would output false or true
-- depending on whether the input number is even or odd. In Agda, with dependent types,
-- we can do better and output an informative witness of the correct alternative.


-- "For every number x, either x is zero or there is a number y such that x ≡ succ y."
-- "∀x. (x = 0 ∨ (∃y. x = succ(y)))"

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

-- Idea: A witness of a claim of the form "∃x : A. P x" is a pair (x , p)
-- consisting of an element x : A and a witness p : P x. The type of witnesses
-- of "∃x : A. P x" will be written "Σ A P".
data Σ (A : Set) (P : A → Set) : Set where
  _,_ : (x : A) → P x → Σ A P
-- The inhabitants of Σ A P look as follows:
-- (x , p)
-- where x : A and p : P x. So the inhabitants are "dependent pairs".

-- "There is an even number."
-- "∃x. Even(x)"
there-is-an-even-number : Σ ℕ Even
there-is-an-even-number = (zero , base-even)

there-is-an-even-number' : Σ ℕ Even
there-is-an-even-number' = (two , step-even base-even)

-- `Σ ℕ Even` is an example for a type of witnesses which contains more than one witness.
-- In fact, it contains infinitely many witnesses.

-- "∀x. (x = 0 ∨ (∃y. x = succ(y)))"
-- The expression "λ y → (x ≡ succ y)" denotes a function of type ℕ → Set.
-- This function does not have a name (it is an anonymous function).
-- This function maps a number `y` to the type `x ≡ succ y`.
-- In blackboard mathematics, this expression is written "y ↦ (...)".
-- In lambda calculus, this expression is written "λy. (...)".
-- If we setup custom syntax, then "Σ ℕ (λ y → (x ≡ succ y))" can also be written as
-- "Σ[ y ∈ ℕ ] x ≡ succ y" or even as "∃[ y ] x ≡ succ y".
zero-or-succ : (x : ℕ) → (x ≡ zero) ⊎ Σ ℕ (λ y → (x ≡ succ y))
zero-or-succ zero     = left refl
zero-or-succ (succ a) = right (a , refl)

-- "It is not the case there exists a value of type Weird."
-- "It is not the case that there exists a value x : Weird such that nothing in particular holds".
theorem' : ¬ Σ Weird (λ x → 𝟙)
theorem' (x , _) = theorem x

-- Idea: A witness of A ∧ B should consist of a witness of A and a witness of B.
-- So the type of witnesses of A ∧ B should be the cartesian product of the type of witnesses of A
-- and the type of witnesses of B.
data _×_ (A B : Set) : Set where  -- \times
  _,_ : A → B → A × B

zero-is-even-and-one-is-odd : Even zero × Odd one
zero-is-even-and-one-is-odd = (base-even , base-odd)

-- Logical reading: If A ∧ B, then A.
-- Computational reading: `conj-elimination₁` is a function which inputs
-- 1. a type A (implicitly)
-- 2. a type B (implicitly)
-- 3. a witness that A and B holds
-- and which outputs a witness of A.
conj-elimination₁ : {A B : Set} → A × B → A
conj-elimination₁ (x , y) = x

data Bool : Set where
  false : Bool
  true  : Bool

id : Bool → Bool
id = (λ x → x)
-- same as: id x = x

neg : Bool → Bool
-- neg false = true
-- neg true  = false
neg = λ { false → true ; true → false }

neg' : Bool → Bool
neg' = λ
  { false → true
  ; true  → false
  }

{-# TERMINATING #-}
f : ℕ → ℕ
f zero     = zero
f (succ x) = f (f x)
-- f one = f (succ zero) = f (f zero) = f zero = zero
-- f two = f (succ one) = f (f one) = f zero = zero
-- ...
-- This definition gives rise to a total well-defined function, but it's not obvious
-- to Agda that this is the case.

trivial-observation : (x : ℕ) → f (succ x) ≡ f (f x)
trivial-observation x = refl

{-# NON_TERMINATING #-}
loop : ⊥
loop = loop

{-
  Six options how to deal with termination issues:
  1. Give up and implement a different function
  2. Promise (without a proof) to Agda that the function is terminating
  3. Mark the function as potentially non-terminating
  4. Use a brittle kind of gas
  5. Use a more sophisticated version of gas
  6. Employ the Bove–Capretta method for proving that the function terminates
-}

f-brittle-gas : ℕ → ℕ → ℕ
f-brittle-gas zero       x        = five  -- some fantasy value, hopefully never reached
f-brittle-gas (succ gas) zero     = zero
f-brittle-gas (succ gas) (succ x) = f-brittle-gas gas (f-brittle-gas gas x)

f-brittle-gas' : ℕ → ℕ
f-brittle-gas' x = f-brittle-gas (succ x) x  -- enough gas so that the fantasy value is not reached

we-should-prove : (x : ℕ) → f-brittle-gas' (succ x) ≡ f-brittle-gas' (f-brittle-gas' x)
we-should-prove x = {!!}

-- Bove–Capretta approach to our function f

-- Idea: First formalize f as a potentially partial function (a
-- function which need not be defined on all inputs), and then prove
-- that f is total (i.e. defined on all inputs).

-- F : ℕ → ℕ
-- F zero     = zero
-- F (succ x) = F (F x)

-- "Def x" is the type of witnesses that F is defined on the input x.
data Def : ℕ → Set
F : (x : ℕ) → Def x → ℕ

data Def where
  base : Def zero
  rec  : {x : ℕ} → (p : Def x) → Def (F x p) → Def (succ x)
  -- If F is defined on the input x (with witness p) and if F is defined on the input (F x p),
  -- then F is defined on the input succ x.

F zero     p         = zero
F (succ x) (rec p q) = F (F x p) q

F-is-total : (x : ℕ) → Def x
F-is-total x = {!!}

F' : ℕ → ℕ
F' x = F x (F-is-total x)


-- Program verification

-- Approach A to establishing correctness: Implement, then verify.

-- The following function has the task of determining whether the two input numbers are equal.
eq? : ℕ → ℕ → Bool
eq? zero     zero     = true
eq? zero     (succ y) = false
eq? (succ x) zero     = false
eq? (succ x) (succ y) = eq? x y

open import Padova2025.ProvingBasics.Equality.General

-- "soundness"
eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ zero     zero     p = refl
eq?-correct₁ (succ x) (succ y) p = cong succ (eq?-correct₁ x y p)

-- "completeness"
eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ x y p = {!!}


-- Approach B: Correct by construction
eq?' : (x y : ℕ) → (x ≡ y) ⊎ (¬ (x ≡ y))
eq?' zero     zero     = left refl
eq?' zero     (succ y) = right (λ { () })
eq?' (succ x) zero     = right {!!}
eq?' (succ x) (succ y) with eq?' x y
... | left  p = left (cong succ p)
... | right p = {!!}

eq?'' : (x y : ℕ) → Bool
eq?'' x y with eq?' x y
... | left  p = true
... | right q = false