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

开发者社区

文档建议反馈控制台

文章/答案/技术大牛

发布

社区首页 >问答首页 >Coq中定义与让的区别

问Coq中定义与让的区别
EN

Stack Overflow用户

提问于 2015-02-11 08:01:34

回答 1查看 670关注 0票数 5

定义和Coq中的“让”有什么区别？为什么有些定义需要证明？就像。这是群论中g1.v的一段代码。

Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n; clear n.
exact e.
intro n.
 elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.

这个证据的目的是什么？

functional-programming

theorem-proving

EN

回答 1

Stack Overflow用户

回答已采纳

发布于 2015-02-11 08:36:05

我认为您所要求的与Coq中的Definition命令和Let命令之间的区别并没有什么关系。相反，您似乎想知道Coq中的某些定义为什么包含验证脚本。

Coq的一个有趣的特性是，用于编写证明和程序的语言实际上是相同的。这种语言被称为Gallina，它是人们在使用Coq时使用的编程语言。当你写一些类似fun x => x + 5的东西时，这是一个用Gallina编写的程序。

然而，在做证明时，人们通常使用另一种语言，称为Ltac。这是出现在exp示例中的语言。这可能会让你相信Coq中的证据是用另一种语言表示的，但事实并非如此: Ltac脚本所做的就是在Gallina中实际构建验证术语。通过使用Print命令可以看到这一点。

Print exp.

即使证据和程序是用同一种语言编写的，也有一种单独的语言来编写校样，这是因为Gallina在写校样时很难直接使用。尝试在一个复杂的定理上直接使用Print命令，看看这有多难。

现在，尽管Ltac主要是用来写证明的，但是没有什么可以禁止你用它来编写正常的程序，因为最终的产品是一样的: Gallina术语。通常，人们喜欢在编写程序时使用Gallina，因为它更容易阅读。然而，当直接用Gallina编写程序时，人们可能会求助于Ltac，这太麻烦了。我个人更倾向于在示例中直接使用Gallina编写诸如exp之类的函数，尽管这可以说是一个品味问题。

票数 11

EN

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

原文链接：

https://stackoverflow.com/questions/28458842

复制

相关文章

C\C++中声明与定义的区别

弗兰克的猫

2018/01/09

9000

PHP中定义常量的区别，define() 与 const[通俗易懂]

php java https 网络安全打包

这两种方式的根本区别在于const会在代码编译时定义一个常量，而define则是在代码运行时才定义一个常量。这就使得const会有以下几个缺点：

全栈程序员站长

2022/07/11

1.2K0

申明与定义的区别

C++编码过程中，我们经常谈及“定义”和“声明”，二者是编程过程中的基本概念。我们需要使用一个变量、类型（类、结构体、枚举、共用体）或者函数时，我们需要提前定义和申明。定义和申明的过程，就像我们向图书馆借阅书籍一般，需要先完成书籍的印刷，即创造出书籍，这是一个定义的过程，有了书籍，我们需要到图书馆完成借阅的登记手续，这是申明的过程。完成了申明，我们有了使用书籍的权限，就可以尽情的畅游在知识的海洋。如果说书籍是自己委托印刷厂印刷的，那么你无需向他人借阅，即无需声明，可以直接使用书籍。一本书籍只需要印刷一次，但是可以被多人多次借阅，也就是说定义只需要一次，但是申明可以有多次。这里的书籍指代的是“定义”和“声明”作用的对象，即变量、类型和函数。C/C++中，使用一个变量、类型或者函数必须先在使用前完成定义和申明。

恋喵大鲤鱼

2018/08/03

1.6K0

JavaScript中var与新定义的ES6中的let的区别

javascript java 编程算法

JavaScript最初由Netscape的Brendan Eich设计，最初将其脚本语言命名为LiveScript，后来Netscape在与Sun合作之后将其改名为JavaScript。JavaScript最初受Java启发而开始设计的，目的之一就是“看上去像Java”，因此语法上有类似之处，一些名称和命名规范也借自Java，但JavaScript的主要设计原则源自Self和Scheme。JavaScript与Java名称上的近似，是当时Netscape为了营销考虑与Sun微系统达成协议的结果。微软同时期也推出了JScript来迎战JavaScript的脚本语言。

淼学派对

2022/11/20

4090

JavaScript中var与新定义的ES6中的let的区别

jQuery中this与$(this)的区别

