Skip to content

Instantly share code, notes, and snippets.

@clayrat

clayrat/sub-even.agda

Created August 24, 2023 17:47
Show Gist options
  • Save clayrat/7e7e33d72fa2cf19dfe855c90981a41f to your computer and use it in GitHub Desktop.
Save clayrat/7e7e33d72fa2cf19dfe855c90981a41f to your computer and use it in GitHub Desktop.
Download ZIP
Evenness examples from "Subtyping Without Reduction"
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment