Very useful tutorial for Coq: notes (cornell.edu)

Coq’s Type

The universe is Set while the collection of universes is Type. So, $\mathbb{N} \in \mathcal{U} \in \bigcup \mathcal{U}$.

Check nat.
> nat: Set.
Check Set.
> Set: Type.

We know that propositions are dependent types, so are they in Coq’s type system.

Check 1 + 1 = 2.
> 1 + 1 = 2: Prop.
Check Prop.
> Prop: Type.
Locate "=".
> "x = y": eq x y 

$\Pi_{x: a} (x =_{A}y)$ can be pattern matched.

So,

Theorem obvious: 1 + 1 = 2.
Proof. trivial. Qed.

We need to pattern match $=$ in this case which requires that the types of $x$ and $y$ should be the same.

Thus $1 + 1$ reduces to $2$ which becomes the component of the constructor of “reflexive type”:

$$ \frac{\Gamma \vdash x:A}{\mathsf{refl}: x =_{A} x} $$

Recall the match rule:

$$ \frac{\Gamma, x: A, y: A, P:x=A y \vdash {\color{red}C(x,y,P)}: \mathcal{U} \qquad \Gamma \vdash {\color{yellow} c: (z: A) \to C[x \mapsto z, y \mapsto z, p \mapsto 1_z]}}{\Gamma \vdash ind=(x,y,P,c) : C(x,y,P)} $$

Coq has inference about the yellow part which serves as the key evidence under typing envrionment $\Gamma$.

Class as Interface

Here comes the most interesting part of Coq. When we try to define a new type $T$, we can declare it as an instance of class which is parameterized by a set of propositions, types, etc. These classes are called type classes. This mechanism would allow uses to overload a set of operations across a class of types. For example,

Require Import RelationClasses.

Class Ordering (A: Type) : = {
	ord: relation A;

	reflexive: Reflexive ord;
	antisymmetric: forall (x y : A), ord x y -> ord y x -> x = y;
	transitive: Transitive ord;
}.

Refine

Perhaps this special tactic would appear confusing for most people. To begin with, let us recall what Agda can do for us when we do not care some specific structures in the proof which are solved later.