Evenness examples from "Subtyping Without Reduction"

sub-even.agda

{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Even where

open import Prelude
open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.Nat.Order.Inductive

private variable
    m n o : ℕ

-- The typical definition of evenness as an inductive family

data isEvenI : ℕ → Type where
  even-zero : isEvenI 0
  even-ss   : isEvenI n → isEvenI (suc (suc n))

-- This is a family of propositions

isPropIsEvenI : is-prop (isEvenI n)
isPropIsEvenI =
  is-prop-η $
  λ where
     even-zero    even-zero  → refl
     (even-ss p) (even-ss q) → ap even-ss (is-prop-β isPropIsEvenI p q)

evenI+ : ∀ n m → isEvenI n → isEvenI m → isEvenI (n + m)
evenI+ .0             y even-zero       q = q
evenI+ .(suc (suc n)) y (even-ss {n} p) q = even-ss (evenI+ n y p q)

{-
  We can easily apply the manual application of our technique to construct
  an alternative representation of isEvenI
-}

data isEven : ℕ → Type where
  even-zero : isEven 0
  even-ss   : isEven n → isEven (suc (suc n))
  even-+    : isEven m → isEven n → isEven (m + n)
  trunc/    : (p q : isEven n) → p ＝ q

isEven-prop : ∀ n → is-prop (isEven n)
isEven-prop n = is-prop-η trunc/

recIsEven : (B : ℕ → Type) → (∀ n → is-prop (B n)) →
            B 0 → (∀ n → B n → B (suc (suc n))) →
            (∀ m n → B m → B n → B (m + n)) →
            isEven n → B n
recIsEven B isPropB B0 Bs B+  even-zero     = B0
recIsEven B isPropB B0 Bs B+ (even-ss p)    =
  Bs _ (recIsEven B isPropB B0 Bs B+ p)
recIsEven B isPropB B0 Bs B+ (even-+ p q)   =
  B+ _ _ (recIsEven B isPropB B0 Bs B+ p)
         (recIsEven B isPropB B0 Bs B+ q)
recIsEven B isPropB B0 Bs B+ (trunc/ p q i) =
  is-prop-β (isPropB _) (recIsEven B isPropB B0 Bs B+ p)
                        (recIsEven B isPropB B0 Bs B+ q) i

isEven-correct : ∀ n → isEven n → isEvenI n
isEven-correct n =
  recIsEven isEvenI (λ x → isPropIsEvenI)
    even-zero
    (λ m → even-ss)
    evenI+

isEven-pred : isEven (suc (suc n)) → isEven n
isEven-pred = recIsEven B isPropB tt Bs B+
  where
    B : ℕ → Type
    B 0 = ⊤
    B 1 = ⊥
    B (suc (suc n)) = isEven n

    isPropB : ∀ n → is-prop (B n)
    isPropB 0 = ⊤-is-of-hlevel _
    isPropB 1 = ⊥-is-of-hlevel _
    isPropB (suc (suc n)) = is-prop-η trunc/

    Bs : ∀ n → B n → isEven n
    Bs zero _ = even-zero
    Bs (suc (suc n)) = even-ss

    B+ : ∀ m n → B m → B n → B (m + n)
    B+ zero n x y = y
    B+ (suc (suc m)) n x y = even-+ x (Bs n y)

¬isEven1 : isEven 1 → ⊥
¬isEven1 = recIsEven B isPropB tt (λ _ _ → tt) B+
  where
    B : ℕ → Type
    B 0 = ⊤
    B 1 = ⊥
    B (suc (suc m)) = ⊤

    isPropB : ∀ n → is-prop (B n)
    isPropB 0             = ⊤-is-of-hlevel _
    isPropB 1             = ⊥-is-of-hlevel _
    isPropB (suc (suc n)) = ⊤-is-of-hlevel _

    B+ : ∀ m n → B m → B n → B (m + n)
    B+ zero n x y = y
    B+ (suc (suc m)) n x y = tt

{-
  In order to construct a div2 function on isEven, we first define the following
  family of propositions.

  isMultipleOf m n is the type witnessing that n is a multiple of m

-}

isMultipleOf : ℕ → ℕ → Type
isMultipleOf m n = Σ[ k ꞉ ℕ ] m · k ＝ n

isPropIsMultipleOf₁ : ∀ m n → is-prop (isMultipleOf (suc m) n)
isPropIsMultipleOf₁ m n = is-prop-η (λ where
  (k , p) (l , q) → Σ-prop-path (λ x → hlevel!)
                                (·-inj-l (suc m) k l (s≤s z≤) (p ∙ sym q)))

isDiv2 : ℕ → Type
isDiv2 = isMultipleOf 2

isDiv2-ss : ∀ n → isDiv2 n → isDiv2 (suc (suc n))
isDiv2-ss _ (m , p) = suc m , cong suc (+-sucr m (m + 0) ∙ cong suc p)

¬isDiv2-1 : isDiv2 1 → ⊥
¬isDiv2-1 (zero , p) = absurd (suc≠zero (sym p))
¬isDiv2-1 (suc m , p) = absurd (suc≠zero (sym (+-sucr _ _) ∙ suc-inj p))

isDiv2-pred : ∀ n → isDiv2 (suc (suc n)) → isDiv2 n
isDiv2-pred n (0 , p) = absurd (suc≠zero (sym p))
isDiv2-pred n (suc m , p) = m , cong pred (sym (+-sucr m (m + 0)) ∙ cong pred p)

isDiv2-+ : ∀ m n → isDiv2 m → isDiv2 n → isDiv2 (m + n)
isDiv2-+ 0             n p q = q
isDiv2-+ 1             n p   = absurd (¬isDiv2-1 p)
isDiv2-+ (suc (suc m)) n p q = isDiv2-ss (m + n) (isDiv2-+ m n (isDiv2-pred m p) q)

isEven→isDiv2 : isEven n → isDiv2 n
isEven→isDiv2 =
  recIsEven isDiv2 (isPropIsMultipleOf₁ 1)
    (zero , refl) isDiv2-ss isDiv2-+

-- approach 1
div2' : isEven n → ℕ
div2' = fst ∘ isEven→isDiv2

-- approach 2/3
div2 : isEven n → ℕ
div2 {n = 0}           p = 0
div2 {n = 1}           p = absurd (¬isEven1 p)
div2 {n = suc (suc n)} p = suc (div2 (isEven-pred p))

--- induction-recursion

data Even : 𝒰 0ℓ
toN : Even → ℕ

data Even where
  EZ  : Even
  E2  : Even → Even
  E+  : Even → Even → Even
  Eeq : (x y : Even) → toN x ＝ toN y → x ＝ y  -- injectivity of toN

toN EZ = 0
toN (E2 x) = suc (suc (toN x))
toN (E+ x y) = toN x + toN y
toN (Eeq x y p i) = p i

toN-emb : is-embedding toN
toN-emb n =
  is-prop-η $
  λ where
     (p , pp) (q , qq) → Σ-prop-path! (Eeq p q (pp ∙ sym qq))

elimEven : {ℓ : Level}
         → (P : ℕ → 𝒰 ℓ)
         → ((n : ℕ) → is-prop (P n))
         → P 0
         → ((n : ℕ) → P n → P (suc (suc n)))
         → ((m n : ℕ) → P m → P n → P (m + n))
         → (e : Even) → P (toN e)
elimEven P Pprop P0 P2 P+ EZ              = P0
elimEven P Pprop P0 P2 P+ (E2 e)          = P2 (toN e) (elimEven P Pprop P0 P2 P+ e)
elimEven P Pprop P0 P2 P+ (E+ e1 e2)      =
  P+ (toN e1) (toN e2)
     (elimEven P Pprop P0 P2 P+ e1)
     (elimEven P Pprop P0 P2 P+ e2)
elimEven P Pprop P0 P2 P+ (Eeq e1 e2 x i) =
  to-pathP {A = λ i → P (x i)}
           {x = elimEven P Pprop P0 P2 P+ e1}
           {y = elimEven P Pprop P0 P2 P+ e2}
           (is-prop-β (Pprop (toN e2)) _ _) i

Even-isEven : (e : Even) → isEven (toN e)
Even-isEven = elimEven isEven isEven-prop even-zero (λ n → even-ss) λ m n → even-+

isEven-fib-Even : ∀ n → isEven n → fibre toN n
isEven-fib-Even n =
  recIsEven (fibre toN) toN-emb
    (EZ , refl)
    (λ where m (e , eq) → E2 e , ap (suc ∘ suc) eq)
    (λ where m p (e1 , eq1) (e2 , eq2) → E+ e1 e2 , ap₂ (_+_) eq1 eq2)

isEven≅fib-Even : ∀ n → isEven n ≅ fibre toN n
isEven≅fib-Even n =
    isEven-fib-Even n
  , iso (λ where (e , eq) → subst isEven eq (Even-isEven e))
        (λ f → is-prop-β (toN-emb n) _ _)
        (λ e → trunc/ _ e)

isEven-Even : ∀ n → isEven n → Even
isEven-Even n ie with (isEven-fib-Even n ie)
... | ie , eq = ie

Even-ΣisEven : (e : Even) → Σ ℕ isEven
Even-ΣisEven e = toN e , Even-isEven e

left : (e : Even) → isEven-Even (toN e) (Even-isEven e) ＝ e
left e = Eeq _ e (go e)
  where
  go : ∀ e → toN (isEven-Even (toN e) (Even-isEven e)) ＝ toN e
  go e with (isEven-fib-Even (toN e) (Even-isEven e))
  ... | e1 , eq = eq

right : (n : ℕ) → (ie : isEven n) → Even-ΣisEven (isEven-Even n ie) ＝ (n , ie)
right n ie with (isEven-fib-Even n ie)
... | e , eq = Σ-prop-path isEven-prop eq

Even≅ΣisEven : Even ≅ Σ ℕ isEven
Even≅ΣisEven =
    Even-ΣisEven
  , iso (λ where (n , ie) → isEven-Even n ie)
        (λ where (n , ie) → right n ie)
        left