From f71fb02c0a58706662fe6170aca1eeaa62a20c80 Mon Sep 17 00:00:00 2001 From: zacharybonagura <157537291+zacharybonagura@users.noreply.github.com> Date: Fri, 4 Oct 2024 18:58:44 -0400 Subject: [PATCH] Revert "Revert "Removed comma necessity after quantifier, fixed formatting errors, fixed old tests to pass with new changes"" --- aris/src/expr.rs | 42 ++++---- aris/src/parser.rs | 12 ++- aris/src/proofs.rs | 2 +- aris/src/proofs/proof_tests.rs | 108 ++++++++++----------- aris/src/rules.rs | 2 +- bindings/java/src/java_proof.rs | 4 +- bindings/js/src/proofs.rs | 1 + bindings/js/src/rules.rs | 1 + web-app/src/components/proof_widget/mod.rs | 12 +-- 9 files changed, 94 insertions(+), 90 deletions(-) diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 4a05920d..2a971738 100644 --- a/aris/src/expr.rs +++ b/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) -> Option { } (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| { // 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); } diff --git a/aris/src/parser.rs b/aris/src/parser.rs index a46d0202..5941e489 100644 --- a/aris/src/parser.rs +++ b/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:?}"); diff --git a/aris/src/proofs.rs b/aris/src/proofs.rs index 559ed52e..fbcecbf4 100644 --- a/aris/src/proofs.rs +++ b/aris/src/proofs.rs @@ -255,7 +255,7 @@ pub trait Proof: Sized { } fn contained_justifications(&self, include_premises: bool) -> HashSet> { 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 { diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index f85a49e4..e56842a9 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -145,7 +145,7 @@ pub fn test_contelim() -> (P, Vec>, Vec>) { let mut prf = P::new(); let r1 = prf.add_premise(p("_|_")); let r2 = prf.add_premise(p("A & B")); - let r3 = prf.add_step(Justification(p("forall x, x & ~ x"), RuleM::ContradictionElim, vec![i(r1)], vec![])); + let r3 = prf.add_step(Justification(p("forall x x & ~ x"), RuleM::ContradictionElim, vec![i(r1)], vec![])); let r4 = prf.add_step(Justification(p("Q"), RuleM::ContradictionElim, vec![i(r2)], vec![])); (prf, vec![i(r3)], vec![i(r4)]) } @@ -459,7 +459,7 @@ where use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); - let r1 = prf.add_premise(p("forall x, p(x)")); + let r1 = prf.add_premise(p("forall x p(x)")); let r2 = prf.add_step(Justification(p("p(a)"), RuleM::ForallElim, vec![i(r1.clone())], vec![])); let r3 = prf.add_step(Justification(p("q(x)"), RuleM::ForallElim, vec![i(r1.clone())], vec![])); let r4 = prf.add_step(Justification(p("p(A & B & C & D)"), RuleM::ForallElim, vec![i(r1)], vec![])); @@ -475,8 +475,8 @@ where use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); - let r1 = prf.add_premise(p("forall x, p(x)")); - let r2 = prf.add_premise(p("forall x, q(x)")); + let r1 = prf.add_premise(p("forall x p(x)")); + let r2 = prf.add_premise(p("forall x q(x)")); let r3 = prf.add_premise(p("r(c)")); let r4 = prf.add_subproof(); let (r5, r6, r7) = prf @@ -487,8 +487,8 @@ where (r5, r6, r7) }) .unwrap(); - let r8 = prf.add_step(Justification(p("forall y, p(y) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); - let r9 = prf.add_step(Justification(p("forall y, p(a) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); + let r8 = prf.add_step(Justification(p("forall y p(y) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); + let r9 = prf.add_step(Justification(p("forall y p(a) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()])); let r10 = prf.add_subproof(); let r11 = prf .with_mut_subproof(&r10, |sub| { @@ -499,7 +499,7 @@ where r11 }) .unwrap(); - let r12 = prf.add_step(Justification(p("forall y, r(y)"), RuleM::ForallIntro, vec![], vec![r10.clone()])); + let r12 = prf.add_step(Justification(p("forall y r(y)"), RuleM::ForallIntro, vec![], vec![r10.clone()])); let r13 = prf.add_subproof(); let (r17, r18, r19) = prf .with_mut_subproof(&r13, |sub1| { @@ -508,11 +508,11 @@ where .with_mut_subproof(&r14, |sub2| { let r15 = sub2.add_subproof(); let r17 = sub2.with_mut_subproof(&r15, |sub3| sub3.add_step(Justification(p("s(a, b)"), RuleM::Reit, vec![], vec![]))).unwrap(); - let r18 = sub2.add_step(Justification(p("forall y, s(a, y)"), RuleM::ForallIntro, vec![], vec![r15])); + let r18 = sub2.add_step(Justification(p("forall y s(a, y)"), RuleM::ForallIntro, vec![], vec![r15])); (r17, r18) }) .unwrap(); - let r19 = sub1.add_step(Justification(p("forall x, forall y, s(x, y)"), RuleM::ForallIntro, vec![], vec![r14])); + let r19 = sub1.add_step(Justification(p("forall x forall y s(x, y)"), RuleM::ForallIntro, vec![], vec![r14])); (r17, r18, r19) }) .unwrap(); @@ -525,7 +525,7 @@ where sub.add_step(Justification(p("a"), RuleM::Reit, vec![i(r21)], vec![])) }) .unwrap(); - let r23 = prf.add_step(Justification(p("forall x, x"), RuleM::ForallIntro, vec![], vec![r20])); + let r23 = prf.add_step(Justification(p("forall x x"), RuleM::ForallIntro, vec![], vec![r20])); (prf, vec![i(r5), i(r6), i(r7), i(r8), i(r11), i(r18), i(r19), i(r22)], vec![i(r9), i(r12), i(r17), i(r23)]) } @@ -541,16 +541,16 @@ where let r1 = prf.add_premise(p("p(a)")); let r2 = prf.add_step(Justification(p("p(b) & p(b)"), RuleM::Reit, vec![], vec![])); - let r3 = prf.add_step(Justification(p("exists x, p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); - let r4 = prf.add_step(Justification(p("exists x, p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); - let r5 = prf.add_step(Justification(p("exists x, p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![])); - let r6 = prf.add_step(Justification(p("exists x, p(x) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r7 = prf.add_step(Justification(p("exists x, p(b) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r8 = prf.add_step(Justification(p("exists x, p(x) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r9 = prf.add_step(Justification(p("exists x, p(b) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r10 = prf.add_step(Justification(p("exists x, p(y) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r11 = prf.add_step(Justification(p("exists x, p(a) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); - let r12 = prf.add_step(Justification(p("exists x, p(y) & p(x)"), RuleM::ExistsIntro, vec![i(r2)], vec![])); + let r3 = prf.add_step(Justification(p("exists x p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("exists x p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); + let r5 = prf.add_step(Justification(p("exists x p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![])); + let r6 = prf.add_step(Justification(p("exists x p(x) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("exists x p(b) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("exists x p(x) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r9 = prf.add_step(Justification(p("exists x p(b) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r10 = prf.add_step(Justification(p("exists x p(y) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r11 = prf.add_step(Justification(p("exists x p(a) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![])); + let r12 = prf.add_step(Justification(p("exists x p(y) & p(x)"), RuleM::ExistsIntro, vec![i(r2)], vec![])); (prf, vec![i(r3), i(r4), i(r6), i(r7), i(r8), i(r9)], vec![i(r5), i(r10), i(r11), i(r12)]) } @@ -563,9 +563,9 @@ where use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); - let r1 = prf.add_premise(p("exists x, p(x)")); + let r1 = prf.add_premise(p("exists x p(x)")); let r2 = prf.add_premise(p("p(a) -> q(a)")); - let r3 = prf.add_premise(p("forall b, (p(b) -> r(b))")); + let r3 = prf.add_premise(p("forall b (p(b) -> r(b))")); let r4 = prf.add_subproof(); let (r6, r7, r8, r9, r10) = prf .with_mut_subproof(&r4, |sub| { @@ -573,28 +573,28 @@ where let r6 = sub.add_step(Justification(p("q(a)"), RuleM::ImpElim, vec![i(r2.clone()), i(r5.clone())], vec![])); let r7 = sub.add_step(Justification(p("p(a) -> r(a)"), RuleM::ForallElim, vec![i(r3.clone())], vec![])); let r8 = sub.add_step(Justification(p("r(a)"), RuleM::ImpElim, vec![i(r7.clone()), i(r5)], vec![])); - let r9 = sub.add_step(Justification(p("exists x, q(x)"), RuleM::ExistsIntro, vec![i(r6.clone())], vec![])); - let r10 = sub.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsIntro, vec![i(r8.clone())], vec![])); + let r9 = sub.add_step(Justification(p("exists x q(x)"), RuleM::ExistsIntro, vec![i(r6.clone())], vec![])); + let r10 = sub.add_step(Justification(p("exists x r(x)"), RuleM::ExistsIntro, vec![i(r8.clone())], vec![])); (r6, r7, r8, r9, r10) }) .unwrap(); - let r11 = prf.add_step(Justification(p("exists x, q(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); - let r12 = prf.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); + let r11 = prf.add_step(Justification(p("exists x q(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); + let r12 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); let r13 = prf.add_step(Justification(p("r(a)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()])); - let s1 = prf.add_premise(p("forall y, man(y) → mortal(y)")); - let s2 = prf.add_premise(p("exists x, man(x)")); + let s1 = prf.add_premise(p("forall y man(y) → mortal(y)")); + let s2 = prf.add_premise(p("exists x man(x)")); let s3 = prf.add_subproof(); let (s5, s6, s7) = prf .with_mut_subproof(&s3, |sub| { let s4 = sub.add_premise(p("man(socrates)")); let s5 = sub.add_step(Justification(p("man(socrates) → mortal(socrates)"), RuleM::ForallElim, vec![i(s1.clone())], vec![])); let s6 = sub.add_step(Justification(p("mortal(socrates)"), RuleM::ImpElim, vec![i(s4), i(s5.clone())], vec![])); - let s7 = sub.add_step(Justification(p("exists foo, mortal(foo)"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![])); + let s7 = sub.add_step(Justification(p("exists foo mortal(foo)"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![])); (s5, s6, s7) }) .unwrap(); - let s8 = prf.add_step(Justification(p("exists foo, mortal(foo)"), RuleM::ExistsElim, vec![i(s2)], vec![s3.clone()])); + let s8 = prf.add_step(Justification(p("exists foo mortal(foo)"), RuleM::ExistsElim, vec![i(s2)], vec![s3.clone()])); let t1 = prf.add_step(Justification(p("p(a) -> r(a)"), RuleM::ForallElim, vec![i(r3.clone())], vec![])); let t2 = prf.add_subproof(); @@ -602,18 +602,18 @@ where .with_mut_subproof(&t2, |sub| { let t3 = sub.add_premise(p("p(a)")); let t4 = sub.add_step(Justification(p("r(a)"), RuleM::ImpElim, vec![i(t1.clone()), i(t3)], vec![])); - let t5 = sub.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsIntro, vec![i(t4.clone())], vec![])); + let t5 = sub.add_step(Justification(p("exists x r(x)"), RuleM::ExistsIntro, vec![i(t4.clone())], vec![])); (t4, t5) }) .unwrap(); - let t6 = prf.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![t2.clone()])); + let t6 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![t2.clone()])); let u1 = prf.add_subproof(); - let u2 = prf.add_premise(p("forall c, forall d, p(c) -> s(d)")); + let u2 = prf.add_premise(p("forall c forall d p(c) -> s(d)")); let (u4, u5, u6) = prf .with_mut_subproof(&u1, |sub| { let u3 = sub.add_premise(p("p(a)")); - let u4 = sub.add_step(Justification(p("forall d, p(a) -> s(d)"), RuleM::ForallElim, vec![i(u2.clone())], vec![])); + let u4 = sub.add_step(Justification(p("forall d p(a) -> s(d)"), RuleM::ForallElim, vec![i(u2.clone())], vec![])); let u5 = sub.add_step(Justification(p("p(a) -> s(foo)"), RuleM::ForallElim, vec![i(u4.clone())], vec![])); // TODO: generalized forall? let u6 = sub.add_step(Justification(p("s(foo)"), RuleM::ImpElim, vec![i(u3), i(u5.clone())], vec![])); (u4, u5, u6) @@ -770,8 +770,8 @@ pub fn test_complement() -> (P, Vec>, Vec>) { let r2 = prf.add_premise(p("~A & A")); let r3 = prf.add_premise(p("A | ~A")); let r4 = prf.add_premise(p("~A | A")); - let r5 = prf.add_premise(p("~(forall A, A) | (forall B, B)")); - let r6 = prf.add_premise(p("~(forall A, A) & (forall B, B)")); + let r5 = prf.add_premise(p("~(forall A A) | (forall B B)")); + let r6 = prf.add_premise(p("~(forall A A) & (forall B B)")); let r19 = prf.add_premise(p("(A -> A) & (B <-> B) & (C <-> ~C) & (~D <-> D)")); let r7 = prf.add_step(Justification(p("_|_"), RuleM::Complement, vec![i(r1.clone())], vec![])); let r8 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r1)], vec![])); @@ -914,7 +914,7 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let p2 = prf.add_premise(p("(~~A | B) & ~A")); let p3 = prf.add_premise(p("(B & ~A) | A")); let p4 = prf.add_premise(p("~B | (A & ~~B)")); - let p5 = prf.add_premise(p("(forall A, (A & (~A | B))) | (~(forall A, (A & (~A | B))) & C)")); + let p5 = prf.add_premise(p("(forall A (A & (~A | B))) | (~(forall A (A & (~A | B))) & C)")); let p6 = prf.add_premise(p("B & (C | (~C & ~A))")); let p7 = prf.add_premise(p("A | (~A & (~~A | B))")); let p8 = prf.add_premise(p("D | (~A & (~~A | B))")); @@ -923,7 +923,7 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let r2 = prf.add_step(Justification(p("~A & B"), RuleM::Reduction, vec![i(p2.clone())], vec![])); let r3 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p3.clone())], vec![])); let r4 = prf.add_step(Justification(p("~B | A"), RuleM::Reduction, vec![i(p4.clone())], vec![])); - let r5 = prf.add_step(Justification(p("(forall A, (A & B)) | C"), RuleM::Reduction, vec![i(p5)], vec![])); + let r5 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p5)], vec![])); let r6 = prf.add_step(Justification(p("A"), RuleM::Reduction, vec![i(p1)], vec![])); let r7 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p2)], vec![])); @@ -1118,7 +1118,7 @@ pub fn test_excluded_middle() -> (P, Vec>, Vec>) { let r8 = prf.add_step(Justification(p("B"), RuleM::ExcludedMiddle, vec![], vec![])); let r9 = prf.add_step(Justification(p("R -> P"), RuleM::ExcludedMiddle, vec![], vec![])); let r10 = prf.add_step(Justification(p("R -> T"), RuleM::ExcludedMiddle, vec![], vec![])); - let r11 = prf.add_step(Justification(p("(A & B & C & forall P, P) | ~(A & B & C & forall P, P)"), RuleM::ExcludedMiddle, vec![], vec![])); + let r11 = prf.add_step(Justification(p("(A & B & C & forall P P) | ~(A & B & C & forall P P)"), RuleM::ExcludedMiddle, vec![], vec![])); (prf, vec![i(r1), i(r4), i(r5), i(r11)], vec![i(r2), i(r3), i(r6), i(r7), i(r8), i(r9), i(r10)]) } @@ -1127,14 +1127,14 @@ pub fn test_weak_induction() -> (P, Vec>, Vec>) { use crate::parser::parse_unwrap as p; let mut prf = P::new(); let r1 = prf.add_premise(p("~LessThan(0,0)")); - let r2 = prf.add_premise(p("forall x, ~LessThan(x,x) -> ~LessThan(s(x),s(x))")); + let r2 = prf.add_premise(p("forall x ~LessThan(x,x) -> ~LessThan(s(x),s(x))")); let r3 = prf.add_premise(p("Equals(0,0)")); - let r4 = prf.add_premise(p("forall 0, Equals(0,0) -> Equals(s(0),s(0))")); - let r5 = prf.add_step(Justification(p("forall x, ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); - let r6 = prf.add_step(Justification(p("forall x, ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r2.clone()), i(r1.clone())], vec![])); - let r7 = prf.add_step(Justification(p("forall n, ~LessThan(n,n)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); - let r8 = prf.add_step(Justification(p("forall x, Equals(x,x)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![])); - let r9 = prf.add_step(Justification(p("forall x, Equals(x,0)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![])); + let r4 = prf.add_premise(p("forall 0 Equals(0,0) -> Equals(s(0),s(0))")); + let r5 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r2.clone()), i(r1.clone())], vec![])); + let r7 = prf.add_step(Justification(p("forall n ~LessThan(n,n)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("forall x Equals(x,x)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![])); + let r9 = prf.add_step(Justification(p("forall x Equals(x,0)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![])); (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8)], vec![i(r9)]) } @@ -1142,13 +1142,13 @@ pub fn test_strong_induction() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); - let r1 = prf.add_premise(p("forall n, (forall x, LessThan(x, n) -> P(x)) -> P(n)")); - let r2 = prf.add_premise(p("forall n, (forall x, LessThan(x, n) -> P(x,n)) -> P(n,n)")); - let r3 = prf.add_step(Justification(p("forall x, P(x)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); - let r4 = prf.add_step(Justification(p("forall n, P(n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); - let r5 = prf.add_step(Justification(p("forall n, P(n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![])); - let r6 = prf.add_step(Justification(p("forall x, P(x,n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); - let r7 = prf.add_step(Justification(p("forall x, P(x,n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![])); - let r8 = prf.add_step(Justification(p("forall a, P(a)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); + let r1 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x)) -> P(n)")); + let r2 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x,n)) -> P(n,n)")); + let r3 = prf.add_step(Justification(p("forall x P(x)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); + let r5 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("forall x P(x,n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); + let r7 = prf.add_step(Justification(p("forall x P(x,n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("forall a P(a)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![])); (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r8)], vec![i(r5), i(r6), i(r7)]) } diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 0cbc6e4c..56e5d613 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -202,8 +202,8 @@ pub type Rule = SharedChecks { diff --git a/bindings/java/src/java_proof.rs b/bindings/java/src/java_proof.rs index bae78e5a..0f3fe47c 100644 --- a/bindings/java/src/java_proof.rs +++ b/bindings/java/src/java_proof.rs @@ -90,12 +90,12 @@ pub extern "system" fn Java_edu_rpi_aris_proof_RustProof_checkRuleAtLine(env: JN println!("RustProof::checkRuleAtLine {self_:?}"); if let Some(line) = self_.lines.get(linenum as _) { if let Err(e) = self_.proof.verify_line(&line.reference) { - Ok(env.new_string(&format!("{e}"))?.into_inner()) + Ok(env.new_string(format!("{e}"))?.into_inner()) } else { Ok(std::ptr::null_mut()) } } else { - Ok(env.new_string(&format!("Failed to dereference line {linenum} in {self_:?}"))?.into_inner()) + Ok(env.new_string(format!("Failed to dereference line {linenum} in {self_:?}"))?.into_inner()) } }) } diff --git a/bindings/js/src/proofs.rs b/bindings/js/src/proofs.rs index cc39b4fa..96900275 100644 --- a/bindings/js/src/proofs.rs +++ b/bindings/js/src/proofs.rs @@ -228,6 +228,7 @@ impl Proof { } #[wasm_bindgen] +#[allow(dead_code)] pub struct Subproof(Sp); #[wasm_bindgen] diff --git a/bindings/js/src/rules.rs b/bindings/js/src/rules.rs index 35a62749..991b4952 100644 --- a/bindings/js/src/rules.rs +++ b/bindings/js/src/rules.rs @@ -12,6 +12,7 @@ pub fn rule_names() -> JsResult> { } #[wasm_bindgen] +#[allow(dead_code)] pub struct Rule(aris::rules::Rule); #[wasm_bindgen] diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs index 784fbb5f..f0ef8496 100644 --- a/web-app/src/components/proof_widget/mod.rs +++ b/web-app/src/components/proof_widget/mod.rs @@ -5,8 +5,6 @@ use crate::components::expr_entry::ExprEntry; use crate::proof_ui_data::ProofUiData; use crate::util::calculate_lineinfo; use crate::util::P; - - use aris::expr::Expr; use aris::proofs::pj_to_pjs; use aris::proofs::JsRef; @@ -176,10 +174,10 @@ impl ProofWidget { .map(|rule| { let pjref = Coproduct::inject(jref); // Create menu item for rule - //tooltip portion addapted from: - // * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip - // * https://getbootstrap.com/docs/4.1/components/tooltips/ - html! { + //tooltip portion addapted from: + // * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip + // * https://getbootstrap.com/docs/4.1/components/tooltips/ + html! { @@ -225,7 +223,7 @@ impl ProofWidget { // Iterator over subproof dependency badges, for rendering list of // dependencies let sdep_badges = just.3.iter().filter_map(|sdep| self.prf.lookup_subproof(sdep)).map(|sub| { - let (mut lo, mut hi) = (usize::max_value(), usize::min_value()); + let (mut lo, mut hi) = (usize::MAX, usize::MIN); for line in sub.premises().into_iter().map(Coproduct::inject).chain(sub.direct_lines().into_iter().map(Coproduct::inject)) { if let Some((i, _)) = self.pud.ref_to_line_depth.get(&line) { lo = std::cmp::min(lo, *i);