coq_practice_31.v

(* Section の練習 *)

Section Poslist.
  (* このセクションの中では、Aが共通の変数として使える。 *)
  Variable A : Type.
  (* 非空なリスト *)
  Inductive poslist : Type := 
     nil : A -> poslist | cons : A -> poslist -> poslist.


  Section Fold.
    (* 二項演算 *)
    Variable g : A -> A -> A.

   (* gによって畳み込む。
    * 次のどちらかを定義すること。どちらでもよい。
    * 左畳み込み : リスト [a; b; c] に対して (a * b) * c を計算する。
    * 右畳み込み : リスト [a; b; c] に対して a * (b * c) を計算する。
    *)
    Fixpoint fold (p : poslist) : A := 
      match p with
      | nil q => q
      | cons q r => g q (fold r)
      end.
    (* DefinitionをFixpointなどに置き換えてもよい。 *)
    Print fold.
  End Fold.
  Print fold.
End Poslist.
Print fold.
(* Poslistから抜けたことにより、poslistは変数Aについて量化された形になる。 *)

(* このリストに関するmap関数 *)
Section PoslistMap.
  Variable A B : Type.
  Variable f : A -> B.
Print fold.
Type poslist.
Type fold.
Type nil.
  Fixpoint map (p :poslist A) : poslist B := 
    match p with
    | nil q => (nil B (f q))
    | cons q r => cons B (f q) (map r)
    end.
End PoslistMap.