今日のCoq: ラムダ式とsubstitute

バリアントでラムダ式を作って、その上でsubstituteを定義してみました。目指してるのは単純型付きラムダ計算です。

覚えたこと

全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。

• 再帰のあるバリアントはInductiveで定義する
• 相互再帰のあるバリアントはwithでつなげる
• andはProp上の演算。andbはbool上の演算
• 文字列を扱いたいときはRequire Import Stringする

よく分かんないこと

文字列上の等価性チェックをどうしたらいいかが分からない。Stringモジュールにあったprefixを使って、

Definition string_eq (xs ys : string) :=
  andb (prefix xs ys) (prefix ys xs).

としてるけど、これを評価するとすごいことになる。

Eval cbv delta iota beta in string_eq "foo" "bar".
     = if if let H :=
               fun b8 : Ascii.ascii =>
               match
                 b8 as a
                 return
....
(5000行ぐらい)
....
         else false
        else false
       else false
     : bool

そもそも評価しようとしてる時点でダメなんですかね?

ソースコード

(* simple typed lambda calculus *)
Require Import String.

(* simple type *)
Inductive type : Set :=
    BoolT : bool -> type
  | FunT  : type -> type -> type.

Inductive value : Set :=
    Var   : string -> value
  | Bool  : bool   -> value
  | Abst  : string -> type -> term -> value
with term : Set :=
    Value : value -> term
  | Apply : term  -> term -> term.

Definition string_eq (xs ys : string) :=
  andb (prefix xs ys) (prefix ys xs).

Fixpoint subst (term : term) (var : string) (val : value) :=
  match term with
  | Value (Bool _) =>
      term
  | Value (Var x) =>
      if string_eq x var then
        Value val
      else
      	term
  | Value (Abst x type body) =>
      if string_eq x var then
      	term
      else
        Value (Abst x type (subst body var val))
  | Apply t1 t2 =>
      Apply (subst t1 var val) (subst t2 var val)
  end.

(*Eval cbv delta iota beta in subst (Value (Var "x")) "x" (Var "y").*)