Add a new ring solver tactic.

2 files changed, 286 insertions, 0 deletions

diff --git a/Everything.agda b/Everything.agda
index 039338b..cd0f148 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -125,3 +125,6 @@ import Helium.Semantics.Axiomatic.Triple
 
 -- Base definitions for the denotational semantics.
 import Helium.Semantics.Denotational.Core
+
+-- Ring solver tactic using integers as coefficients
+import Helium.Tactic.CommutativeRing.NonReflective
diff --git a/src/Helium/Tactic/CommutativeRing/NonReflective.agda b/src/Helium/Tactic/CommutativeRing/NonReflective.agda
new file mode 100644
index 0000000..12029a5
--- /dev/null
+++ b/src/Helium/Tactic/CommutativeRing/NonReflective.agda
@@ -0,0 +1,283 @@
+--------------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Ring solver tactic using integers as coefficients
+--------------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles using (CommutativeRing)
+import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as Ringₚ
+open import Relation.Nullary
+
+module Helium.Tactic.CommutativeRing.NonReflective
+  {ℓ₁ ℓ₂ ℓ₃}
+  (R : CommutativeRing ℓ₁ ℓ₂ ℓ₃)
+  (1≉0 : let module R = CommutativeRing R in ¬ R.1# R.≈ R.0#)
+  where
+
+open import Data.Bool.Base
+open import Data.Sign using (Sign) renaming (_*_ to _S*_)
+open import Level using (0ℓ; _⊔_)
+
+open import Relation.Binary.Reasoning.StrictPartialOrder (CommutativeRing.strictPartialOrder R)
+
+module R where
+  open CommutativeRing R public
+     renaming
+     ( trans to <-trans
+     ; irrefl to <-irrefl
+     ; asym to <-asym
+     ; 0<a+0<b⇒0<ab to x>0∧y>0⇒xy>0
+     )
+
+  open Ringₚ R public
+
+  infixr 2 _,_
+
+  record Positive : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
+    constructor _,_
+    field
+      val   : Carrier
+      proof : val ≥ 0#
+
+  open Positive
+
+  infixl 6 _*⁺_ _*′_
+  infix 5 _◃_
+
+  _*⁺_ : Positive → Positive → Positive
+  +x *⁺ +y = +x .val * +y .val , x≥0∧y≥0⇒x*y≥0 (+x .proof) (+y .proof)
+
+  _◃_ : Sign → Positive → Carrier
+  Sign.- ◃ +x = - (+x .val)
+  Sign.+ ◃ +x = +x .val
+
+  sign : Carrier → Sign
+  sign x with does (x <? 0#)
+  ... | true  = Sign.-
+  ... | false = Sign.+
+
+  ∣_∣ : Carrier → Positive
+  ∣ x ∣ with x <? 0#
+  ... | yes x<0 = - x , <⇒≤ (x<0⇒-x>0 x<0)
+  ... | no x≮0  = x , ≮⇒≥ x≮0
+
+  ◃-congˡ : ∀ s +x +y → +x .val ≈ +y .val → s ◃ +x ≈ s ◃ +y
+  ◃-congˡ Sign.- +x +y x≈y = -‿cong x≈y
+  ◃-congˡ Sign.+ +x +y x≈y = x≈y
+
+  _*′_ : Carrier → Carrier → Carrier
+  x *′ y = sign x S* sign y ◃ ∣ x ∣ *⁺ ∣ y ∣
+
+  *′≈* : ∀ x y → x *′ y ≈ x * y
+  *′≈* x y with x <? 0# | y <? 0#
+  ... | yes x<0 | yes y<0 = -x*-y≈x*y x y
+  ... | yes x<0 | no y≮0  = begin-equality
+    - (- x * y) ≈⟨ -‿cong (-‿*-distribˡ x y) ⟩
+    - - (x * y) ≈⟨ -‿involutive (x * y) ⟩
+    x * y       ∎
+  ... | no x≮0  | yes y<0 = begin-equality
+    - (x * - y) ≈⟨ -‿cong (-‿*-distribʳ x y) ⟩
+    - - (x * y) ≈⟨ -‿involutive (x * y) ⟩
+    x * y       ∎
+  ... | no x≮0  | no y≮0  = Eq.refl
+
+open import Algebra.Bundles using (Ring)
+open import Algebra.Morphism
+import Data.Bool.Properties as Boolₚ
+open import Data.Empty using (⊥-elim)
+open import Data.Integer as ℤ hiding (suc)
+open import Data.Integer.Properties as ℤₚ
+open import Data.Maybe.Base
+open import Data.Nat.Base as ℕ using (ℕ; suc; z≤n; s≤s)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product
+import Data.Unit
+open import Data.Vec hiding (_⊛_)
+open import Data.Vec.N-ary
+open import Function
+
+open import Relation.Binary.PropositionalEquality
+
+open import Tactic.RingSolver.Core.AlmostCommutativeRing
+open import Tactic.RingSolver.Core.Expression public
+open import Tactic.RingSolver.Core.Polynomial.Parameters
+
+private
+  T-≡ : ∀ {x} → T x ⇔ x ≡ true
+  T-≡ {false} = mk⇔ (λ ()) (λ ())
+  T-≡ {true}  = mk⇔ (λ _ → refl) (λ _ → _)
+
+  T-≡′ : ∀ {x} → T (not x) ⇔ x ≡ false
+  T-≡′ {false} = mk⇔ (λ _ → refl) (λ _ → _)
+  T-≡′ {true}  = mk⇔ (λ ()) λ ()
+
+  T-¬ : ∀ {x} → T (not x) ⇔ (¬ T x)
+  T-¬ {false} = mk⇔ (λ _ ⊥ → ⊥) (λ ¬⊥ → _)
+  T-¬ {true}  = mk⇔ (λ ⊥ _ → ⊥) (λ ¬⊤ → ¬⊤ _)
+
+module Ops where
+  ℤ-coeff : RawCoeff 0ℓ 0ℓ
+  ℤ-coeff = record
+    { rawRing = Ring.rawRing ℤₚ.+-*-ring
+    ; isZero = does ∘ (0ℤ ℤ.≟_)
+    }
+
+  ring : AlmostCommutativeRing ℓ₁ ℓ₂
+  ring = fromCommutativeRing R.Unordered.commutativeRing (decToMaybe ∘ (R.0# R.≟_))
+
+  ℤ⟶R : RawCoeff.rawRing ℤ-coeff -Raw-AlmostCommutative⟶ ring
+  ℤ⟶R = record
+    { ⟦_⟧    = ⟦_⟧
+    ; +-homo = +-homo
+    ; *-homo = *-homo
+    ; -‿homo = -‿homo
+    ; 0-homo = R.Eq.refl
+    ; 1-homo = R.Eq.refl
+    }
+    where
+    ⟦_⟧ : ℤ → R.Carrier
+    ⟦ + n      ⟧ = n R.× R.1#
+    ⟦ -[1+ n ] ⟧ = R.- (suc n R.× R.1#)
+
+    ∸-homo : ∀ {m n} → m ℕ.≤ n → ⟦ + (n ℕ.∸ m) ⟧ R.≈ ⟦ + n ⟧ R.- ⟦ + m ⟧
+    ∸-homo {.0}     {n}      z≤n       = begin-equality
+      n R.× R.1#          ≈˘⟨ R.+-identityʳ _ ⟩
+      n R.× R.1# R.+ R.0# ≈˘⟨ R.+-congˡ R.-0≈0 ⟩
+      n R.× R.1# R.- R.0# ∎
+    ∸-homo {.suc m} {.suc n} (s≤s m≤n) = begin-equality
+      (n ℕ.∸ m) R.× R.1#                                ≈⟨  ∸-homo m≤n ⟩
+      n R.× R.1# R.- m R.× R.1#                         ≈˘⟨ R.+-congʳ (R.+-identityʳ _) ⟩
+      n R.× R.1# R.+ R.0# R.- m R.× R.1#                ≈˘⟨ R.+-congʳ (R.+-congˡ (R.-‿inverseʳ R.1#)) ⟩
+      n R.× R.1# R.+ (R.1# R.- R.1#) R.- m R.× R.1#     ≈˘⟨ R.+-congʳ (R.+-assoc _ _ _) ⟩
+      n R.× R.1# R.+ R.1# R.- R.1# R.- m R.× R.1#       ≈⟨  R.+-assoc _ _ _ ⟩
+      n R.× R.1# R.+ R.1# R.+ (R.- R.1# R.- m R.× R.1#) ≈⟨  R.+-cong (R.+-comm _ R.1#) (R.-‿+-comm R.1# _) ⟩
+      R.1# R.+ n R.× R.1# R.- (R.1# R.+ m R.× R.1#)     ≈˘⟨ R.+-cong (R.1+× n R.1#) (R.-‿cong (R.1+× m R.1#)) ⟩
+      suc n R.× R.1# R.- suc m R.× R.1#                 ∎
+
+    -‿homo : ∀ n → ⟦ - n ⟧ R.≈ R.- ⟦ n ⟧
+    -‿homo -[1+ n ] = R.Eq.sym (R.-‿involutive _)
+    -‿homo +0       = R.Eq.sym R.-0≈0
+    -‿homo +[1+ n ] = R.Eq.refl
+
+    ⊖-homo : ∀ m n → ⟦ m ⊖ n ⟧ R.≈ ⟦ + m ⟧ R.- ⟦ + n ⟧
+    ⊖-homo m n with m ℕ.<ᵇ n in eq
+    ... | true  = begin-equality
+      ⟦ - (+ (n ℕ.∸ m)) ⟧         ≈⟨  -‿homo (+ (n ℕ.∸ m)) ⟩
+      R.- ⟦ + (n ℕ.∸ m) ⟧         ≈⟨  R.-‿cong (∸-homo (ℕₚ.<⇒≤ (ℕₚ.<ᵇ⇒< m n (Equivalence.g T-≡ eq)))) ⟩
+      R.- (⟦ + n ⟧ R.- ⟦ + m ⟧)   ≈˘⟨ R.-‿+-comm ⟦ + n ⟧ (R.- ⟦ + m ⟧) ⟩
+      R.- ⟦ + n ⟧ R.- R.- ⟦ + m ⟧ ≈⟨  R.+-congˡ (R.-‿involutive ⟦ + m ⟧) ⟩
+      R.- ⟦ + n ⟧ R.+ ⟦ + m ⟧     ≈⟨  R.+-comm (R.- ⟦ + n ⟧) ⟦ + m ⟧ ⟩
+      ⟦ + m ⟧ R.- ⟦ + n ⟧         ∎
+    ... | false = ∸-homo (ℕₚ.≮⇒≥ {m} {n} (Equivalence.f T-¬ (Equivalence.g T-≡′ eq) ∘ ℕₚ.<⇒<ᵇ))
+
+    +-homo : ∀ m n → ⟦ m + n ⟧ R.≈ ⟦ m ⟧ R.+ ⟦ n ⟧
+    +-homo -[1+ m ] -[1+ n ] = begin-equality
+      R.- (suc (suc (m ℕ.+ n)) R.× R.1#)        ≡˘⟨ cong (λ x → R.- (x R.× R.1#)) (ℕₚ.+-suc (suc m) n) ⟩
+      R.- ((suc m ℕ.+ suc n) R.× R.1#)          ≈⟨  R.-‿cong (R.×-homo-+ R.1# (suc m) (suc n)) ⟩
+      R.- (suc m R.× R.1# R.+ suc n R.× R.1#)   ≈˘⟨ R.-‿+-comm _ _ ⟩
+      R.- (suc m R.× R.1#) R.- (suc n R.× R.1#) ∎
+    +-homo -[1+ m ] (+ n)    = begin-equality
+      ⟦ n ⊖ suc m ⟧             ≈⟨ ⊖-homo n (suc m) ⟩
+      ⟦ + n ⟧ R.+ ⟦ -[1+ m ] ⟧  ≈⟨ R.+-comm ⟦ + n ⟧ ⟦ -[1+ m ] ⟧ ⟩
+      ⟦ -[1+ m ] ⟧ R.+ ⟦ + n ⟧  ∎
+    +-homo (+ m)    -[1+ n ] = ⊖-homo m (suc n)
+    +-homo (+ m)    (+ n)    = R.×-homo-+ R.1# m n
+
+    ∣∙∣-homo : ∀ n → ⟦ + ∣ n ∣ ⟧ R.≈ R.Positive.val R.∣ ⟦ n ⟧ ∣
+    ∣∙∣-homo n with ⟦ n ⟧ R.<? R.0#
+    ∣∙∣-homo (+ n)    | yes n<0 = ⊥-elim (R.<⇒≱ n<0 (R.x≥0⇒n×x≥0 n R.0≤1))
+    ∣∙∣-homo (+ n)    | no n≮0  = R.Eq.refl
+    ∣∙∣-homo -[1+ n ] | yes n<0 = R.Eq.sym (R.-‿involutive _)
+    ∣∙∣-homo -[1+ n ] | no n≮0  = ⊥-elim (n≮0 (R.x>0⇒-x<0 (R.n≢0∧x>0⇒n×x>0 (suc n) (R.x≉y⇒0<1 1≉0))))
+
+    sign-homo : ∀ n → sign n ≡ R.sign ⟦ n ⟧
+    sign-homo n with ⟦ n ⟧ R.<? R.0#
+    sign-homo (+ n)    | yes n<0 = ⊥-elim (R.<⇒≱ n<0 (R.x≥0⇒n×x≥0 n R.0≤1))
+    sign-homo (+ n)    | no n≮0  = refl
+    sign-homo -[1+ n ] | yes n<0 = refl
+    sign-homo -[1+ n ] | no n≮0  = ⊥-elim (n≮0 (R.x>0⇒-x<0 (R.n≢0∧x>0⇒n×x>0 (suc n) (R.x≉y⇒0<1 1≉0))))
+
+    ◃-homo : ∀ s n → ⟦ s ◃ n ⟧ R.≈ s R.◃ (⟦ + n ⟧ R., R.x≥0⇒n×x≥0 n R.0≤1)
+    ◃-homo Sign.- 0       = R.Eq.sym R.-0≈0
+    ◃-homo Sign.- (suc n) = R.Eq.refl
+    ◃-homo Sign.+ 0       = R.Eq.refl
+    ◃-homo Sign.+ (suc n) = R.Eq.refl
+
+    *ⁿ-homo : ∀ m n → ⟦ + (m ℕ.* n) ⟧ R.≈ ⟦ + m ⟧ R.* ⟦ + n ⟧
+    *ⁿ-homo 0       n = R.Eq.sym (R.zeroˡ ⟦ + n ⟧)
+    *ⁿ-homo (suc m) n = begin-equality
+      (n ℕ.+ m ℕ.* n) R.× R.1#                          ≈⟨  R.×-homo-+ R.1# n (m ℕ.* n) ⟩
+      n R.× R.1# R.+ (m ℕ.* n) R.× R.1#                 ≈⟨  R.+-congˡ (*ⁿ-homo m n) ⟩
+      n R.× R.1# R.+ m R.× R.1# R.* n R.× R.1#          ≈˘⟨ R.+-congʳ (R.*-identityˡ _) ⟩
+      R.1# R.* n R.× R.1# R.+ m R.× R.1# R.* n R.× R.1# ≈˘⟨ R.distribʳ _ R.1# _ ⟩
+      (R.1# R.+ m R.× R.1#) R.* n R.× R.1#              ≈˘⟨ R.*-congʳ (R.1+× m R.1#) ⟩
+      suc m R.× R.1# R.* n R.× R.1#                     ∎
+
+    *-homo : ∀ m n → ⟦ m * n ⟧ R.≈ ⟦ m ⟧ R.* ⟦ n ⟧
+    *-homo m n = begin-equality
+      ⟦ m * n ⟧                                          ≡⟨⟩
+      ⟦ sm*sn ◃ ∣ m ∣ ℕ.* ∣ n ∣ ⟧                        ≈⟨ ◃-homo sm*sn (∣ m ∣ ℕ.* ∣ n ∣) ⟩
+      sm*sn R.◃ (⟦ + (∣ m ∣ ℕ.* ∣ n ∣) ⟧ R., ∣m∣∣n∣≥0)   ≈⟨ R.◃-congˡ sm*sn _ _ (*ⁿ-homo ∣ m ∣ ∣ n ∣) ⟩
+      sm*sn R.◃ (⟦ + ∣ m ∣ ⟧ R.* ⟦ + ∣ n ∣ ⟧ R., ∣mn∣≥0) ≈⟨ R.◃-congˡ sm*sn _ _ (R.*-cong (∣∙∣-homo m) (∣∙∣-homo n)) ⟩
+      sm*sn R.◃ R.∣ ⟦ m ⟧ ∣ R.*⁺ R.∣ ⟦ n ⟧ ∣             ≡⟨ cong₂ (λ x y → x S* y R.◃ R.∣ ⟦ m ⟧ ∣ R.*⁺ R.∣ ⟦ n ⟧ ∣) (sign-homo m) (sign-homo n) ⟩
+      Rsm*Rsn R.◃ R.∣ ⟦ m ⟧ ∣ R.*⁺ R.∣ ⟦ n ⟧ ∣           ≡⟨⟩
+      ⟦ m ⟧ R.*′ ⟦ n ⟧                                   ≈⟨ R.*′≈* ⟦ m ⟧ ⟦ n ⟧ ⟩
+      ⟦ m ⟧ R.* ⟦ n ⟧                                    ∎
+      where
+      ∣m∣∣n∣≥0 = R.x≥0⇒n×x≥0 (∣ m ∣ ℕ.* ∣ n ∣) R.0≤1
+      ∣mn∣≥0 = R.x≥0∧y≥0⇒x*y≥0 (R.x≥0⇒n×x≥0 ∣ m ∣ R.0≤1) (R.x≥0⇒n×x≥0 ∣ n ∣ R.0≤1)
+      sm*sn = sign m S* sign n
+      Rsm*Rsn = R.sign ⟦ m ⟧ S* R.sign ⟦ n ⟧
+
+  homo : Homomorphism 0ℓ 0ℓ ℓ₁ ℓ₂
+  homo = record
+    { from          = ℤ-coeff
+    ; to            = ring
+    ; morphism      = ℤ⟶R
+    ; Zero-C⟶Zero-R = λ { +0 _  → R.Eq.refl }
+    }
+
+  open Eval R.Unordered.rawRing (_-Raw-AlmostCommutative⟶_.⟦_⟧ ℤ⟶R) public
+
+  open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
+
+  norm : ∀ {n} → Expr ℤ n → Poly n
+  norm (Κ x)   = κ x
+  norm (Ι x)   = ι x
+  norm (x ⊕ y) = norm x ⊞ norm y
+  norm (x ⊗ y) = norm x ⊠ norm y
+  norm (x ⊛ i) = norm x ⊡ i
+  norm (⊝ x)   = ⊟ norm x
+
+  ⟦_⇓⟧ : ∀ {n} → Expr ℤ n → Vec R.Carrier n → R.Carrier
+  ⟦ expr ⇓⟧ = ⟦ norm expr ⟧ₚ
+    where open import Tactic.RingSolver.Core.Polynomial.Semantics homo renaming (⟦_⟧ to ⟦_⟧ₚ)
+
+  correct : ∀ {n} (expr : Expr ℤ n) ρ → ⟦ expr ⇓⟧ ρ R.≈ ⟦ expr ⟧ ρ
+  correct {n = n} = go
+    where
+    open import Tactic.RingSolver.Core.Polynomial.Homomorphism homo
+
+    go : ∀ (expr : Expr ℤ n) ρ → ⟦ expr ⇓⟧ ρ R.≈ ⟦ expr ⟧ ρ
+    go (Κ x)   ρ = κ-hom x ρ
+    go (Ι x)   ρ = ι-hom x ρ
+    go (x ⊕ y) ρ = ⊞-hom (norm x) (norm y) ρ ⟨ R.Eq.trans ⟩ (go x ρ ⟨ R.+-cong ⟩ go y ρ)
+    go (x ⊗ y) ρ = ⊠-hom (norm x) (norm y) ρ ⟨ R.Eq.trans ⟩ (go x ρ ⟨ R.*-cong ⟩ go y ρ)
+    go (x ⊛ i) ρ = ⊡-hom (norm x) i ρ ⟨ R.Eq.trans ⟩ R.^-congˡ i (go x ρ)
+    go (⊝ x)   ρ = ⊟-hom (norm x) ρ ⟨ R.Eq.trans ⟩ R.-‿cong (go x ρ)
+
+  open import Relation.Binary.Reflection R.strictTotalOrder.Eq.setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public
+
+solve : ∀ (n : ℕ) →
+        (f : N-ary n (Expr ℤ n) (Expr ℤ n × Expr ℤ n)) →
+        Eqʰ n R._≈_ (curryⁿ (Ops.⟦_⇓⟧ (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⇓⟧ (proj₂ (Ops.close n f)))) →
+        Eq  n R._≈_ (curryⁿ (Ops.⟦_⟧  (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⟧  (proj₂ (Ops.close n f))))
+solve = Ops.solve
+{-# INLINE solve #-}
+
+infixl 6 _⊜_
+_⊜_ : ∀ {n} → Expr ℤ n → Expr ℤ n → Expr ℤ n × Expr ℤ n
+_⊜_ = _,_
+{-# INLINE _⊜_ #-}