Coqでちょっと複雑なデータ構造を書こうと思ったらハマった

何となくMinCamlにCoqで証明を付けたいと思い立ったのでOccurrence checkの検証を証明しようと思ったのですが、ちょっとした問題に遭遇したのでメモ。

まず識別子に使う型を定義します。

Require Import Arith.

(* 識別子に用いる型 *)
Definition t := nat.

(* 等価性判定 *)
Definition eq_dec : forall x y : t, { x = y } + { x <> y } := eq_nat_dec.

それでは、MinCamlの型をCoqで書き下してみます。

Require Id.

(* MinCamlの型を表すデータ構造 *)
Inductive t : Set :=
  | Unit
  | Bool
  | Int
  | Float
  | Fun : list t -> t -> t
  | Tuple : list t -> t
  | Array : t -> t
  | Var : Id.t -> t.

すると、"Warning: Ignoring recursive call"などと不穏な反応が返ってきます。

これはひとまず無視する事にして、Occurrence check行う関数と、型変数が型の中に現れるかを表す述語を定義します。

Require Import Bool List.

(* 型変数が型の中に現れるかを表す述語 *)
Inductive In x : t -> Prop :=
  | In_Fun_dom : forall ts t t',
      List.In t' ts ->
      In x t' ->
      In x (Fun ts t)
  | In_Fun_cod : forall ts t,
      In x t ->
      In x (Fun ts t)
  | In_Tuple : forall ts t',
      List.In t' ts ->
      In x t' ->
      In x (Tuple ts)
  | In_Array : forall t,
      In x t ->
      In x (Array t)
  | In_Var : In x (Var x).

(* 型変数が型の中に現れるかを判定する関数 *)
Fixpoint occur x t :=
  match t with
  | Fun t1s t1 => existsb (occur x) t1s || occur x t1
  | Tuple t1s => existsb (occur x) t1s
  | Array t1 => occur x t1
  | Var y => if Id.eq_dec x y then true else false
  | _ => false
  end.

関数を定義したら正当性を証明したくなるのは人の性ですよね。

Theorem occur_true_firsttry : forall x t,
  occur x t = true <-> In x t.
Proof.
  intros x t.
  split.
    intros Hoccur.
    induction t;
      inversion Hoccur;
      simpl in Hoccur.

      apply orb_true_iff in Hoccur.
      destruct Hoccur.
        apply existsb_exists in H.
        destruct H as [t1 [HIn Hoccur]].
        eapply In_Fun_dom with (t' := t1).
          assumption.
          (* lに含まれる型に関する帰納法の仮定が無いため、帰納法が回らない *)
Abort.

しかし、欲しい仮定が無くて帰納法が回りませんでした。嫌な予感がするので帰納法の規則を表示してみます。

Check t_ind.
(*
t_ind
     : forall P : t -> Prop,
       P Unit ->
       P Bool ->
       P Int ->
       P Float ->
       (forall (l : list t) (t : t), P t -> P (Fun l t)) ->
       (forall l : list t, P (Tuple l)) ->
       (forall t : t, P t -> P (Array t)) ->
       (forall t : Id.t, P (Var t)) -> forall t : t, P t
*)

主にFunやTupleといったlist tを含むコンストラクタに対しての規則がおかしいですね。リストに含まれるtに対しても帰納法の仮定が欲しいところです。

気になったので調べてみたところ、このようにネストしたデータ構造を定義するとCoqは帰納法の規則を弱めてしまうとCPDTの3.8章に書いてありました。冒頭の"Warning: Ignoring recursive call"なるメッセージはこの事を警告してたんですね。

仕方ないので整礎帰納法を使って自分で使いやすい帰納法の規則を作ります。

Require Import Wf_nat Omega.

(* 自然数の総和 *)
Definition sum := fold_right plus O.

Lemma sum_app : forall l1 l2,
  sum (l1 ++ l2) = sum l1 + sum l2.
Proof.
  intros l1 l2.
  induction l1; simpl; omega.
Qed.

(* MinCamlの型のサイズ *)
Fixpoint size t :=
  match t with
  | Fun t1s t2 => S (sum (map size t1s) + size t2)
  | Tuple t1s => S (sum (map size t1s))
  | Array t1 => S (size t1)
  | _ => 1
  end.

(* 使いやすい帰納法の規則 *)
Theorem t_ind' : forall P : t -> Prop,
  P Unit ->
  P Bool ->
  P Int ->
  P Float ->
  (forall ts t,
    (* リストの中身についてもちゃんと言及している *)
    (forall t', List.In t' ts -> P t') ->
    P t ->
    P (Fun ts t)) ->
  (forall ts,
    (forall t', List.In t' ts -> P t') ->
    P (Tuple ts)) ->
  (forall t, P t -> P (Array t)) ->
  (forall x, P (Var x)) ->
  forall t, P t.
Proof.
  intros P IHUnit IHBool IHInt IHFloat IHFun IHTuple IHArray IHVar t.
  (* MinCamlの型のサイズが減少するように整礎帰納法を回す *)
  induction t as [t IHt] using (induction_ltof1 _ size).
  unfold ltof in IHt.
  destruct t as [| | | | ts t' | ts | t' | x ]; try assumption.
    apply IHFun.
      intros t'0 HIn.
      apply IHt.
      simpl.
      apply in_split in HIn.
      destruct HIn as [l1 [l2 Hsplit]].
      rewrite Hsplit.
      repeat rewrite map_app.
      repeat rewrite sum_app.
      simpl.
      omega.

      apply IHt.
      simpl.
      omega.
    apply IHTuple.
      intros t' HIn.
      apply IHt.
      simpl.
      apply in_split in HIn.
      destruct HIn as [l1 [l2 Hsplit]].
      rewrite Hsplit.
      repeat rewrite map_app.
      repeat rewrite sum_app.
      simpl.
      omega.
    apply IHArray.
      apply IHt.
      simpl.
      omega.
    apply IHVar.
Qed.

これを使うと、目的の命題が証明できました。

Theorem occur_true : forall x t,
  occur x t = true <-> In x t.
Proof.
  intros x t.
  split.
    intros Hoccur.
    induction t using t_ind';
      inversion Hoccur;
      simpl in Hoccur.

      apply orb_true_iff in Hoccur.
      destruct Hoccur.
        apply existsb_exists in H0.
        destruct H0 as [t' [HIn Hoccur]].
        apply In_Fun_dom with (t' := t'); auto.

        apply In_Fun_cod; auto.

      apply existsb_exists in Hoccur.
      destruct Hoccur as [t' [HIn Hoccur]].
      apply In_Tuple with (t' := t'); auto.

      constructor.
      auto.

      destruct (Id.eq_dec x x0).
        rewrite e.
        constructor.

        inversion Hoccur.

    intros HIn.
    induction HIn; simpl.
      apply orb_true_iff.
      left.
      apply existsb_exists.
      exists t'.
      split; assumption.

      apply orb_true_iff.
      right.
      assumption.

      apply existsb_exists.
      exists t'.
      split; assumption.

      assumption.

      destruct (Id.eq_dec x x).
        reflexivity.

        exfalso.
        auto.
Qed.

(* ついでにsumboolを使ってみる *)
Definition In_dec x t : { In x t } + { ~In x t }.
Proof.
  remember (occur x t) as b.
  symmetry in Heqb.
  destruct b.
    left.
    apply occur_true.
    assumption.

    right.
    intros HIn.
    apply occur_true in HIn.
    rewrite Heqb in HIn.
    inversion HIn.
Defined.

fetburner.core

コアダンプ

Coqでちょっと複雑なデータ構造を書こうと思ったらハマった