Purely Functional Data Structures Exercise 2.1 and 2.2

fmf_20111010.v

Require Import List.

Check 1::2::nil.

Fixpoint suffixes{A:Set}(xs:list A):list (list A) :=
match xs with
| nil => nil
| _::xs' => xs :: (suffixes xs')
end.

Eval compute in (suffixes (1::2::3::4::nil)).

Fixpoint suffixes' {A:Set}(xs:list A)(c:nat):
(nat * (list (list A)))%type :=
match xs with
| nil => (0,nil)
| _::xs' =>
(*  match (suffixes' xs' c) with
  | (c',ys) => (c'+1, xs::ys)
  end *)
  let (c',ys) := (suffixes' xs' c)
  in (S c', xs::ys)
end.
Eval compute in (suffixes' (1::2::nil) 0).

Require Import Omega.

Theorem suffixes'_length : forall (A:Set)(xs:list A),
  fst(suffixes' xs 0) = length xs.
Proof.
  intros A xs.
  induction xs.
    simpl. trivial.
    simpl. destruct (suffixes' xs 0). simpl.
    simpl in IHxs. rewrite <- IHxs. trivial.
Qed.

Print suffixes'_length.

(* 計算量も空間量もconsを呼んだ回数になってるはず *)

(* Exercise2.2 *)

Module Type SET.
  Parameter Elem : Set.
  Parameter Set_ : Set.
  Parameter empty : Set_.
  Parameter insert : Elem -> Set_ -> Set_.
  Parameter member : Elem -> Set_ -> bool.
End SET.

Module Type ORDERED.
  Parameter T: Set.
  Parameter eq_ : T -> T -> bool.
  Parameter lt_ : T -> T -> bool.
  Parameter leq : T -> T -> bool.
End ORDERED.

Module Type UnbalancedSet (Element:ORDERED) <: SET.
  Definition Elem := Element.T.
  Inductive Tree :=
  | E : Tree
  | T : Tree -> Elem -> Tree -> Tree. 
  Definition Set_ := Tree.
  Definition empty := E.
(*Fixpoint member (x:Elem)(tr:Tree) :=
  match tr with
  | E => false
  | (T a y b) =>
     if (Element.lt_ x y)
     then (member x a)
     else (if (Element.lt_ y x)
           then (member x b)
           else true)
  end.*)

  (* Exercise 2.2 の関数 *)

  Fixpoint find_cand (x:Elem)(tr:Tree)(c:Tree) :=
  match tr with
  | E => c
  | T a y b => if (Element.lt_ x y)
                 then find_cand x a c
                 else find_cand x b tr
  end.

  Fixpoint member' (x:Elem)(tr:Tree) :=
  match (find_cand x tr E) with
  | T a y b => if (Element.eq_ x y) then true else false
  | _ => false
  end.

  Fixpoint member (x:Elem)(tr:Tree) :=
  match tr with
  | E => false
  | (T a y b) =>
     if (Element.lt_ x y)
     then (member x a)
     else (if (Element.lt_ y x)
           then (member x b)
           else true)
  end.

  Fixpoint insert (x:Elem)(tr:Tree) :=
  match tr with
  | E => T E x E
  | T a y b =>
    if (Element.lt_ x y) then (T (insert x a) y b)
    else (if (Element.lt_ y x) then (T a y (insert x b)) else tr)
  end.

  Fixpoint depth (tr:Tree) :=
  match tr with
  | E => 0
  | T a y b =>
    S (MinMax.max (depth a) (depth b))
  end.

End UnbalancedSet.

Check beq_nat.

Fixpoint blt_nat (x y:nat):bool :=
match x,y with
| 0,0 => false
| 0,_ => true
| _,0 => false
| S x', S y' => blt_nat x' y'
end.
Eval compute in (blt_nat 2 2).
Eval compute in (blt_nat 2 3).
Eval compute in (blt_nat 3 2).
Eval compute in (blt_nat 0 0).

Fixpoint leq_nat (x y:nat):bool :=
match x,y with
| 0,0 => true
| _,_ => (blt_nat x y)
end.

Module NAT <: ORDERED.
  Definition T := nat.
  Definition eq_ := beq_nat.
  Definition lt_ := blt_nat.
  Definition leq := leq_nat.
End NAT.

Print NAT.T.

Module UnbalancedNatSet <: (UnbalancedSet NAT).
Include UnbalancedSet NAT.
End UnbalancedNatSet.

Print UnbalancedNatSet.

Module UNS := UnbalancedNatSet.

Eval compute in (UNS.empty).

Eval compute in (UNS.insert 1 UNS.empty).

Eval compute in (UNS.insert 1 (UNS.insert 4 UNS.empty)).




Definition E := UNS.E.
Definition T := UNS.T.

Eval compute in (UNS.member 0
                 (UNS.insert 3
                 (UNS.insert 5 
                 (UNS.insert 1 
                 (UNS.empty))))).

Print T.

Eval compute in (T E 1 E).

Notation "a << x >> b" := (UNS.T a x b) (at level 60, no associativity).

Eval compute in ((E << 1 >> E) << 2 >> E).

(*
Module ident : module_type と
Module ident <: module_typeの違い

Module A.
  Parameter T : Set.
End A.
Coq は型も値も違いはないから、これ(パラメータのみのModule)は許される。
ただし、内容もチェックするなら、 <: を使う。
*)

Eval compute in (UNS.insert 3 (UNS.insert 1 (UNS.insert 2 E))).

Eval compute in (UNS.insert 1 (UNS.insert 3 (UNS.insert 2 E))).