From c1a41d447ed1c791efa3f93892048b3005df454e Mon Sep 17 00:00:00 2001 From: Benjamin Levy <7348004+io12@users.noreply.github.com> Date: Mon, 27 Mar 2023 18:18:37 -0400 Subject: [PATCH] Add strong induction (#104) --- aris/src/proofs/proof_tests.rs | 17 ++++++++++- aris/src/rules.rs | 53 ++++++++++++++++++++++++++++------ 2 files changed, 60 insertions(+), 10 deletions(-) diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index 96868509..f85a49e4 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -69,7 +69,7 @@ macro_rules! enumerate_subproofless_tests { test_inverse, test_absorption, test_reduction, test_adjacency, test_resolution, test_tautcon, test_empty_rule, test_modus_tollens, test_hypothetical_syllogism, test_disjunctive_syllogism, test_constructive_dilemma, test_excluded_middle, - test_weak_induction, + test_weak_induction, test_strong_induction, } }; } @@ -1137,3 +1137,18 @@ pub fn test_weak_induction() -> (P, Vec>, 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)]) } + +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![])); + (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 363af8d5..0cbc6e4c 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -177,6 +177,7 @@ pub enum QuantifierEquivalence { #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum Induction { Weak, + Strong, } /// This should be the default rule when creating a new step in a UI. It @@ -311,6 +312,7 @@ pub mod RuleM { [PrenexLaws, "PRENEX_LAWS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::PrenexLaws)))))))))], [WeakInduction, "WEAK_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Weak))))))))))], + [StrongInduction, "STRONG_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Strong))))))))))], [EmptyRule, "EMPTY_RULE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(super::EmptyRule)))))))))))] } @@ -1457,6 +1459,7 @@ impl RuleT for Induction { fn get_name(&self) -> String { match self { Induction::Weak => "Weak induction", + Induction::Strong => "Strong induction", } .into() } @@ -1468,24 +1471,23 @@ impl RuleT for Induction { fn num_deps(&self) -> Option { match self { Induction::Weak => Some(2), + Induction::Strong => Some(1), } } fn num_subdeps(&self) -> Option { - match self { - Induction::Weak => Some(0), - } + Some(0) } fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + // Check conclusion + let (quantified_var, property) = match &conclusion { + Expr::Quant { kind: QuantKind::Forall, name, body } => (name, &**body), + _ => return Err(ProofCheckError::ConclusionOfWrongForm(Expr::quant_placeholder(QuantKind::Forall))), + }; + match self { Induction::Weak => { - // Check conclusion - let (quantified_var, property) = match &conclusion { - Expr::Quant { kind: QuantKind::Forall, name, body } => (name, &**body), - _ => return Err(ProofCheckError::ConclusionOfWrongForm(Expr::quant_placeholder(QuantKind::Forall))), - }; - let prem1 = p.lookup_expr_or_die(&deps[0])?; let prem2 = p.lookup_expr_or_die(&deps[1])?; either_order( @@ -1525,6 +1527,39 @@ impl RuleT for Induction { || ProofCheckError::Other("Failed finding base case that matches conclusion".into()), ) } + Induction::Strong => { + // ∀ n, (∀ x, x < n → property(x)) → property(n) + // ---- + // ∀ quantified_var, property(quantified_var) + let prem = p.lookup_expr_or_die(&deps[0])?; + let (n, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = prem { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(prem, Expr::quant_placeholder(QuantKind::Forall))) }; + let (e, property_n) = if let Expr::Impl { left, right } = e { (*left, *right) } else { return Err(ProofCheckError::DepOfWrongForm(e, Expr::impl_place_holder())) }; + if crate::expr::free_vars(&conclusion).contains(&n) { + return Err(ProofCheckError::Other(format!("Variable '{n}' is free in '{conclusion}'"))); + } + let expected_property_n = crate::expr::subst(property.clone(), quantified_var, Expr::var(&n)); + if property_n != expected_property_n { + return Err(ProofCheckError::DepOfWrongForm(property_n, expected_property_n)); + } + let (x, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = e { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(e, Expr::quant_placeholder(QuantKind::Forall))) }; + let (x_lt_n, property_x) = if let Expr::Impl { left, right } = e { + (*left, *right) + } else { + return Err(ProofCheckError::DepOfWrongForm(e, Expr::impl_place_holder())); + }; + if crate::expr::free_vars(&conclusion).contains(&x) { + return Err(ProofCheckError::Other(format!("Variable '{x}' is free in '{conclusion}'"))); + } + let expected_x_lt_n = Expr::apply(Expr::var("LessThan"), &[Expr::var(&x), Expr::var(&n)]); + if x_lt_n != expected_x_lt_n { + return Err(ProofCheckError::DepOfWrongForm(x_lt_n, expected_x_lt_n)); + } + let expected_property_x = crate::expr::subst(property.clone(), quantified_var, Expr::var(&x)); + if property_x != expected_property_x { + return Err(ProofCheckError::DepOfWrongForm(property_x, expected_property_x)); + } + Ok(()) + } } } }