and_intro checking (extra rule)

carcara/src/checker/rules/extras.rs

@@ -86,6 +86,30 @@ pub fn weakening(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult
     Ok(())
 }
 
+pub fn and_intro(RuleArgs { conclusion, premises, pool, .. }: RuleArgs) -> RuleResult {
+    assert_clause_len(conclusion, 1)?;
+    let and_contents = match_term_err!((and ...) = &conclusion[0])?;
+    assert_num_premises(premises, and_contents.len())?;
+
+    // for the rule to be correct, each element of `and_contents` must
+    // be the conclusion of a premise, in the right order. If a
+    // premise has a non-unit conclusion, it must correspond to an OR
+    // term in `and_contents`
+    for i in 0..and_contents.len() {
+        let and_arg = &and_contents[i];
+        match premises[i].clause {
+            [term] => {
+                assert_eq(and_arg, term)?;
+            }
+            _ => {
+                let premise_as_or = pool.add(Term::Op(Operator::Or, premises[i].clause.to_vec()));
+                assert_eq(and_arg, &premise_as_or)?;
+            }
+        };
+    }
+    Ok(())
+}
+
 pub fn bind_let(
     RuleArgs {
         conclusion,

carcara/src/checker/shared.rs

@@ -213,6 +213,7 @@ pub fn get_rule_shared(rule_name: &str, elaborated: bool) -> Option<crate::check
         "trans" => transitivity::trans,
         "cong" => congruence::cong,
         "ho_cong" => congruence::ho_cong,
+        "and_intro" => extras::and_intro,
         "and" => clausification::and,
         "tautology" => resolution::tautology,
         "not_or" => clausification::not_or,

carcara/tests/rules/extras.rs

@@ -128,6 +128,70 @@ fn weakening() {
     }
 }
 
+#[test]
+fn and_intro() {
+    test_cases! {
+        definitions = "
+            (declare-fun p () Bool)
+            (declare-fun q () Bool)
+            (declare-fun r () Bool)
+        ",
+        "Simple working examples" {
+            "(assume h1 p)
+            (assume h2 q)
+            (step t1 (cl (and p q)) :rule and_intro :premises (h1 h2))": true,
+
+            "(assume h1 p)
+            (assume h2 q)
+            (assume h3 r)
+            (step t1 (cl (and p q r)) :rule and_intro :premises (h1 h2 h3))": true,
+        }
+        "Non-unit premise corresponds to a disjunction" {
+            "(step t1 (cl p q) :rule hole)
+            (assume h2 r)
+            (step t2 (cl (and (or p q) r)) :rule and_intro :premises (t1 h2))": true,
+
+            // A unit premise whose term is itself an `or` matches the same conjunct.
+            "(assume h1 (or p q))
+            (assume h2 r)
+            (step t1 (cl (and (or p q) r)) :rule and_intro :premises (h1 h2))": true,
+        }
+        "Premises must be in the right order" {
+            "(assume h1 p)
+            (assume h2 q)
+            (step t1 (cl (and q p)) :rule and_intro :premises (h1 h2))": false,
+        }
+        "A conjunct does not match its premise" {
+            "(assume h1 p)
+            (assume h2 q)
+            (step t1 (cl (and p r)) :rule and_intro :premises (h1 h2))": false,
+
+            // The disjuncts of the conjunct must match the clause order.
+            "(step t1 (cl p q) :rule hole)
+            (assume h2 r)
+            (step t2 (cl (and (or q p) r)) :rule and_intro :premises (t1 h2))": false,
+
+            // A non-unit premise must correspond to an `or`, not a single literal.
+            "(step t1 (cl p q) :rule hole)
+            (assume h2 r)
+            (step t2 (cl (and p r)) :rule and_intro :premises (t1 h2))": false,
+        }
+        "Wrong number of premises" {
+            "(assume h1 p)
+            (step t1 (cl (and p q)) :rule and_intro :premises (h1))": false,
+
+            "(assume h1 p)
+            (assume h2 q)
+            (assume h3 r)
+            (step t1 (cl (and p q)) :rule and_intro :premises (h1 h2 h3))": false,
+        }
+        "Conclusion is not a conjunction" {
+            "(assume h1 p)
+            (step t1 (cl p) :rule and_intro :premises (h1))": false,
+        }
+    }
+}
+
 #[test]
 fn bind_let() {
     test_cases! {