KD: Add reverse (length xs) = length xs proof.

CHANGES.md

@@ -9,6 +9,8 @@
     by the same name: https://github.com/philzook58/knuckledragger.
 
   * Added several KnuckleDragger proof examples, see Documentation.SBV.Examples.KnuckleDragger modules.
+    Amongst the proofs are the irrationality of square-root of 2, several list lemmas, and a few
+    inductive proofs over naturals.
 
   * Add sDivides, which takes a concrete integer and a (possibly symbolic), and returns sTrue
     if the first argument divides the second. It is essentially equivalent to @a `sMod` n .== 0`,

Documentation/SBV/Examples/KnuckleDragger/RevLen.hs

@@ -0,0 +1,42 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.RevLen
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Proof that reversing a list does not change its length.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.RevLen where
+
+import Prelude hiding (length, reverse)
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+import Data.SBV.List (reverse, length)
+
+-- | @length xs == length (reverse xs)@
+--
+-- We have:
+--
+-- >>> revLen
+-- Lemma: revLen                           Q.E.D.
+revLen :: IO Proven
+revLen = do
+   let p :: SList Integer -> SBool
+       p xs = length (reverse xs) .== length xs
+
+   induct <- inductionPrinciple p
+
+   lemma "revLen"
+         (\(Forall @"xs" xs) -> p xs)
+         [induct]

sbv.cabal

@@ -156,6 +156,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen
+                  , Documentation.SBV.Examples.KnuckleDragger.RevLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate