Edit detail for SandBoxInequation revision 6 of 11

spad
)abbrev domain NE Inequation
++ Author: Bill Page
++ Based on: Equation by Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: June 2008
++ Basic Operations: ~=
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: inequation
++ Examples:
++ References:
++ Description:
++   Inequations as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "~=" to "inequation".  Otherwise, it will
--   find a modemap for "~=" in the domain of the arguments.
Inequation(S: Type): public == private where
  public ==> Type with
    "~=": (S, S) -> $
        ++ a~=b creates an inequation.
    inequation: (S, S) -> $
        ++ inequation(a,b) creates an inequation.
    _not: $ -> Equation(S)
    swap: $ -> $
        ++ swap(neq) interchanges left and right hand side of inequation neq.
    lhs: $ -> S
        ++ lhs(neq) returns the left hand side of inequation neq.
    rhs: $ -> S
        ++ rhs(neq) returns the right hand side of inequation neq.
    map: (S -> S, $) -> $
        ++ map(f,neq) constructs a new inequation by applying f to both
        ++ sides of neq. (f must be an injection)
    if S has InnerEvalable(Symbol,S) then
             InnerEvalable(Symbol,S)
    if S has SetCategory then
        SetCategory
        CoercibleTo Boolean
        if S has Evalable(S) then
           eval: ($, Equation S) -> $
               ++ eval(neq, x=f) replaces x by f in inequation neq.
           eval: ($, List Equation S) -> $
               ++ eval(neq, [x1=v1, ... xn=vn]) replaces xi by vi in inequation neq.
    if S has AbelianSemiGroup then
        "+": (S, $) -> $
            ++ x+neq produces a new inequation by adding x to both sides of
            ++ inequation neq.
        "+": ($, S) -> $
            ++ neq+x produces a new inequation by adding x to both sides of
            ++ inequation neq.
    if S has AbelianGroup then
        "-": $ -> $
        leftZero : $ -> $
          ++ leftZero(neq) subtracts the left hand side.
        rightZero : $ -> $
          ++ rightZero(neq) subtracts the right hand side.
        "-": (S, $) -> $
            ++ x-neq produces a new equation by subtracting both sides of
            ++ equation neq from x.
        "-": ($, S) -> $
            ++ neq-x produces a new equation by subtracting x from  both sides of
            ++ equation neq.
    if S has Monoid then
        recip: $ -> Union($,"failed")
        leftOne : $ -> Union($,"failed")
          ++ leftOne(neq) divides by the left hand side, if possible.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(neq) divides by the right hand side, if possible.
    if S has Group then
        leftOne : $ -> Union($,"failed")
          ++ leftOne(neq) divides by the left hand side.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(neq) divides by the right hand side.
    if S has IntegralDomain then
      factorAndSplit : $ -> List $
        ++ factorAndSplit(neq) make the right hand side 0 and
        ++ factors the new left hand side. Each factor is equated
        ++ to 0 and put into the resulting list without repetitions.
    if S has ExpressionSpace then
        subst: ($, Equation S) -> $
             ++ subst(neq1,eq2) substitutes eq2 into both sides of neq1
             ++ the lhs of eq2 should be a kernel
  private ==> add
    Rep := Record(lhs: S, rhs: S)
    neq1,neq2, neq: $
    eq2: Equation S
    s : S
    if S has IntegralDomain then
        factorAndSplit neq ==
          (S has factor : S -> Factored S) =>
            neq0 := rightZero neq
            [inequation(rcf.factor,0) for rcf in factors factor lhs neq0]
          [neq]
    l:S ~= r:S      == [l, r]
    inequation(l, r) == [l, r]    -- hack!  See comment above.
    _not neq  == equation(neq.lhs,neq.rhs)
    lhs neq  == neq.lhs
    rhs neq  == neq.rhs
    swap neq == [rhs neq, lhs neq]
    map(fn, neq)   == inequation(fn(neq.lhs), fn(neq.rhs))
    if S has InnerEvalable(Symbol,S) then
        s:Symbol
        ls:List Symbol
        x:S
        lx:List S
        eval(neq,s,x) == eval(neq.lhs,s,x) ~= eval(neq.rhs,s,x)
        eval(neq,ls,lx) == eval(neq.lhs,ls,lx) ~= eval(neq.rhs,ls,lx)
    if S has Evalable(S) then
        eval(neq1:$, eqn2:Equation S):$ ==
           eval(neq1.lhs, eqn2) ~= eval(neq1.rhs, eqn2)
        eval(neq1:$, leqn2:List Equation S):$ ==
           eval(neq1.lhs, leqn2) ~= eval(neq1.rhs, leqn2)
    if S has SetCategory then
        neq1 = neq2 == (neq1.lhs = neq2.lhs)@Boolean and
                     (neq1.rhs = neq2.rhs)@Boolean
        coerce(neq:$):OutputForm == blankSeparate([neq.lhs::OutputForm, "~=", neq.rhs::OutputForm])$OutputForm
        coerce(neq:$):Boolean == neq.lhs ~= neq.rhs
    if S has AbelianSemiGroup then
        s + neq2 == s+neq2.lhs ~= s+neq2.rhs
        neq1 + s == neq1.lhs+s ~= neq1.rhs+s
    if S has AbelianGroup then
        - neq == -neq.lhs ~= -neq.rhs
        s - neq2 == s-neq2.lhs ~= s-neq2.rhs
        neq1 - s == neq1.lhs-s ~= neq1.rhs-s
        leftZero neq == 0 ~= rhs neq - lhs neq
        rightZero neq == lhs neq - rhs neq ~= 0
    if S has Monoid then
        recip neq ==
          (lh := recip lhs neq) case "failed" => "failed"
          (rh := recip rhs neq) case "failed" => "failed"
          [lh :: S, rh :: S]
        leftOne neq ==
          (re := recip lhs neq) case "failed" => "failed"
          1 ~= rhs neq * re
        rightOne neq ==
          (re := recip rhs neq) case "failed" => "failed"
          lhs neq * re ~= 1
    if S has Group then
        leftOne neq == 1 ~= rhs neq * inv rhs neq
        rightOne neq == lhs neq * inv rhs neq ~= 1
    if S has IntegralDomain then
        factorAndSplit neq ==
          (S has factor : S -> Factored S) =>
            neq0 := rightZero neq
            [inequation(rcf.factor,0) for rcf in factors factor lhs neq0]
          (S has Polynomial Integer) =>
            neq0 := rightZero neq
            MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _
               Integer, Polynomial Integer)
            p : Polynomial Integer := (lhs neq0) pretend Polynomial Integer
            [inequation((rcf.factor) pretend S,0) for rcf in factors factor(p)$MF]
          [neq]
    if S has ExpressionSpace then
        subst(neq1,eq2) ==
            [subst(lhs neq1,eq2),subst(rhs neq1,eq2)]

