読者です 読者をやめる 読者になる 読者になる

チラシの裏

プログラミングとか色々

Term Rewriting and All Thatの練習問題をCoqで解く

この記事はTheorem Prover Advent Calendar 2016の8日目のために書かれました。

8日目の記事がまだ埋まっていないようなので、タイトルの通りTerm Rewriting and All Thatの練習問題で出てきた証明をいくつかCoqでやってみようと思います。

Exercise 2.4

これは{\rightarrow_+}が強正規化する事と\rightarrowが強正規化する事は同値である事を証明する問題です。 普通にやればできます。

Require Import Relations Program.

Definition terminating A (R : relation A) :=
  (well_founded (fun x y => R y x)).

Lemma terminating_transitive_closure A R :
  terminating A R <-> terminating _ (clos_trans _ R).
Proof.
  Local Hint Constructors clos_trans.
  split;
    intros Ht x;
    induction x as [x IH] using (well_founded_induction Ht);
    constructor;
    intros y HR;
    [ apply clos_trans_t1n in HR;
      inversion HR as [ ? HR' | ? ? HR' HR'' ]; subst;
      specialize (IH _ HR');
      [ | apply clos_t1n_trans in HR'';
          inversion IH; subst ] | ];
    eauto.
Qed.

Exercise 2.5

{\rightarrow_+}がstrict partial orderである事と\rightarrowがacyclicである事が同値である事を証明する問題です。 本当に自明過ぎて何一つ証明らしき事が無いので割愛。

Exercise 2.6 (b)

\rightarrowがとりうるreductionの長さが有界であるとき、\rightarrow有界であると言うらしいです。 これはfinitely branchingである関係が強正規化する事と有界である事は同値である事を証明する問題です。

これまでの問題が簡単だったのでこの問題も簡単かと思いきや、かなり曲者でした。

Require Import Ensembles Finite_sets_facts Relations Program Omega.

Inductive nfold_composition A R : nat -> relation A :=
  | nfold_composition_ident : forall x,
      nfold_composition A R 0 x x
  | nfold_composition_comp : forall n x y z,
      R x y ->
      nfold_composition A R n y z ->
      nfold_composition A R (S n) x z.
Hint Constructors nfold_composition.

Definition terminating A (R : relation A) :=
  (well_founded (fun x y => R y x)).
Definition bounded A (R : relation A) :=
  forall x, exists n, forall y, ~nfold_composition _ R n x y.

Definition finitely_branching A (R : relation A):= forall x, Finite _ (R x).

Lemma terminating_iff_bounded A R :
  finitely_branching A R ->
  (terminating A R <-> bounded A R).
Proof.
  intros Hfb.
  split.
  - intros Ht x.
    assert (Hbounded' : exists n, forall m, n <= m -> forall y, ~nfold_composition _ R m x y).
    { induction x as [ x IH ] using (well_founded_induction Ht).
      assert (IHys : forall P,
        Finite _ P ->
        forall Q,
        Finite _ Q ->
        Same_set _ (R x) (Union _ P Q) ->
        (exists n, forall m,
        n <= m ->
        Included _ Q (fun y => forall z, ~ nfold_composition _ R m y z)) ->
        exists n, forall m,
        n <= m ->
        forall y, ~nfold_composition _ R m x y).
      { induction 1 as [ | P ? ? y ]; intros Q ? [ Hsound Hcomplete ] [ n Hacc ].
        - exists (S n).
          intros m ? z Hnfold.
          inversion Hnfold as [ | m' ? ? ? HR Hnfold' ]; subst.
          + omega.
          + eapply Hacc with (m := m').
            * omega.
            * specialize (Hsound _ HR).
              destruct Hsound as [ ? Hcontra | ? HIn ].
              { inversion Hcontra. }
              { apply HIn. }
            * apply Hnfold'. 
        - assert (HR : R x y) by (apply Hcomplete; eauto with v62).
          apply IHFinite with (Q := Add _ Q y).
          + apply Union_preserves_Finite.
            * assumption.
            * apply Singleton_is_finite.
          + split.
            * intros ? HR'.
              specialize (Hsound _ HR').
              destruct Hsound as [ ? [ | ? HSingleton ] | ];
                [ | inversion HSingleton; subst | ];
                eauto with v62.
            * intros ? [ ? ? | ? [ ? ? | ? HSingleton ] ];
                [ | | inversion HSingleton; subst ];
                eauto with v62.
          + destruct (IH _ HR) as [ n' IH' ].
            destruct (le_dec n n');
              [ exists n'
              | exists n ];
              (intros m ? ? [ ? ? | ? HSingleton ];
                [ apply Hacc
                | inversion HSingleton; subst;
                  intros z ?;
                  apply IH' with (m := m) (y := z) ]; eauto); omega. }
      apply IHys with (P := R x) (Q := Empty_set _).
      - apply Hfb.
      - constructor.
      - eauto with v62.
      - exists 0.
        intros ? ? ? []. }
    destruct Hbounded' as [n Hbounded'].
    exists n.
    apply Hbounded'.
    omega.
  - intros Hbounded x.
    destruct (Hbounded x) as [ n Hbounded' ].
    generalize dependent x.
    induction n as [ | ? IHn ];
      intros ? Hbounded';
      constructor;
      intros.
    + exfalso.
      eapply Hbounded'; eauto.
    + apply IHn.
      intros z ?.
      apply Hbounded' with (y := z).
      eauto.
Qed.

この帰納法の仮定の一般化に次ぐ一般化!
カリーハワード対応を考えると、強正規化するならば有界である事の証明は最長のreductionの長さを求める事に相当します。 従って、やっている事は単に最大値を求めるだけの事ですが、求めた値がきちんとreductionの長さの最大値になっているかどうかの証明も引き回さないといけないため、 アキュムレータを追加したような形になります。

Exercise 2.6

ケーニヒの補題を木に制限して対偶を取ったような命題を証明する問題です。 つまり、acyclicかつglobally finiteな関係は強正規化する事を証明する事になります。

Definition globally_finite A (R : relation A) := forall x, Finite _ (clos_trans _ R x).

Definition acyclic A (R : relation A) := forall x, ~clos_trans _ R x x.

Lemma acyclic_and_globally_finite_impl_terminating A R :
  acyclic A R ->
  globally_finite _ R ->
  terminating _ R.
Proof.
  intros Hacyclic Hgf.
  apply terminating_transitive_closure.
  intros x.
  destruct (finite_cardinal _ _ (Hgf x)) as [n].
  generalize dependent x.
  induction n as [n IH]
    using (well_founded_induction (well_founded_ltof _ (fun x => x)));
    unfold ltof in *.
  intros x Hcardinal.
  constructor.
  intros y Htc.
  destruct (finite_cardinal _ _ (Hgf y)) as [m].
  apply IH with (y := m); eauto.
  apply incl_st_card_lt with
    (X := clos_trans _ R y)
    (Y := clos_trans _ R x); eauto.
  split; eauto with v62.
  intros Heq.
  apply Hacyclic with (x := y).
  rewrite Heq.
  assumption.
Qed.

ステートメントで一瞬面食らいますが、そこまで難しくはないです。
Rはglobally finiteなのでsuccessorの数は有限です。 これによってsuccessorの数を求められるので、これについての完全帰納法で証明します。
そして、acyclicの定義よりtransitive closureでxとxは関係付かないため、reductionが進むにつれてsuccessorの数は少なくとも1つは減っていく訳です。 これにより帰納法の仮定が使えて、やったねって感じです。