Skip to content

Fix normalize_prenex_laws and add prenex law tests (closes #146) #151

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
etbala merged 4 commits into from
Apr 18, 2025
Merged

Fix normalize_prenex_laws and add prenex law tests (closes #146) #151

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
bc7b967
Add PrenexLaw Tests
etbala Apr 18, 2025
e480292
Fix PrenexLaw Evaluating to False in some Cases
etbala Apr 18, 2025
3430591
Run Formatter
etbala Apr 18, 2025
ed78968
Readd biconditional sub test
etbala Apr 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 47 additions & 30 deletions aris/src/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1444,50 +1444,67 @@ impl Expr {
let body = Box::new(Expr::Impl { left, right });
(Expr::Quant { kind, name, body }, true)
};
self.transform(&|expr| {
let prenex_step = |expr: Expr| -> (Expr, bool) {
match expr {
Expr::Assoc { op, exprs } => match op {
Op::And => transform_7ab(Op::And, exprs),
Op::Or => transform_7ab(Op::Or, exprs),
Op::And | Op::Or => transform_7ab(op, exprs),
_ => (Expr::Assoc { op, exprs }, false),
},

Expr::Impl { mut left, mut right } => {
let left_free = free_vars(&left);
let right_free = free_vars(&right);

// 7c: Quant on left and not captured on right → flip
left = match *left {
Expr::Quant { kind, name, body } if !right_free.contains(&name) => {
// 7c case, quantifier is flipped
match kind {
QuantKind::Forall => {
return reconstruct_7cd(QuantKind::Exists, name, body, right);
}
QuantKind::Exists => {
return reconstruct_7cd(QuantKind::Forall, name, body, right);
}
}
}
left => Box::new(left),
Expr::Quant { kind, name, body } if !right_free.contains(&name) => match kind {
QuantKind::Forall => return reconstruct_7cd(QuantKind::Exists, name, body, right),
QuantKind::Exists => return reconstruct_7cd(QuantKind::Forall, name, body, right),
},
other => Box::new(other),
};

// 7d: Quant on right and not captured on left → no flip
right = match *right {
Expr::Quant { kind, name, body } if !left_free.contains(&name) => {
// 7d case, quantifier is not flipped
// exhaustive match despite the bodies being the same: since if more quantifiers are added, should reconsider here instead of blindly hoisting the new quantifier
match kind {
QuantKind::Forall => {
return reconstruct_7cd(QuantKind::Forall, name, left, body);
}
QuantKind::Exists => {
return reconstruct_7cd(QuantKind::Exists, name, left, body);
}
}
}
right => Box::new(right),
Expr::Quant { kind, name, body } if !left_free.contains(&name) => match kind {
QuantKind::Forall => return reconstruct_7cd(QuantKind::Forall, name, left, body),
QuantKind::Exists => return reconstruct_7cd(QuantKind::Exists, name, left, body),
},
other => Box::new(other),
};

// if neither side hoisted, leave the implication intact
(Expr::Impl { left, right }, false)
}
_ => (expr, false),

// everything else is a no‑op
other => (other, false),
}
})
};

// 1) do *all* possible one‑step hoists
let expr = self.transform(&prenex_step);

// 2) now peel off the entire quantifier prefix
let mut prefix = Vec::new();
let mut body = expr;
while let Expr::Quant { kind, name, body: inner } = body {
prefix.push((kind, name));
body = *inner;
}

// 3) stable‑sort so ∀s come before ∃s (same‐kind keep their relative order)
prefix.sort_by_key(|(kind, _)| match kind {
QuantKind::Forall => 0,
QuantKind::Exists => 1,
});

// 4) rebuild in reverse (so the first in `prefix` is the outermost)
let mut result = body;
for (kind, name) in prefix.into_iter().rev() {
result = Expr::Quant { kind, name, body: Box::new(result) };
}
result
}

/// ¬∀x (φ(x) → ψ(x)) ⇔ ∃x (φ(x) ∧ ¬ψ(x))
Expand Down
87 changes: 87 additions & 0 deletions aris/src/proofs/proof_tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ macro_rules! enumerate_subproofless_tests {
test_bicon_elim, test_bicon_elim_negation, test_exclusion,
test_excluded_middle, test_weak_induction, test_strong_induction,
test_bicon_contraposition, test_biconditionalsubstitution,
test_prenex_basic, test_prenex_full,
}
};
}
Expand Down Expand Up @@ -1512,3 +1513,89 @@ pub fn test_biconditionalsubstitution<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRe
// Return proof and categorized results
(prf, vec![i(r4), i(r5)], vec![i(r6), i(r7), i(r8)])
}

pub fn test_prenex_basic<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
use self::coproduct_inject as i;
use crate::parser::parse_unwrap as p;
let mut prf = P::new();

let p1 = prf.add_premise(p("forall x (P(x) & Q)"));
let p2 = prf.add_premise(p("exists x (P(x) & Q)"));
let p3 = prf.add_premise(p("forall x (P(x) | Q)"));
let p4 = prf.add_premise(p("exists x (P(x) | Q)"));
let p5 = prf.add_premise(p("forall x (P(x) -> Q)"));
let p6 = prf.add_premise(p("exists x (P(x) -> Q)"));
let p7 = prf.add_premise(p("forall x (Q -> P(x))"));
let p8 = prf.add_premise(p("exists x (Q -> P(x))"));

