标签: proof

我们如何证明以下内容？：

Lemma forfun: forall (A B : nat->nat), (forall x:nat, A x = B x) ->
                                       (fun x => A x) = (fun x => B x).
Proof.

众所周知，内存中的负数通常表示为二进制补码

from x to ~x + 1

为了回来，我们不会做明显的事情，比如

~([~x + 1] - 1)

但我们这样做

~[~x + 1] + 1

有人可以解释为什么它总是有效吗？我想我可以用 1 位、2 位、3 位数字来证明它，然后使用数学归纳法，但这并不能帮助我理解它究竟是如何工作的。

谢谢！

优化编译器的最终目的是在程序空间中搜索与原始程序等效但速度更快的程序。这已在实践中针对非常小的基本块完成：https : //en.wikipedia.org/wiki/Superoptimization

听起来困难的部分是搜索空间的指数性质，但实际上并非如此；困难的部分是，假设你找到了你正在寻找的东西，你如何证明新的、更快的程序真的等同于原始程序？

上次我研究它时，在证明某些上下文中程序的某些属性方面取得了一些进展，特别是在讨论标量变量或小的固定位向量时在很小的范围内，但在证明程序的等效性方面并没有真正取得进展当您谈论复杂的数据结构时，规模更大。

有没有人想出一种方法来做到这一点，甚至“模解决这个我们还不知道如何解决的 NP 难搜索问题”？

编辑：是的，我们都知道停机问题。它是根据一般情况定义的。人类是一个存在证明，这可以用于许多感兴趣的实际案例。

我需要证明：256 * (x / 256) <= 256 * x / 256，或更一般地说forall a b c : N, c > 0 -> a * (b / c) <= a * b / c。这是真的，因为要么 b 可以被 c 整除并且它们相等，要么不相等，首先乘法可以扩大数字并导致更高的精度。但是，我在标准库中找不到任何可以证明这一点的定理，而且我知道的任何自动策略（auto、intuition、easy、zify 和 omega）都不起作用。如果有帮助，我也知道x < 256 * 256，但是检查所有 65536 个案例并不是一个很好的证明......

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ? false) -> CoNat

open CoNat public

我定义zero和plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ? iszero n
pred (plus m n) _ with iszero m | inspect iszero m …

在 Cubical Agda 的标准库中，有一些有限的多重集，我在下面重现了它们的优雅定义：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude

infixr 20 _?_

data FMSet (A : Set) : Set where
  []    : FMSet A
  _?_   : (x : A) ? (xs : FMSet A) ? FMSet A
  comm  : ? x y xs ? x ? y ? xs ? y ? x ? xs
  trunc : isSet (FMSet A)

_++_ : ? {A : Set} -> FMSet A ? FMSet A ? FMSet A …

我有这些类型的家庭：

type family xs ++ ys where
  '[]      ++ ys = ys
  (x : xs) ++ ys = x : (xs ++ ys)

type family Drop n xs where
  Drop  O         xs  = xs
  Drop (S n) (_ : xs) = Drop n xs

type family Length xs where
  Length '[] = O
  Length  (x : xs) = S (Length xs)

在某些时候，GHC 想要证明

forall a. Drop (Length a) (a ++ c) ~ c

我曾经把它推到一些构造函数的上下文中。

我如何普遍证明这个属性？

当对cases归纳数据类型使用 - 策略时，精益会生成多个案例，但不会创建说明当前案例假设的假设。例如：

inductive color | blue | red\n\ntheorem exmpl (c : color) : true :=\nbegin\n    cases c,\nend\n

导致以下战术状态

case color.blue\n\xe2\x8a\xa2 true\ncase color.red\n\xe2\x8a\xa2 true\n

但没有创建一个单独的假设（如c = color.red）来使用。你如何得到这样的假设？

我想知道这个陈述背后的逻辑,证据.对于任何x,C表达式-x,~x + 1和〜(x-1)都产生相同的结果.我可以证明这对于具体的例子是正确的.我认为证明这一点的方法与两个补码的属性有关.有任何想法吗？

我有这个定理(不确定这是否是正确的词),我想得到所有的解决方案.

pairCube limit = do
    m <- natural exists "m"
    n <- natural exists "n"
    a <- natural exists "a"
    constrain $ m^3 .== n^2
    constrain $ m .< limit
    return $ m + n .== a^2

res <- allSat (pairCube 1000)

-- Run from ghci
extractModels res :: [[Integer]]

这是试图解决问题:

存在无限的整数对(m,n),使得m ^ 3 = n ^ 2并且m + n是完美的正方形.什么是最小m小于1000的那对？

我知道实际的答案,只是通过暴力强迫,但我想用SBV做.

但是,当我运行代码时,它只给出以下值(格式为[m,n,a]):[[9,27,6],[64,512,24],[]]

但是,还有其他一些m值小于1000的解决方案,不包括在内.