Drake: Consistency among ==, <=, >=, <, >, != operators for symbolic expressions/formulas ....

[mitiguy]

Suggested improvements for symbolics.

1. The following operators should have consistent behavior:
   ==, <=, >=, <, >, !=

2. When expressions/formulas involving these operators are evaluated to a C++ bool (true or false), whether with an empty map or partial map or full map, it would be helpful to:
   (a) return "true" if the current algorithms in Drake surely know they are _mathematically_ true.
   (b) return "false" if the current algorithms in Drake surely know they are _mathematically_ false.
   (c) throw an exception if the current algorithms in Drake are unsure.

---

Below is code that gave surprising results:

  const symbolic::Variable x("x");
  symbolic::Expression e = x;
  Bool<symbolic::Expression> test_equal = e == 2;
  Bool<symbolic::Expression> test_less_than_equal = e <= 2;

  // The 1st line below does not throw an exception (I think it should).
  // The 2nd line below does throw an exception (I agree it should).
  // The 3rd line below can be untrue.  What if x is 2 (unlikely, but possible)?
  bool is_equal = ExtractBoolOrThrow(test_equal);  // Should throw ?
  EXPECT_THROW(ExtractBoolOrThrow(test_less_than_equal), std::runtime_error);
  EXPECT_FALSE(is_equal);  // Possibly incorrect result here.

  // The next example (next 5 lines) work as expected.
  e = 2*x + 3;
  test_equal = e == 3 + 2*x;
  test_less_than_equal = e <= 3 + 2*x;
  EXPECT_TRUE(ExtractBoolOrThrow(test_equal));
  EXPECT_TRUE(ExtractBoolOrThrow(test_less_than_equal));

  // The next example (next 3 lines) did _not_ work as expected.
  // After compile/link/running this test, the following error message appeared:
  // Value of: ExtractBoolOrThrow(test_equal)
  // Actual: false
  // Expected: true
  // Since the expressions 2*(x+3) and 6 + 2*x _are_ equal, the return value
  // should be true.  Perhaps the simplifier was unable to determine that these
  // expressions are equal (assuming conventional mathematical meaning of ==).
  // If the simplifier could not determine whether or not these expressions are
  // mathematically equal, an exception should be thrown (not return false).
  e = 2*(x + 3);
  test_equal = e == 6 + 2*x;
  EXPECT_TRUE(ExtractBoolOrThrow(test_equal));  // This returned false !

  // The next example (next 2 lines) is inconsistent with the previous example.
  // After compile/link/running this test, the following error message appeared:
  // C++ exception with description "The following environment does not have an
  // entry for the variable x".
  // Perhaps Drake's symbolic simplifier could not determine whether or not
  // these expressions are mathematically equal.  If this is the case, then I
  // agree that an exception should be thrown.  However, if Drake's symbolic
  // simplifier could determine that they are mathematically equal, the return
  // value should be true.  In general, throwing an exception should be a last-
  // case scenario when equality or inequality is indeterminate.
  // Note: Soonho pointed us towards Richardson's theorem which states that it
  // can be undecidable whether two mathematical expressions are equal.
  // https://en.wikipedia.org/wiki/Richardson%27s_theorem.
  // Hence, there are occassions when throwing an exception is correct.
  test_less_than_equal = e <= 6 + 2*x;
  EXPECT_TRUE(ExtractBoolOrThrow(test_less_than_equal));  // Throws exception.

---

Note: Somewhat related (perhaps confusing) lengthy discussion (Soonho/Sean/Paul) in reviewable:
https://reviewable.io/reviews/RobotLocomotion/drake/9037#-LH4NLNU3n3vu_WdV68e

[soonho-tri]

/cc @SeanCurtis-TRI, @sherm1, @jwnimmer-tri as you were included in the email thread.

I see your points. I'll change the following implementation of FormulaEq::Evaluate (and also FormulaNeq::Evaluate)

https://github.com/RobotLocomotion/drake/blob/749e93a6f81e08c77b6a0504348430ed44374059/common/symbolic_formula_cell.cc#L265-L268

to be:

bool FormulaEq::Evaluate(const Environment& env) const {
  return get_lhs_expression().Evaluate(env) ==
         get_rhs_expression().Evaluate(env);
}

This should give you consistent behaviors across the relational operators (<,<=,>,>=,==,!=). That is, (e1 rop e2).Evaluate(env) will throw if there is a variable in e1 rop e2 whose value is not found in env (modulo simplifications at the construction time).

I'll use some of your examples when I write new test cases.

[sherm1]

Thanks, Soonho! Presumably you could relax that requirement at some point since the truth of some formulas can be determined without knowing values, like a == a or sin(x) <= 1.

[soonho-tri]

FYI, a == a works as we simplify it to True at construction. If we remove this simplification, a user has to call this simplifier explicitly before evaluating it. Otherwise, it will throw.

sin(x) <= 1 is another interesting case as we need a simplifier at the formula level (e.g. sin(x) <=1 ↦ True).

[sherm1]

Gotcha, sounds good -- and just to be clear, I'm _not_ requesting sin(x) <= 1 ↦ True! That was just a made-up example.