Use eq_symmetric rule in elaboration

carcara/src/checker/rules/extras.rs

@@ -47,9 +47,8 @@ pub fn not_symm(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
 }
 
 pub fn eq_symmetric(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
-    assert_clause_len(conclusion, 2)?;
-    let (t_1, u_1) = match_term_err!((not (= t u)) = &conclusion[0])?;
-    let (u_2, t_2) = match_term_err!((= u t) = &conclusion[1])?;
+    assert_clause_len(conclusion, 1)?;
+    let ((t_1, u_1), (u_2, t_2)) = match_term_err!((= (= t u) (= u t)) = &conclusion[0])?;
     assert_eq(t_1, t_2)?;
     assert_eq(u_1, u_2)
 }
@@ -278,12 +277,12 @@ mod tests {
                 (declare-fun b () T)
             ",
             "Simple working examples" {
-                "(step t1 (cl (not (= b a)) (= a b)) :rule eq_symmetric)": true,
-                "(step t1 (cl (not (= a a)) (= a a)) :rule eq_symmetric)": true,
+                "(step t1 (cl (= (= b a) (= a b))) :rule eq_symmetric)": true,
+                "(step t1 (cl (= (= a a) (= a a))) :rule eq_symmetric)": true,
             }
             "Failing examples" {
-                "(step t1 (cl (not (= a b)) (= a b)) :rule eq_symmetric)": false,
-                "(step t1 (cl (not (= a b)) (not (= b a))) :rule eq_symmetric)": false,
+                "(step t1 (cl (= (= a b) (= a b))) :rule eq_symmetric)": false,
+                "(step t1 (cl (= (not (= a b)) (not (= b a)))) :rule eq_symmetric)": false,
             }
         }
     }

carcara/src/checker/rules/simplification.rs

@@ -347,18 +347,6 @@ pub fn equiv_simplify(args: RuleArgs) -> RuleResult {
 
             // phi = false => ¬phi
             (= phi_1 false): (phi_1, _) => build_term!(pool, (not {phi_1.clone()})),
-
-            // This is a special case for the `equiv_simplify` rule that was added to make
-            // elaboration of polyequality less verbose. This transformation can very easily lead to
-            // cycles, so it must always be the last transformation rule. Unfortunately, this means
-            // that failed simplifications in the `equiv_simplify` rule will frequently reach this
-            // transformation and reach a cycle, in which case the error message may be a bit
-            // confusing.
-            //
-            // phi_1 = phi_2 => phi_2 = phi_1
-            (= phi_1 phi_2): (phi_1, phi_2) => {
-                build_term!(pool, (= {phi_2.clone()} {phi_1.clone()}))
-            },
         })
     })
 }

carcara/src/elaborator/polyeq.rs

