Add strong induction (#104)

Bram-Hub · Mar 27, 2023 · c1a41d4 · c1a41d4
1 parent f34c9a8
commit c1a41d4
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 10 deletions.
diff --git 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: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     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: 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 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
@@ -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<usize> {
         match self {
             Induction::Weak => Some(2),
+            Induction::Strong => Some(1),
         }
     }
 
     fn num_subdeps(&self) -> Option<usize> {
-        match self {
-            Induction::Weak => Some(0),
-        }
+        Some(0)
     }
 
     fn check<P: Proof>(self, p: &P, conclusion: Expr, deps: Vec<PjRef<P>>, _sdeps: Vec<P::SubproofReference>) -> Result<(), ProofCheckError<PjRef<P>, 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(())
+            }
         }
     }
 }