Sort with LPO leads to Exception "Comparison method violates its general contract!"

[quicquid]

I tried to have a look at expansion proof deskolemization for my nTapeX proofs. For the nTape2 variant, I get some errors I was looking to fix but when I checked the nTape3 proof, I got a very strange error message:

 gapt> deskolemizeET( nTape3.expansion_proof )
java.lang.IllegalArgumentException: Comparison method violates its general contract!
  at java.base/java.util.TimSort.mergeLo(TimSort.java:777)
  at java.base/java.util.TimSort.mergeAt(TimSort.java:514)
  at java.base/java.util.TimSort.mergeForceCollapse(TimSort.java:457)
  at java.base/java.util.TimSort.sort(TimSort.java:254)
  at java.base/java.util.Arrays.sort(Arrays.java:1440)
  at scala.collection.SeqLike.sorted(SeqLike.scala:656)
  at scala.collection.SeqLike.sorted$(SeqLike.scala:644)
  at scala.collection.AbstractSeq.sorted(Seq.scala:41)
  at scala.collection.SeqLike.sortWith(SeqLike.scala:609)
  at scala.collection.SeqLike.sortWith$(SeqLike.scala:609)
  at scala.collection.AbstractSeq.sortWith(Seq.scala:41)
  at scala.collection.SeqViewLike.$anonfun$sortWith$1(SeqViewLike.scala:261)
  at scala.collection.SeqViewLike$$anon$1.<init>(SeqViewLike.scala:193)
  at scala.collection.SeqViewLike.newForced(SeqViewLike.scala:193)
  at scala.collection.SeqViewLike.newForced$(SeqViewLike.scala:193)
  at scala.collection.SeqViewLike$AbstractTransformed.newForced(SeqViewLike.scala:37)
  at scala.collection.SeqViewLike.sortWith(SeqViewLike.scala:261)
  at scala.collection.SeqViewLike.sortWith$(SeqViewLike.scala:260)
  at scala.collection.SeqViewLike$AbstractTransformed.sortWith(SeqViewLike.scala:37)
  at gapt.proofs.expansion.removeSkolemCongruences$.simplCongrs(removeSkolemCongruences.scala:71)
  at gapt.proofs.expansion.removeSkolemCongruences$.remove(removeSkolemCongruences.scala:83)
  at gapt.proofs.expansion.removeSkolemCongruences$.apply(removeSkolemCongruences.scala:87)
  at gapt.proofs.expansion.deskolemizeET$.apply(deskolemizeET.scala:17)
  ... 25 elided

Looking into removeSkolemCongruences, the offending function defines:

val lpo = LPO( containedNames( congrs ).collect { case c: Const => c }.toSeq.sortBy( _.name ) )
def lt( a: Expr, b: Expr ): Boolean = lpo.lt( a, b, true )

and later on calls

sortWith( ( c1, c2 ) => lt( c1._1, c2._1 ) )

where the error occurs. I still need to look up if LPOs naturally generalize to higher order terms (which occur in there) but in any case, the compare should be the one throwing an error for cases where the ordering breaks, not the sorting algorithm.

[gebner]

This is strange. On the elements of congr, the function lt is both irreflexive and transitive.

It's not necessary to use a term order here at all. To be honest, the LPO was a bit of overkill. The function lt only needs to be a total order that includes the subterm relation (and it should be stable between different calls to simplCongrs).