7-99.v

Require Import Bool.
Require Import Arith.
Require Import List.

(*E1 Find the last element of a list. *)

(*E2 Find the last but one element of a list. *)

(*E3 Find the K'th element of a list. The first element in the list is number 1. *)

(*E4 Find the number of elements of a list. *)

(*E5 Reverse a list. *)

(*E6 Find out whether a list is a palindrome. A palindrome can be read forward or backward; e.g. (x a m a x). *)

(*E7 Flatten a nested list structure. *)

fp.v

Require Import Bool.
Require Import Arith.

Definition example1 := fun x : nat => x*x+2*x+1.
Definition example11 (x : nat) := x*x+2*x+1.

Eval compute in example1 1.
Eval compute in if true then 3 else 5.

Definition is_zero (n:nat) :=
  match n with
    0 => true
  | S p => false
  end.

Fixpoint sum_n n :=
  match n with
    0 => 0
  | S p => p + sum_n p
  end.

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

Fixpoint evenb n :=
  match n with
    0 => true
  | 1 => false
  | S (S p) => evenb p
  end.

Require Import List.

Check 1::2::3::nil.

Check nil.

Check (nil: list nat).

Eval compute in map (fun x => x + 3) (1::3::2::nil).

Eval compute in map S (1::22::3::nil).

Eval compute in
  let l := (1::2::3::nil) in l ++ map (fun x => x + 3) l.

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

Eval compute in tolist 10.

Definition head_evb l :=
  match l with
    nil => false
  | a::tl => evenb a
  end.

Eval compute in head_evb (2::3::1::nil).
Eval compute in head_evb (nil).

Fixpoint sum_list l :=
  match l with
    nil => 0
  | n::tl => n + sum_list tl
  end.

Fixpoint insert n l :=
  match l with
    nil => n::nil
  | a::tl => if leb n a then n::l else a::insert n tl
  end.

Fixpoint sort l :=
  match l with
    nil => nil
  | a::tl => insert a (sort tl)
  end.

Eval compute in sort (1::4::3::22::5::16::7::nil).

Fixpoint lel l :=
  match l with
    nil => true
  | a::nil => true
  | a::b::tl => if leb a b then true else false
  end.

Fixpoint issorted l :=
  match l with
    nil => true
  | h::tl => if lel l then issorted tl else false
  end.

Eval compute in issorted (0::1::2::3::4::5::6::7::8::9::10::nil).