Loading [MathJax]/jax/output/CommonHTML/config.js

开发者社区

文档建议反馈控制台

文章/答案/技术大牛

发布

社区首页 >问答首页 >没有特定目标的交互式定理证明

问没有特定目标的交互式定理证明
EN

Stack Overflow用户

提问于 2018-03-30 06:37:09

回答 1查看 60关注 0票数 2

在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？

数字工厂场景解决方案

帮助企业实现数字化、智能化，解决企业工厂内设备数据采集、设备指标分析、企业信息系统间数据孤岛打通、数据应用困难的问题

EN

回答 1

Stack Overflow用户

发布于 2018-03-30 12:34:42

一种方便的方法是使用Variable/Hypothesis命令(它们做同样的事情)来添加假设并引入示例对象(例如，Variable n:nat.引入了您现在可以使用的nat )。然后进入定理证明模式，我偶尔会做的是，Goal False.，开始证明，False，只是为了确保我不会意外地证明定理。您还可以assert和admit事物，以获得额外的假设，而无需重新启动证明。

票数 0

EN

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/49569621

复制

相关文章

费马小定理证明

　　任意取一个质数，比如13。考虑从1到12的一系列整数1,2,3,4,5,6,7,8,9,10,11,12，给这些数都乘上一个与13互质的数，比如3，得到3,6,9,12,15,18,21,24,27,30,33,36。对于模13来说，这些数同余于3,6,9,12,2,5,8,11,1,4,7,10。这些余数实际上就是原来的1,2,3,4,5,6,7,8,9,10,11,12，只是顺序不同而已。

饶文津

2020/06/02

1.1K0

素数定理整合_素数定理简单证明

https java 网络安全

任何数都可以构造成6N+1,6N+2,6N+3,6N+4,6N+5 只有形如：6N+1和6N+5有可能是素数，其中2，3是特殊的

全栈程序员站长

2022/09/20

5300

裴蜀定理(贝祖定理)及证明

在数论中，裴蜀定理是一个关于最大公约数（或最大公约式）的定理在数论中，裴蜀定理是一个关于最大公约数（或最大公约式）的定理。裴蜀定理得名于法国数学家艾蒂安·裴蜀，说明了对任何整数a、b和它们的最大公约数d，关于未知数x和y的线性丢番图方程（称为裴蜀等式）：　　ax + by = m 　　有解当且仅当m是d的倍数。裴蜀等式有解时必然有无穷多个整数解，每组解x、y都称为裴蜀数，可用辗转相除法求得。　　例如，12和42的最大公因子是6，则方程12x + 42y = 6有解。事实上有(-3)×12 + 1×42

Angel_Kitty

2018/04/09

2.3K0

2.1.2 奈奎斯特定理与香农定理

奈奎斯特定理又称奈氏准则，它指出在理想低通（没有噪音、带宽有限）的信道中，极限码元传输率为2WBaud。其中，W是理想低通信道的带宽，单位是HZ。若用V表示每个码元离散电平的数目，则极限数据率为

week

2018/08/24

2.1K0

贝叶斯定理证明：直觉未必正确

机器学习神经网络深度学习人工智能

直觉是否是第六感，尚且不得而知，仿佛是灵机一动，又或者突然有所感，但从深层次去分析，或许还是来自生活的经验。这些经验未必是自己亲身体验，多数还是道听途说，又或者是被看似真实实则虚假的数据欺骗了。一个例子让数学定理如何证明直觉之虚妄。让我们先来看看生活中的一个小例子。假设有某种疾病D，在10000人中会有1人患此病；又假设对患此病的人进行测试，测试为阳性的比例达到99%，也就是说100名患者中，有99名患者检测结果皆为阳性（positive）。问题：在检测为阳性的情况下，某一个人确定患该病的概率是多少？

张逸

2018/03/07

1.1K0

【运筹学】对偶理论 : 互补松弛性 ( 定理内容 | 定理证明 )

那么其目标函数就是最大值与最小值的界限值 , 将这两个最优解代入到对应的目标函数中 , 求得的两个值是相等的 ;

韩曙亮

2023/03/28

2.2K0

NFL：没有免费午餐定理

机器学习编程算法运维

最近在看机器学习相关的内容，一开始就学到了NFL定理，No Free Lunch Theorem，“没有免费的午餐”定理。这个定理的最重要的寓意就是：

赵成

2018/08/09

8350

【专题】公共数学_中值定理证明题

，则 \(\exists \delta_1 > 0\), \(x\in(a,a+\delta_1)\), \(\exists \delta_2 > 0\), \(x\in(b-\delta_2,b)\), 又由连续函数最值定理可知，

一只野生彩色铅笔

2022/09/20

1.1K0

【专题】公共数学_中值定理证明题

费雪分离定理的证明与评价

