Edit detail for SandBoxInequation revision 4 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 lessThan(y,x)"
--   and "x >= y" to "not lessThan(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: $ -> Union($, Equation S)
    _not: Union($, Equation S) -> $
    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 SetCategory 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.
    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 leqn.
    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, rhs: S)
    leq1,leq2,leg: $
    eq2: Equation S
    s : S
    l:S < r:S      == [l, r]
    inequality(l, r) == [l, r]    -- hack!  See comment above.
    not(leq:$):Union($,Equation S) == (leq.rhs < leq.lhs) pretend Union($,Equation S)
    not(gre:Union($,Equation S)):$ ==
      leq := gre pretend $
      leq.rhs < leq.lhs
    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 SetCategory then
        leq1 = leq2 == (leq1.lhs = leq2.lhs)@Boolean and
                     (leq1.rhs = leq2.rhs)@Boolean
        coerce(leq:$):OutputForm == blankSeparate([eqn.lhs::OutputForm, "<", eqn.rhs::OutputForm])$OutputForm
        coerce(leq:Union($,Equation S):OutputForm == blankSeparate([eqn.lhs::OutputForm, "<=", eqn.rhs::OutputForm])$OutputForm
        coerce(leq:$):Boolean == leq.lhs < leq.rhs
    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),subst(rhs leq1,eq2)]

axiom
)set output tex on
)set output algebra on
lessThan(a,b)
   There are no library operations named lessThan
      Use HyperDoc Browse or issue
                              )what op lessThan
      to learn if there is any operation containing " lessThan " in its
      name.
   Cannot find a definition or applicable library operation named
      lessThan with argument type(s)
                                 Variable a
                                 Variable b
      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
t1:=lessThan(2,3)
   There are no library operations named lessThan
      Use HyperDoc Browse or issue
                              )what op lessThan
      to learn if there is any operation containing " lessThan " in its
      name.
   Cannot find a definition or applicable library operation named
      lessThan with argument type(s)
                               PositiveInteger
                               PositiveInteger
      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
t1::Boolean
   (8)  true

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

axiom
t2::Boolean
   (10)  false