let r1 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
let r2 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
let r3 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
let r4 = prf.add_step(Justification(p("(exists x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
let r5 = prf.add_step(Justification(p("(exists x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
let r6 = prf.add_step(Justification(p("(forall x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
let r7 = prf.add_step(Justification(p("Q -> (forall x P(x))"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
let r8 = prf.add_step(Justification(p("Q -> (exists x P(x))"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));

let r9 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
let r10 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
let r11 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
let r12 = prf.add_step(Justification(p("(exists x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
let r13 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
let r14 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
let r15 = prf.add_step(Justification(p("(forall x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
let r16 = prf.add_step(Justification(p("(exists x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
let r17 = prf.add_step(Justification(p("Q -> (exists x P(x))"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
let r18 = prf.add_step(Justification(p("Q -> (forall x P(x))"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));

(prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8)], vec![i(r9), i(r10), i(r11), i(r12), i(r13), i(r14), i(r15), i(r16), i(r17), i(r18)])
}

pub fn test_prenex_full<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
use self::coproduct_inject as i;
use crate::parser::parse_unwrap as p;
let mut prf = P::new();

let p1 = prf.add_premise(p("exists x P(x) -> exists y Q(y)"));
let p2 = prf.add_premise(p("exists x (P(x) & exists y Q(y))"));
let p3 = prf.add_premise(p("forall x (P(x) | exists y Q(y))"));
let p4 = prf.add_premise(p("forall x (P(x) & exists x Q(x))"));
let p5 = prf.add_premise(p("exists y (P & Q & S(y))"));
let p6 = prf.add_premise(p("forall x (A(x) | B | C)"));
let p7 = prf.add_premise(p("exists x (P(x) & (Q | R))"));
let p8 = prf.add_premise(p("forall x (R | (P(x) -> Q))"));
let p9 = prf.add_premise(p("((exists x (P(x) & ~Q(x))) | (exists y R(y)))"));
let p10 = prf.add_premise(p("exists x (P(x) | forall y Q(y))"));
let p11 = prf.add_premise(p("exists x (P(x) -> exists y (Q(y) -> exists z R(z)))"));
let p15 = prf.add_premise(p("P & Q"));
let p16 = prf.add_premise(p("forall x P(x) & Q(x)"));
let p17 = prf.add_premise(p("exists x P(x) & exists x Q(x)"));
let p18 = prf.add_premise(p("forall x P(x) -> Q(x)"));
let p19 = prf.add_premise(p("exists y forall x R(x,y)"));

let r1 = prf.add_step(Justification(p("forall x (P(x) -> exists y Q(y))"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
let r2 = prf.add_step(Justification(p("exists y (exists x P(x) -> Q(y))"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
let r3 = prf.add_step(Justification(p("(exists x P(x)) & exists y Q(y)"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
let r4 = prf.add_step(Justification(p("exists x P(x) & exists y Q(y)"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
let r5 = prf.add_step(Justification(p("(forall x P(x)) | exists y Q(y)"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
let r6 = prf.add_step(Justification(p("forall x P(x) | exists y Q(y)"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
let r7 = prf.add_step(Justification(p("forall x (P(x) & exists x Q(x))"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
let r8 = prf.add_step(Justification(p("P & Q & exists y S(y)"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
let r9 = prf.add_step(Justification(p("(forall x A(x) | B | C)"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
let r10 = prf.add_step(Justification(p("(exists x P(x)) & (Q | R)"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
let r11 = prf.add_step(Justification(p("R | forall x (P(x) -> Q)"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));
let r12 = prf.add_step(Justification(p("(exists x (exists y ((P(x) & ~Q(x)) | R(y))))"), RuleM::PrenexLaws, vec![i(p9.clone())], vec![]));
let r13 = prf.add_step(Justification(p("((exists x P(x)) | forall y Q(y))"), RuleM::PrenexLaws, vec![i(p10.clone())], vec![]));
let r14 = prf.add_step(Justification(p("((forall x P(x)) -> ((forall y Q(y)) -> exists z R(z)))"), RuleM::PrenexLaws, vec![i(p11.clone())], vec![]));
let r15 = prf.add_step(Justification(p("P & Q"), RuleM::PrenexLaws, vec![i(p15.clone())], vec![]));
let r16 = prf.add_step(Justification(p("forall x P(x) & Q(x)"), RuleM::PrenexLaws, vec![i(p16.clone())], vec![]));
let r17 = prf.add_step(Justification(p("exists x P(x) & exists x Q(x)"), RuleM::PrenexLaws, vec![i(p17.clone())], vec![]));
let r18 = prf.add_step(Justification(p("forall x P(x) -> Q(x)"), RuleM::PrenexLaws, vec![i(p18.clone())], vec![]));
let r19 = prf.add_step(Justification(p("forall x exists y R(x,y)"), RuleM::PrenexLaws, vec![i(p19.clone())], vec![]));

let e1 = prf.add_step(Justification(p("exists x (P & Q)"), RuleM::PrenexLaws, vec![i(p15.clone())], vec![]));
let e2 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p16.clone())], vec![]));
let e3 = prf.add_step(Justification(p("forall x (P(x) -> Q(x))"), RuleM::PrenexLaws, vec![i(p18.clone())], vec![]));

(prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8), i(r9), i(r10), i(r11), i(r12), i(r13), i(r14), i(r15), i(r16), i(r17), i(r18), i(r19)], vec![i(e1), i(e2), i(e3)])
}