费雪分离定理(Fisher Separation Theorem)由经济学家欧文·费雪(Irving Fisher, 1867-1947)提出，该定理指出在完美资本市场(PCM)中，经济主体的投资决策与消费决策可以相互分离，也即投资决策与其消费偏好无关。

数据科学实战

2020/03/25

2.2K0

NFL（没有免费的午餐）定理

编程算法 https 网络安全

NLF讲的是在不考虑具体问题的情况下，没有任何一个算法比另一个算法更优，甚至没有胡乱猜测更好。

里克贝斯

2021/05/21

1.4K0

裴蜀定理、扩展欧几里得算法及其证明

裴蜀定理说明了对任何整数a,b和它们的最大公约数d，关于未知数x和y的线性不定方程：若a,b是整数，且gcd(a,b)=d，那么对于任意的整数x,y,ax+by都一定是d的倍数，特别的，一定存在整数x,y使ax+by=d成立。

fishhh

2022/08/31

1.2K0

裴蜀定理、扩展欧几里得算法及其证明

关于奈奎斯特定理（Nyquist's Theorem）和香农定理（Shannon's Theorem）的理解

我们需要对我们所收到的基带模拟信号（连续信号）进行采样；需要用到狄拉克梳妆函数（采样函数）:

HandSomeHe_In_Fzu

2022/11/23

3.2K0

使用Unsafe获取数组某个特定下标的内容

看ForkJoin源码的时候，发现了一个有趣的用法，在每一个WorkQueue里面都有一个array来存放任务，如果要取一个具体的任务，首先这个array的长度一定是2的次幂，这时候就可以用unsafe里的arrayBaseOffset获取到第一个元素的偏移地址，然后和arrayIndexScale（获取数组里每一个元素的大小）联合使用便可以获得某一个下标的具体位置:

gzq大数据

2022/05/11

8860

扒一扒那些叫欧拉的定理们（七）——欧拉线定理的证明

今天我们接着上一讲，来继续看平面几何欧拉定理的最后一部分内容：欧拉线定理，它也是在上一讲的九点圆定理的基础上的。

magic2728

2021/07/14

3.7K0

扒一扒那些叫欧拉的定理们（六）——九点圆定理的证明

今天我们接着上一讲的平面几何欧拉定理的证明，来看看与之相关的九点圆定理的证明以及其中的数学智慧。

magic2728

2021/07/14

1.4K0

观点 | 不要引用「没有免费的午餐定理」了

编程算法机器学习神经网络深度学习人工智能

AI 科技评论按：「没有免费的午餐定理」一度是机器学习界最常被谈起的定理之一（真正长期被谈起的自然是「更多的数据等于更好的表现」）。不过机器学习科学家 Andreas Mueller 最近撰文表示大家都引用错定理了，其实事情比这更复杂，也有更深远的启示。

AI研习社

2019/07/15

1.3K0

观点 | 不要引用「没有免费的午餐定理」了

扒一扒那些叫欧拉的定理们（五）——平面几何欧拉定理的证明

如下图所示，三角形外心与内心的距离d可表示为：d ^ 2 = R(R - 2r)，其中R为外接圆半径，r为内切圆半径。

magic2728

2021/07/14

3K0

勾股定理竟然有500种证明方法，你会几种？

一个直角三角形，短的直角边叫勾，长的直角边叫股，斜边叫弦。勾的平方加股的平方等于弦的平方，所以称之为勾股定理。

小K算法

2021/05/31

17.9K0

hdu-1098 Ignatius's puzzle（费马小定理）费马小定理同余式证明应用Ignatius's puzzle运行结果

费马小定理费马小定理是数论中的一个定理：假如a是一个整数，p是一个质数，那么是p的倍数，可以表示为如果a不是p的倍数，这个定理也可以写成(同余式写法) 同余式如果两个正整数 a和 b之差能被

致Great

2018/04/11

1.4K0

hdu-1098 Ignatius's puzzle（费马小定理）费马小定理同余式证明应用Ignatius's puzzle运行结果

【组合数学】多项式定理 ( 多项式定理 | 多项式定理证明 | 多项式定理推论 1 项数是非负整数解个数 | 多项式定理推论 2 每项系数之和 )

配置数学原理

根据分步计数原理 , 乘法法则 , 将上面每步的种类个数相乘 , 就是所有的种类个数 :

韩曙亮

2023/03/28

1.3K0

【组合数学】多项式定理 ( 多项式定理 | 多项式定理证明 | 多项式定理推论 1 项数是非负整数解个数 | 多项式定理推论 2 每项系数之和 )

相似问题

证明换位定理

11

自动定理证明

30

命题定理证明

11

MST定理证明

12

Parseval定理的证明

12

活动推荐

SaaS建站+私有服务器，拖拉式完成多端建站，5分钟搭建企业官网

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例