Don't allow polyequal outside assumes

Author: bpandreotti

carcara/src/checker/mod.rs

@@ -334,6 +334,7 @@ impl<'c> ProofChecker<'c> {
             previous_command,
             discharge: &discharge,
             polyeq_time: &mut polyeq_time,
+            allow_polyeq: !self.config.isabelle_mode,
         };
 
         rule(rule_args)?;

carcara/src/checker/parallel/mod.rs

@@ -395,6 +395,7 @@ impl<'c> ParallelProofChecker<'c> {
             previous_command,
             discharge: &discharge,
             polyeq_time: &mut polyeq_time,
+            allow_polyeq: !self.config.isabelle_mode,
         };
 
         rule(rule_args)?;

carcara/src/checker/rules/mod.rs

@@ -26,6 +26,8 @@ pub struct RuleArgs<'a> {
     pub(super) discharge: &'a [&'a ProofCommand],
 
     pub(super) polyeq_time: &'a mut Duration,
+
+    pub(super) allow_polyeq: bool,
 }
 
 #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]

carcara/src/checker/rules/reflexivity.rs

@@ -13,17 +13,26 @@ pub fn refl(
         pool,
         context,
         polyeq_time,
+        allow_polyeq,
         ..
     }: RuleArgs,
 ) -> RuleResult {
+    let mut compare = |a, b| -> bool {
+        if allow_polyeq {
+            alpha_equiv(a, b, polyeq_time)
+        } else {
+            a == b
+        }
+    };
+
     assert_clause_len(conclusion, 1)?;
 
     let (left, right) = match_term_err!((= l r) = &conclusion[0])?;
 
     // If the two terms are directly identical, we don't need to do any more work. We make sure to
     // do this check before we try to get the context substitution, because `refl` can be used
     // outside of any subproof
-    if alpha_equiv(left, right, polyeq_time) {
+    if compare(left, right) {
         return Ok(());
     }
 
@@ -36,10 +45,9 @@ pub fn refl(
     // don't compute the new left and right terms until they are needed, to avoid doing unnecessary
     // work
     let new_left = context.apply(pool, left);
-    let result = alpha_equiv(&new_left, right, polyeq_time) || {
+    let result = compare(&new_left, right) || {
         let new_right = context.apply(pool, right);
-        alpha_equiv(left, &new_right, polyeq_time)
-            || alpha_equiv(&new_left, &new_right, polyeq_time)
+        compare(left, &new_right) || compare(&new_left, &new_right)
     };
     rassert!(
         result,

carcara/src/checker/rules/subproof.rs

@@ -13,6 +13,7 @@ pub fn subproof(
         previous_command,
         discharge,
         polyeq_time,
+        allow_polyeq,
         ..
     }: RuleArgs,
 ) -> RuleResult {
@@ -44,7 +45,11 @@ pub fn subproof(
         }
     };
 
-    assert_polyeq(conclusion.last().unwrap(), &phi, polyeq_time)
+    if allow_polyeq {
+        assert_polyeq(conclusion.last().unwrap(), &phi, polyeq_time)
+    } else {
+        assert_eq(conclusion.last().unwrap(), &phi)
+    }
 }
 
 pub fn bind(

carcara/src/checker/rules/tautology.rs

@@ -1,6 +1,6 @@
 use super::{
-    assert_clause_len, assert_eq, assert_num_premises, assert_polyeq, get_premise_term,
-    CheckerError, RuleArgs, RuleResult,
+    assert_clause_len, assert_eq, assert_num_premises, get_premise_term, CheckerError, RuleArgs,
+    RuleResult,
 };
 use crate::{ast::*, checker::rules::assert_operation_len};
 
@@ -258,7 +258,22 @@ pub fn not_ite2(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
     assert_eq(phi_2, conclusion[1].remove_negation_err()?)
 }
 
-pub fn ite_intro(RuleArgs { conclusion, polyeq_time, .. }: RuleArgs) -> RuleResult {
+pub fn ite_intro(
+    RuleArgs {
+        conclusion,
+        polyeq_time,
+        allow_polyeq,
+        ..
+    }: RuleArgs,
+) -> RuleResult {
+    let mut compare = |a, b| -> bool {
+        if allow_polyeq {
+            polyeq(a, b, polyeq_time)
+        } else {
+            a == b
+        }
+    };
+
     assert_clause_len(conclusion, 1)?;
 
     let (root_term, right_side) = match_term_err!((= t u) = &conclusion[0])?;
@@ -278,25 +293,25 @@ pub fn ite_intro(RuleArgs { conclusion, polyeq_time, .. }: RuleArgs) -> RuleResu
     // ```
     // For cases like this, we first check if `t` equals the right side term modulo reordering of
     // equalities. If not, we unwrap the conjunction and continue checking the rule normally.
-    if polyeq(root_term, right_side, polyeq_time) {
+    if compare(root_term, right_side) {
         return Ok(());
     }
     let us = match_term_err!((and ...) = right_side)?;
 
     // `us` must be a conjunction where the first term is the root term
-    assert_polyeq(&us[0], root_term, polyeq_time)?;
+    if !allow_polyeq || !compare(&us[0], root_term) {
+        assert_eq(&us[0], root_term)?;
+    }
 
     // The remaining terms in `us` should be of the correct form
     for u_i in &us[1..] {
         let (cond, (a, b), (c, d)) = match_term_err!((ite cond (= a b) (= c d)) = u_i)?;
 
         let mut is_valid = |r_1, s_1, r_2, s_2| {
             // s_1 == s_2 == (ite cond r_1 r_2)
-            if polyeq(s_1, s_2, polyeq_time) {
+            if compare(s_1, s_2) {
                 if let Some((a, b, c)) = match_term!((ite a b c) = s_1) {
-                    return polyeq(a, cond, polyeq_time)
-                        && polyeq(b, r_1, polyeq_time)
-                        && polyeq(c, r_2, polyeq_time);
+                    return compare(a, cond) && compare(b, r_1) && compare(c, r_2);
                 }
             }
             false