From ca6ad3288b7a9759ebe9a48f9edc0c8b82d965e4 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 7 Oct 2024 10:01:24 -0700 Subject: [PATCH] Add KD proof for 11^n-4^n divides 7 --- .../SBV/Examples/KnuckleDragger/Induction.hs | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs index ea027b459..68fe97e09 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs @@ -80,3 +80,26 @@ sumSquareProof = runKD $ do p n = observe "imp" (sumSquare n) .== observe "spec" (spec n) lemma "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct p] + +-- | Prove that @11^n - 4^n@ is always divisible by 7. Note that power operator is hard for +-- SMT solvers to deal with due to non-linearity, so we use an axiomatization of it instead. +-- +-- We have: +-- +-- >>> elevenMinusFour +-- Axiom: pow0 Axiom. +-- Axiom: powN Axiom. +-- Lemma: elevenMinusFour Q.E.D. +-- [Proven] elevenMinusFour +elevenMinusFour :: IO Proof +elevenMinusFour = runKD $ do + let pow :: SInteger -> SInteger -> SInteger + pow = uninterpret "pow" + + emf :: SInteger -> SBool + emf n = 7 `sDivides` (11 `pow` n - 4 `pow` n) + + pow0 <- axiom "pow0" (\(Forall @"x" x) -> x `pow` 0 .== 1) + powN <- axiom "powN" (\(Forall @"x" x) (Forall @"n" n) -> x `pow` (n+1) .== x * x `pow` n) + + lemma "elevenMinusFour" (\(Forall @"n" n) -> n .>= 0 .=> emf n) [pow0, powN, induct emf]