module EqDec where open import Data.Empty open import Data.Unit open import Data.Bool hiding (_∧_; _∨_) open import Data.Bool.Properties open import Data.Sum open import Data.Product open import Relation.Nullary hiding (_⇔_) open import Relation.Binary.PropositionalEquality as PropEq open import Relation.Binary.HeterogeneousEquality using (_≅_; refl; ≡-to-≅) import Relation.Binary.EqReasoning as EqR -- axiom of choice ac : {A B : Set} → (R : A → B → Set) → (∀ x → ∃ (λ y → R x y)) → (∃ {A → B} (λ f → ∀ x → R x (f x))) ac R g = ((λ x → proj₁ (g x)) , λ x → proj₂ (g x)) -- we need a language of propositions that talks about equality data † (A : Set) : Set where TT : † A FF : † A _≐_ : A → A → † A _≘_ : Bool → Bool → † A _∧_ : † A → † A → † A _⇒_ : † A → † A → † A _∨_ : † A → † A → † A ⌈_⌉ : ∀ {A} → † A → Set ⌈ TT ⌉ = ⊤ ⌈ FF ⌉ = ⊥ ⌈ a ≐ b ⌉ = a ≡ b ⌈ a ≘ b ⌉ = a ≡ b ⌈ P ∧ Q ⌉ = ⌈ P ⌉ × ⌈ Q ⌉ ⌈ P ⇒ Q ⌉ = ⌈ P ⌉ → ⌈ Q ⌉ ⌈ P ∨ Q ⌉ = ⌈ P ⌉ ⊎ ⌈ Q ⌉ ￢ : ∀ {A} → † A → † A ￢ P = P ⇒ FF -- proof irrelevance! postulate irr : ∀ {A} (P Q : † A) → (p : ⌈ P ⌉)(q : ⌈ Q ⌉) → (P ≡ Q) → p ≅ q -- cong-× : ∀ {A B} {x y : Σ A B} → proj₁ x ≡ proj₁ y → proj₂ x ≅ proj₂ y → x ≡ y cong-× {A}{B} {(x₁ , x₂)} {(.x₁ , .x₂)} refl refl = refl -- oneof : {A : Set} → (a b : A) → Set oneof {A} a b = Σ A (λ x → ⌈ (x ≐ a) ∨ (x ≐ b) ⌉) Ψ : {A : Set} → (a b : A) → oneof a b → Bool → Set Ψ {A} a b z e = ⌈ ((e ≘ false) ∧ (proj₁ z ≐ a)) ∨ ((e ≘ true) ∧ (proj₁ z ≐ b)) ⌉ Ψ-total : {A : Set} → (a b : A) → (z : oneof a b) → ∃ (λ e → Ψ a b z e) Ψ-total a b (x , inj₁ x≡a) = (false , inj₁ (refl , x≡a)) Ψ-total a b (x , inj₂ x≡b) = (true , inj₂ (refl , x≡b)) Ψ-fun : {A : Set} → (a b : A) → ∃ {oneof a b → Bool} (λ f → (z : oneof a b) → Ψ a b z (f z)) Ψ-fun a b = ac (Ψ a b) (Ψ-total a b) ff≢tt : false ≢ true ff≢tt = not-¬ refl eq_dec : {A : Set} → (a b : A) → ⌈ (a ≐ b) ∨ (￢ (a ≐ b)) ⌉ eq_dec {A} a b = body where a' : oneof a b a' = (a , inj₁ refl) b' : oneof a b b' = (b , inj₂ refl) body : (a ≡ b) ⊎ (¬ (a ≡ b)) body with Ψ-fun a b ... | (f , f⊆Ψ) with f⊆Ψ a' | f⊆Ψ b' ... | inj₁ (fa'≡ff , a≡a) | inj₁ (fb'≡ff , b≡a) = inj₁ (sym b≡a) ... | inj₂ (fa'≡tt , a≡b) | inj₁ (fb'≡ff , b≡a) = inj₁ a≡b ... | inj₂ (fa'≡tt , a≡b) | inj₂ (fb'≡tt , b≡b) = inj₁ a≡b ... | inj₁ (fa'≡ff , a≡a) | inj₂ (fb'≡tt , b≡b) = inj₂ (cont fa'≡ff fb'≡tt) where cont : f a' ≡ false → f b' ≡ true → a ≢ b cont fa'≡ff fb'≡tt a≡b = let P≡Q : ((a ≐ a) ∨ (a ≐ b)) ≡ ((b ≐ a) ∨ (b ≐ b)) P≡Q = let open EqR (PropEq.setoid († A)) in begin (a ≐ a) ∨ (a ≐ b) ≈⟨ cong (λ x → (a ≐ a) ∨ (a ≐ x)) (sym a≡b) ⟩ (a ≐ a) ∨ (a ≐ a) ≈⟨ cong (λ x → (x ≐ a) ∨ (x ≐ x)) a≡b ⟩ (b ≐ a) ∨ (b ≐ b) ∎ a'≡b' : a' ≡ b' a'≡b' = cong-× a≡b (irr ((a ≐ a) ∨ (a ≐ b)) ((b ≐ a) ∨ (b ≐ b)) (proj₂ a') (proj₂ b') P≡Q) fa'≡fb' : f a' ≡ f b' fa'≡fb' = cong f a'≡b' in let open EqR (PropEq.setoid Bool) in ff≢tt (begin false ≈⟨ sym fa'≡ff ⟩ f a' ≈⟨ fa'≡fb' ⟩ f b' ≈⟨ fb'≡tt ⟩ true ∎)