Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

open import foundations.BasicTypes using (Level)

module foundations.Nat (ℓ : Level)
  where
  open import foundations.Core
  open import foundations.NaturalsType

  module dec-< where
    open ℕ-ordering ℓ
    _?<_ : (Decidable {A = ℕ}{B = ℕ} _<_)
    zero ?< zero     = no (λ z → z)
    zero ?< succ b   = yes ∗
    succ a ?< zero   = no (λ z → z)
    succ a ?< succ b = a ?< b

  open ℕ-ordering ℓ public

  <-succ
    : (k : ℕ)
    → k < succ k

  <-succ zero     = unit
  <-succ (succ k) = <-succ k

  <-inj
    : ∀ {n m : ℕ}
    → (succ m < n)
    → m < n

  <-inj {zero} {zero} p = p
  <-inj {zero} {succ m} p = p
  <-inj {succ n} {zero} p = ★
  <-inj {succ n} {succ m} p = <-inj {n}{m} p

  positive-is-suc-of
    : ∀ (n : ℕ)
    → n > 
    → ∑[ k ∶ ℕ ] (succ k ≡ n)
  positive-is-suc-of zero ()
  positive-is-suc-of (succ k) ∗ = k , idp

  mono-succ
    : ∀ {n m : ℕ}
    → n < m
    → succ n < succ m

  mono-succ {n}{m} x = x

  succ-<-remove
    : ∀ {n m}
    → succ n < succ m
    → n < m

  succ-<-remove {} {succ m} ∗ = ∗
  succ-<-remove {succ n} {succ m} p
   = mono-succ {n}{m} (succ-<-remove {n}{m} p)

  <-trans
    : ∀ {x y z : ℕ}
    → x < y → y < z
    → x < z

  <-trans {zero} {succ y} {succ z} x<y y<z = ∗
  <-trans {succ x} {succ y} {succ z} x<y y<z
    = mono-succ {x}{z} (<-trans {x}{y}{z} (succ-<-remove {x}{y} x<y) (succ-<-remove {y}{z} y<z))

  +>0
    : ∀ {x y : ℕ}
    →  < x
    →  < (x +ₙ y)

  +>0 {succ x} {zero} 0<x = ∗
  +>0 {succ x} {succ y} 0<x = ∗

  n⁺<k→n<k
    : ∀ {n k : ℕ}
    → succ n < k
    → n < k

  n⁺<k→n<k {zero} {zero} m = m
  n⁺<k→n<k {zero} {succ k} m = ★
  n⁺<k→n<k {succ n} {zero} ()
  n⁺<k→n<k {succ n} {succ k} m = n⁺<k→n<k {n}{k} m

  <-prop
    : {n m : ℕ}
    → (p1 p2 : m < n)
    → p1 ≡ p2

  <-prop {zero} {zero} () p2
  <-prop {zero} {succ m} () p2
  <-prop {succ n} {zero} unit unit = idp
  <-prop {succ n} {succ m} p1 p2 = <-prop {n}{m} p1 p2

  n=m-is-prop
    : {n m : ℕ}
    → isProp (n ≡ m)

  n=m-is-prop {n}{m} p q = nat-is-set n m p q

  n=m-is-set
    : {n m : ℕ}
    → isSet (n ≡ m)

  n=m-is-set = prop-is-set n=m-is-prop

  pre : ℕ → ℕ
  pre zero     = zero
  pre (succ n) = n

  <and=→⊥
    : ∀ {m : ℕ}
    → zero < m
    → (zero ≡ m)
    → ⊥ ℓ

  <and=→⊥ {zero} ()
  <and=→⊥ {succ m} x ()

  succ-n>0
    : {n : ℕ}
    →  < succ n

  succ-n>0 {}     = unit
  succ-n>0 {succ n} = unit

  n<0
    : ∀ {ℓ} → {n : ℕ}
    → (n < ) → ⊥ ℓ

  n<0 {ℓ = ℓ} {zero} ()
  n<0 {ℓ = ℓ} {succ n} ()

  n≠0
    : ∀ {n : ℕ}
    → ¬ (n ≡ )
    →  < n

  n≠0 {zero} p = ⊥-elim (p idp)
  n≠0 {succ n} p = unit

  trichotomy
    : (x y : ℕ)
    → ((x ≡ y) + (x < y)) + (y < x)

  trichotomy zero zero = inl (inl idp)
  trichotomy zero (succ y) = inl (inr unit)
  trichotomy (succ x) zero = inr unit
  trichotomy (succ x) (succ y) with trichotomy x y
  ... | inl (inl p) = inl (inl (ap succ p))
  ... | inl (inr p) = inl (inr (mono-succ {x}{y} p))
  ... | inr p = inr $ mono-succ {y}{x} p

  n<n→⊥
    : ∀ {n : ℕ}
    → ¬ (n < n)

  n<n→⊥ {succ n} p = n<n→⊥ {n} (succ-<-remove {n}{n} p)

  k<1→k≡0
    : ∀ {k : ℕ}
    → k < 
    → k ≡ 

  k<1→k≡0 {} p = idp
  k<1→k≡0 {succ } p = ⊥-elim $ n<n→⊥ {n = } p
  k<1→k≡0 {succ (succ k)} p = ⊥-elim (n<0 {lzero} {n = } (succ-<-remove {n = succ k}{m = } p))

  <s-to-<=
    : ∀ p q → p < succ q
    → (p ≡ q) + (p < q)
  <s-to-<= zero zero ∗ = inl idp
  <s-to-<= zero (succ q) ∗ = inr ∗
  <s-to-<= (succ p) zero p<q+ = inl (k<1→k≡0 p<q+)
  <s-to-<= (succ p) (succ q) p<q+
    with <s-to-<= p q (succ-<-remove {n = p} p<q+)
  ... | inl idp = inl idp
  ... | inr x = inr x

  <-=-→⊥
    : ∀ {k n : ℕ}
    → k < n
    → k ≡ n
    → ⊥ ℓ

  <-=-→⊥ {} {.} () idp
  <-=-→⊥ {succ k} {.(succ k)} p idp = <-=-→⊥ {k = k}{n = k} p idp

  module NatDecidable where
    nat-succ-inj
      : ∀ {n m : ℕ}
      → succ n ≡ succ m
      → n ≡ m
    nat-succ-inj {zero} {zero} = λ _ → idp
    nat-succ-inj {} {succ m} ()
    nat-succ-inj {succ n} {zero} ()
    nat-succ-inj {succ n} {succ .n} idp = idp

    _≟nat_ : Decidable {A = ℕ} _≡_
    zero ≟nat zero = yes idp
    zero ≟nat succ b = no (λ ())
    succ a ≟nat zero = no (λ ())
    succ a ≟nat succ b with a ≟nat b
    (succ a ≟nat succ b) | yes p = yes (ap succ p)
    (succ a ≟nat succ b) | no ¬p = no λ r → (¬p (nat-succ-inj r))

  open NatDecidable public

  <-suc-suc<
    : ∀ {ℓ}{n k : ℕ}
    → n < k
    → ((k ≡ succ n) → ⊥ ℓ)
    → succ n < k

  <-suc-suc<  {ℓ = ℓ} {zero} {succ zero} ★ ¬p = ⊥-elim (¬p idp)
  <-suc-suc<  {ℓ = ℓ}{zero} {succ (succ k)} ★ ¬p = ★
  <-suc-suc< {ℓ = ℓ} {succ n} {succ k} n<k ¬p = <-suc-suc< {ℓ}{n}{k} n<k λ q → ¬p (ap succ q)

  k≠0-k>0
      : ∀ {ℓ}{k : ℕ}
      →  ((k ≡ ) → ⊥ ℓ)
      →  < k

  k≠0-k>0 {ℓ = ℓ}{zero} ¬p = ⊥-elim (¬p idp)
  k≠0-k>0 {ℓ = ℓ} {succ p} ¬p = ★

  the-obvious
    : {n : ℕ}
    → succ n ≡ n → ⊥ ℓ

  the-obvious {} ()
  the-obvious {succ n} ()

  n⁺⁺≠n
    : {n : ℕ}
    → succ (succ n) ≡ n → ⊥ ℓ

  n⁺⁺≠n {} ()
  n⁺⁺≠n {succ n} ()

  n+1≡n⁺
    : {n : ℕ}
    → n +ₙ  ≡ succ n

  n+1≡n⁺ {} = idp
  n+1≡n⁺ {succ n} = ap succ (n+1≡n⁺{n})

  n+1≡m→m=n⁺
    : {n m : ℕ}
    → (n +ₙ ) ≡ m
    → m ≡ succ n

  n+1≡m→m=n⁺ {n} {.(plus n )} idp = n+1≡n⁺{n}

  n+1+1≡n→⊥
    : {n : ℕ}
    → ((n +ₙ ) +ₙ  ≡ n) → ⊥ ℓ

  n+1+1≡n→⊥ {succ n} q rewrite n+1≡n⁺{n} | ! (n+1≡n⁺ {n}) = n⁺⁺≠n {plus n } q

  n+1≡mANDn≡m+1→⊥
    : {n m : ℕ}
    → (n +ₙ  ≡ m)
    → (n ≡ m +ₙ )
    → ⊥ ℓ

  n+1≡mANDn≡m+1→⊥ {n} {.(plus n )} idp q = n+1+1≡n→⊥ {n} (sym q)

  _≠ℕ_ : ∀ (n m : ℕ) → Type ℓ
  n ≠ℕ m = (n ≡ m) → ⊥ ℓ

  <k→<k⁺
    : ∀ {n k : ℕ}
    → n < k
    → n < succ k
  <k→<k⁺ {zero} {succ k} x = ★
  <k→<k⁺ {succ n} {succ k} x = <k→<k⁺ {n}{k} x

  ≤-to-<
    : {p q : ℕ}
    → p ≤ q
    → p < succ q
  ≤-to-< {p = p} (inl p<q) = <k→<k⁺ {n = p} p<q
  ≤-to-< {p = p} (inr idp) = <-succ p

  minus : (n k : ℕ) → (k < n) → ℕ
  minus   ()
  minus  (succ k) ()
  minus (succ n)  k< = succ n
  minus (succ n) (succ k) k< = succ (minus n k k<)

  +≡-to-<
    : ∀ {k n : ℕ}
    → (sol : ∑ ℕ (\x → k +ₙ x ≡ n))
    → ( < π₁ sol) → k < n

  +≡-to-< {} {succ n} (succ x , p) ∗ = ∗
  +≡-to-< {succ k} {succ n} (succ x , p) ∗ = mono-succ {k}{n} IH
    where
    IH : k < n
    IH = +≡-to-< {k}{n} (succ x , succ-inj p) ∗

  to-reach>0
    : ∀ {k x n : ℕ}
    → k < n
    → k +ₙ x ≡ n
    →  < x

  to-reach>0 {zero} {succ x} {succ n} k<n k+x≡n = ∗
  to-reach>0 {succ k} {zero} {succ n} k<n k+x≡n
    = ⊥-elim (<-=-→⊥ k<n (! plus-runit (succ k) · k+x≡n))
  to-reach>0 {succ k} {succ x} {succ n} k<n k+x≡n = ∗

  find-x-to-<
    : ∀ {k n : ℕ}
    → k < n
    → ∑ ℕ (\x → (k +ₙ x ≡ n) × ( < x))

  find-x-to-< {} {succ n} ∗ = succ n , (idp , ∗)
  find-x-to-< {succ k} {succ n} k<
    with find-x-to-< {k = k}{n = succ n} (<-inj {n = succ n}{m = k} k<)
  ... |  , p , 0<sol    rewrite plus-runit k
      = ⊥-elim (<-=-→⊥ (<k→<k⁺ {n = k} k<)  p)
  ... | succ x , p , 0<sol rewrite ! p | plus-comm k (succ x)
      = x , (ap succ (plus-comm k x) , to-reach>0 {k}{x}{n}  k< (succ-inj (ap succ (plus-comm k x) · p)))

  unique-solution-find-x-to-<
    : ∀ {k n : ℕ}
    → k < n
    → (x : ℕ) → (k +ₙ x ≡ n)
    → (x' : ℕ) → (k +ₙ x' ≡ n)
    → x ≡ x'

  unique-solution-find-x-to-< {k = k} k< x p1 x' p2 = +-inj k (p1 · ! p2)

  {-
  _^-ℕ_ : ℕ → ℕ → ℕ
  0 ^-ℕ 0      = 1
  succ a ^-ℕ 0 = 1
  zero ^-ℕ succ b = 0
  succ a ^-ℕ succ b = {!!}
  -}

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides