在讨论 Idris 中定理证明的细节之前，我们先介绍一些基本概念：
命题与判断（Propositions and Judgments）
布尔逻辑与构造性逻辑（Boolean and Constructive Logic）
Curry-Howard 对应（Curry-Howard Correspondence）
定义等式与命题等式（Definitional and Propositional Equalities）
公理化与构造性方法（Axiomatic and Constructive Approaches）
命题与判断（Propositions and Judgments）
命题是我们证明的对象。在证明之前，我们无法正式判断它们是否为真。如果证明成功，那么结果就是一个'判断'。例如，如果``proposition``是，
1+1=2 |
当我们证明它时，判断 为：
1+1=2 成立（true） |
或者如果 命题 为：
1+1=3 |
我们无法证明它为真，但它依然是一个有效命题，也许我们可以证明它为假，因此 判断 为：
1+1=3 不成立（false） |
这看起来有些迂腐，但必须谨慎：在数学中，并非每个命题都是真或假。例如，有些命题可能尚未被证明，甚至无法被证明。
因此，这里的逻辑不同于布尔代数中的逻辑。在布尔逻辑中，非真即假，非假即真。而我们这里使用的逻辑并不具备这种"排中律（Law of Excluded Middle）"，因此不能使用它。
一个假命题被视为矛盾（contradiction），而一旦有矛盾就可以推出任何结论，因此我们要避免这种情况。一些用于证明助理的语言会防止矛盾的出现。
我们使用的逻辑被称为构造性逻辑（constructive logic，或称直觉主义逻辑），因为我们是在构建一个"判断数据库（database of judgments）"。
Curry-Howard 对应（Curry-Howard Correspondence）
那么，如何将这些证明与 Idris 程序关联起来？事实证明，构造性逻辑与类型理论（type theory）之间存在对应关系。它们具有相同的结构，我们可以在两种记法之间自由切换。
其原理是：命题就是类型（a proposition is a type），因此...
Main> 1 + 1 = 2
2 = 2
Main> :t 1 + 1 = 2
(fromInteger 1 + fromInteger 1) === fromInteger 2 : Type
......既是命题，也是类型。下列写法同样会产生一个等式类型：
Main> 1 + 1 = 3
2 = 3
这两者都是有效命题，因此也是有效的等式类型。但我们如何表示一个"成立的判断"呢？也就是说，如何表示 1+1=2 成立而 1+1=3 不成立？一个"成立"的类型是可被实例化（inhabited）的，即它可以被构造。等式类型只有一个构造器 'Refl'，因此 1+1=2 的证明为：
onePlusOne : 1+1=2
onePlusOne = Refl
既然我们可以用类型表示命题，命题逻辑的其他方面也可以如下转化为类型：
命题（propositions） |
可能的类型示例（example of possible type） |
|
A |
x=y |
|
B |
y=z |
|
与（and） |
A /\ B |
Pair(x=y,y=z) |
或（or） |
A \/ B |
Either(x=y,y=z) |
蕴含（implies） |
A -> B |
(x=y) -> (y=z) |
对所有（for all） |
y=z |
|
存在（exists） |
y=z |
与（合取，And/Conjunction）
我们可以有一个与合取对应的类型：
AndIntro : a -> b -> A a b
内置有一个名为 'Pair' 的类型。
或（析取，Or/Disjunction）
我们可以有一个与析取对应的类型：
data Or : Type -> Type -> Type where
OrIntroLeft : a -> A a b
OrIntroRight : b -> A a b
内置有一个名为 'Either' 的类型。
定义等式与命题等式（Definitional and Propositional Equalities）
我们已经看到，可以通过构造一个项来"证明"一个类型。对于等式类型，只有一个构造器 Refl。我们还看到，等式两边不必像 '2=2' 那样完全相同，只要两边*定义上相等*即可，例如：
onePlusOne : 1+1=2
onePlusOne = Refl
该等式两边都归约为 2，因此 Refl 匹配，命题得证。
我们不必局限于具体项，也可以使用符号参数，因此如下类型也是可通过类型检查的：
varIdentity : m = m
varIdentity = Refl
如果一个命题/等式类型不是定义等价但依然为真，那么它就是*命题等价（propositionally equal）*。在这种情况下，我们仍然可以证明它，但证明过程中可能需要对项做一些变换，或者采取一些间接步骤来完成证明。
尤其是在处理包含变量项（如函数内部）的等式时，判断哪些等式类型是定义等价的会比较困难。在本例中，plusReducesL 是*定义等价*，而 plusReducesR 不是（尽管它是*命题等价*）。两者唯一的区别在于操作数的顺序。
plusReducesL : (n:Nat) -> plus Z n = n
plusReducesL n = Refl
plusReducesR : (n:Nat) -> plus n Z = n
plusReducesR n = Refl
检查 plusReducesR 时会出现如下错误：
Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1:
Can't solve constraint between:
plus n Z
and
n
那么，为什么 Refl 能证明某些等式类型而不能证明其他的？
第一个原因是 plus 是按第一个参数递归定义的。因此，当第一个参数为 Z 时可以归约，但第二个参数为 Z 时则不能。
如果一个等式类型可以仅用 Refl 证明/构造，则称为*定义等式（definitional equality）*。要定义等价，等式两边必须归约为同一个值。
因此，在 Idris 中输入 1+1 时会立即归约为 2，因为定义等式是内建的。
Main> 1+1
2
在接下来的页面中，我们将讨论如何解决命题等式。