Coqで「停止性 + 弱合流性 = 合流性」の証明

小ネタです。

Abstract Rewriting Systemにおいて、「停止性と弱合流性(局所合流性)を持つ書き換え系は合流性を持つ」という定理があります*1。 この証明は、書き換え系の停止性から整礎帰納法を使って示すのが一般的です。 整礎帰納法はCoqでどうやるんだろう...と思って調べていたらwell_foundedというのがあるらしいと知ったので、やってみました。

Section Confluency.
  Variable X : Set.
  Definition relation (X : Type) : Type :=
    X -> X -> Prop.
  Variable R : relation X.
  Notation "x '==>' y" := (R x y) (at level 80).

  Reserved Notation "x '==>*' y" (at level 80).
  Inductive multiR : relation X :=
  | multi_refl :
      forall (x : X), x ==>* x
  | multi_step :
      forall (x y z : X),
      x ==> y ->
      y ==>* z ->
      x ==>* z
  where "x '==>*' y" := (multiR x y).

  Hint Constructors multiR.

  Lemma multiR_trans :
    forall x y z, x ==>* y -> y ==>* z -> x ==>* z.
  Proof.
    intros. generalize dependent z.
    induction H as [x | x w y]; auto.
    - intros. apply multi_step with w; auto.
  Qed.

  Definition weak_confluent_R :=
    forall x y y' : X, x ==> y -> x ==> y' ->
    exists z : X, y ==>* z /\ y' ==>* z.

  Definition confluent_R :=
    forall x y y' : X, x ==>* y -> x ==>* y' ->
    exists z : X, y ==>* z /\ y' ==>* z.

  Definition terminating_R :=
    well_founded (fun x y => y ==> x).

  Theorem newman :
    terminating_R -> weak_confluent_R -> confluent_R.
  Proof.
    unfold weak_confluent_R, confluent_R.
    intros termination weak_confluent x.
    induction x as [x IH] using (well_founded_ind termination);
      intros.

    destruct H as [x | x w y].
    - (* x = y *)
      exists y'; split...
    - destruct H0 as [x | x w' y'].
      + (* x = y' *)
        exists y; split...
      + assert (exists u, w ==>* u /\ w' ==>* u) by
          (apply weak_confluent with x; auto).
        destruct H3 as [u [? ?]].
        assert (exists v, y ==>* v /\ u ==>* v) by
          (apply IH with (y:=w); auto).
        destruct H5 as [v [? ?]].
        assert (multiR w' v) by (apply multiR_trans with u; auto).
        assert (exists d, v ==>* d /\ y' ==>* d) by
          (apply IH with w'; auto).
        destruct H8 as [d [? ?]].
        exists d; split...
        apply multiR_trans with v...
  Qed.
End Confluency.

帰納法を回す部分の証明のイメージはこんな感じです*2:

f:id:momohatt:20190831134623p:plain:w400

*1:Newmanの補題というらしい

*2:参考にしたどこかの大学のスライドの図をお借りしようと思ったのですが、アクセスできなくなってしまっていた...