相关疑难解决方法(0)

我来自JavaScript/Ruby编程背景,我习惯这是真/假的工作原理(在JS中):

!true
// false
!false
// true

然后你就可以使用这些真/假值与&&像

var a = true, b = false;
a && !b;

所以,而不是(和其他逻辑/布尔运算符)是单个系统的一部分; 似乎"逻辑"系统和"布尔"系统是同一个系统.

但是,在Coq中,逻辑和布尔值是两个不同的东西.为什么是这样？下面的引用/链接演示了如何将定理与它们联系起来.

我们已经看到过几个可以在Coq的计算(类型)和逻辑(Prop)世界中找到类似结构的地方.还有一个:布尔运算符andb和orb显然是逻辑连接词的类似物？和？通过以下定理可以使这种类比更加精确,这些定理表明如何将关于orb和orb在某些输入上的行为的知识转化为关于这些输入的命题事实.

Theorem andb_prop : ?b c,
  andb b c = true ? b = true ? c = true.

Run Code Online (Sandbox Code Playgroud)

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211