@@ -245,7 +245,7 @@ impl<'a> PolyeqElaborator<'a> {
         //     b := (= y' x')
         // The simpler case that we have to consider is when x equals x' and y equals y'
         // (syntactically), that is, if we just flip the b equality, the terms will be
-        // syntactically equal. In this case, we can simply introduce an `equiv_simplify` step that
+        // syntactically equal. In this case, we can simply introduce an `eq_symmetric` step that
         // derives `(= (= x y) (= y x))`.
         //
         // The more complex case happens when x is equal to x', but they are not syntactically
@@ -256,7 +256,7 @@ impl<'a> PolyeqElaborator<'a> {
         // In this case, we need to elaborate the polyequality between x and x' (or y and y'), and
         // from that, prove that `(= (= x y) (= y' x'))`. We do that by first proving that
         // `(= x x')` (1) and `(= y y')` (2). Then, we introduce a `cong` step that uses (1) and (2)
-        // to show that `(= (= x y) (= x' y'))` (3). After that, we add an `equiv_simplify` step
+        // to show that `(= (= x y) (= x' y'))` (3). After that, we add an `eq_symmetric` step
         // that derives `(= (= x' y') (= y' x'))` (4). Finally, we introduce a `trans` step with
         // premises (3) and (4) that proves `(= (= x y) (= y' x'))`. The general format looks like
         // this:
@@ -266,21 +266,21 @@ impl<'a> PolyeqElaborator<'a> {
         //     ...
         //     (step t2 (cl (= y y')) ...)
         //     (step t3 (cl (= (= x y) (= x' y'))) :rule cong :premises (t1 t2))
-        //     (step t4 (cl (= (= x' y') (= y' x'))) :rule equiv_simplify)
+        //     (step t4 (cl (= (= x' y') (= y' x'))) :rule eq_symmetric)
         //     (step t5 (cl (= (= x y) (= y' x'))) :rule trans :premises (t3 t4))
         //
         // If x equals x' syntactically, we can omit the derivation of step `t1`, and remove that
         // premise from step `t3`. We can do the same with step `t2` if y equals y' syntactically.
         // Of course, if both x == x' and y == y', we fallback to the simpler case, where we only
-        // need to introduce an `equiv_simplify` step.
+        // need to introduce an `eq_symmetric` step.
 
         // Simpler case
         if a_left == b_right && a_right == b_left {
             return Rc::new(ProofNode::Step(StepNode {
                 id: self.ids.next_id(),
                 depth: self.depth(),
                 clause: vec![build_term!(pool, (= {a} {b}))],
-                rule: "equiv_simplify".to_owned(),
+                rule: "eq_symmetric".to_owned(),
                 ..Default::default()
             }));
         }
@@ -295,20 +295,11 @@ impl<'a> PolyeqElaborator<'a> {
             (&[a_left, a_right], &[b_right, b_left]),
         );
 
-        // It might be the case that `x'` is syntactically equal to `y'`, which would mean that we
-        // are adding an `equiv_simplify` step to prove a reflexivity step. This is not valid
-        // according to the `equiv_simplify` specification, so we must change the rule to `refl` in
-        // this case.
-        let rule = if b == flipped_b {
-            "refl".to_owned()
-        } else {
-            "equiv_simplify".to_owned()
-        };
         let equiv_step = Rc::new(ProofNode::Step(StepNode {
             id: self.ids.next_id(),
             depth: self.depth(),
             clause: vec![build_term!(pool, (= {flipped_b} {b.clone()}))],
-            rule,
+            rule: "eq_symmetric".to_owned(),
             ..Default::default()
         }));
 

carcara/src/elaborator/transitivity.rs

@@ -216,20 +216,28 @@ fn flip_eq_transitive_premises(
         .iter()
         .map(|&i| {
             let (a, b) = match_term!((not (= a b)) = new_clause[i]).unwrap();
-            let pivot = build_term!(pool, (= {a.clone()} {b.clone()}));
-            let to_introduce = build_term!(pool, (not (= {b.clone()} {a.clone()})));
-            let clause = vec![to_introduce.clone(), pivot.clone()];
-            let new_step = Rc::new(ProofNode::Step(StepNode {
+
+            let a_eq_b = build_term!(pool, (= {a.clone()} {b.clone()}));
+            let b_eq_a = build_term!(pool, (= {b.clone()} {a.clone()}));
+            let eq_symm_step = Rc::new(ProofNode::Step(StepNode {
                 id: ids.next_id(),
                 depth,
-                clause,
+                clause: vec![build_term!(pool, (= {a_eq_b.clone()} {b_eq_a.clone()}))],
                 rule: "eq_symmetric".to_owned(),
-                premises: Vec::new(),
-                args: Vec::new(),
-                discharge: Vec::new(),
-                previous_step: None,
+                ..StepNode::default()
+            }));
+
+            let not_b_eq_a = build_term!(pool, (not {(b_eq_a)}));
+            let equiv2_step = Rc::new(ProofNode::Step(StepNode {
+                id: ids.next_id(),
+                depth,
+                clause: vec![a_eq_b.clone(), not_b_eq_a.clone()],
+                rule: "equiv2".to_owned(),
+                premises: vec![eq_symm_step],
+                ..StepNode::default()
             }));
-            (new_step, pivot, to_introduce)
+
+            (equiv2_step, a_eq_b, not_b_eq_a)
         })
         .collect();