scala - Leon: カスタム `==` 演算子の使い方は?

Question

レオンと有理数で作業しているときに、次の問題に遭遇しました。inverse1関数の検証は反例を示しますが、inverse2検証中にはあまり意味がありません。

import leon.lang._

case class Rational (n: BigInt, d: BigInt) {

  def +(that: Rational): Rational = {
    require(isRational && that.isRational)
    Rational(n * that.d + that.n * d, d * that.d)
  } ensuring { _.isRational }

  def *(that: Rational): Rational = {
    require(isRational && that.isRational)
    Rational(n * that.n, d * that.d)
  } ensuring { _.isRational }

  def <=(that: Rational): Boolean = {
    require(isRational && that.isRational)
    if (that.d * d > 0)
      n * that.d <= d * that.n
    else
      n * that.d >= d * that.n
  }

  def ==(that: Rational): Boolean = {
    require(isRational && that.isRational)
    //that <= this && this <= that
    true // for testing purpose of course!
  }

  // fails to verify
  def inverse1: Rational = {
    require(isRational && nonZero)
    Rational(d, n)
  }.ensuring { res => res.isRational && res.nonZero && res * this == Rational(1, 1) }

  // verifies
  def inverse2: Rational = {
    require(isRational && nonZero)
    Rational(d, n)
  }.ensuring { res => res.isRational && res.nonZero /*&& res * this == Rational(1, 1)*/ }

  def isRational = !(d == 0)
  def nonZero = n != 0

}

レオンが私に与える反例はこれです：

[  Info  ]  - Now considering 'postcondition' VC for Rational$inverse1 @33:16...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   $this -> Rational(-2, -2)

しかし、数学的に言えば意味がありません。

私はこのコードが==私が定義した演算子を呼び出すことを期待していましたが、これは常に返さtrueれ、関数は検証されないため、そうではないと考える傾向があります...

誰かがこのプログラムの何が問題なのか、または私の Scala/leon の理解を示すことができますか? ありがとう。