module Qtest where 

open import Data.Nat
open import Data.Nat.Properties as Nat
open import Relation.Binary 
open import Quotient
open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open ≡-Reasoning
open Nat.SemiringSolver

Int : Setoid _ _
Int = record
  { Carrier       = ℕ × ℕ
  ; _≈_           = λ { (x+ , x-) (y+ , y-) → x+ + y- ≡ y+ + x- }
  ; isEquivalence = record
    { refl  = λ {_} → refl
    ; sym   = λ p → sym p
    ; trans = λ { {x+ , x-}{y+ , y-}{z+ , z-} p q →
        cancel-+-left (y- + y+) (begin
          (y- + y+) + (x+ + z-)  ≡⟨ solve  (λ y- y+ x+ z- → (y- :+ y+) :+ (x+ :+ z-) :=
                                                             x+ :+ y- :+ (y+ :+ z-))
                                            refl y- y+ x+ z- ⟩
          x+ + y- + (y+ + z-)    ≡⟨ cong₂ _+_ p q ⟩
          y+ + x- + (z+ + y-)    ≡⟨ solve  (λ y+ x- z+ y- → y+ :+ x- :+ (z+ :+ y-) :=
                                                             (y- :+ y+) :+ (z+ :+ x-))
                                            refl y+ x- z+ y- ⟩
          (y- + y+) + (z+ + x-)  ∎) }
    }
  }

ℤ : Set
ℤ = Quotient Int

zeroℤ : ℤ
zeroℤ = [  ,  ]

open import Algebra
module CS = CommutativeSemiring Nat.commutativeSemiring

minus : ℤ → ℤ 
minus x = rec {A = Int} 
              ℤ 
              (λ {(x+ , x-) → [ x- , x+ ]}) 
              (λ { {x+ , x-} {y+ , y-} x≈y → [ sym (trans (CS.+-comm y- x+) 
                                                          (trans x≈y 
                                                                 (CS.+-comm y+ x-))) ]-cong})
              x

minus-lem : (x : ℤ) → minus (minus x) ≡ x
minus-lem x = elim {A = Int} (λ x → minus (minus x) ≡ x) 
  (λ { (x+ , x-) → refl}) (λ x≈y → proof-irrelevance _ _) x