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 4 (λ 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 4 (λ 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ℤ = [ 0 , 0 ] 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