Removed comma necessity after quantifier, fixed formatting errors, fixed old tests to pass with new changes

aris/src/expr.rs

@@ -8,7 +8,7 @@ Parsing an expression that's statically known to be valid:
 ```
 use aris::parser::parse_unwrap as p;
 
-let expr1 = p("forall x, p(x) -> (Q & R)");
+let expr1 = p("forall x p(x) -> (Q & R)");
 ```
 
 Parsing a potentially malformed expression (e.g. user input):
@@ -389,7 +389,7 @@ pub fn unify(mut c: HashSet<Constraint>) -> Option<Substitution> {
         }
         (Expr::Apply { func: sf, args: sa }, Expr::Apply { func: tf, args: ta }) if sa.len() == ta.len() => {
             c.insert(Constraint::Equal(*sf, *tf));
-            c.extend(sa.into_iter().zip(ta.into_iter()).map(|(x, y)| Constraint::Equal(x, y)));
+            c.extend(sa.into_iter().zip(ta).map(|(x, y)| Constraint::Equal(x, y)));
             unify(c)
         }
         (Expr::Assoc { op: so, exprs: se }, Expr::Assoc { op: to, exprs: te }) if so == to && se.len() == te.len() => {
@@ -887,7 +887,7 @@ impl Expr {
                     Expr::Var { name: format!("{i}") }
                 }
                 // push the name onto gamma from the actual quantifier,
-                // Example: for forall x, P(x)
+                // Example: for forall x P(x)
                 // push x onto gamma
                 // save the length of gamma before recursing, to use as the new name
                 Expr::Quant { kind, name, body } => {
@@ -966,14 +966,14 @@ impl Expr {
         })
     }
 
-    /// 7a1. forall x, (phi(x) ∧ psi) == (forall x, phi(x)) ∧ psi
-    /// 7a2. exists x, (phi(x) ∧ psi) == (exists x, phi(x)) ∧ psi
-    /// 7b1. forall x, (phi(x) ∨ psi) == (forall x, phi(x)) ∨ psi
-    /// 7b2. exists x, (phi(x) ∨ psi) == (exists x, phi(x)) ∨ psi
-    /// 7c1. forall x, (phi(x) → psi) == (exists x, phi(x)) → psi (! Expr::Quantifier changes!)
-    /// 7c2. exists x, (phi(x) → psi) == (forall x, phi(x)) → psi (! Expr::Quantifier changes!)
-    /// 7d1. forall x, (psi → phi(x)) == psi → (forall x, phi(x))
-    /// 7d2. exists x, (psi → phi(x)) == psi → (exists x, phi(x))
+    /// 7a1. forall x (phi(x) ∧ psi) == (forall x phi(x)) ∧ psi
+    /// 7a2. exists x (phi(x) ∧ psi) == (exists x phi(x)) ∧ psi
+    /// 7b1. forall x (phi(x) ∨ psi) == (forall x phi(x)) ∨ psi
+    /// 7b2. exists x (phi(x) ∨ psi) == (exists x phi(x)) ∨ psi
+    /// 7c1. forall x (phi(x) → psi) == (exists x phi(x)) → psi (! Expr::Quantifier changes!)
+    /// 7c2. exists x (phi(x) → psi) == (forall x phi(x)) → psi (! Expr::Quantifier changes!)
+    /// 7d1. forall x (psi → phi(x)) == psi → (forall x phi(x))
+    /// 7d2. exists x (psi → phi(x)) == psi → (exists x phi(x))
     pub fn normalize_prenex_laws(self) -> Expr {
         let transform_7ab = |op: Op, exprs: Vec<Expr>| {
             // hoist a forall out of an and/or when the binder won't capture any of the other arms
@@ -1534,11 +1534,11 @@ mod tests {
     #[test]
     fn test_subst() {
         use crate::parser::parse_unwrap as p;
-        assert_eq!(subst(p("x & forall x, x"), "x", p("y")), p("y & forall x, x")); // hit (true, _) case in Expr::Quantifier
-        assert_eq!(subst(p("forall x, x & y"), "y", p("x")), p("forall x0, x0 & x")); // hit (false, true) case in Expr::Quantifier
-        assert_eq!(subst(p("forall x, x & y"), "y", p("z")), p("forall x, x & z")); // hit (false, false) case in Expr::Quantifier
-        assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("h")), p("forall f, f(x) & h(y, z)"));
-        assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("f")), p("forall f0, f0(x) & f(y, z)"));
+        assert_eq!(subst(p("x & forall x x"), "x", p("y")), p("y & forall x x")); // hit (true, _) case in Expr::Quantifier
+        assert_eq!(subst(p("forall x x & y"), "y", p("x")), p("forall x0 x0 & x")); // hit (false, true) case in Expr::Quantifier
+        assert_eq!(subst(p("forall x x & y"), "y", p("z")), p("forall x x & z")); // hit (false, false) case in Expr::Quantifier
+        assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("h")), p("forall f f(x) & h(y, z)"));
+        assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("f")), p("forall f0 f0(x) & f(y, z)"));
     }
 
     #[test]