jQuery中this与$(this)的区别 $("#textbox").hover( function() { this.title = "Test"; }, fucntion() { this.title = "OK”; } ); 这里的this其实是一个Html 元素(textbox)，textbox有text属性，所以这样写是完全没有什么问题的。但是如果将this换成$(thi

用户1258909

2018/07/03

8500

shell中$(( ))、$( )与${ }的区别

bash 编程算法

在bash中，$( )与` `（反引号）都是用来作命令替换的。命令替换与变量替换差不多，都是用来重组命令行的，先完成引号里的命令行，然后将其结果替换出来，再重组成新的命令行。

wuweixiang

2019/04/09

1.3K0

shell中$(( ))、$( )与${ }的区别

mybatis 中#与$的区别

先看一个例子例如对于如下sql select xxx t where t.name=#{name} order by ${name} 如果传入的值是张三，那么mybatis内部解析之后就会变成 select xxx t where t.name='张三' order by 张三如你所见，他们之间大概有以下几点区别 #将传入的数据都当成一个字符串，会对自动传入的数据加一个双引号。$将传入的数据直接显示生成在sql中。因为第一点，所以#更适合传递参数，而$更适合传递数据库对象，如字段或者表名。因为第一点

诺浅

2020/08/21

7260

Mybatis中#{}与${}的区别

腾讯云测试服务 sql mybatis

总结：也就是说使用#{}时，mybatis会自动加上引号。如果不想让加那么就使用${}

手撕代码八百里

2020/07/28

6530

Mybatis中#{}与${}的区别

Mybatis中的#与$的区别

数据库 mybatis time 数据字符串

解决办法：将collect_#{tblNum}修改为collect_${tblNum}即可解决问题。

翎野君

2023/05/12

7310

Python中的 // 与 / 的区别

通常C/C++中，"/ " 算术运算符的计算结果是根据参与运算的两边的数据决定的，比如：　　6 / 3 = 2 ; 6,3都是整数，那么结果也就是整数2; 　　6.0 / 3.0 = 2.0 ; 6.0,3.0是浮点数，那么结果也是浮点数2.0，跟精确的说，只要" / " 两边有一个数是浮点数，那么结果就是浮点数。　　在Python2.2版本以前也是这么规定的，但是，Python的设计者认为这么做不符合Python简单明了的特性，于是乎就在Python2.2以及以后的版本中增加了一个算术运算符" //

py3study

2020/01/10

7900

Python中的 // 与 / 的区别

" / " 表示浮点数除法，返回浮点结果;" // " 表示整数除法,返回不大于结果的一个最大的整数print("6 // 4 = " + str(6 // 4))print("6 / 4 =" + str(6 / 4))Output:------------6 // 4 = 16 / 4 =1.5------------

狼啸风云

2019/10/22

1K0

白盒测试与黑盒测试的定义与区别

白盒测试方法按照程序内部的结构测试程序，检验程序中的每条通路是否都能按预定要求正确工作，而不顾它的功能。

week

2018/08/27

9430

Python中的/与//的区别

java https 网络安全

问题，在/与//的应用中会出现整数与浮点数判定的情况，而具体的解释自己也没发现合理的解释：

全栈程序员站长

2022/09/07

5560

java中 == 与 equal 的区别

废话不多说了，开门见山吧，先来看一段代码： String str1 = new String("str"); String str2 = new String("str"); System.out.println("==比较："+ (str1 == str2)); System.out.println("equal比较："+ str1.equals(str2)); String str3 = "str1"; String st

Java帮帮

2018/03/16

8370

java中 == 与 equal 的区别

MyBatis 中$与#号的区别

sql mybatis 网络安全编程算法

#号的功能非常强大，如果有自定义类型需要调整，如将java中自定义的枚举类型转换为数据库中的数字时，只需要自定义一个typeHandler，在参数中指定就可以。

兜兜毛毛

2021/09/06

1.1K0

C#中？与？？的区别

mvc 人工智能 .net

起初我也不知道C#中有？？操作符，今天张鹏在查看我的MVC示例程序的时候问了这个问题，检查代码后发现，下面的代码是VS2010在生成MVC应用程序自己添加的： public Accou

用户1177503

2018/02/26

9890

js中const,var,let定义变量的区别

js中const,var,let定义变量的区别 1.const定义变量不可以修改，而且必须初始化 const b = 2;//正确 // const b;//错误，必须初始化 console.log('函数外const定义b：' + b);//有输出值 // b = 5; // console.log('函数外修改const定义b：' + b);//无法输出 2.var定义的变量可以修改，如果不初始化会输出undefined，不会报错 var a = 1;

别盯着我的名字看

2022/06/09

3.4K0

bash shell 中，$* 与 $@ 的区别与联系

两段脚本差别很小，只是多了两个引号而已。也就是说：$* 是带了引号分割的；$@ 是没有带引号分割的，原模原样的字符串。使用的时候注意区分即可。再来看一下下面的例子：

耕耘实录

2019/07/03

1.1K0

mysql 中 and 与&& 区别与用法

python 编程算法

CREATE FUNCTION `get_times_weeek` ( last_accting_date DATETIME, nursePerformTime VARCHAR (50) ) RETURNS INT (11) COMMENT '计算以周为单位的计费次数' BEGIN DECLARE return_val INT DEFAULT 0 ; DECLARE flag BOOLEAN DEFAULT FALSE ; DECLARE weekNo INT ; DECLARE s_index INT ; IF last_accting_date IS NOT NULL && DATE_FORMAT(NOW(), '%Y-%m-%d') = DATE_FORMAT(last_accting_date, '%Y-%m-%d') THEN SET return_val = 0 ; ELSE SELECT DAYOFWEEK(NOW()) INTO weekNo ; IF weekNo = 1 THEN SET weekNo = 7 ; ELSE SET weekNo = weekNo - 1 ; END IF ; SELECT LOCATE(weekNo, nursePerformTime) INTO s_index ; IF s_index > 0 THEN SET return_val = 1 ; ELSE SET return_val = 0 ; END IF ; END IF ; RETURN return_val ;

爱明依

2019/03/12

4.7K0

点击加载更多

相似问题

Z3与coq的区别

11

定义中的“其他”- Coq

21

coq中范式的定义

21

Coq中循环类型的定义

11

Coq中的合取与隐含

10

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例