今日のCoq: 型づけ規則とそれに関する補題

とうとう、型づけ規則の定義ができました。
というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。

証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediate from the definitionらしいです。

(*
  typing t tenvは、型環境tenvにおいてtが型づけ可能ならSome type、型がつかないならNoneを返す。
*)
Lemma InvTypeRelVar :
  forall (tenv : list (string * type)) (x : string) (r : type),
  Some r = typing (Var x) tenv -> In (x,r) tenv.

というわけで証明にチャレンジします。
まずは、forallを仮定に移します。

InvTypeRelVar < Proof.
InvTypeRelVar < intros until r.
1 subgoal

  tenv : list (string * type)
  x : string
  r : type
  ============================
   Some r = typing (Var x) tenv -> In (x, r) tenv

そして、tenvに関する帰納法を用います。

InvTypeRelVar < induction tenv.
2 subgoals

  x : string
  r : type
  ============================
   Some r = typing (Var x) nil -> In (x, r) nil

subgoal 2 is:
 Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

tenvがnilのときの証明は簡単です。

InvTypeRelVar < simpl.
2 subgoals

  x : string
  r : type
  ============================
   Some r = None -> False

subgoal 2 is:
 Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

InvTypeRelVar < discriminate.
1 subgoal

  a : string * type
  tenv : list (string * type)
  x : string
  r : type
  IHtenv : Some r = typing (Var x) tenv -> In (x, r) tenv
  ============================
   Some r = typing (Var x) (a :: tenv) -> In (x, r) (a :: tenv)

で、問題は再帰ステップのほうです。とりあえず、simplで簡約します。

InvTypeRelVar < simpl.
1 subgoal

  a : string * type
  tenv : list (string * type)
  x : string
  r : type
  IHtenv : Some r = typing (Var x) tenv -> In (x, r) tenv
  ============================
   Some r =
   (let (key, v) := a in if string_dec x key then Some v else assoc x tenv) ->
   a = (x, r) \/ In (x, r) tenv

で、ここから先に進めない。string_dec x keyが成立する場合と成立しない場合の2つのsubgoalに分けれればいけそうなんだけど・・・。

ソースコード

(* simple typed lambda calculus *)
Require Import Arith.EqNat.
Require Import Arith.
Require Import Recdef.
Require Import List.
Require Import String.
Require Import Bool.DecBool.

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

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term.

(* Eval *)
Fixpoint subst (t : term) (old : string) (new : term) :=
  match t with
  | Bool _ =>
      t
  | Var x =>
      if string_dec x old then
      	new
      else
      	t
  | Lambda x type body =>
      if string_dec x old then
      	t
      else
        Lambda x type (subst body old new)
  | Apply t1 t2 =>
      Apply (subst t1 old new) (subst t2 old new)
  end.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  =>
      false
  end.

Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

Fixpoint term_length (t : term) :=
  match t with
    Bool _ | Var _  =>
      1
  | Lambda _ _ body =>
      1 + term_length body
  | Apply t1 t2 =>
      1 + term_length t1 + term_length t2
  end.

(* typing *)
Fixpoint assoc {A : Type} (x : string) (xs : list (string * A)) :=
  match xs with
  | nil =>
      None
  | (key, v) :: ys =>
      if string_dec x key then
        Some v
      else
      	assoc x ys
  end.

Fixpoint beq_type (t1 : type) (t2 : type) :=
  match (t1,t2) with
    (BoolT,BoolT) => true
  | (FunT t1 t2, FunT t3 t4) => andb (beq_type t1 t3) (beq_type t2 t4)
  | _ => false
  end.

Fixpoint typing (t : term) (tenv : list (string * type)) :=
  match t with
    Bool _ =>
    Some BoolT
  | Var x =>
    assoc x tenv
  | Lambda x ty1 body =>
    match typing body ((x,ty1)::tenv) with
      None => None
    | Some ty2 => Some (FunT ty1 ty2)
   end
  | Apply t1 t2 =>
    match (typing t1 tenv, typing t2 tenv) with
       (Some (FunT ty11 ty12),Some ty13) =>
        if beq_type ty11 ty13 then
          Some ty12
      	else
	  None
      | _ => None
    end
  end.

(* theorem *)
Definition value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      True
  | Apply _ _  =>
      False
  end.

Lemma NoneSome :
  forall (A : Type) (t : A), None = Some t -> False.
Proof.
  intros A t.
  discriminate.
Qed.

(* Inversion of the typing relation *)
Lemma InvTypeRelVar :
  forall (tenv : list (string * type)) (x : string) (r : type),
  Some r = typing (Var x) tenv -> In (x,r) tenv.

(*
Lemma CanonicalForms_Bool :
  forall (v : term),
  (value v /\ typing v nil = Some BoolT) -> (v = Bool true \/ v = Bool false).
*)