Require Import Arith List Bool NPeano.

Definition four := 4.

Definition polynom1 (x:nat) := x * x + 3 * x + 1.

Check polynom1 (polynom1 (polynom1 (polynom1 (polynom1 4)))).

(* Don't try to compute the expression that was checked above, it will
  hang for a huge amount of time. *)

Compute polynom1 (polynom1 4).

Check (fun x => x * x, fun x => x * polynom1 x).

Check let x := 3 * 4 in x * x * x.

Fail Check x.

Check (S O).

Compute 3 + 7.

Compute leb 7 3.

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

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

Fixpoint slnat (l : list nat) :=
 match l with nil => 0 | a::tl => a + slnat tl end.

Compute slnat (1 :: 3 :: 4 :: nil).

Fixpoint teo (l : list nat) :=
  match l with
    nil => nil
  | a::nil => a::nil
  | a::b::tl => a::teo tl
  end.

Compute teo (1 :: 3 :: 4 :: nil).

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

Compute lsn 4.

(* A complex example: computing PI to high precision in a dozen line. *)
Require Import QArith.
Open Scope Q_scope.

Fixpoint atanx n (acc : Q) s p (y x : Z) :=
match n with O => acc
| S n' => atanx n' (acc + (s#p) * /(y#1)) (-s)%Z (p + 2)%positive (y * x ^ 2) x
end.

Definition atanV n x := atanx n (/(x#1)) (-1) 3 (x ^ 3) x.

Definition PI_approx := Qred ((4#1) * ((4#1) * atanV 7 5 - atanV 1 239)).

Time Compute match PI_approx with (a#b) => Zdiv (10 ^ 10 * a) (Zpos b) end.