COQ REFERENCE
A reference for Coq-isms and vocabulary.

CH.1 WAYS TO READ PROOFS

A -> B

"A" is a hypothesis

There may be some facts presented too, like:

n is a nat
s is a string
etc.

"A -> B" is a goal

given an A, conclude a B.

We deconstruct the goal to add "A" into a context.

A
n
s
-----
B

And we try to prove B with the hypothesis and facts!


CH.2 SYNTAX

Require Import Some.Import.
Local Open Scope some_scope.

Inductive name (arg : nat) : Type :=
| thing
| thang (p : nat) : name 5.

Definition name (n : nat) := 3.

(* {} = implicit type, () = explicit type *)
Fixpoint name {A : Type} (B : Type) (a : A) :=
  match a with
  | thing =>
  | thang _ _ ok =>
end.

Theorem name : (forall x : Type), (forall n : nat), n + x.
Proof.
intro.
unfold.
rewrite.
simpl.
reflexivity.
induction.
destruct.
split.
Qed.

(*
  A Prop is a Type.
  A Set is a Type.
  A Type is a Type.
*)

Definition a (A : Type) (B : Type) (C : B): B := C.

A is a proof of Type.
B is a proof of Type.

So `a nat nat` is valid because nat is proof that B is a Type, since nat is a
type. That's why it's called "proof". It should be called evidence I guess.

Curry-Howard correspondence.

So `a nat nat 4` means C is a proof of B, and since B is nat in this specific
case, C must be a proof of nat, which is any type constructor for a nat, so any
number is valid.

There are only a few main ways to create a Prop:

=, ->, and True and False

False is special in that it doesn't have any constructors, or any proofs.

So while the proposition "False" exists, there is no proof.

The proposition "True" exists, and the proof (or constructor) is "I".

Check I.

For some things, you have to use proofs as the input!