今日のCoq

昨日のアレは、splitの定義があんまり一般的でなかったためのようだ。
変な定義でも証明が出来ることが分かったのでよしとする。

(* 私のやつ *)
Fixpoint split' {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) :=
 match l with
 | [] => ([], [])
 | (x, y) :: l' => ((x :: (fst (split' l'))), (y :: (snd (split' l'))))
end.
(* 他の人の *)
Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) :=
 match l with
 | [] => ([], [])
 | (x, y) :: l' => match (split l') with
                   | (lx, ly) => (x::lx, y::ly)
                  end
end.

確かに 二回splitを呼んでたりイマイチな実装だった。

• • -

mumble grumbleが分からぬ。

Inductive mumble : Type :=
 | a : mumble
 | b : mumble -> nat -> mumble
 | c : mumble.

Inductive grunble (X : Type) : Type :=
 | d : mumble -> grunble X
 | e : X -> grunble X.

(*次の式のうち、ある型Xについてgrumble Xの要素として正しく定義されているものはどれでしょうか。

    d (b a 5)
    d mumble (b a 5)
    d bool (b a 5)
    e bool true
    e mumble (b c 0)
    e bool (b c 0)
    c
*)

Check b a 5. (* : mumble（型の値）*)
(* Check d (b a 5). (b a 5) は Typeでなく、mumble型の値 なので NG *)
Check d. (* d : forall X : Type, mumble -> grunble X *)
Check d bool.  (* d bool : mumble -> grunble bool なぜ 逆転してるの？ *)
Check d mumble (b a 5).
Check d bool (b a 5). (* OK? なんで ？ *)
Check e bool true.
Check e mumble (b c 0).
(* Check e bool (b c 0). NG *)
Check c. (* NG mumble型だから *)

型とその型を持つ値の区別がどうも自分のなかでついていないようだ。
そういや、lispやってたときもCLOSがよーわからんので投げた思い出が。