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.