open import Atom
module Computability (atoms : χ-atoms) where
open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (_∘_; Decidable)
open import Tactic.By.Propositional
open import Bool equality-with-J
open import Bijection equality-with-J using (_↔_)
open import Double-negation equality-with-J
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J as Eq using (_≃_)
open import Excluded-middle equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
as Trunc
open import Monad equality-with-J
open import Chi atoms
open import Coding atoms
import Coding.Instances atoms as Dummy
open import Deterministic atoms
open import Free-variables atoms
open import Propositional atoms
open import Reasoning atoms
open import Values atoms
record _⇀_ {a b} (A : Type a) (B : Type b) : Type (lsuc (a ⊔ b)) where
infix 4 _[_]=_
field
_[_]=_ : A → B → Type (a ⊔ b)
deterministic : ∀ {a b₁ b₂} → _[_]=_ a b₁ → _[_]=_ a b₂ → b₁ ≡ b₂
propositional : ∀ {a b} → Is-proposition (_[_]=_ a b)
∃[]=-propositional :
∀ {a} →
Is-proposition (∃ (_[_]=_ a))
∃[]=-propositional (b₁ , [a]=b₁) (b₂ , [a]=b₂) =
Σ-≡,≡→≡ (deterministic [a]=b₁ [a]=b₂)
(propositional _ _)
open _⇀_ public using (_[_]=_)
semantics : Closed-exp ⇀ Closed-exp
semantics = record
{ _[_]=_ = _⇓_ on proj₁
; deterministic = λ e⇓v₁ e⇓v₂ →
closed-equal-if-expressions-equal (⇓-deterministic e⇓v₁ e⇓v₂)
; propositional = ⇓-propositional
}
infixr 9 _∘_
_∘_ : ∀ {ℓ c} {A B : Type ℓ} {C : Type c} →
B ⇀ C → A ⇀ B → A ⇀ C
f ∘ g = record
{ _[_]=_ = λ a c → ∃ λ b → g [ a ]= b × f [ b ]= c
; deterministic = λ where
(b₁ , g[a]=b₁ , f[b₁]=c₁) (b₂ , g[a]=b₂ , f[b₂]=c₂) →
_⇀_.deterministic f
(subst (f [_]= _) (_⇀_.deterministic g g[a]=b₁ g[a]=b₂) f[b₁]=c₁)
f[b₂]=c₂
; propositional = λ {a c} → $⟨ Σ-closure 1 (_⇀_.∃[]=-propositional g) (λ _ → _⇀_.propositional f) ⟩
Is-proposition (∃ λ (p : ∃ λ b → g [ a ]= b) → f [ proj₁ p ]= c) ↝⟨ H-level.respects-surjection (_↔_.surjection $ inverse Σ-assoc) 1 ⟩□
Is-proposition (∃ λ b → g [ a ]= b × f [ b ]= c) □
}
as-partial : ∀ {a b} {A : Type a} {B : Type b} →
Is-set B → (A → B) → A ⇀ B
as-partial {ℓa} B-set f = record
{ _[_]=_ = λ a b → ↑ ℓa (f a ≡ b)
; deterministic = λ {a b₁ b₂} fa≡b₁ fa≡b₂ →
b₁ ≡⟨ sym (lower fa≡b₁) ⟩
f a ≡⟨ lower fa≡b₂ ⟩∎
b₂ ∎
; propositional = ↑-closure 1 (+⇒≡ {n = 1} B-set)
}
pre-apply : ∀ {ℓ c} {A B : Type ℓ} {C : Type c}
(f : B ⇀ C) {g : A → B} {a c}
(B-set : Is-set B) →
f [ g a ]= c → f ∘ as-partial B-set g [ a ]= c
pre-apply _ _ f[ga]=b = _ , lift refl , f[ga]=b
post-apply : ∀ {ℓ c} {A B : Type ℓ} {C : Type c}
{f : B → C} (g : A ⇀ B) {a b}
(C-set : Is-set C) →
g [ a ]= b → as-partial C-set f ∘ g [ a ]= f b
post-apply _ _ g[a]=b = _ , g[a]=b , lift refl
Total : ∀ {a b} {A : Type a} {B : Type b} →
(Type (a ⊔ b) → Type (a ⊔ b)) →
A ⇀ B → Type (a ⊔ b)
Total P f = ∀ a → P (∃ λ b → f [ a ]= b)
Total-propositional :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
{P : Type (a ⊔ b) → Type (a ⊔ b)}
(f : A ⇀ B) →
(∀ {A} → Is-proposition A → Is-proposition (P A)) →
Is-proposition (Total P f)
Total-propositional f pres =
Π-closure ext 1 λ _ →
pres $
_⇀_.∃[]=-propositional f
total-with-∥∥→total :
∀ {a b} {A : Type a} {B : Type b} (f : A ⇀ B) →
Total ∥_∥ f →
Total id f
total-with-∥∥→total f total a =
Trunc.rec
(_⇀_.∃[]=-propositional f)
id
(total a)
Implements :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
(Type (a ⊔ b) → Type (a ⊔ b)) →
Exp → A ⇀ B → Type (a ⊔ b)
Implements P p f =
Closed p
×
(∀ x y → f [ x ]= y → apply p ⌜ x ⌝ ⇓ ⌜ y ⌝)
×
(∀ x y → apply p ⌜ x ⌝ ⇓ y →
P (∃ λ y′ → f [ x ]= y′ × y ≡ ⌜ y′ ⌝))
private
Σ[]=×≡⌜⌝-propositional :
∀ {a b} {A : Type a} {B : Type b} ⦃ rB : Rep B Consts ⦄
{x} {y : Exp}
(p : Exp) (f : A ⇀ B) →
Is-proposition (∃ λ y′ → f [ x ]= y′ × y ≡ ⌜ y′ ⌝)
Σ[]=×≡⌜⌝-propositional {x = x} {y = y} _ f = $⟨ (Σ-closure 1 (_⇀_.∃[]=-propositional f) λ _ → Exp-set) ⟩
Is-proposition (∃ λ ((y′ , _) : ∃ (f [ x ]=_)) → y ≡ ⌜ y′ ⌝) →⟨ H-level-cong _ 1 (inverse Σ-assoc) ⟩□
Is-proposition (∃ λ y′ → f [ x ]= y′ × y ≡ ⌜ y′ ⌝) □
Implements-¬¬≃Implements-id :
∀ {a b} {A : Type a} {B : Type b} {p : Exp}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
Excluded-middle (a ⊔ b) →
(f : A ⇀ B) → Implements ¬¬_ p f ≃ Implements id p f
Implements-¬¬≃Implements-id {p = p} em f =
∃-cong λ _ → ∃-cong λ _ →
∀-cong ext λ x → ∀-cong ext λ y → ∀-cong ext λ _ →
¬¬≃ (Σ[]=×≡⌜⌝-propositional p f)
(Excluded-middle→Double-negation-elimination em) ext
Implements-propositional :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
{P : Type (a ⊔ b) → Type (a ⊔ b)} {p : Exp}
(f : A ⇀ B) →
(∀ {A} → Is-proposition A → Is-proposition (P A)) →
Is-proposition (Implements P p f)
Implements-propositional {p = p} f pres =
×-closure 1 Closed-propositional $
×-closure 1 (Π-closure ext 1 λ _ →
Π-closure ext 1 λ _ →
Π-closure ext 1 λ _ →
⇓-propositional)
(Π-closure ext 1 λ x →
Π-closure ext 1 λ y →
Π-closure ext 1 λ _ →
pres $
Σ[]=×≡⌜⌝-propositional p f)
Computable′ :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
(Type (a ⊔ b) → Type (a ⊔ b)) →
A ⇀ B → Type (a ⊔ b)
Computable′ P f = ∃ λ p → Implements P p f
Computable :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
A ⇀ B → Type (a ⊔ b)
Computable = Computable′ id
Computable′-¬¬≃Computable :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
Excluded-middle (a ⊔ b) →
(f : A ⇀ B) → Computable′ ¬¬_ f ≃ Computable f
Computable′-¬¬≃Computable em f =
∃-cong λ _ → Implements-¬¬≃Implements-id em f
total→almost-computable→computable :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄
(P : Type (a ⊔ b) → Type (a ⊔ b)) →
(∀ {X Y} → (X → Y) → P X → P Y) →
(f : A ⇀ B) →
Total P f →
(∃ λ p →
Closed p
×
(∀ x y → f [ x ]= y → apply p ⌜ x ⌝ ⇓ ⌜ y ⌝)) →
Computable′ P f
total→almost-computable→computable P map f total (p , cl-p , hyp) =
p
, cl-p
, hyp
, λ x y px⇓y →
flip map (total x) λ where
(y′ , f[x]=y′) →
y′ , f[x]=y′ , ⇓-deterministic px⇓y (hyp x y′ f[x]=y′)
Computable″ :
∀ {ℓ} {A B : Type ℓ}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
A ⇀ B → Type ℓ
Computable″ f =
∃ λ (p : Closed-exp) → ∀ a →
∀ q → semantics [ apply-cl p ⌜ a ⌝ ]= q
⇔
as-partial Closed-exp-set ⌜_⌝ ∘ f [ a ]= q
Computable⇔Computable″ :
∀ {ℓ} {A B : Type ℓ} ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
(f : A ⇀ B) →
Computable f ⇔ Computable″ f
Computable⇔Computable″ f = record { to = to; from = from }
where
to : Computable f → Computable″ f
to (p , cl , hyp₁ , hyp₂) =
(p , cl) , λ { a (q , cl-q) → record
{ to = Σ-map id (Σ-map id (lift P.∘
closed-equal-if-expressions-equal P.∘
sym))
P.∘
hyp₂ a q
; from = λ { (b , f[a]=b , ⌜b⌝≡q) →
apply p ⌜ a ⌝ ⇓⟨ hyp₁ a b f[a]=b ⟩
⌜ b ⌝ ≡⟨ cong proj₁ (lower ⌜b⌝≡q) ⟩⟶
q ■⟨ subst Value (cong proj₁ (lower ⌜b⌝≡q)) (rep-value b) ⟩ }
} }
from : Computable″ f → Computable f
from ((p , cl) , hyp) =
p , cl ,
(λ a b f[a]=b →
apply p ⌜ a ⌝ ⇓⟨ _⇔_.from (hyp a ⌜ b ⌝) (post-apply f Closed-exp-set f[a]=b) ⟩■
⌜ b ⌝) ,
λ a q p⌜a⌝⇓q →
let cl-q : Closed q
cl-q = closed⇓closed p⌜a⌝⇓q
(Closed′-closed-under-apply
(Closed→Closed′ cl)
(Closed→Closed′ (rep-closed a)))
in
Σ-map id (Σ-map id (cong proj₁ P.∘ sym P.∘ lower))
(_⇔_.to (hyp a (q , cl-q)) p⌜a⌝⇓q)
Computable‴ :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
A ⇀ B → Type (a ⊔ b)
Computable‴ f =
∃ λ (p : Closed-exp) →
∀ a →
∃ λ b →
apply (proj₁ p) ⌜ a ⌝ ⇓ ⌜ b ⌝
×
f [ a ]= b
Computable‴→Computable :
∀ {a b} {A : Type a} {B : Type b}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
(f : A ⇀ B) →
Computable‴ f → Computable f
Computable‴→Computable f ((p , cl-p) , hyp) =
p
, cl-p
, (λ a b f[a]=b → case hyp a of λ where
(b′ , p⌜a⌝⇓⌜b′⌝ , f[a]=b′) →
apply p ⌜ a ⌝ ⇓⟨ p⌜a⌝⇓⌜b′⌝ ⟩
⌜ b′ ⌝ ≡⟨ by (_⇀_.deterministic f f[a]=b f[a]=b′) ⟩⟶
⌜ b ⌝ ■⟨ rep-value b ⟩)
, (λ a v p⌜a⌝⇓v → case hyp a of λ where
(b , p⌜a⌝⇓⌜b⌝ , f[a]=b) →
b
, f[a]=b
, ⇓-deterministic p⌜a⌝⇓v p⌜a⌝⇓⌜b⌝)
module _ {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d}
⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄
⦃ rC : Rep C Consts ⦄ ⦃ rD : Rep D Consts ⦄ where
Reduction : A ⇀ B → C ⇀ D → Type (a ⊔ b ⊔ c ⊔ d)
Reduction f g = Computable g → Computable f
Reduction→¬Computable→¬Computable :
(f : A ⇀ B) (g : C ⇀ D) →
Reduction f g → ¬ Computable f → ¬ Computable g
Reduction→¬Computable→¬Computable _ _ red ¬f g = ¬f (red g)
as-partial-function-to-Bool₁ :
∀ {a} {A : Type a} → (A → Type a) → A ⇀ Bool
as-partial-function-to-Bool₁ P = record
{ _[_]=_ = λ a b →
(P a → b ≡ true)
×
¬ ¬ P a
; deterministic = λ where
{b₁ = true} {b₂ = true} _ _ → refl
{b₁ = false} {b₂ = false} _ _ → refl
{b₁ = true} {b₂ = false} _ f →
⊥-elim $ proj₂ f (Bool.true≢false P.∘ sym P.∘ proj₁ f)
{b₁ = false} {b₂ = true} f _ →
⊥-elim $ proj₂ f (Bool.true≢false P.∘ sym P.∘ proj₁ f)
; propositional = ×-closure 1
(Π-closure ext 1 λ _ →
Bool-set)
(¬-propositional ext)
}
as-partial-function-to-Bool₂ :
∀ {a} {A : Type a} →
(P : A → Type a) →
(∀ {a} → Is-proposition (P a)) →
A ⇀ Bool
as-partial-function-to-Bool₂ P P-prop = record
{ _[_]=_ = λ a b → P a × b ≡ true
; deterministic = λ { (_ , refl) (_ , refl) → refl }
; propositional = ×-closure 1 P-prop Bool-set
}
partial-to-Bool₂→partial-to-Bool₁ :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
as-partial-function-to-Bool₂ P P-prop [ a ]= b →
as-partial-function-to-Bool₁ P [ a ]= b
partial-to-Bool₂→partial-to-Bool₁
P _ {a = a} {b = b} =
P a × b ≡ true →⟨ (λ (hyp₁ , hyp₂) → P.const hyp₂ , return hyp₁ .run) ⟩□
(P a → b ≡ true) × ¬ ¬ P a □
partial-to-Bool₁→partial-to-Bool₂ :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
as-partial-function-to-Bool₁ P [ a ]= b →
¬¬ as-partial-function-to-Bool₂ P P-prop [ a ]= b
partial-to-Bool₁→partial-to-Bool₂
P P-prop {a = a} {b = b} =
(P a → b ≡ true) × ¬ ¬ P a →⟨ (λ (hyp₁ , hyp₂) →
wrap hyp₂ >>= λ Pa → return (Pa , hyp₁ Pa)) ⟩□
¬¬ (P a × b ≡ true) □
partial-to-Bool₁-computable→partial-to-Bool₂-computable :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) →
Computable′ (λ A → ¬¬ A) (as-partial-function-to-Bool₁ P) →
Computable′ (λ A → ¬¬ A) (as-partial-function-to-Bool₂ P P-prop)
partial-to-Bool₁-computable→partial-to-Bool₂-computable P
P-prop (p , cl , hyp₁ , hyp₂) =
p
, cl
, (λ a b →
as-partial-function-to-Bool₂ P P-prop [ a ]= b →⟨ partial-to-Bool₂→partial-to-Bool₁ P P-prop ⟩
as-partial-function-to-Bool₁ P [ a ]= b →⟨ hyp₁ a b ⟩□
apply p ⌜ a ⌝ ⇓ ⌜ b ⌝ □)
, (λ a b →
apply p ⌜ a ⌝ ⇓ b →⟨ hyp₂ a b ⟩
¬¬ (∃ λ b′ →
as-partial-function-to-Bool₁ P [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) →⟨ _>>= (λ (b′ , =b′ , ≡⌜b′⌝) →
partial-to-Bool₁→partial-to-Bool₂ P P-prop =b′ >>= λ =b′ →
return (b′ , =b′ , ≡⌜b′⌝)) ⟩□
¬¬ (∃ λ b′ →
as-partial-function-to-Bool₂ P P-prop [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) □)
partial-to-Bool₂-computable→partial-to-Bool₁-computable :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
Excluded-middle a →
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) →
Computable (as-partial-function-to-Bool₂ P P-prop) →
Computable (as-partial-function-to-Bool₁ P)
partial-to-Bool₂-computable→partial-to-Bool₁-computable
em P P-prop (p , cl , hyp₁ , hyp₂) =
p
, cl
, (λ a b →
as-partial-function-to-Bool₁ P [ a ]= b →⟨ partial-to-Bool₁→partial-to-Bool₂ P P-prop ⟩
¬¬ as-partial-function-to-Bool₂ P P-prop [ a ]= b →⟨ Excluded-middle→Double-negation-elimination em $
×-closure 1 P-prop Bool-set ⟩
as-partial-function-to-Bool₂ P P-prop [ a ]= b →⟨ hyp₁ a b ⟩□
apply p ⌜ a ⌝ ⇓ ⌜ b ⌝ □)
, (λ a b →
apply p ⌜ a ⌝ ⇓ b →⟨ hyp₂ a b ⟩
(∃ λ b′ →
as-partial-function-to-Bool₂ P P-prop [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) →⟨ Σ-map id (Σ-map (partial-to-Bool₂→partial-to-Bool₁ P P-prop) id) ⟩□
(∃ λ b′ →
as-partial-function-to-Bool₁ P [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) □)
_→Bool : ∀ {ℓ} → Type ℓ → Type (lsuc ℓ)
A →Bool = ∃ λ (f : A ⇀ Bool) → Total (λ A → ¬¬ A) f
as-function-to-Bool₁ : ∀ {a} {A : Type a} → (A → Type a) → A →Bool
as-function-to-Bool₁ P =
(record
{ _[_]=_ = λ a b →
(P a → b ≡ true)
×
(¬ P a → b ≡ false)
; deterministic = λ where
{b₁ = true} {b₂ = true} _ _ → refl
{b₁ = false} {b₂ = false} _ _ → refl
{b₁ = true} {b₂ = false} f₁ f₂ →
proj₂ f₁ (Bool.true≢false P.∘ sym P.∘ proj₁ f₂)
{b₁ = false} {b₂ = true} f₁ f₂ →
sym (proj₂ f₂ (Bool.true≢false P.∘ sym P.∘ proj₁ f₁))
; propositional = ×-closure 1
(Π-closure ext 1 λ _ →
Bool-set)
(Π-closure ext 1 λ _ →
Bool-set)
})
, λ a →
[ (λ p → true , (λ _ → refl) , ⊥-elim P.∘ (_$ p))
, (λ ¬p → false , ⊥-elim P.∘ ¬p , (λ _ → refl))
] ⟨$⟩ excluded-middle
as-function-to-Bool₂ :
∀ {a} {A : Type a} →
(P : A → Type a) →
(∀ {a} → Is-proposition (P a)) →
A →Bool
as-function-to-Bool₂ P P-prop =
(record
{ _[_]=_ = λ a b →
P a × b ≡ true
⊎
¬ P a × b ≡ false
; deterministic = λ where
(inj₁ (_ , refl)) (inj₁ (_ , refl)) → refl
(inj₁ (p , _)) (inj₂ (¬p , _)) → ⊥-elim (¬p p)
(inj₂ (¬p , _)) (inj₁ (p , _)) → ⊥-elim (¬p p)
(inj₂ (_ , refl)) (inj₂ (_ , refl)) → refl
; propositional = λ {_ b} →
⊎-closure-propositional
(λ { (_ , b≡true) (_ , b≡false) →
Bool.true≢false (
true ≡⟨ sym b≡true ⟩
b ≡⟨ b≡false ⟩∎
false ∎) })
(×-closure 1 P-prop Bool-set)
(×-closure 1 (¬-propositional ext) Bool-set)
})
, λ a →
[ (λ p → true , inj₁ (p , refl))
, (λ ¬p → false , inj₂ (¬p , refl))
] ⟨$⟩ excluded-middle
to-Bool₂→to-Bool₁ :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b →
proj₁ (as-function-to-Bool₁ P) [ a ]= b
to-Bool₂→to-Bool₁ _ _ = λ where
(inj₁ (Pa , refl)) → (λ _ → refl) , ⊥-elim P.∘ (_$ Pa)
(inj₂ (¬Pa , refl)) → ⊥-elim P.∘ ¬Pa , λ _ → refl
to-Bool₁→to-Bool₂ :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
proj₁ (as-function-to-Bool₁ P) [ a ]= b →
¬¬ proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b
to-Bool₁→to-Bool₂ _ _ (Pa→b≡true , ¬Pa→b≡false) =
⊎-map (λ Pa → Pa , Pa→b≡true Pa) (λ ¬Pa → ¬Pa , ¬Pa→b≡false ¬Pa) ⟨$⟩
excluded-middle
to-Bool₁-computable→to-Bool₂-computable :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) →
Computable′ (λ A → ¬¬ A) (proj₁ (as-function-to-Bool₁ P)) →
Computable′ (λ A → ¬¬ A) (proj₁ (as-function-to-Bool₂ P P-prop))
to-Bool₁-computable→to-Bool₂-computable
P P-prop (p , cl-p , hyp₁ , hyp₂) =
p
, cl-p
, (λ a b →
proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b ↝⟨ to-Bool₂→to-Bool₁ P P-prop ⟩
proj₁ (as-function-to-Bool₁ P) [ a ]= b ↝⟨ hyp₁ a b ⟩□
apply p ⌜ a ⌝ ⇓ ⌜ b ⌝ □)
, λ a e →
apply p ⌜ a ⌝ ⇓ e ↝⟨ hyp₂ a e ⟩
¬¬ (∃ λ b → proj₁ (as-function-to-Bool₁ P) [ a ]= b ×
e ≡ ⌜ b ⌝) ↝⟨ _>>= (λ { (b , =b , ≡⌜b⌝) →
to-Bool₁→to-Bool₂ P P-prop =b >>= λ =b →
return (b , =b , ≡⌜b⌝) }) ⟩□
¬¬ (∃ λ b → proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b ×
e ≡ ⌜ b ⌝) □
×≡true⊎¬×≡false-propositional :
∀ {a} {A : Type a}
(P : A → Type a) → (∀ {a} → Is-proposition (P a)) →
∀ {a b} → Is-proposition (P a × b ≡ true ⊎ ¬ P a × b ≡ false)
×≡true⊎¬×≡false-propositional P P-prop =
⊎-closure-propositional
(λ (Pa , _) (¬Pa , _) → ¬Pa Pa)
(×-closure 1 P-prop Bool-set)
(×-closure 1 (¬-propositional ext) Bool-set)
×≡true⊎¬×≡false≃⇔T :
∀ {a} {A : Type a} {P : A → Type a} →
(∀ {a} → Is-proposition (P a)) →
∀ {a b} → (P a × b ≡ true ⊎ ¬ P a × b ≡ false) ≃ (P a ⇔ T b)
×≡true⊎¬×≡false≃⇔T {P = P} P-prop {a = a} {b = b} = Eq.⇔→≃
(×≡true⊎¬×≡false-propositional P P-prop)
(⇔-closure ext 1 P-prop (T-propositional b))
(λ where
(inj₁ (p , refl)) → record { from = λ _ → p }
(inj₂ (¬p , refl)) → record { to = ¬p; from = ⊥-elim })
(helper b)
where
helper : ∀ b → P a ⇔ T b → P a × b ≡ true ⊎ ¬ P a × b ≡ false
helper true hyp = inj₁ (_⇔_.from hyp _ , refl)
helper false hyp = inj₂ (_⇔_.to hyp , refl)
to-Bool₂-computable→to-Bool₁-computable :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
Excluded-middle a →
(P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) →
Computable (proj₁ (as-function-to-Bool₂ P P-prop)) →
Computable (proj₁ (as-function-to-Bool₁ P))
to-Bool₂-computable→to-Bool₁-computable
em P P-prop (p , cl-p , hyp₁ , hyp₂) =
p
, cl-p
, (λ a b →
proj₁ (as-function-to-Bool₁ P) [ a ]= b →⟨ to-Bool₁→to-Bool₂ P P-prop ⟩
¬¬ proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b →⟨ Excluded-middle→Double-negation-elimination em $
×≡true⊎¬×≡false-propositional P P-prop ⟩
proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b →⟨ hyp₁ a b ⟩□
apply p ⌜ a ⌝ ⇓ ⌜ b ⌝ □)
, (λ a b →
apply p ⌜ a ⌝ ⇓ b →⟨ hyp₂ a b ⟩
(∃ λ b′ →
proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) →⟨ Σ-map id (Σ-map (to-Bool₂→to-Bool₁ P P-prop) id) ⟩□
(∃ λ b′ →
proj₁ (as-function-to-Bool₁ P) [ a ]= b′ ×
b ≡ ⌜ b′ ⌝) □)
Decidable :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
A →Bool → Type a
Decidable = Computable P.∘ proj₁
Decidable′ :
∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
A →Bool → Type a
Decidable′ = Computable‴ P.∘ proj₁