All syntactically well-formed propositions in Coq have type `Prop`

in Coq. Propositions are not necessarily provable.

Functions that return propositions are called *parameterized* propositions; they define *properties* of their arguments.

For a *conjunction*, we use `split`

to separate it and prove each of them if it appears in the goal, but use `destruct`

if it appears in the hypothesis.

For a *disjunction*, we use `left`

or `right`

to prove only one branch if it appears in the goal, but use `destruct`

to separate them into branches and prove the goal with each branch taken as the premise.

`¬`

`P`

is a representation of to `P`

`→`

`False`

. Anything can follow from `False`

; this rule is called *ex falso quodlibet*, or the principle of explosion. If the goal is controversial, we can use this rule by the `exfalso`

tactic, turning the goal into `False`

.

The “if and only if” connective is reflexive, symmetric, and transitive; it is an equivalence relation. This means we can use `reflexivity`

, `symmetry`

, and `rewrite`

on “`↔`

” connected propositions, like on equations.

To prove a statement containing an existential quantification, we find a value that *witnesses* the existential.

We can define propositions recursively, but this method is limited by Coq’s requirements for functions, for example, “obviously terminating.” We can also define propositions *inductively*.

Coq treats *proofs* as first-class objects. The type of a proof is the proposition which it is a proof of. We can apply theorems to statements like applying a function; they have the same inference mechanism.

In Coq, we say that a property holds for a mathematical object, not that a mathematical object belongs to some set. This is because Coq’s logical core is the *Calculus of Inductive Constructions*, instead of set theory (e.g. Zermelo–Fraenkel Set Theory).

Coq’s equality operator is polymorphic, we can use it to claim that two *functions* are equal. It is common to consider two functions the same if we observe the same behavior from them:

```
(∀ x, f x = g x) → f = g
```

This is the principle of *functional extensionality*, we can define it as an axiom in Coq. Sometimes adding an axiom to Coq can break *consistency*, that is, we may be able to prove every proposition.

Coq’s language is *computational*, every function it can express is computable and total. Coq doesn’t have an operation to do case analyses on propositions, since allowing such operation would allow non-computable functions.

Many *computable* properties are easier to express using propositions rather than booleans, since recursive function definitions in Coq are subject to significant restrictions.

If a boolean function gives `true`

if and only if a proposition holds, we say that the boolean computation is *reflected* in the truth of the proposition. We could exploit boolean computation to prove propositions; this technique is known as *proof by reflection*.

Logics that do not assume the excluded middle are referred to as *constructive logics*. Every proof of existence in such logics are constructive.

Although constructive logic is useful, constructive proofs of many statements are complicated. What’s worse, some statements only have non-constructive proofs.