证明一个简单的列表函数应用四次就是恒等式

Question

以下视频包含Colm Mulcahy的数学卡技巧：https://www.youtube.com/watch?v=dHzUQnRjbuM

特技中的按键操作定义如下：

COAT(计数和转移)

给定一包n卡，COATingk卡指的是从顶部数出那么多张卡片，形成一堆，从而颠倒它们的顺序，并将它们作为一个单元转移到底部。

(定义取自http://graphics8.nytimes.com/packages/pdf/crossword/Mulcahy_Mathematical_Card_Magic-Sample2.pdf)

在Haskell:

coat k cards = (drop k cards) ++ (reverse . take k $ cards)

示例：

Main> take 5 $ iterate (coat 3) [1..5]

[[1,2,3,4,5],[4,5,3,2,1],[2,1,3,5,4],[5,4,3,1,2],[1,2,3,4,5]]

COAT运算的一个特性是，在4次迭代之后，列表返回到其原始顺序，iffk >= n/2。

为Haskell代码证明这个属性实用吗？证明是否需要使用依赖类型来表达对k的约束？(也许伊德里斯语会是一种更好的语言？)

(我不知道如何处理证明中的迭代。我想在这种情况下，四次迭代可以展开。)

Answer 1

SMT求解器可以处理任何混凝土甲板尺寸的此类证明。对任意甲板尺寸的n进行验证将需要诱导，这超出了自动证明仪的能力，至少目前是这样。(此外，没有任何现成的工具可以使用任意的Haskell程序为您做这样的证明。Liquid Haskell做得很好，但我不确定它是否适合这个目的。)

Haskell的SBV库允许您方便地表达此类问题，将证明义务发送给z3(或其他SMT解决者)以获得按钮体验。以下是如何使用SBV对问题进行编码。

首先介绍一下：

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV
import Data.SBV.List
import Prelude hiding (length, take, drop, reverse, (++))

注意前奏曲中常见函数length/take等的隐藏。我们将使用Data.SBV.List提供的符号等价物。(你必须相信SBV，它们是相同的忠实实现，并将它们扩展到你可以用来证明的符号输入领域。)

正如您所指出的，以下是coat的定义：

coat :: SymVal a => SInteger -> SList a -> SList a
coat k cards = drop k cards ++ reverse (take k cards)

除了"；时髦的"；签名，定义与您给出的相同，即定型的Haskell。签名"；概括"；从具体的整数/列表到它们的符号对应，所以我们可以对它们进行证明。

涂层四次可使用规则成分表示：

fourCoat :: SymVal a => SInteger -> SList a -> SList a
fourCoat k = coat k . coat k . coat k . coat k

让我们将牌组表示为整数列表：

type Deck = SList Integer

把SList Integer想象成[Integer]，它的内容可以是符号值。请注意，一副普通牌会有不同的牌，我们不会在我们的证明中强加这一点。也就是说，无论我们是否将副本放入甲板，证明都是有效的，这概括了你试图建立的定理。

以下是如何将定理作为SBV查询：

coatCheck :: Integer -> IO ThmResult
coatCheck n = prove $ do
deck :: Deck <- free "deck"
k            <- free "k"
constrain $ length deck .== literal n
constrain $ 2*k .>= literal n
pure $ deck .== fourCoat k deck

这部分代码有点涉及。但我们本质上是说，对于任何任意的甲板(free "deck")和任何k，如果你fourCoat甲板，那么你就可以原封不动地把它拿回来(最后一行)。第一个约束将牌组的大小限制在给定的文字值内，即，我们将为一个正好有n张牌的牌组进行证明。第二个约束正是你的定理所规定的，写得稍微重排以避免除以2。注意，k不是固定的：根据给定的约束条件，该证明对任何k都有效。

这个证明怎么样？好吧，这取决于n有多大！以下是n = 6:的演示

*Main> coatCheck 6
Q.E.D.

这大约需要3秒钟才能在我的机器上运行。随着n的增加，解算器时间将增加；但如果你等得足够久，你就会得到证据。(除非你的内存用完，这取决于你的硬件！)

请注意，也可以使参数n具有符号性。虽然SMT求解器能够表达这一点，但在我的实验中，我无法得到任何证据。(它根本没有在合理的时间内返回。)我也没想到：如上所述，这样的证明需要归纳，而SMT解决者还不能完全处理这样的问题。

所以，你的问题的答案是肯定的：如果你愿意斜视正确的方向，为固定尺寸的甲板做证明，那么是的；在Haskell中，有一种自动的方法可以通过使用SMT求解器作为底层引擎来进行此类证明。如果你想要一个任意n的证明，那么你必须使用一个合适的定理证明器，比如Isabelle、Coq、Lean等，当然你必须用他们的母语编程，而不是用Haskell。(尽管他们或多或少接受相同系列的功能程序，而且这个特殊的问题在这些工具中都不难编码。)

您可以在SBV发行版中找到这个问题的完整代码作为示例。