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.