Check Nat.add 3 5. (* the result shows predefined notation. *)

Check (fun x => 3 + x).  (* temporary use of x *)

Check (fun x => 3 + x) 5. (* at execution x receives 5 *)

Compute (fun x => 3 + x) 5.

Fail Check x. (* x only exists inside the scope of the function *)

Inductive mod3 : Type := Zero | One | Two.

Check Zero.

Definition mod3_to_nat (x : mod3) : nat :=
  match x with Zero => 0 | One => 1 | Two => 2 end.

Definition mod3_succ (x : mod3) : mod3 :=
  match x with Zero => One | One => Two | Two => Zero end.

Definition le_2_2 : 2 <= 2 := le_n 2.

Definition le_1_2 : 1 <= 2 := le_S 1 1 (le_n 1).

Definition le_0_2 : 0 <= 2 := le_S 0 1 (le_S 0 0 (le_n 0)).

Definition mod3_to_nat_le_2 (x : mod3) :
  mod3_to_nat x <= 2 :=
match x with
| Zero => le_0_2
| One => le_1_2
| Two => le_2_2
end.

Definition mod3_cases (P : mod3 -> Prop) (x : mod3)
  (h0 : P Zero) (h1 : P One) (h2 : P Two) : P x :=
  match x with
  | Zero => h0
  | One => h1
  | Two => h2
  end.

Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Check cons nat 3 (cons nat 2 (cons nat 1 (nil nat))).

Fixpoint fold_right (A B : Type)
  (f : A -> B -> B)(v : B)(l : list A) : B :=
match l with
| nil _ => v
| cons _ x tl => f x (fold_right A B f v tl)
end.

Compute fold_right nat nat Nat.add 0 
  (cons nat 3 (cons nat 2 (cons nat 1 (nil nat)))).

Require Import ZArith.

Fixpoint fact' (p : positive) (offset : Z) : Z :=
match p with
| xH => (offset + 1)%Z
| xO p => fact' p offset * (fact' p (offset + (Zpos p)))
| xI p => (2 * (Zpos p) + 1 + offset) *
          fact' p offset * fact' p (offset + (Zpos p))
end.

Definition Zfact (x : Z) : Z :=
  match x with | Zpos p => fact' p 0 | _ => 1%Z end.

Compute Zfact 50.

Inductive eq (A : Type) (x : A) : A -> Prop :=
  eq_refl : eq A x x.

Definition eq_cases (A : Type) (x : A) (P : A -> Prop) (h : P x) (y : A)
 (p : eq A x y) : P y :=
  match p with
  | eq_refl _ _ => h
  end.

(* An example using all the datatypes between nat and Q to compute
  PI up to ten digits of accuracy (but not theorem to guarantee the result) *)
Require Import Arith QArith.

Coercion Z.of_nat : nat >-> Z.

Fixpoint atan_approx (n : nat) (x : Q) :=
  match n with
  | 0%nat => x
  | S p => (-1) ^ S p / (2 * S p + 1 # 1) *
           x ^ (2 * S p + 1) + atan_approx p x
  end.

Definition pi_digits (n m : nat) :=
  let v := 4 * (atan_approx n (1/2) + atan_approx n (1/3)) in
  (Qnum v * 10 ^ m / Zpos (Qden v))%Z.

Time Compute pi_digits 15 10.
(* result in less than 0.02 secs on my machine *)

Lemma example0 : forall A : Prop, A -> A.
Proof.
intros A hyp_A.
exact hyp_A.
Qed.

Lemma example0_1 : forall P Q : nat -> Prop,
  (exists x, P x \/ Q x) -> (exists x, Q x) \/ (exists y, P y).
Proof.
intros P Q Hex_disj.
destruct Hex_disj as [x PoQ].
destruct PoQ as [Px | Qx].
  right.
  exists x.
  exact Px.
left.
exists x.
exact Qx.
Qed.

Open Scope nat_scope.

Lemma sum_n :
  forall f : nat -> nat,
    f 0 = 0 ->
    (forall n, f (n + 1) = n + 1 + f n) ->
    forall n, 2 * f n = n * (n + 1).
Proof.
intros f f0 fsucc.
induction n as [ | p Ih].
  rewrite f0.
  ring.
replace (S p) with (p + 1) by ring.
rewrite fsucc.
Search (_ * ( _ + _)).
rewrite Nat.mul_add_distr_l.
rewrite Ih.
ring.
Qed.

Fixpoint sum (n : nat) : nat :=
  match n with 0 => 0 | S p => n + sum p end.

Lemma sum0 : sum 0 = 0.
Proof. easy. Qed.

Lemma sum_succ n : sum (n + 1) = n + 1 + sum n.
Proof.
Search (_ + 1).
rewrite Nat.add_1_r.
simpl.
reflexivity.
Qed.

Lemma sum_n' n : 2 * sum n = n * (n + 1).
Proof.
exact (sum_n sum sum0 sum_succ n).
Qed.