fix(language): the case check reads each pair of relation columns as its own fact

CHANGELOG.md

@@ -13,6 +13,7 @@ it releases that version ([RELEASING.md](https://github.com/energy-models/mathsp
 ## Upcoming version
 
 - fix(language): the case check reads a comparison on a relation as false where the relation has no row ([#949](https://github.com/energy-models/mathspec/pull/949))
+- fix(language): the case check reads each pair of relation columns as its own fact ([#950](https://github.com/energy-models/mathspec/pull/950))
 - docs(language): a comparison on a relation is false where the relation has no row, whatever its operator ([#947](https://github.com/energy-models/mathspec/pull/947))
 - docs(language): the relations page shows a variable masked by a bare relation, so it exists only at the pairs the relation lists ([#946](https://github.com/energy-models/mathspec/pull/946))
 

src/mathspec/_exclusivity.py

@@ -150,20 +150,23 @@ class Subject:
     A comparison on a relation is split by the column it reads, because two
     columns of one row hold two values. The relation's own subject, with no
     column, is whether it has a row, and every comparison on it reads that too.
+    A comparison of two columns is keyed by both relations and both columns,
+    in one order whichever side each is written on.
     """
 
     kind: Literal['param', 'expression', 'dim', 'rank', 'relation', 'relation_pair', 'variable']
     name: str
     qualifier: str | None = None
-    #: A rank's group columns: two positions by one relation into different columns are two subjects.
+    #: A rank's group columns, or a pair's two columns: a different column is a different subject.
     group: tuple[str, ...] = ()
 
     def __str__(self) -> str:
         if self.kind == 'rank':
             within = f' within {self.qualifier}' if self.qualifier else ''
             return f'the position of {self.name}{within}'
         if self.kind == 'relation_pair':
-            return f'{self.name} vs {self.qualifier}'
+            column, other_column = self.group
+            return f'{self.name}[{column}] vs {self.qualifier}[{other_column}]'
         if self.kind == 'relation' and self.qualifier:
             return f'{self.name}[{self.qualifier}]'
         return self.name
@@ -338,8 +341,9 @@ def _subject_of(node: TypedCondition) -> Subject:
             return Subject('relation', name)
         case RelationComparison(name=name, column=column):
             return Subject('relation', name, column)
-        case RelationPairComparison(name=name, other=other):
-            return Subject('relation_pair', name, other)
+        case RelationPairComparison(name=name, column=column, other=other, other_column=other_column):
+            (name, column), (other, other_column) = sorted([(name, column), (other, other_column)])
+            return Subject('relation_pair', name, other, (column, other_column))
         case ExpressionComparison():
             return Subject('expression', 'a comparison of expressions')
         case CountComparison():

tests/test_exclusivity.py

@@ -365,7 +365,7 @@ def test_a_relation_proved_apart_stays_apart_on_every_row(self, seed: int):
             Subject('relation', 'ends', 'bus0'),
             Subject('relation', 'ends', 'bus1'),
         )
-        pair = Subject('relation_pair', 'ends', 'ends')
+        pair = Subject('relation_pair', 'ends', 'ends', ('bus0', 'bus1'))
         labels = ['north', 'south', 'east', 'west']
         grid = [{row: Special.NULL, bus0: 'north', bus1: 'north', pair: True}] + [
             {row: True, bus0: first, bus1: second, pair: first == second}
@@ -457,7 +457,7 @@ def test_a_comparison_and_the_missing_row_are_apart(self, cases: dict[str, str],
         [
             pytest.param(
                 {'loop': 'ends[bus0] == ends[bus1]', 'north': "ends[bus0] == 'north'"},
-                "where ends vs ends is equal, ends[bus0] is 'north'.",
+                "where ends[bus0] vs ends[bus1] is equal, ends[bus0] is 'north'.",
                 id='a-column-value-says-the-row-exists',
             ),
             pytest.param({'listed': 'ends', 'again': 'ends'}, 'where ends has a row.', id='the-bare-name-says-it'),
@@ -467,3 +467,27 @@ def test_a_row_both_cases_read_is_still_found(self, cases: dict[str, str], witne
         """The mirror: the row is there for both cases, and the witness says so once."""
         [refusal] = refusals(to_spec(NETWORK), cases)
         assert witness in refusal
+
+
+class TestAPairOfColumns:
+    """A comparison of two columns is one fact per pair of columns, whichever side each is written on."""
+
+    #: `ends` with a third column, so one relation offers more than one pair of columns.
+    THREE_ENDS: ClassVar[dict[str, Any]] = varied(NETWORK, **{'relations.ends.values.bus2': 'bus'})
+
+    def test_two_pairs_of_columns_are_two_facts(self):
+        """Both cases claim a line whose `bus0` and `bus1` are equal and whose `bus2` is another bus.
+
+        The prover keyed a comparison of two columns by the two relation names
+        only. `ends[bus0] == ends[bus1]` and `ends[bus0] != ends[bus2]` read one
+        fact, so it proved the two cases apart.
+        """
+        [refusal] = refusals(
+            to_spec(self.THREE_ENDS), {'a': 'ends[bus0] == ends[bus1]', 'b': 'ends[bus0] != ends[bus2]'}
+        )
+        assert 'where ends[bus0] vs ends[bus1] is equal, ends[bus0] vs ends[bus2] is different.' in refusal
+
+    def test_one_pair_written_both_ways_is_one_fact(self):
+        assert refusals(to_spec(NETWORK), {'a': 'ends[bus0] == ends[bus1]', 'b': 'ends[bus1] != ends[bus0]'}) == [], (
+            'a pair of columns with its sides swapped is the same pair'
+        )