axiom
)set output tex on
)set output algebra on
inequation(a,b)
   (1)  a ~= b

axiom
t1:=inequation(2,3)
   (2)  2 ~= 3

axiom
t1::Boolean
   (3)  true

axiom
t2:=equation(2,3)
   (4)  2= 3

axiom
t2::Boolean
   (5)  false

axiom
s1:= not t1
   (6)  2= 3

axiom
s1::Boolean
   (7)  false

axiom
t1*4
   There are 34 exposed and 23 unexposed library operations named *
      having 2 argument(s) but none was determined to be applicable.
      Use HyperDoc Browse, or issue
                                )display op *
      to learn more about the available operations. Perhaps
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.
   Cannot find a definition or applicable library operation named *
      with argument type(s)
                         Inequation PositiveInteger
                               PositiveInteger
      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
t1+t2
   There are 13 exposed and 5 unexposed library operations named +
      having 2 argument(s) but none was determined to be applicable.
      Use HyperDoc Browse, or issue
                                )display op +
      to learn more about the available operations. Perhaps
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.
   Cannot find a definition or applicable library operation named +
      with argument type(s)
                         Inequation PositiveInteger
                          Equation PositiveInteger
      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
t1*t2
   There are 34 exposed and 23 unexposed library operations named *
      having 2 argument(s) but none was determined to be applicable.
      Use HyperDoc Browse, or issue
                                )display op *
      to learn more about the available operations. Perhaps
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.
   Cannot find a definition or applicable library operation named *
      with argument type(s)
                         Inequation PositiveInteger
                          Equation PositiveInteger
      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.

