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.