@@ -1556,15 +1556,15 @@ mod tests {
             }
             ret
         };
-        println!("{:?}", u("x", "forall y, y"));
-        println!("{:?}", u("forall y, y", "y"));
+        println!("{:?}", u("x", "forall y y"));
+        println!("{:?}", u("forall y y", "y"));
         println!("{:?}", u("x", "x"));
-        assert_eq!(u("forall x, x", "forall y, y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
+        assert_eq!(u("forall x x", "forall y y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
         println!("{:?}", u("f(x,y,z)", "g(x,y,y)"));
         println!("{:?}", u("g(x,y,y)", "f(x,y,z)"));
-        println!("{:?}", u("forall foo, foo(x,y,z) & bar", "forall bar, bar(x,y,z) & baz"));
+        println!("{:?}", u("forall foo foo(x,y,z) & bar", "forall bar bar(x,y,z) & baz"));
 
-        assert_eq!(u("forall x, z", "forall y, y"), None);
+        assert_eq!(u("forall x z", "forall y y"), None);
         assert_eq!(u("x & y", "x | y"), None);
     }
 

aris/src/parser.rs

@@ -87,8 +87,12 @@ fn quantifier(input: &str) -> IResult<&str, QuantKind> {
     alt((forall_quantifier, exists_quantifier))(input)
 }
 
+fn space_after_quantifier(input: &str) -> IResult<&str, ()> {
+    value((), many1(one_of(" \t")))(input)
+}
+
 fn binder(input: &str) -> IResult<&str, Expr> {
-    map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(tuple((space, tag(","), space)), expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
+    map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(space_after_quantifier, expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
 }
 
 fn impl_term(input: &str) -> IResult<&str, Expr> {
@@ -165,11 +169,11 @@ fn test_parser() {
     println!("{:?}", predicate("a(   b, c)"));
     println!("{:?}", predicate("s(s(s(s(s(z)))))"));
     println!("{:?}", expr("a & b & c(x,y)\n"));
-    println!("{:?}", expr("forall a, (b & c)\n"));
-    let e = expr("exists x, (Tet(x) & SameCol(x, b)) -> ~forall x, (Tet(x) -> LeftOf(x, b))\n").unwrap();
+    println!("{:?}", expr("forall a (b & c)\n"));
+    let e = expr("exists x (Tet(x) & SameCol(x, b)) -> ~forall x (Tet(x) -> LeftOf(x, b))\n").unwrap();
     let fv = free_vars(&e.1);
     println!("{e:?} {fv:?}");
-    let e = expr("forall a, forall b, ((forall x, in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
+    let e = expr("forall a forall b ((forall x in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
     let fv = free_vars(&e.1);
     assert_eq!(fv, ["eq", "in"].iter().map(|x| String::from(*x)).collect());
     println!("{e:?} {fv:?}");

aris/src/proofs.rs

@@ -255,7 +255,7 @@ pub trait Proof: Sized {
     }
     fn contained_justifications(&self, include_premises: bool) -> HashSet<PjRef<Self>> {
         let mut ret = self.lines().into_iter().filter_map(|x| x.fold(hlist![|r: Self::JustificationReference| Some(vec![r].into_iter().map(Coproduct::inject).collect()), |r: Self::SubproofReference| self.lookup_subproof(&r).map(|sub| sub.contained_justifications(include_premises)),])).fold(HashSet::new(), |mut x, y| {
-            x.extend(y.into_iter());
+            x.extend(y);
             x
         });
         if include_premises {