blob: 159fbad0a6df826b64fe6f2624fccba636bfc2f5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
+++
title = "Inductive Predicates"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b3b"]
forwardlinks = ["3b3d"]
zettelid = "3b3c"
+++
`tauto` is a complete decision procedure to solve propositional proofs,
however, if other theorems are needed, then intuition can be used to
prove more about those theorems.
Coq implements *constructive*, or *intuitionistic* logic. Therefore,
simple theorems like $\neg \neg P \rightarrow P$ do not always hold, and
can only be proven if *P* is decidable.
Therefore, the difference between `Prop` and `bool` is that `Prop` is
often not decidable and cannot be constructed, whereas `bool` terms can
be constructed by default.
We can also think of `forall` as the type constructor for dependent
function type constructor. This is because implication and `forall` are
actually the same, for example we can define `forall x : P, Q`, where x
does not appear in `Q`, which is equivalent to `P -> Q`.
|
