------------------------------------------------------------------------
-- Solver for commutative ring or semiring equalities
------------------------------------------------------------------------

-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
-- code below is not optimised like theirs, though.

open import Algebra
open import Algebra.RingSolver.AlmostCommutativeRing

module Algebra.RingSolver
  (coeff : RawRing)            -- Coefficient "ring".
  (r : AlmostCommutativeRing)  -- Main "ring".
  (morphism : coeff -Raw-AlmostCommutative⟶ r)
  where

import Algebra.RingSolver.Lemmas as L; open L coeff r morphism
private module C = RawRing coeff
open AlmostCommutativeRing r hiding (zero)
import Algebra.FunctionProperties as P; open P setoid
open import Algebra.Morphism
open _-RawRing⟶_ morphism renaming (⟦_⟧ to ⟦_⟧')
import Algebra.Operations as Ops; open Ops semiring

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Nat using (; suc; zero) renaming (_+_ to _ℕ-+_)
import Data.Fin as Fin
open Fin using (Fin; zero; suc)
open import Data.Vec
open import Data.Function

infix  9 _↑-NF :-_ --NF_
infixr 9 _:^_ _^-NF_ _:↑_
infix  8 _*x _*x+_
infixl 8 _:*_ _*-NF_ _↑-*-NF_
infixl 7 _:+_ _+-NF_ _:-_
infixl 0 _∷-NF_

------------------------------------------------------------------------
-- Polynomials

data Op : Set where
  [+] : Op
  [*] : Op

-- The polynomials are indexed over the number of variables.

data Polynomial (m : ) : Set where
  op   : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m)  Polynomial m
  con  : (c : C.carrier)  Polynomial m
  var  : (x : Fin m)  Polynomial m
  _:^_ : (p : Polynomial m) (n : )  Polynomial m
  :-_  : (p : Polynomial m)  Polynomial m

-- Short-hand notation.

_:+_ :  {n}  Polynomial n  Polynomial n  Polynomial n
_:+_ = op [+]

_:*_ :  {n}  Polynomial n  Polynomial n  Polynomial n
_:*_ = op [*]

_:-_ :  {n}  Polynomial n  Polynomial n  Polynomial n
x :- y = x :+ :- y

-- Semantics.

sem : Op  Op₂
sem [+] = _+_
sem [*] = _*_

⟦_⟧_ :  {n}  Polynomial n  Vec carrier n  carrier
 op o p₁ p₂  ρ =  p₁  ρ  sem o   p₂  ρ
 con c       ρ =  c ⟧'
 var x       ρ = lookup x ρ
 p :^ n      ρ =  p  ρ ^ n
 :- p        ρ = -  p  ρ

private

  -- Equality.

  _≛_ :  {n}  Polynomial n  Polynomial n  Set
  p₁  p₂ =  {ρ}   p₁  ρ   p₂  ρ

  -- Reindexing.

  _:↑_ :  {n}  Polynomial n  (m : )  Polynomial (m ℕ-+ n)
  op o p₁ p₂ :↑ m = op o (p₁ :↑ m) (p₂ :↑ m)
  con c      :↑ m = con c
  var x      :↑ m = var (Fin.raise m x)
  (p :^ n)   :↑ m = (p :↑ m) :^ n
  (:- p)     :↑ m = :- (p :↑ m)

------------------------------------------------------------------------
-- Normal forms of polynomials

