Hoogle Search

Within LTS Haskell 24.32 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. sum0Coefficients :: SHA w -> (Int, Int, Int)

   sbv	Documentation.SBV.Examples.Crypto.SHA

   Section 4.1.2-3 : Coefficients of the Sum0 function

2. sum1 :: Bits a => SHA w -> a -> a

   sbv	Documentation.SBV.Examples.Crypto.SHA

   The sum-1 function. Again, parameterized.

3. sum1Coefficients :: SHA w -> (Int, Int, Int)

   sbv	Documentation.SBV.Examples.Crypto.SHA

   Section 4.1.2-3 : Coefficients of the Sum1 function

4. sumHalves :: IO Proof

   sbv	Documentation.SBV.Examples.KnuckleDragger.Lists

   We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses strong induction. We have:

   >>> sumHalves
   Inductive lemma: sumAppend
   Step: Base                            Q.E.D.
   Step: 1                               Q.E.D.
   Step: 2                               Q.E.D.
   Step: 3                               Q.E.D.
   Result:                               Q.E.D.
   Inductive lemma (strong): sumHalves
   Step: Measure is non-negative         Q.E.D.
   Step: 1 (2 way full case split)
   Step: 1.1                           Q.E.D.
   Step: 1.2 (2 way full case split)
   Step: 1.2.1                       Q.E.D.
   Step: 1.2.2.1                     Q.E.D.
   Step: 1.2.2.2                     Q.E.D.
   Step: 1.2.2.3                     Q.E.D.
   Step: 1.2.2.4                     Q.E.D.
   Step: 1.2.2.5                     Q.E.D.
   Step: 1.2.2.6 (simplify)          Q.E.D.
   Result:                               Q.E.D.
   [Proven] sumHalves
   

5. sumConstProof :: IO Proof

   sbv	Documentation.SBV.Examples.KnuckleDragger.Numeric

   Prove that sum of constants c from 0 to n is n*c. We have:

   >>> sumConstProof
   Inductive lemma: sumConst_correct
   Step: Base                            Q.E.D.
   Step: 1                               Q.E.D.
   Step: 2                               Q.E.D.
   Step: 3                               Q.E.D.
   Step: 4                               Q.E.D.
   Step: 5                               Q.E.D.
   Result:                               Q.E.D.
   [Proven] sumConst_correct
   

6. sumProof :: IO Proof

   sbv	Documentation.SBV.Examples.KnuckleDragger.Numeric

   Prove that sum of numbers from 0 to n is n*(n-1)/2.

   >>> sumProof
   Inductive lemma: sum_correct
   Step: Base                            Q.E.D.
   Step: 1                               Q.E.D.
   Step: 2                               Q.E.D.
   Step: 3                               Q.E.D.
   Result:                               Q.E.D.
   [Proven] sum_correct
   

7. sumSquareProof :: IO Proof

   sbv	Documentation.SBV.Examples.KnuckleDragger.Numeric

   Prove that sum of square of numbers from 0 to n is n*(n+1)*(2n+1)/6.

   >>> sumSquareProof
   Inductive lemma: sumSquare_correct
   Step: Base                            Q.E.D.
   Step: 1                               Q.E.D.
   Step: 2                               Q.E.D.
   Step: 3                               Q.E.D.
   Result:                               Q.E.D.
   [Proven] sumSquare_correct
   

8. sumToN :: SInteger -> SInteger

   sbv	Documentation.SBV.Examples.Misc.Definitions

   Sum of numbers from 0 to the given number. Since this is a recursive definition, we cannot simply symbolically simulate it as it wouldn't terminat. So, we use the function generation facilities to define it directly in SMTLib. Note how the function itself takes a "recursive version" of itself, and all recursive calls are made with this name.

9. sumToNExample :: IO SatResult

   sbv	Documentation.SBV.Examples.Misc.Definitions

   Prove that sumToN works as expected. We have:

   >>> sumToNExample
   Satisfiable. Model:
   s0 =  5 :: Integer
   s1 = 15 :: Integer
   

10. sumCorrect :: IO (InductionResult (S Integer))

    sbv	Documentation.SBV.Examples.ProofTools.Sum

    Encoding partial correctness of the sum algorithm. We have:

    >>> sumCorrect
    Q.E.D.
    

Page 58 of many | Previous | Next