spad
)abbrev domain LT Inequality
++ Author: Bill Page
++ Based on: Equation by Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: June 2008
++ Basic Operations: <
++ Related Domains: Equation Inequation
++ Also See:
++ AMS Classifications:
++ Keywords: inequality
++ Examples:
++ References:
++ Description:
++   Inequalities as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "x < y" to "inequality(x,y)",
--   "x > y" to "inequality(y,x)", "x <= y" to "not inequality(y,x)"
--   and "x >= y" to "not inequality(x,y)".
Inequality(S: Type): public == private where
  public ==> Type with
    "<": (S, S) -> $
        ++ a~=b creates an inequality.
    inequality: (S, S) -> $
        ++ equality(a,b) creates an inequality.
    _not: $ -> $
    lhs: $ -> S
        ++ lhs(leq) returns the left hand side of inequality leq.
    rhs: $ -> S
        ++ rhs(leq) returns the right hand side of inequality leq.
    if S has InnerEvalable(Symbol,S) then
             InnerEvalable(Symbol,S)
    if S has OrderedSet then
        SetCategory
        CoercibleTo Boolean
        if S has Evalable(S) then
           eval: ($, Equation S) -> $
               ++ eval(leq, x=f) replaces x by f in inequality leq.
           eval: ($, List Equation S) -> $
               ++ eval(leq, [x1=v1, ... xn=vn]) replaces xi by vi in inequality leq.
        coerce:Union($,Equation S)->OutputForm
    if S has AbelianSemiGroup then
        "+": (S, $) -> $
            ++ x+leq produces a new inequality by adding x to both sides of
            ++ inequality leq.
        "+": ($, S) -> $
            ++ leq+x produces a new inequality by adding x to both sides of
            ++ inequality leq.
    if S has AbelianGroup then
        "-": $ -> $
        leftZero : $ -> $
          ++ leftZero(leq) subtracts the left hand side.
        rightZero : $ -> $
          ++ rightZero(leq) subtracts the right hand side.
        "-": (S, $) -> $
            ++ x-leq produces a new inquality by subtracting both sides of
            ++ inequality leq from x.
        "-": ($, S) -> $
            ++ leq-x produces a new inequality by subtracting x from both sides of
            ++ inequality leq.
    if S has ExpressionSpace then
        subst: ($, Equation S) -> $
             ++ subst(leq,eq2) substitutes eq2 into both sides of leq
             ++ the lhs of eq2 should be a kernel
  private ==> add
    Rep := Record(lhs: S, cmp:String ,rhs: S)
    leq1,leq2,leq: $
    eq2: Equation S
    s : S
    l:S < r:S      == [l, "<", r]
    inequality(l, r) == [l, "<",  r]    -- hack!  See comment above.
    _not(leq:$):$ ==
       leq.cmp="<" => [leq.lhs, ">=", leq.rhs]
       [leq.lhs, "<", leq.rhs]
    lhs leq        == leq.lhs
    rhs leq        == leq.rhs
    if S has InnerEvalable(Symbol,S) then
        s:Symbol
        ls:List Symbol
        x:S
        lx:List S
        eval(leq,s,x) == eval(leq.lhs,s,x) < eval(leq.rhs,s,x)
        eval(leq,ls,lx) == eval(leq.lhs,ls,lx) < eval(leq.rhs,ls,lx)
    if S has Evalable(S) then
        eval(leq:$, eqn2:Equation S):$ ==
           eval(leq.lhs, eqn2) < eval(leq.rhs, eqn2)
        eval(leq:$, eqn2:List Equation S):$ ==
           eval(leq.lhs, eqn2) < eval(leq.rhs, eqn2)
    if S has OrderedSet then
        leq1 = leq2 == (leq1.lhs = leq2.lhs)@Boolean and
                     (leq1.rhs = leq2.rhs)@Boolean
        coerce(leq:$):OutputForm ==
            leq.cmp="<" => blankSeparate([leq.lhs::OutputForm, "<", leq.rhs::OutputForm])$OutputForm
            blankSeparate([leq.lhs::OutputForm, ">=", leq.rhs::OutputForm])$OutputForm
        coerce(leq:$):Boolean ==
            leq.cmp="<" => leq.lhs < leq.rhs
            (leq.lhs >= leq.rhs)$S
    if S has AbelianSemiGroup then
        s + leq2 == s+leq2.lhs < s+leq2.rhs
        leq1 + s == leq1.lhs+s < leq1.rhs+s
    if S has AbelianGroup then
        - leq ==  (-rhs leq) < (- lhs leq)
        leftZero leq == 0 < rhs leq - lhs leq
        rightZero leq == lhs leq - rhs leq < 0
        s - leq2 ==  s-leq2.rhs < s-leq2.lhs
        leq1 - s == leq1.lhs-s < leq1.rhs-s
    if S has ExpressionSpace then
        subst(leq1,eq2) ==
            [subst(lhs leq1,eq2),leq1.cmp,subst(rhs leq1,eq2)]

axiom
)set output tex on
)set output algebra on
w1:=inequality(a,b)
   (8)  a < b

axiom
w2:=inequality(2,3)
   (9)  2 < 3

axiom
w2::Boolean
   (10)  true

axiom
not w1
   (11)  a >= b

axiom
w3:=not w2
   (12)  2 >= 3

axiom
w3::Boolean
   (13)  false