Theorem foo:1=1. Proof. Proof. reflexivity. Qed.

Theorem foo : 1 = 1.
Proof.
  reflexivity.
Qed.

Theorem foo : 1 = 1.
Proof.
Proof.
  reflexivity.
Qed.

Theorem foo : 1 = 1.
Proof.
  Proof.
    reflexivity.
  Qed.

Require Import Arith.

Compute 1 + 1.
Compute 1 + 2 * 3.

(* how to write a function *)
Definition add (x:nat) (y:nat) : nat := x + y.

Compute add 3 4.

Compute (add 3 4).

Compute add (1*9) (1*9).

(* Gives me type signature *)
Check add.

Definition hypotenuse (x:nat) (y:nat) : nat :=
  (* how to write scoped variables *)
  let xsquared := x * x in
  let ysquared := y * y in
  let sum := xsquared + ysquared in
  sum.

Check hypotenuse.
Compute hypotenuse 3 4.

Compute 3 * 4.
Compute Nat.mul 3 4.
(* This tells me what "*" is! *)
Print "*".
Print add.
Print "+".

(* remember that the comparison operators of Coq have "?" *)
Compute 3 <=? 4.
Compute true.
Compute false.
Compute 4 <=? 3.
Compute leb 4 3.
(* Then, what does "<=" mean? *)
Print "<=".
Print "<=?".

(* ternary operator *)
Compute if (leb 3 4) then (add 1 2) else (4 - 3). (* => 3 *)
Compute if (leb 4 3) then (add 1 2) else (4 - 3). (* => 1 *)

Compute andb true false.
Compute orb false false.

(* Now, you can use more boolean operators *)
Open Scope bool_scope.
Compute true && false.
Compute false || true.

(* Require Import imports a library *)
(* The library contains a scoped library *)
(* Require Import String.
Open Scope string_scope.

Compute "foo".
Compute "foo" ++ "bar".

(* tuple type: bool * nat *)
Compute (true, 3).
(* we can nest it bool * nat * nat *)
Compute ((false, 3), add 3 4).
(* we can nest it nat * (bool * nat) *)
Compute (add 3 4, (false, 3)).
(* thus, this is left-associative *)

(* you can take either one of them *)
Compute fst (true, 3).
Compute fst (true, false, "aaa").
Compute fst (true, (false, "aaa")).
Compute snd (true, (false, "aaa")).
Compute snd (snd (true, (false, "aaa"))). "aaa" *)

(* Inductive is like a function *)
Inductive color : Type :=
  | Red : color
  | Blue : color
  | Dark (c:color) : color
  | Light (c:color) : color
.

Compute Red.
(* left-associative *)
Compute Dark (Light (Dark Blue)).
Compute Dark Blue.

(* You cannot define a type that already exists *)
(* Inductive color : Type :=
  | Yello : color. *)

Definition isdark (c:color) : bool :=
  (* you can use pattern-match *)
  match c with
  | Dark _ => true
  | _ => false (* without this clause, the compiler errs *)
  end.

Compute isdark (Dark Red).
Compute isdark (Light Red).
Compute isdark Red.

(* we use Fixpoint to write a recursive function *)
(* Definition is for a normal function *)
Fixpoint isred (c:color) : bool :=
  match c with
  | Red => true
  | Blue => false
  (* x is a value, contructor, and not an expression *)
  | Dark x => isred x
  | Light x => isred x
  end.

Compute isred Red.
Compute isred Blue.
Compute isred (Dark Red).
Compute isred (Light (Dark (Dark Red))).
Compute isred (Light (Dark (Dark Blue))).

Fixpoint factorial (n:nat) : nat :=
  match n with
  | O => 1
  | S n' => n * factorial n'
  end.

Compute factorial 10.
Compute factorial 6.

(* empty *)

From X Require Export Foo.

Inductive foo : Type := (* not foo: Type *)
  | bar (x y : nat). (* not (x y: nat) *)