private

  -- The normal forms (Horner forms) are indexed over
  -- * the number of variables in the polynomial, and
  -- * an equivalent polynomial.

  data Normal : (n : )  Polynomial n  Set where
    con-NF : (c : C.carrier)  Normal 0 (con c)
    _↑-NF  :  {n p'} (p : Normal n p')  Normal (suc n) (p' :↑ 1)
    _*x+_  :  {n p' c'} (p : Normal (suc n) p') (c : Normal n c') 
             Normal (suc n) (p' :* var zero :+ c' :↑ 1)
    _∷-NF_ :  {n p₁ p₂} (p : Normal n p₁) (eq : p₁  p₂)  Normal n p₂

  ⟦_⟧-NF_ :  {n p}  Normal n p  Vec carrier n  carrier
   p ∷-NF _ ⟧-NF ρ       =  p ⟧-NF ρ
   con-NF c ⟧-NF ρ       =  c ⟧'
   p ↑-NF   ⟧-NF (x  ρ) =  p ⟧-NF ρ
   p *x+ c  ⟧-NF (x  ρ) = ( p ⟧-NF (x  ρ) * x) +  c ⟧-NF ρ

------------------------------------------------------------------------
-- Normalisation

private

  con-NF⋆ :  {n}  (c : C.carrier)  Normal n (con c)
  con-NF⋆ {zero}  c = con-NF c
  con-NF⋆ {suc _} c = con-NF⋆ c ↑-NF

  _+-NF_ :  {n p₁ p₂} 
           Normal n p₁  Normal n p₂  Normal n (p₁ :+ p₂)
  (p₁ ∷-NF eq₁) +-NF (p₂ ∷-NF eq₂) = p₁ +-NF p₂                    ∷-NF eq₁   +-pres-≈  eq₂
  (p₁ ∷-NF eq)  +-NF p₂            = p₁ +-NF p₂                    ∷-NF eq    +-pres-≈  refl
  p₁            +-NF (p₂ ∷-NF eq)  = p₁ +-NF p₂                    ∷-NF refl  +-pres-≈  eq
  con-NF c₁     +-NF con-NF c₂     = con-NF (C._+_ c₁ c₂)          ∷-NF +-homo _ _
  p₁ ↑-NF       +-NF p₂ ↑-NF       = (p₁ +-NF p₂) ↑-NF             ∷-NF refl
  p₁ *x+ c₁     +-NF p₂ ↑-NF       = p₁ *x+ (c₁ +-NF p₂)           ∷-NF sym (+-assoc _ _ _)
  p₁ *x+ c₁     +-NF p₂ *x+ c₂     = (p₁ +-NF p₂) *x+ (c₁ +-NF c₂) ∷-NF lemma₁ _ _ _ _ _
  p₁ ↑-NF       +-NF p₂ *x+ c₂     = p₂ *x+ (p₁ +-NF c₂)           ∷-NF lemma₂ _ _ _

  _*x :  {n p}  Normal (suc n) p  Normal (suc n) (p :* var zero)
  p *x = p *x+ con-NF⋆ C.0# ∷-NF lemma₀ _

  mutual

    -- The first function is just a variant of _*-NF_ which I used to
    -- make the termination checker believe that the code is
    -- terminating.

    _↑-*-NF_ :  {n p₁ p₂} 
               Normal n p₁  Normal (suc n) p₂ 
               Normal (suc n) (p₁ :↑ 1 :* p₂)
    p₁ ↑-*-NF (p₂ ∷-NF eq) = p₁ ↑-*-NF p₂                    ∷-NF refl  *-pres-≈  eq
    p₁ ↑-*-NF p₂ ↑-NF      = (p₁ *-NF p₂) ↑-NF               ∷-NF refl
    p₁ ↑-*-NF (p₂ *x+ c₂)  = (p₁ ↑-*-NF p₂) *x+ (p₁ *-NF c₂) ∷-NF lemma₄ _ _ _ _

    _*-NF_ :  {n p₁ p₂} 
             Normal n p₁  Normal n p₂  Normal n (p₁ :* p₂)
    (p₁ ∷-NF eq₁) *-NF (p₂ ∷-NF eq₂) = p₁ *-NF p₂                         ∷-NF eq₁   *-pres-≈  eq₂
    (p₁ ∷-NF eq)  *-NF p₂            = p₁ *-NF p₂                         ∷-NF eq    *-pres-≈  refl
    p₁            *-NF (p₂ ∷-NF eq)  = p₁ *-NF p₂                         ∷-NF refl  *-pres-≈  eq
    con-NF c₁     *-NF con-NF c₂     = con-NF (C._*_ c₁ c₂)               ∷-NF *-homo _ _
    p₁ ↑-NF       *-NF p₂ ↑-NF       = (p₁ *-NF p₂) ↑-NF                  ∷-NF refl
    (p₁ *x+ c₁)   *-NF p₂ ↑-NF       = (p₁ *-NF p₂ ↑-NF) *x+ (c₁ *-NF p₂) ∷-NF lemma₃ _ _ _ _
    p₁ ↑-NF       *-NF (p₂ *x+ c₂)   = (p₁ ↑-NF *-NF p₂) *x+ (p₁ *-NF c₂) ∷-NF lemma₄ _ _ _ _
    (p₁ *x+ c₁)   *-NF (p₂ *x+ c₂)   =
      (p₁ *-NF p₂) *x *x +-NF
      (p₁ *-NF c₂ ↑-NF +-NF c₁ ↑-*-NF p₂) *x+ (c₁ *-NF c₂)                ∷-NF lemma₅ _ _ _ _ _

  --NF_ :  {n p}  Normal n p  Normal n (:- p)
  --NF_ (p ∷-NF eq) = --NF_ p ∷-NF --pres-≈ eq
  --NF_ (con-NF c)  = con-NF (C.-_ c) ∷-NF --homo _
  --NF_ (p ↑-NF)    = --NF_ p ↑-NF
  --NF_ (p *x+ c)   = --NF_ p *x+ --NF_ c ∷-NF lemma₆ _ _ _

  var-NF :  {n}  (i : Fin n)  Normal n (var i)
  var-NF zero    = con-NF⋆ C.1# *x+ con-NF⋆ C.0# ∷-NF lemma₇ _
  var-NF (suc i) = var-NF i ↑-NF

  _^-NF_ :  {n p}  Normal n p  (i : )  Normal n (p :^ i)
  p ^-NF zero  = con-NF⋆ C.1#    ∷-NF 1-homo
  p ^-NF suc n = p *-NF p ^-NF n ∷-NF refl

  normaliseOp :  (o : Op) {n p₁ p₂} 
                Normal n p₁  Normal n p₂  Normal n (p₁  op o  p₂)
  normaliseOp [+] = _+-NF_
  normaliseOp [*] = _*-NF_

  normalise :  {n} (p : Polynomial n)  Normal n p
  normalise (op o p₁ p₂) = normalise p₁  normaliseOp o  normalise p₂
  normalise (con c)      = con-NF⋆ c
  normalise (var i)      = var-NF i
  normalise (p :^ n)     = normalise p ^-NF n
  normalise (:- p)       = --NF normalise p

⟦_⟧↓_ :  {n}  Polynomial n  Vec carrier n  carrier
 p ⟧↓ ρ =  normalise p ⟧-NF ρ

------------------------------------------------------------------------
-- Correctness

private
  sem-pres-≈ :  op  sem op Preserves₂ _≈_  _≈_  _≈_
  sem-pres-≈ [+] = +-pres-≈
  sem-pres-≈ [*] = *-pres-≈

  raise-sem :  {n x} (p : Polynomial n) ρ 
               p :↑ 1  (x  ρ)   p  ρ
  raise-sem (op o p₁ p₂) ρ = raise-sem p₁ ρ  sem-pres-≈ o 
                             raise-sem p₂ ρ
  raise-sem (con c)      ρ = refl
  raise-sem (var x)      ρ = refl
  raise-sem (p :^ n)     ρ = raise-sem p ρ  ^-pres-≈  ≡-refl {x = n}
  raise-sem (:- p)       ρ = --pres-≈ (raise-sem p ρ)

  nf-sound :  {n p} (nf : Normal n p) ρ 
              nf ⟧-NF ρ   p  ρ
  nf-sound (nf ∷-NF eq)         ρ       = nf-sound nf ρ  trans  eq
  nf-sound (con-NF c)           ρ       = refl
  nf-sound (_↑-NF {p' = p'} nf) (x  ρ) =
    nf-sound nf ρ  trans  sym (raise-sem p' ρ)
  nf-sound (_*x+_ {c' = c'} nf₁ nf₂) (x  ρ) =
    (nf-sound nf₁ (x  ρ)  *-pres-≈  refl)
       +-pres-≈ 
    (nf-sound nf₂ ρ  trans  sym (raise-sem c' ρ))

-- Completeness can presumably also be proved (i.e. the normal forms
-- should be unique, if the casts are ignored).

------------------------------------------------------------------------
-- "Tactic"

prove :  {n} (ρ : Vec carrier n) p₁ p₂ 
         p₁ ⟧↓ ρ   p₂ ⟧↓ ρ 
         p₁   ρ   p₂   ρ
prove ρ p₁ p₂ eq =
  sym (nf-sound (normalise p₁) ρ)
     trans 
  eq
     trans 
  nf-sound (normalise p₂) ρ

-- For examples of how the function above can be used to
-- semi-automatically prove ring equalities, see
-- Prelude.RingSolver.Examples.