Relax decidability module parameter of Algebra.Solver.Ring (#511)

Author: mwageringel

CHANGELOG.md

@@ -43,6 +43,27 @@ Splitting up `Data.Maybe` into the standard hierarchy.
   Eq-isDecEquivalence ↦ isDecEquivalence
   ```
 
+#### Refactoring of ring solvers
+
+* In the ring solvers below, the `Decidable` module parameter was replaced by a
+  strictly weaker parameter `Relation.Binary.Core.WeaklyDecidable`, which makes
+  the ring solvers more versatile.
+  ```
+  Algebra.Solver.Ring
+  Algebra.Solver.Ring.NaturalCoefficients
+  ```
+
+* Added `_:×_` operator to `Algebra.Solver.Ring`.
+
+* Created a module `Algebra.Solver.Ring.NaturalCoefficients.Default` that
+  instantiates the solver for any `CommutativeSemiring`.
+
+#### Other
+
+* Moved `_≟_` from `Data.Bool.Base` to `Data.Bool.Properties`. Backwards
+  compatibility has been (nearly completely) preserved by having `Data.Bool`
+  publicly re-export `_≟_`.
+
 Other major changes
 -------------------
 

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -8,7 +8,7 @@
 
 open import Algebra
 
-open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_; _∨_)
+open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin using (Fin; zero; suc)
 open import Data.Maybe as Maybe
   using (Maybe; decToMaybe; From-just; from-just)

src/Algebra/Solver/Ring.agda

@@ -11,15 +11,14 @@
 
 open import Algebra
 open import Algebra.Solver.Ring.AlmostCommutativeRing
-
-open import Relation.Binary
+open import Relation.Binary.Core using (WeaklyDecidable)
 
 module Algebra.Solver.Ring
   {r₁ r₂ r₃}
   (Coeff : RawRing r₁)               -- Coefficient "ring".
   (R : AlmostCommutativeRing r₂ r₃)  -- Main "ring".
   (morphism : Coeff -Raw-AlmostCommutative⟶ R)
-  (_coeff≟_ : Decidable (Induced-equivalence morphism))
+  (_coeff≟_ : WeaklyDecidable (Induced-equivalence morphism))
   where
 
 open import Algebra.Solver.Ring.Lemmas Coeff R morphism
@@ -40,11 +39,12 @@ import Relation.Binary.Reflection as Reflection
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Fin using (Fin; zero; suc)
 open import Data.Vec using (Vec; []; _∷_; lookup)
+open import Data.Maybe.Base using (just; nothing)
 open import Function
 open import Level using (_⊔_)
 
 infix  9 :-_ -H_ -N_
-infixr 9 _:^_ _^N_
+infixr 9 _:×_ _:^_ _^N_
 infix  8 _*x+_ _*x+HN_ _*x+H_
 infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_
 infixl 7 _:+_ _:-_ _+H_ _+N_
@@ -77,6 +77,10 @@ _:*_ = op [*]
 _:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
 x :- y = x :+ :- y
 
+_:×_ : ∀ {n} → ℕ → Polynomial n → Polynomial n
+zero :× p = con C.0#
+suc m :× p = p :+ m :× p
+
 -- Semantics.
 
 sem : Op → Op₂ Carrier
@@ -161,24 +165,24 @@ mutual
 
 mutual
 
-  -- Equality is decidable.
+  -- Equality is weakly decidable.
 
-  _≟H_ : ∀ {n} → Decidable (_≈H_ {n = n})
-  ∅           ≟H ∅           = yes ∅
-  ∅           ≟H (_ *x+ _)   = no λ()
-  (_ *x+ _)   ≟H ∅           = no λ()
+  _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n})
+  ∅           ≟H ∅           = just ∅
+  ∅           ≟H (_ *x+ _)   = nothing
+  (_ *x+ _)   ≟H ∅           = nothing
   (p₁ *x+ c₁) ≟H (p₂ *x+ c₂) with p₁ ≟H p₂ | c₁ ≟N c₂
-  ... | yes p₁≈p₂ | yes c₁≈c₂ = yes (p₁≈p₂ *x+ c₁≈c₂)
-  ... | _         | no  c₁≉c₂ = no  λ { (_ *x+ c₁≈c₂) → c₁≉c₂ c₁≈c₂ }
-  ... | no  p₁≉p₂ | _         = no  λ { (p₁≈p₂ *x+ _) → p₁≉p₂ p₁≈p₂ }
+  ... | just p₁≈p₂ | just c₁≈c₂ = just (p₁≈p₂ *x+ c₁≈c₂)
+  ... | _          | nothing    = nothing
+  ... | nothing    | _          = nothing
 
-  _≟N_ : ∀ {n} → Decidable (_≈N_ {n = n})
+  _≟N_ : ∀ {n} → WeaklyDecidable (_≈N_ {n = n})
   con c₁ ≟N con c₂ with c₁ coeff≟ c₂
-  ... | yes c₁≈c₂ = yes (con c₁≈c₂)
-  ... | no  c₁≉c₂ = no  λ { (con c₁≈c₂) → c₁≉c₂ c₁≈c₂}
+  ... | just c₁≈c₂ = just (con c₁≈c₂)
+  ... | nothing    = nothing
   poly p₁ ≟N poly p₂ with p₁ ≟H p₂
-  ... | yes p₁≈p₂ = yes (poly p₁≈p₂)
-  ... | no  p₁≉p₂ = no  λ { (poly p₁≈p₂) → p₁≉p₂ p₁≈p₂ }
+  ... | just p₁≈p₂ = just (poly p₁≈p₂)
+  ... | nothing    = nothing
 
 mutual
 
@@ -226,8 +230,8 @@ mutual
 _*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
 (p *x+ c′) *x+HN c = (p *x+ c′) *x+ c
 ∅          *x+HN c with c ≟N 0N
-... | yes c≈0 = ∅
-... | no  c≉0 = ∅ *x+ c
+... | just c≈0 = ∅
+... | nothing  = ∅ *x+ c
 
 mutual
 
@@ -254,14 +258,14 @@ mutual
   _*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n)
   c *NH ∅          = ∅
   c *NH (p *x+ c′) with c ≟N 0N
-  ... | yes c≈0 = ∅
-  ... | no  c≉0 = (c *NH p) *x+ (c *N c′)
+  ... | just c≈0 = ∅
+  ... | nothing  = (c *NH p) *x+ (c *N c′)
 
   _*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
   ∅          *HN c = ∅
   (p *x+ c′) *HN c with c ≟N 0N
-  ... | yes c≈0 = ∅
-  ... | no  c≉0 = (p *HN c) *x+ (c′ *N c)
+  ... | just c≈0 = ∅
+  ... | nothing  = (p *HN c) *x+ (c′ *N c)
 
   _*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
   ∅           *H _           = ∅
@@ -342,17 +346,17 @@ normalise (:- t)         = -N normalise t
             ∀ ρ → ⟦ p *x+HN c ⟧H ρ ≈ ⟦ p *x+ c ⟧H ρ
 *x+HN≈*x+ (p *x+ c′) c ρ       = refl
 *x+HN≈*x+ ∅          c (x ∷ ρ) with c ≟N 0N
-... | yes c≈0 = begin
+... | just c≈0 = begin
   0#                 ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟩
   ⟦ c ⟧N ρ           ≈⟨ sym $ lemma₆ _ _ ⟩
   0# * x + ⟦ c ⟧N ρ  ∎
-... | no c≉0 = refl
+... | nothing = refl
 
 ∅*x+HN-homo : ∀ {n} (c : Normal n) x ρ →
               ⟦ ∅ *x+HN c ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ
 ∅*x+HN-homo c x ρ with c ≟N 0N
-... | yes c≈0 = 0≈⟦0⟧ c≈0 ρ
-... | no  c≉0 = lemma₆ _ _
+... | just c≈0 = 0≈⟦0⟧ c≈0 ρ
+... | nothing = lemma₆ _ _
 
 mutual
 
@@ -396,11 +400,11 @@ mutual
     ⟦ c *NH p ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)
   *NH-homo c ∅          x ρ = sym (*-zeroʳ _)
   *NH-homo c (p *x+ c′) x ρ with c ≟N 0N
-  ... | yes c≈0 = begin
+  ... | just c≈0 = begin
     0#                                            ≈⟨ sym (*-zeroˡ _) ⟩
     0# * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)         ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟨ *-cong ⟩ refl ⟩
     ⟦ c ⟧N ρ  * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)  ∎
-  ... | no c≉0 = begin
+  ... | nothing = begin
     ⟦ c *NH p ⟧H (x ∷ ρ) * x + ⟦ c *N c′ ⟧N ρ                 ≈⟨ (*NH-homo c p x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c c′ ρ ⟩
     (⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)) * x + (⟦ c ⟧N ρ * ⟦ c′ ⟧N ρ)  ≈⟨ lemma₃ _ _ _ _ ⟩
     ⟦ c ⟧N ρ * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)               ∎
@@ -410,11 +414,11 @@ mutual
     ⟦ p *HN c ⟧H (x ∷ ρ) ≈ ⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ
   *HN-homo ∅          c x ρ = sym (*-zeroˡ _)
   *HN-homo (p *x+ c′) c x ρ with c ≟N 0N
-  ... | yes c≈0 = begin
+  ... | just c≈0 = begin
     0#                                           ≈⟨ sym (*-zeroʳ _) ⟩
     (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * 0#        ≈⟨ refl ⟨ *-cong ⟩ 0≈⟦0⟧ c≈0 ρ ⟩
     (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ  ∎
-  ... | no c≉0 = begin
+  ... | nothing = begin
     ⟦ p *HN c ⟧H (x ∷ ρ) * x + ⟦ c′ *N c ⟧N ρ                 ≈⟨ (*HN-homo p c x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c′ c ρ ⟩
     (⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ) * x + (⟦ c′ ⟧N ρ * ⟦ c ⟧N ρ)  ≈⟨ lemma₂ _ _ _ _ ⟩
     (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ               ∎

src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -7,22 +7,21 @@
 
 open import Algebra
 import Algebra.Operations.Semiring as SemiringOps
-open import Relation.Nullary
+open import Data.Maybe.Base using (Maybe; just; nothing; map)
 
 module Algebra.Solver.Ring.NaturalCoefficients
          {r₁ r₂}
          (R : CommutativeSemiring r₁ r₂)
          (dec : let open CommutativeSemiring R
                     open SemiringOps semiring in
-                ∀ m n → Dec (m × 1# ≈ n × 1#)) where
+                ∀ m n → Maybe (m × 1# ≈ n × 1#)) where
 
 import Algebra.Solver.Ring
 open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
 open import Data.Product using (module Σ)
 open import Function
 import Relation.Binary.EqReasoning
-import Relation.Nullary.Decidable as Dec
 
 open CommutativeSemiring R
 open SemiringOps semiring
@@ -60,8 +59,8 @@ private
 
   -- Equality of certain expressions can be decided.
 
-  dec′ : ∀ m n → Dec (m ×′ 1# ≈ n ×′ 1#)
-  dec′ m n = Dec.map′ to from (dec m n)
+  dec′ : ∀ m n → Maybe (m ×′ 1# ≈ n ×′ 1#)
+  dec′ m n = map to (dec m n)
     where
     to : m × 1# ≈ n × 1# → m ×′ 1# ≈ n ×′ 1#
     to m≈n = begin
@@ -70,13 +69,6 @@ private
       n ×  1#  ≈⟨ ×≈×′ n 1# ⟩
       n ×′ 1#  ∎
 
-    from : m ×′ 1# ≈ n ×′ 1# → m × 1# ≈ n × 1#
-    from m≈n = begin
-      m ×  1#  ≈⟨ ×≈×′ m 1# ⟩
-      m ×′ 1#  ≈⟨ m≈n ⟩
-      n ×′ 1#  ≈⟨ sym $ ×≈×′ n 1# ⟩
-      n ×  1#  ∎
-
 -- The instantiation.
 
 open Algebra.Solver.Ring _ _ homomorphism dec′ public

src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda

@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instantiates the natural coefficients ring solver, using coefficient
+-- equality induced by ℕ.
+--
+-- This is sufficient for proving equalities that are independent of the
+-- characteristic.  In particular, this is enough for equalities in rings of
+-- characteristic 0.
+------------------------------------------------------------------------
+
+open import Algebra
+
+module Algebra.Solver.Ring.NaturalCoefficients.Default
+         {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where
+
+import Algebra.Operations.Semiring as SemiringOps
+open import Data.Maybe.Base using (Maybe; map)
+open import Data.Nat using (_≟_)
+open import Relation.Binary.Consequences using (dec⟶weaklyDec)
+import Relation.Binary.PropositionalEquality as P
+
+open CommutativeSemiring R
+open SemiringOps semiring
+
+private
+  dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)
+  dec m n = map (λ { P.refl → refl }) (dec⟶weaklyDec _≟_ m n)
+
+open import Algebra.Solver.Ring.NaturalCoefficients R dec public

src/Algebra/Solver/Ring/Simple.agda

@@ -7,6 +7,7 @@
 
 open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Relation.Binary
+open import Relation.Binary.Consequences using (dec⟶weaklyDec)
 
 module Algebra.Solver.Ring.Simple
          {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
@@ -15,4 +16,4 @@ module Algebra.Solver.Ring.Simple
 
 open AlmostCommutativeRing R
 import Algebra.Solver.Ring as RS
-open RS rawRing R (-raw-almostCommutative⟶ R) _≟_ public
+open RS rawRing R (-raw-almostCommutative⟶ R) (dec⟶weaklyDec _≟_) public

src/Data/Bool.agda

@@ -16,6 +16,12 @@ open import Relation.Binary.PropositionalEquality as PropEq
 
 open import Data.Bool.Base public
 
+------------------------------------------------------------------------
+-- Publicly re-export queries
+
+open import Data.Bool.Properties public
+  using (_≟_)
+
 ------------------------------------------------------------------------
 -- Some properties
 

src/Data/Bool/Base.agda

@@ -8,8 +8,6 @@ module Data.Bool.Base where
 open import Data.Unit.Base using (⊤)
 open import Data.Empty
 open import Relation.Nullary
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 infixr 6 _∧_
 infixr 5 _∨_ _xor_
@@ -49,14 +47,3 @@ false ∨ b = b
 _xor_ : Bool → Bool → Bool
 true  xor b = not b
 false xor b = b
-
-------------------------------------------------------------------------
--- Queries
-
-infix 4 _≟_
-
-_≟_ : Decidable {A = Bool} _≡_
-true  ≟ true  = yes refl
-false ≟ false = yes refl
-true  ≟ false = no λ()
-false ≟ true  = no λ()

src/Data/Bool/Properties.agda

@@ -7,22 +7,35 @@
 module Data.Bool.Properties where
 
 open import Algebra
-open import Data.Bool
+open import Data.Bool.Base
 open import Data.Empty
 open import Data.Product
 open import Data.Sum
 open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence
   using (_⇔_; equivalence; module Equivalence)
+open import Relation.Binary.Core using (Decidable)
 open import Relation.Binary.PropositionalEquality
   hiding ([_]; proof-irrelevance)
+open import Relation.Nullary using (yes; no)
 open import Relation.Unary using (Irrelevant)
 
 open import Algebra.FunctionProperties (_≡_ {A = Bool})
 open import Algebra.Structures (_≡_ {A = Bool})
 open ≡-Reasoning
 
+------------------------------------------------------------------------
+-- Queries
+
+infix 4 _≟_
+
+_≟_ : Decidable {A = Bool} _≡_
+true  ≟ true  = yes refl
+false ≟ false = yes refl
+true  ≟ false = no λ()
+false ≟ true  = no λ()
+
 ------------------------------------------------------------------------
 -- Properties of _∨_
 

src/Data/Fin/Subset/Properties.agda

@@ -12,7 +12,6 @@ import Algebra.Structures as AlgebraicStructures
 import Algebra.Properties.Lattice as L
 import Algebra.Properties.DistributiveLattice as DL
 import Algebra.Properties.BooleanAlgebra as BA
-open import Data.Bool.Base using (_≟_)
 open import Data.Bool.Properties
 open import Data.Fin using (Fin; suc; zero)
 open import Data.Fin.Subset