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 ∎)