Decidable types in elementary number theory

module elementary-number-theory.decidable-types where
Imports
open import foundation.decidable-dependent-pair-types public

open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers
open import elementary-number-theory.upper-bounds-natural-numbers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.functions
open import foundation.unit-type
open import foundation.universe-levels

Idea

We describe conditions under which dependent sums and dependent products are decidable.

Properties

Given a family of decidable types and a number m such that Σ (m ≤ x), P x is decidable, then Σ ℕ P is decidable.

is-decidable-Σ-ℕ :
  {l : Level} (m : ) (P :   UU l) (d : is-decidable-fam P) 
  is-decidable (Σ   x  (leq-ℕ m x) × (P x)))  is-decidable (Σ  P)
is-decidable-Σ-ℕ m P d (inl (pair x (pair l p))) = inl (pair x p)
is-decidable-Σ-ℕ zero-ℕ P d (inr f) =
  inr  p  f (pair (pr1 p) (pair star (pr2 p))))
is-decidable-Σ-ℕ (succ-ℕ m) P d (inr f) with d zero-ℕ
... | inl p = inl (pair zero-ℕ p)
... | inr g with
  is-decidable-Σ-ℕ m
    ( P  succ-ℕ)
    ( λ x  d (succ-ℕ x))
    ( inr  p  f (pair (succ-ℕ (pr1 p)) (pr2 p))))
... | inl p = inl (pair (succ-ℕ (pr1 p)) (pr2 p))
... | inr h = inr α
  where
  α : Σ  P  empty
  α (pair zero-ℕ p) = g p
  α (pair (succ-ℕ x) p) = h (pair x p)

Bounded sums of decidable families over ℕ are decidable

is-decidable-bounded-Σ-ℕ :
  {l1 l2 : Level} (m : ) (P :   UU l1) (Q :   UU l2)
  (dP : is-decidable-fam P) (dQ : is-decidable-fam Q)
  (H : is-upper-bound-ℕ P m)  is-decidable (Σ   x  (P x) × (Q x)))
is-decidable-bounded-Σ-ℕ m P Q dP dQ H =
  is-decidable-Σ-ℕ
    ( succ-ℕ m)
    ( λ x  (P x) × (Q x))
    ( λ x  is-decidable-prod (dP x) (dQ x))
    ( inr
      ( λ p 
        contradiction-leq-ℕ
          ( pr1 p)
          ( m)
          ( H (pr1 p) (pr1 (pr2 (pr2 p))))
          ( pr1 (pr2 p))))

is-decidable-bounded-Σ-ℕ' :
  {l : Level} (m : ) (P :   UU l) (d : is-decidable-fam P) 
  is-decidable (Σ   x  (leq-ℕ x m) × (P x)))
is-decidable-bounded-Σ-ℕ' m P d =
  is-decidable-bounded-Σ-ℕ m
    ( λ x  leq-ℕ x m)
    ( P)
    ( λ x  is-decidable-leq-ℕ x m)
    ( d)
    ( λ x  id)

Strictly bounded sums of decidable families over ℕ are decidable

is-decidable-strictly-bounded-Σ-ℕ :
  {l1 l2 : Level} (m : ) (P :   UU l1) (Q :   UU l2)
  (dP : is-decidable-fam P) (dQ : is-decidable-fam Q)
  (H : is-strict-upper-bound-ℕ P m) 
  is-decidable (Σ   x  (P x) × (Q x)))
is-decidable-strictly-bounded-Σ-ℕ m P Q dP dQ H =
  is-decidable-bounded-Σ-ℕ m P Q dP dQ
    ( is-upper-bound-is-strict-upper-bound-ℕ P m H)

is-decidable-strictly-bounded-Σ-ℕ' :
  {l : Level} (m : ) (P :   UU l) (d : is-decidable-fam P) 
  is-decidable (Σ   x  (le-ℕ x m) × (P x)))
is-decidable-strictly-bounded-Σ-ℕ' m P d =
  is-decidable-strictly-bounded-Σ-ℕ m
    ( λ x  le-ℕ x m)
    ( P)
    ( λ x  is-decidable-le-ℕ x m)
    ( d)
    ( λ x  id)

Given a family P of decidable types over ℕ and a number m such that Π (m ≤ x), P x, the type Π ℕ P is decidable

is-decidable-Π-ℕ :
  {l : Level} (P :   UU l) (d : is-decidable-fam P) (m : ) 
  is-decidable ((x : )  (leq-ℕ m x)  P x)  is-decidable ((x : )  P x)
is-decidable-Π-ℕ P d zero-ℕ (inr nH) = inr  f  nH  x y  f x))
is-decidable-Π-ℕ P d zero-ℕ (inl H) = inl  x  H x (leq-zero-ℕ x))
is-decidable-Π-ℕ P d (succ-ℕ m) (inr nH) = inr  f  nH  x y  f x))
is-decidable-Π-ℕ P d (succ-ℕ m) (inl H) with d zero-ℕ
... | inr np = inr  f  np (f zero-ℕ))
... | inl p with
  is-decidable-Π-ℕ
    ( λ x  P (succ-ℕ x))
    ( λ x  d (succ-ℕ x))
    ( m)
    ( inl  x  H (succ-ℕ x)))
... | inl g = inl (ind-ℕ p  x y  g x))
... | inr ng = inr  f  ng  x  f (succ-ℕ x)))

Bounded dependent products of decidable types are decidable

is-decidable-bounded-Π-ℕ :
  {l1 l2 : Level} (P :   UU l1) (Q :   UU l2) (dP : is-decidable-fam P) 
  (dQ : is-decidable-fam Q) (m : ) (H : is-upper-bound-ℕ P m) 
  is-decidable ((x : )  P x  Q x)
is-decidable-bounded-Π-ℕ P Q dP dQ m H =
  is-decidable-Π-ℕ
    ( λ x  P x  Q x)
    ( λ x  is-decidable-function-type (dP x) (dQ x))
    ( succ-ℕ m)
    ( inl  x l p  ex-falso (contradiction-leq-ℕ x m (H x p) l)))

is-decidable-bounded-Π-ℕ' :
  {l : Level} (P :   UU l) (d : is-decidable-fam P) (m : ) 
  is-decidable ((x : )  (leq-ℕ x m)  P x)
is-decidable-bounded-Π-ℕ' P d m =
  is-decidable-bounded-Π-ℕ
    ( λ x  leq-ℕ x m)
    ( P)
    ( λ x  is-decidable-leq-ℕ x m)
    ( d)
    ( m)
    ( λ x  id)

Strictly bounded dependent products of decidable types are decidable

is-decidable-strictly-bounded-Π-ℕ :
  {l1 l2 : Level} (P :   UU l1) (Q :   UU l2) (dP : is-decidable-fam P) 
  (dQ : is-decidable-fam Q) (m : ) (H : is-strict-upper-bound-ℕ P m) 
  is-decidable ((x : )  P x  Q x)
is-decidable-strictly-bounded-Π-ℕ P Q dP dQ m H =
  is-decidable-bounded-Π-ℕ P Q dP dQ m  x p  leq-le-ℕ x m (H x p))

is-decidable-strictly-bounded-Π-ℕ' :
  {l : Level} (P :   UU l) (d : is-decidable-fam P) (m : ) 
  is-decidable ((x : )  le-ℕ x m  P x)
is-decidable-strictly-bounded-Π-ℕ' P d m =
  is-decidable-strictly-bounded-Π-ℕ
    ( λ x  le-ℕ x m)
    ( P)
    ( λ x  is-decidable-le-ℕ x m)
    ( d)
    ( m)
    ( λ x  id)