<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
Require Import Arith List Bool.

(* Q1: Define a function that adds up the first k odd numbers,
  1, 3, 2 k - 1 (the value for 0 is 0). *)

Fixpoint sum_odd (k : nat) :=
  match k with 0 => 0 | S p => 2 * p + 1 + sum_odd p end.

(* Test these functions on values from 1 to 10 *)

Eval vm_compute in map (fun i => (i, sum_odd i)) (seq 1 10).

(* The following is a model of string searching in a text and decomposing
   a text into lines. *)

(* Q2: Define a function headeq : list nat -> list nat -> bool, which
   returns true exactly when the first list is the head of the second one. *)

Fixpoint headeq (pat txt : list nat) : bool :=
  match pat, txt with
    nil, _ => true
  | a::p, a'::t => if beq_nat a a' then headeq p t else false
  | _::_, nil => false
  end.

(* Q3: Define a function index : list nat -> list nat -> bool, which
   returns true exactly when the first list occurs in the second one;
   use the previous function. *)

Fixpoint index (pat txt : list nat) : bool :=
  match txt with
    nil => match pat with nil => true | _ => false end
  | a::t => headeq pat (a::t) || index pat t
  end.

(* Q4: Definition a function decompose : nat -> list nat -> list (list nat)
   which breaks down a list of numbers into the fragments separated
   by the number given as argument.  Intuition: think of the natural number
   as the code for end of lines, we want to decompose a text into the
   list of lines. *)

Fixpoint decompose (fs : nat) (txt : list nat) :=
  match txt with
    nil => nil
  | a::nil => if beq_nat a fs then nil::nil::nil else (a::nil)::nil
  | a::t => if beq_nat a fs then nil::decompose fs t else
    match decompose fs t with
      nil => (a::nil)::nil
    | l::ll => (a::l)::ll
    end
  end.

Lemma decompose_eqn : forall (fs : nat) (txt : list nat),
  decompose fs txt = match txt with
    nil => nil
  | a::nil => if beq_nat a fs then nil::nil::nil else (a::nil)::nil
  | a::t => if beq_nat a fs then nil::decompose fs t else
    match decompose fs t with
      nil => (a::nil)::nil
    | l::ll => (a::l)::ll
    end
  end.
intros fs txt; destruct txt; auto.
Qed.

(* Define a function recompose : nat -> list (list nat) -> list nat 
  so that (recompose fs) is the inverse of (decompose fs) *)

Fixpoint recompose fs (l: list (list nat)) : list nat :=
  match l with
    nil => nil
  | l::nil => l
  | l'::(l''::_) as ll => l'++fs::recompose fs ll
  end.

Lemma recompose_eqn : forall fs (l: list (list nat)), 
  recompose fs l = 
  match l with
    nil => nil
  | l::nil => l
  | l'::(l''::_) as ll => l'++fs::recompose fs ll
  end.
intros fs [ | l' ll]; reflexivity.
Qed.

Definition re_decompose :
  forall fs txt a, recompose fs (decompose fs (a::txt)) = a::txt.
intros fs txt; induction txt.
  simpl.
  intros a; case_eq (beq_nat a fs); intros tst.
  simpl; rewrite (beq_nat_true _ _ tst).
    reflexivity.
  reflexivity.
intros a'.
rewrite decompose_eqn. 
assert (tmp := IHtxt a).
destruct (decompose fs (a ::txt)) as [ | l ll].
  discriminate.
case_eq (beq_nat a' fs); intros tst.
  rewrite recompose_eqn, tmp, (beq_nat_true _ _ tst); reflexivity.
rewrite recompose_eqn.
destruct ll.
  simpl in tmp; rewrite tmp; reflexivity.
rewrite recompose_eqn in tmp.
change (a' :: l++ fs::recompose fs (l0 :: ll) = a' :: a::txt).
rewrite tmp; reflexivity.
Qed.


(* Define a function replace : list nat -> list nat -> list nat -> list nat
   which substitutes every instance of the first argument with the second
   argument in the third argument.  for instance
   replace (2::3::nil) (7::8::nil) (1::2::3::4::5::6::nil)
   should return 1::7::8::4::5::6

   Assume that the pattern is non empty.
*)

Fixpoint replace pat targ txt :=
  match txt with
    nil => nil
  | a::t => if headeq pat (a::t) then
               targ::replace pat targ t
            else a::replace pat targ t
  end.