From 37940f00777f26229ecb47b65236a60afbc46e8e Mon Sep 17 00:00:00 2001 From: Zachary Bonagura Date: Wed, 27 Nov 2024 19:12:19 -0500 Subject: [PATCH 1/5] Refactored method for loading rule tooltip images, new Equivalence sub category Refactored the function that loads images for each rule to ensure optimization in program so images are only loaded once. Additionally, regrouped all equivalence rules into one sub category named "Equivalence". --- web-app/src/components/proof_widget/mod.rs | 151 ++++++--------------- web-app/static/dark-theme.css | 25 ++++ web-app/static/styles.css | 18 ++- 3 files changed, 81 insertions(+), 113 deletions(-) diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs index ff65423c..3aea749d 100644 --- a/web-app/src/components/proof_widget/mod.rs +++ b/web-app/src/components/proof_widget/mod.rs @@ -166,90 +166,44 @@ impl ProofWidget { /// /// [lib]: https://github.com/vsn4ik/bootstrap-submenu fn render_rules_menu(&self, ctx: &Context, jref:

::JustificationReference, cur_rule_name: &str) -> Html { - let menu = RuleClassification::iter() - .map(|rule_class| { - let rules = rule_class - .rules() - .map(|rule| { - let pjref = Coproduct::inject(jref); - - // Determine the folder for the current theme - let get_folder = || { - if theme() == "dark" { - "proofImages_dark" - } else { - "proofImages_light" - } - }; - let image_src = format!("{}/{}.png", get_folder(), rule.get_name()); - - html! { -

- - {rule.get_name()} -
- } - }) - .collect::>(); + let equivalence_classes = [RuleClassification::BooleanEquivalence, RuleClassification::ConditionalEquivalence, RuleClassification::BiconditionalEquivalence, RuleClassification::QuantifierEquivalence]; + + let render_rules = |rules: Vec| { + rules + .into_iter() + .map(|rule| { + let pjref = Coproduct::inject(jref); + let image_src = format!("{}/{}.png", if theme() == "dark" { "proofImages_dark" } else { "proofImages_light" }, rule.get_name()); + html! { + + } + }) + .collect::>() + }; - let rules = yew::virtual_dom::VList::with_children(rules, None); + let render_class = |rule_class: RuleClassification| { + let rules = render_rules(rule_class.rules().collect()); + html! { +
+ +
{ rules }
+
+ } + }; - html! { -
- -
{ rules }
-
- } - }) - .collect::>(); - let menu = yew::virtual_dom::VList::with_children(menu, None); + let equivalence_submenu = equivalence_classes.iter().map(|&class| render_class(class)).collect::>(); + let non_equivalence_menu = RuleClassification::iter().filter(|class| !equivalence_classes.contains(class)).map(render_class).collect::>(); html! {
@@ -257,7 +211,11 @@ impl ProofWidget { { cur_rule_name }
- { menu } + { non_equivalence_menu } +
+ +
{ equivalence_submenu }
+
} @@ -266,8 +224,7 @@ impl ProofWidget { fn render_justification_widget(&self, ctx: &Context, jref:

::JustificationReference) -> Html { let just = self.prf.lookup_justification_or_die(&jref).expect("proofref should exist in self.prf"); - // Iterator over line dependency badges, for rendering list of - // dependencies + // Iterator over line dependency badges, for rendering list of dependencies let dep_badges = just.2.iter().map(|dep| { let (dep_line, _) = self.pud.ref_to_line_depth[dep]; html! { @@ -275,8 +232,7 @@ impl ProofWidget { } }); - // Iterator over subproof dependency badges, for rendering list of - // dependencies + // 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, usize::MIN); for line in sub.premises().into_iter().map(Coproduct::inject).chain(sub.direct_lines().into_iter().map(Coproduct::inject)) { @@ -897,26 +853,7 @@ impl Component for ProofWidget { } } - fn rendered(&mut self, _: &Context, first_render: bool) { + fn rendered(&mut self, _: &Context, _: bool) { js_sys::eval("$('[data-submenu]').submenupicker(); $('[data-toggle=popover]').popover()").unwrap_throw(); - if !first_render { - let js = r#" - document.querySelectorAll('.dropdown-item').forEach(item => { - const imgId = `tooltip-img-${item.innerText.trim().replace(/\s+/g, '_')}`; - const imgElem = document.getElementById(imgId); - item.addEventListener('mouseover', function() { - if (imgElem) { - imgElem.style.display = 'block'; - } - }); - item.addEventListener('mouseout', function() { - if (imgElem) { - imgElem.style.display = 'none'; - } - }); - }); - "#; - js_sys::eval(js).unwrap_throw(); - } } } diff --git a/web-app/static/dark-theme.css b/web-app/static/dark-theme.css index ccf7397f..415a59da 100644 --- a/web-app/static/dark-theme.css +++ b/web-app/static/dark-theme.css @@ -163,3 +163,28 @@ background-color: black; } +[theme="dark"] .tooltip { + overflow: visible; +} + +[theme="dark"] .tooltip-inner { + border: 3px solid white; + padding: 4px; +} + +/* Tooltip Arrow Colors in Dark Mode */ +[theme="dark"] .bs-tooltip-bottom .arrow::before { + border-bottom-color: white; +} + +[theme="dark"] .bs-tooltip-top .arrow::before { + border-top-color: white; +} + +[theme="dark"] .bs-tooltip-left .arrow::before { + border-left-color: white; +} + +[theme="dark"] .bs-tooltip-right .arrow::before { + border-right-color: white; +} \ No newline at end of file diff --git a/web-app/static/styles.css b/web-app/static/styles.css index dbe4cc6f..afddb198 100644 --- a/web-app/static/styles.css +++ b/web-app/static/styles.css @@ -54,9 +54,15 @@ html, body { margin-top: 10px; } +.tooltip { + overflow: visible; +} + .tooltip-inner { - max-width: 100%; - background-color: #0062cc; + border: 1px solid black; /* Set uniform border width and color */ + padding: 3px; /* Add consistent padding around the image */ + width: auto; /* Ensure tooltip width adjusts to content */ + max-width: none; } .tooltip.show { @@ -64,14 +70,14 @@ html, body { } .bs-tooltip-bottom .arrow::before{ - border-bottom-color: #0062cc; + border-bottom-color: black; } .bs-tooltip-top .arrow::before{ - border-top-color: #0062cc; + border-top-color: black; } .bs-tooltip-left .arrow::before{ - border-left-color: #0062cc; + border-left-color: black; } .bs-tooltip-right .arrow::before{ - border-right-color: #0062cc; + border-right-color: black; } From 1a7d99c51c647f1d72bbd810d70c153e3cb042f9 Mon Sep 17 00:00:00 2001 From: Zachary Bonagura Date: Wed, 27 Nov 2024 19:13:24 -0500 Subject: [PATCH 2/5] Modified quantifier parsing Fixed glitch where quantifiers would distribute across multiple expressions, now only distributes over single Expr, whether it's one term or multiple wrapped in parenthesis --- aris/src/parser.rs | 21 ++++++++++-- aris/src/proofs/proof_tests.rs | 63 +++++++++++++++++++++------------- 2 files changed, 57 insertions(+), 27 deletions(-) diff --git a/aris/src/parser.rs b/aris/src/parser.rs index 4c35df14..4e32f92b 100644 --- a/aris/src/parser.rs +++ b/aris/src/parser.rs @@ -102,7 +102,22 @@ fn conditional_space(input: &str) -> IResult<&str, ()> { } fn binder(input: &str) -> IResult<&str, Expr> { - map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(conditional_space, expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input) + map( + tuple(( + preceded(space, quantifier), + preceded(space, variable), + preceded( + conditional_space, + alt(( + // Parse multiple terms enclosed in parentheses + delimited(tuple((space, tag("("), space)), expr, tuple((space, tag(")"), space))), + // Parse a single term without parentheses + paren_expr, + )), + ), + )), + |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) }, + )(input) } fn impl_term(input: &str) -> IResult<&str, Expr> { @@ -180,10 +195,10 @@ fn test_parser() { 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(); + 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/proof_tests.rs b/aris/src/proofs/proof_tests.rs index bb9f13fa..959d6f68 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -489,8 +489,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| { @@ -514,7 +514,7 @@ where (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(); @@ -546,13 +546,13 @@ where 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 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)]) } @@ -584,7 +584,7 @@ where 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 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 @@ -592,7 +592,7 @@ where 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(); @@ -611,11 +611,11 @@ where 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) @@ -958,20 +958,22 @@ 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))")); let p9 = prf.add_premise(p("P & M & (~P | Q)")); let p10 = prf.add_premise(p("P | M | (~P & Q)")); - // let p11 = prf.add_premise(p("~P & (P | Q)")); + + let p11 = prf.add_premise(p("~P & (P | Q)")); + let p12 = prf.add_premise(p("P & M & (~(P & M) | Q)")); + let p13 = prf.add_premise(p("(forall A (A & B)) | (~(forall A (A & B)) & C)")); let r1 = prf.add_step(Justification(p("A & B"), RuleM::Reduction, vec![i(p1.clone())], 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 r18 = prf.add_step(Justification(p("¬P ∧ Q"), RuleM::Reduction, vec![i(p11.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)) | (~(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![])); @@ -988,7 +990,11 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let r16 = prf.add_step(Justification(p("P | M | Q"), RuleM::Reduction, vec![i(p10.clone())], vec![])); let r17 = prf.add_step(Justification(p("(P | M) & Q"), RuleM::Reduction, vec![i(p10)], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r10), i(r12), i(r13), i(r14), i(r16)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) + let r18 = prf.add_step(Justification(p("~P & Q"), RuleM::Reduction, vec![i(p11.clone())], vec![])); + let r19 = prf.add_step(Justification(p("P & M & Q"), RuleM::Reduction, vec![i(p12.clone())], vec![])); + let r20 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p13)], vec![])); + + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r19), i(r18), i(r10), i(r12), i(r13), i(r14), i(r16), i(r20)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) } pub fn test_adjacency() -> (P, Vec>, Vec>) { @@ -998,6 +1004,10 @@ pub fn test_adjacency() -> (P, Vec>, Vec>) { let p1 = prf.add_premise(p("(A & B) | (A & ~B)")); let p2 = prf.add_premise(p("(A | B) & (A | ~B)")); + let p3 = prf.add_premise(p("(¬(P∧M) ∨ Q) ∧ ((P∧M) ∨ Q)")); + let p4 = prf.add_premise(p("(¬(P∧M) ∨ Q) ∧ ((P) ∨ Q)")); + let p5 = prf.add_premise(p("(A | B) & M & (A | ~B)")); + let p6 = prf.add_premise(p("(M ∨ (P ∧ Q ∧ W) ∨ (P ∧ W ∧ ¬Q))")); let r1 = prf.add_step(Justification(p("A"), RuleM::Adjacency, vec![i(p1.clone())], vec![])); let r2 = prf.add_step(Justification(p("A"), RuleM::Adjacency, vec![i(p2.clone())], vec![])); @@ -1007,7 +1017,12 @@ pub fn test_adjacency() -> (P, Vec>, Vec>) { let r5 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p1)], vec![])); let r6 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p2)], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4)], vec![i(r5), i(r6)]) + let r7 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p3)], vec![])); + let r8 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p4)], vec![])); + let r9 = prf.add_step(Justification(p("A & M"), RuleM::Adjacency, vec![i(p5.clone())], vec![])); + + let r10 = prf.add_step(Justification(p("(P & W) | M"), RuleM::Adjacency, vec![i(p6.clone())], vec![])); + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r7), i(r9), i(r10)], vec![i(r5), i(r6), i(r8)]) } pub fn test_resolution() -> (P, Vec>, Vec>) { @@ -1202,9 +1217,9 @@ 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 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![])); @@ -1217,8 +1232,8 @@ 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 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![])); From a74c2677d99ec64353da0acec2bc3ada27c6ed28 Mon Sep 17 00:00:00 2001 From: Zachary Bonagura Date: Wed, 27 Nov 2024 19:22:10 -0500 Subject: [PATCH 3/5] Split Quantifier Distribution into two seperate rules Split Quantifier Distribution into two separate rules, one Quantifier Distribution under Quantifier Equivalence, the other Quantifier Inference under Misc. Inference --- aris/src/expr.rs | 276 ++++++++++++++++++++++++++------------ aris/src/rules.rs | 50 ++++++- web-app/static/index.html | 10 +- 3 files changed, 244 insertions(+), 92 deletions(-) diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 808cfdd8..21f57a99 100644 --- a/aris/src/expr.rs +++ b/aris/src/expr.rs @@ -28,9 +28,8 @@ assert_eq!(&handle_user_input("bad(missing, paren"), "unsuccessful parse"); use std::collections::BTreeSet; use std::collections::{HashMap, HashSet}; -use std::fmt; -use std::mem; use std::ops::Not; +use std::{fmt, mem}; use itertools::Itertools; use maplit::hashset; @@ -897,7 +896,7 @@ impl Expr { Expr::collect_unique_exprs_idempotence(&normalized_expr, op, &mut unique_exprs); } - // If there's only one unique expression, return it; otherwise, reassemble the expression + // If there's only one unique expression, return it. Otherwise, reassemble the expression let unique_exprs: Vec = unique_exprs.into_iter().collect(); if unique_exprs.len() == 1 { @@ -951,13 +950,51 @@ impl Expr { } } + fn collect_reduction_exprs(expr: &Expr, op: Op, reduced_exprs: &mut BTreeSet) { + match expr { + Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { + exprs.iter().for_each(|sub_expr| Self::collect_reduction_exprs(sub_expr, op, reduced_exprs)); + } + Expr::Assoc { op: inner_op, exprs } if (op, *inner_op) == (Op::And, Op::Or) || (op, *inner_op) == (Op::Or, Op::And) => { + let (mut other_terms, mut negated_match) = (vec![], None); + + for sub_expr in exprs { + match sub_expr { + Expr::Not { operand } => { + if Self::is_subset_of_assoc(operand, reduced_exprs, Op::And) { + negated_match = Some(sub_expr.clone()); + } else { + other_terms.push(sub_expr.clone()); + } + } + _ if reduced_exprs.contains(&Expr::Not { operand: Box::new(sub_expr.clone()) }) => { + negated_match = Some(sub_expr.clone()); + } + _ => other_terms.push(sub_expr.clone()), + } + } + + if negated_match.is_some() { + reduced_exprs.extend(other_terms); + } else { + reduced_exprs.insert(expr.clone()); + } + } + Expr::Quant { kind, name, body } => { + reduced_exprs.insert(Expr::Quant { kind: *kind, name: name.clone(), body: Box::new(body.clone().normalize_reduction()) }); + } + _ => { + reduced_exprs.insert(expr.clone()); + } + } + } + pub fn normalize_reduction(self) -> Expr { match self { - // Handle Associative operations (AND/OR) Expr::Assoc { op, exprs } => { let mut reduced_exprs = BTreeSet::new(); - // Recurse through the expressions inside the Assoc operation + // Recurse through the expressions for expr in exprs { let normalized_expr = expr.normalize_reduction(); Self::collect_reduction_exprs(&normalized_expr, op, &mut reduced_exprs); @@ -968,75 +1005,127 @@ impl Expr { let first = expr_iter.next().unwrap(); let second = expr_iter.next().unwrap(); - // Check if the second expression is a quantifier if let Expr::Quant { kind, name, body } = second { return Expr::Assoc { op: Op::Or, exprs: vec![first, Expr::Quant { kind, name, body }] }; } } + Expr::Assoc { op, exprs: reduced_exprs.into_iter().collect() } } - // Recursively normalize quantifier body + + // If the expression is a quantifier, recursively normalize its body Expr::Quant { kind, name, body } => { let normalized_body = body.normalize_reduction(); Expr::Quant { kind, name, body: Box::new(normalized_body) } } + // If the expression is a negation, attempt to simplify the negated quantifier - Expr::Not { operand } => { - match *operand { - // If the operand is a quantifier, recursively normalize its body - Expr::Quant { kind, name, body } => { - let normalized_body = body.normalize_reduction(); - Expr::Quant { kind, name, body: Box::new(normalized_body) } - } - _ => Expr::Not { operand: Box::new(operand.normalize_reduction()) }, + Expr::Not { operand } => match *operand { + Expr::Quant { kind, name, body } => { + let normalized_body = body.normalize_reduction(); + Expr::Quant { kind, name, body: Box::new(normalized_body) } } - } + _ => Expr::Not { operand: Box::new(operand.normalize_reduction()) }, + }, + _ => self, } } - fn collect_reduction_exprs(expr: &Expr, op: Op, reduced_exprs: &mut BTreeSet) { + fn is_subset_of_assoc(expr: &Expr, set: &BTreeSet, op: Op) -> bool { match expr { - // If the expression is an associative operation with the same operator, recurse into its subexpressions - Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { - for sub_expr in exprs { - Self::collect_reduction_exprs(sub_expr, op, reduced_exprs); + Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().all(|sub_expr| set.contains(sub_expr)), + single_expr => set.contains(single_expr), + } + } + + pub fn normalize_adjacency(self) -> Expr { + match self { + Expr::Assoc { op, exprs } => { + let unique_exprs = exprs.into_iter().flat_map(|e| e.normalize_adjacency().extract_associative(op)).collect::>(); + + match Self::simplify_general(unique_exprs.clone(), op) { + Some(simplified) => simplified, + None => match unique_exprs.len() { + 1 => unique_exprs.into_iter().next().unwrap(), + _ => Expr::Assoc { op, exprs: unique_exprs }, + }, } } - // If the expression involves an AND/OR between a quantifier and another expression, handle simplifications - Expr::Assoc { op: inner_op, exprs } => match (op, inner_op) { - (Op::And, Op::Or) | (Op::Or, Op::And) => { - let mut other_terms = vec![]; - let mut negated_match = None; - for sub_expr in exprs { - match sub_expr { - // If the subexpression involves a negated quantifier, simplify it - Expr::Not { operand } if reduced_exprs.contains(operand) => { - negated_match = Some(operand.as_ref().clone()); - } - _ => other_terms.push(sub_expr.clone()), - } - } - if negated_match.is_some() { - reduced_exprs.extend(other_terms); - } else { - reduced_exprs.insert(expr.clone()); - } - } - _ => { - reduced_exprs.insert(expr.clone()); - } - }, - // Simplify quantifier body Expr::Quant { kind, name, body } => { - let normalized_body = body.clone().normalize_reduction(); - let simplified_expr = Expr::Quant { kind: *kind, name: name.clone(), body: Box::new(normalized_body) }; - reduced_exprs.insert(simplified_expr); + // Normalize the body of the quantifier + let normalized_body = body.normalize_adjacency(); + Expr::Quant { kind, name, body: Box::new(normalized_body) } } - _ => { - reduced_exprs.insert(expr.clone()); + _ => self, + } + } + + fn extract_associative(self, op: Op) -> Vec { + match self { + Expr::Assoc { op: expr_op, exprs } if expr_op == op => exprs, + _ => vec![self], + } + } + + fn simplify_general(mut exprs: Vec, op: Op) -> Option { + for i in 0..exprs.len() { + for j in (i + 1..exprs.len()).rev() { + if let Some(simplified) = Self::try_simplify_pair(&exprs[i], &exprs[j], op) { + exprs.swap_remove(j); + exprs[i] = simplified; + return Self::simplify_general(exprs, op); // Restart with updated list + } } } + exprs.sort(); + exprs.dedup(); + match exprs.len() { + 0 => None, + 1 => Some(exprs.into_iter().next().unwrap()), + _ => Some(Expr::Assoc { op, exprs }), + } + } + + fn try_simplify_pair(e1: &Expr, e2: &Expr, op: Op) -> Option { + match op { + Op::Or | Op::And => Self::simplify_logic(e1, e2), + _ => None, + } + } + + fn simplify_logic(e1: &Expr, e2: &Expr) -> Option { + match (e1, e2) { + (Expr::Assoc { op: sub_op1, exprs: exprs1 }, Expr::Assoc { op: sub_op2, exprs: exprs2 }) if *sub_op1 == *sub_op2 => { + let common: Vec<_> = exprs1.iter().filter(|e| exprs2.contains(e)).cloned().collect(); + if common.is_empty() { + return None; + } + let rest1: Vec<_> = exprs1.iter().filter(|e| !common.contains(*e)).collect(); + let rest2: Vec<_> = exprs2.iter().filter(|e| !common.contains(*e)).collect(); + if Self::is_complementary(&rest1, &rest2) { + return Some(Self::assoc_or_single(common, *sub_op1)); + } + } + _ => {} + } + None + } + + fn assoc_or_single(mut exprs: Vec, op: Op) -> Expr { + exprs.sort(); + exprs.dedup(); + match exprs.len() { + 1 => exprs.pop().unwrap(), + _ => Expr::Assoc { op, exprs }, + } + } + + fn is_complementary(others1: &[&Expr], others2: &[&Expr]) -> bool { + matches!( + (others1, others2), + ([Expr::Not { operand: o1 }], [e2]) | ([e2], [Expr::Not { operand: o1 }]) if **o1 == **e2 + ) } /// Helper function for complement quantified expressions @@ -1399,46 +1488,67 @@ impl Expr { }) } - /// Distribute forall/exists into and/or - pub fn quantifier_distribution(self) -> Expr { - let push_quantifier_inside = |kind: QuantKind, qname: String, exprs: &mut Vec| { - for iter in exprs.iter_mut() { - match kind { - QuantKind::Exists => { - let tmp = mem::replace(iter, Expr::Contra); - *iter = Expr::exists(qname.as_str(), tmp); + pub fn quantifier_inference(self) -> Expr { + let distribute_quantifiers = |expr: &Expr| -> Option { + match expr { + // (∃ x (P(x) ∧ Q(x))) => ((∃ x P(x)) ∧ (∃ x Q(x))) + Expr::Quant { kind: QuantKind::Exists, name, body } if matches!(body.as_ref(), Expr::Assoc { op: Op::And, .. }) => { + if let Expr::Assoc { op: Op::And, exprs } = body.as_ref() { + let distributed = exprs.iter().map(|inner| Expr::exists(name, inner.clone())).collect::>(); + return Some(Expr::assoc(Op::And, &distributed)); } - - QuantKind::Forall => { - let tmp = mem::replace(iter, Expr::Contra); - *iter = Expr::forall(qname.as_str(), tmp); + } + // ((∀ x P(x)) ∨ (∀ x Q(x))) => (∀ x (P(x) ∨ Q(x))) + Expr::Assoc { op: Op::Or, exprs } if exprs.iter().all(|e| matches!(e, Expr::Quant { kind: QuantKind::Forall, .. })) => { + let names_and_bodies: Vec<(&str, &Expr)> = exprs + .iter() + .filter_map(|e| match e { + Expr::Quant { kind: QuantKind::Forall, name, body } => Some((name.as_str(), body.as_ref())), + _ => None, + }) + .collect(); + + let first_name = names_and_bodies[0].0; + if names_and_bodies.iter().all(|(name, _)| name == &first_name) { + let combined_body = Expr::assoc(Op::Or, &names_and_bodies.iter().map(|(_, body)| (*body).clone()).collect::>()); + return Some(Expr::forall(first_name, combined_body)); } } + _ => {} } + None }; - self.transform(&|expr| { - let orig_expr = expr.clone(); + self.transform(&|expr| distribute_quantifiers(&expr).map_or((expr.clone(), false), |transformed| (transformed, true))) + } - match expr { - Expr::Quant { kind, name, body } => { - match *body { - Expr::Assoc { op, mut exprs } => { - // continue only if op is And or Or - match op { - Op::And | Op::Or => {} - _ => return (orig_expr, false), - }; - - // inline push_quantifier_inside here - push_quantifier_inside(kind, name, &mut exprs); - (Expr::assoc(op, &exprs), true) - } - _ => (orig_expr, false), + pub fn quantifier_distribution(self) -> Expr { + let push_quantifier_inside = |kind: QuantKind, qname: String, exprs: &mut Vec| { + exprs.iter_mut().for_each(|iter| { + let tmp = mem::replace(iter, Expr::Contra); + *iter = match kind { + QuantKind::Exists => Expr::exists(qname.as_str(), tmp), + QuantKind::Forall => Expr::forall(qname.as_str(), tmp), + }; + }); + }; + + self.transform(&|expr| match expr.clone() { + Expr::Quant { kind, name, body } => match *body { + Expr::Assoc { op, mut exprs } => match op { + Op::And if kind == QuantKind::Forall => { + push_quantifier_inside(kind, name, &mut exprs); + (Expr::assoc(Op::And, &exprs), true) } - } - _ => (expr, false), - } + Op::Or if kind == QuantKind::Exists => { + push_quantifier_inside(kind, name, &mut exprs); + (Expr::assoc(Op::Or, &exprs), true) + } + _ => (expr.clone(), false), + }, + _ => (expr.clone(), false), + }, + _ => (expr, false), }) } diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 771d9b9d..89a618d2 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -165,6 +165,7 @@ pub enum RedundantPrepositionalInference { ExcludedMiddle, ConstructiveDilemma, HalfDeMorgan, + QuantifierInference, } #[allow(missing_docs)] @@ -321,6 +322,7 @@ pub mod RuleM { [ExcludedMiddle, "EXCLUDED_MIDDLE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ExcludedMiddle))))))))], [ConstructiveDilemma, "CONSTRUCTIVE_DILEMMA", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ConstructiveDilemma))))))))], [HalfDeMorgan, "HALF_DE_MORGAN", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::HalfDeMorgan))))))))], + [QuantifierInference, "QUANTIFIER_INFERENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::QuantifierInference))))))))], [Resolution, "RESOLUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::Resolution)))))))))], [TruthFunctionalConsequence, "TRUTHFUNCTIONAL_CONSEQUENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::TruthFunctionalConsequence)))))))))], @@ -536,7 +538,6 @@ impl RuleT for PrepositionalInference { fn check(self, p: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { use PrepositionalInference::*; use ProofCheckError::*; - match self { Reit => { let prem = p.lookup_expr_or_die(&deps[0])?; @@ -547,6 +548,12 @@ impl RuleT for PrepositionalInference { } } AndIntro => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } if let Expr::Assoc { op: Op::And, ref exprs } = conclusion { // ensure each dep appears in exprs for d in deps.iter() { @@ -567,6 +574,12 @@ impl RuleT for PrepositionalInference { } } AndElim => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::And, ref exprs } = prem { let premise_set: HashSet<_> = exprs.iter().collect(); @@ -592,6 +605,12 @@ impl RuleT for PrepositionalInference { } } OrIntro => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::Or, ref exprs } = conclusion { if !exprs.iter().any(|e| e == &prem) { @@ -603,6 +622,12 @@ impl RuleT for PrepositionalInference { } } OrElim => { + if deps.len() == 1 { + let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; + if single_dep_expr == conclusion { + return Ok(()); + } + } let prem = p.lookup_expr_or_die(&deps[0])?; if let Expr::Assoc { op: Op::Or, ref exprs } = prem { let sproofs = sdeps.into_iter().map(|r| p.lookup_subproof_or_die(&r)).collect::, _>>()?; @@ -1020,11 +1045,13 @@ where F: Fn(Expr) -> Expr, { let mut premise = p.lookup_expr_or_die(&deps[0])?; + let mut conclusion_mut = conclusion; if commutative { premise = premise.sort_commutative_ops(restriction); + conclusion_mut = conclusion_mut.sort_commutative_ops(restriction); } let mut p = normalize_fn(premise.clone()); - let mut q = normalize_fn(conclusion); + let mut q = normalize_fn(conclusion_mut); if commutative { p = p.sort_commutative_ops(restriction); q = q.sort_commutative_ops(restriction); @@ -1036,6 +1063,19 @@ where } } +fn check_by_normalize_first_expr_one_way(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> +where + F: Fn(Expr) -> Expr, +{ + let premise = p.lookup_expr_or_die(&deps[0])?; + let p = normalize_fn(premise.clone()); + if p == conclusion.clone() { + Ok(()) + } else { + Err(ProofCheckError::Other(format!("{p} and {conclusion} are not equal. {:?}", premise))) + } +} + fn check_by_normalize_multiple_possibilities(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> where F: Fn(Expr) -> Vec, @@ -1128,7 +1168,7 @@ impl RuleT for BooleanEquivalence { Inverse => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::INVERSE, "none"), Absorption => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_absorption(), "none"), Reduction => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_reduction(), "none"), - Adjacency => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::ADJACENCY, "none"), + Adjacency => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_adjacency(), "none"), } } } @@ -1229,6 +1269,7 @@ impl RuleT for RedundantPrepositionalInference { ExcludedMiddle => "Excluded Middle", ConstructiveDilemma => "Constructive Dilemma", HalfDeMorgan => "Half DeMorgan", + QuantifierInference => "Quantifier Inference", } .into() } @@ -1241,7 +1282,7 @@ impl RuleT for RedundantPrepositionalInference { ModusTollens | HypotheticalSyllogism | DisjunctiveSyllogism => Some(2), ExcludedMiddle => Some(0), ConstructiveDilemma => Some(3), - HalfDeMorgan => Some(1), + HalfDeMorgan | QuantifierInference => Some(1), } } fn num_subdeps(&self) -> Option { @@ -1414,6 +1455,7 @@ impl RuleT for RedundantPrepositionalInference { ) } HalfDeMorgan => check_by_normalize_multiple_possibilities(proof, deps, conclusion, |e| e.normalize_halfdemorgans()), + QuantifierInference => check_by_normalize_first_expr_one_way(proof, deps, conclusion, |e| e.quantifier_inference()), } } } diff --git a/web-app/static/index.html b/web-app/static/index.html index a9761657..260db32d 100644 --- a/web-app/static/index.html +++ b/web-app/static/index.html @@ -5,20 +5,20 @@ Aris - + - + - + - + - + + - + - +