Library Confluence



The goal is to show that a locally confluent and terminating rewriting system is confluent. The rewriting system is abstracted as a relation R : A -> A -> Prop.

Require Export Arith.

A notion of non-empty lists list_ne.

Section Lists_NE.

  Variable A : Type.

  Inductive list_ne : Type :=
    | lne_end : A -> list_ne
    | lne_cons : A -> list_ne -> list_ne.

  Definition head l :=
    match l with
      | lne_end a => a
      | lne_cons a _ => a
    end.

  Fixpoint last l :=
    match l with
      | lne_end a => a
      | lne_cons _ t => last t
    end.

  Fixpoint length l :=
    match l with
      | lne_end _ => 1
      | lne_cons _ t => 1 + length t
    end.

  Lemma end_cons : forall l a b, lne_end a <> lne_cons b l.
  Proof.
    intros.
    discriminate.
  Qed.

  Lemma length_0 : forall l, length l <> 0.
  Proof.
    intro l; induction l; simpl; auto.
  Qed.

  Lemma length_1 : forall l, length l = 1 -> exists a, l = lne_end a.
  Proof.
    intro l.
    intro H.
    induction l.
    exists a.
    auto.
    simpl in H.
    apply (eq_add_S (length l) 0) in H.
    assert (H' := length_0 l).
    contradiction.
  Qed.

  Lemma cons_not_end : forall l, forall a,
            head l = a
            -> (forall t, l <> lne_cons a t)
            -> exists a, l = lne_end a.
  Proof.
    intros l a H1 H2.
    induction l; simpl in *.
    exists a0.
    auto.
    specialize (H2 l).
    rewrite H1 in H2.
    assert (lne_cons a l = lne_cons a l).
    auto. contradiction.
  Qed.

End Lists_NE.

An abstract rewriting system.

We pre-suppose the existence of a relation R : A -> A -> Prop and we construct a notion of path Path a b relating two elements a : A and b : A, using the notion of list_ne defined above. A point a : A satisfies EndPoint : A -> Prop if it does not rewrite.

Section RW_sec.

  Variable A : Set.
  Variable R : A -> A -> Prop.


  Definition EndPoint (s:A) := forall t, ~ (R s t).


  Fixpoint path_relation (l:list_ne A) := match l with
      | lne_end a => True
      | lne_cons a q => match q with
           | lne_end b => (R a b)
           | lne_cons b r => R a b /\ path_relation q
           end
      end.

  Lemma path_relation_cons :
          forall a l, path_relation (lne_cons A a l)
                      -> (R a (head A l) /\ path_relation l).
  Proof.
    intros a l.
    generalize a. clear a.
    induction l;
    intro b; simpl in *; [auto | split; elim H; intros; auto].
  Qed.




  Record Path (a b:A) : Set := mkPath {
     Path_obj : list_ne A;
     Path_R : path_relation Path_obj;
     Path_start : head A Path_obj = a;
     Path_end : last A Path_obj = b
  }.


Adding an element to a path.

  Lemma path_cons_R :forall (a b c:A) (p:Path b c) (H:R a b),
                        path_relation (lne_cons A a (Path_obj _ _ p)).
  Proof.
    simpl. intros.
    cut (exists p', p' = Path_obj b c p);
      [ intro H'; elim H'; clear H'; intros p' H'
      | exists (Path_obj b c p); auto].
    rewrite <- H'.
    induction p'.
    cut (a0 = b);
    [intro U; rewrite U
    | assert (U := Path_start _ _ p); rewrite <- H' in U; simpl in U];
    auto.
    split;
      [assert (U := Path_start _ _ p) | assert (U := Path_R _ _ p)];
      rewrite <- H' in U; simpl in U; auto.
    rewrite U; auto.
  Qed.


  Lemma path_cons_start :forall (a b c:A) (p:Path b c) (H:R a b),
                      head A (lne_cons A a (Path_obj _ _ p)) = a.
  Proof.
    intros. simpl. auto.
  Qed.


  Lemma path_cons_end :forall (a b c:A) (p:Path b c) (H:R a b),
                      last A (lne_cons A a (Path_obj _ _ p)) = c.
  Proof.
    intros. simpl. apply (Path_end _ _ p).
  Qed.

  Definition path_cons (a b c:A) (p:Path b c) (H:R a b) :=
       mkPath a c
         (lne_cons A a (Path_obj _ _ p))
         (path_cons_R a b c p H)
         (path_cons_start a b c p H)
         (path_cons_end a b c p H).



Creating an empty path

  Lemma path_end_R :forall a:A, path_relation (lne_end A a).
  Proof.
    simpl. auto.
  Qed.

  Lemma path_end_start :forall a:A, head A (lne_end A a) = a.
  Proof.
    simpl. auto.
  Qed.

  Lemma path_end_end :forall a:A, last A (lne_end A a) = a.
  Proof.
    simpl. auto.
  Qed.


  Definition path_end (a:A) : (Path a a) :=
       mkPath a a
              (lne_end A a)
              (path_end_R a)
              (path_end_start a)
              (path_end_end a).



Length of a path.

  Definition path_length {a b:A} (p:Path a b) :=
        (length A (p.(Path_obj a b))).


  Lemma endpoint_length_path : forall a,
        (EndPoint a) -> forall (b:A) (p:Path a b), path_length p = 1.
  Proof.
    intros a H b p.
    unfold path_length.
    induction p.
    simpl.
    cut (Path_obj0 = lne_end A a).
    intro. rewrite H0. simpl. auto.
    cut (forall t, Path_obj0 <> lne_cons A a t).
    intro.
    assert (U := cons_not_end A Path_obj0 a Path_start0 H0).
    elim U.
    intros.
    rewrite H1 in Path_start0.
    simpl in Path_start0.
    rewrite Path_start0 in H1.
    auto.
    intro.
    intro.
    rewrite H0 in Path_R0.
    simpl in Path_R0.
    unfold EndPoint in H.
    induction t; [|elim Path_R0; clear Path_R0; intros];
    specialize (H a0);
    contradiction.
  Qed.


A path is either a singleton, or the cons of an element and a path.

  Lemma path_case : forall a c, forall (p:Path a c),
                (a = c /\ path_length p = 1) \/
                (exists b, exists p':Path b c, exists H:R a b,
                     Path_obj _ _ p = Path_obj _ _ (path_cons a b c p' H)).
  Proof.
    intros a c p.
    assert (U : exists l, l = Path_obj _ _ p);
      [exists (Path_obj _ _ p); auto|].
    elim U; clear U; intros l U.
    generalize a c p U. clear a c p U.
    induction l; intros a' c p U.
    assert (H1 := Path_end _ _ p).
    assert (H2 := Path_start _ _ p).
    assert (H3 : path_length p = 1);
      [unfold path_length|];
      rewrite <- U in *;
      simpl in *;[reflexivity|].
    assert (H4 : a' = c); [rewrite <- H1; rewrite <- H2; reflexivity|].
    auto.
    assert (H2 := Path_start _ _ p).
    rewrite <- U in H2.
    simpl in H2.
    rewrite H2 in *.
    assert (P_R : path_relation l).
    assert (P_R' : path_relation (lne_cons A a' l)).
    rewrite U.
    apply (Path_R _ _ p).
    apply (path_relation_cons _ _ P_R').
    assert (P_start : head A l = (head A l)).
    auto.
    assert (P_end : last A l = c).
    cut (last A (lne_cons A a' l) = c); [intro H; simpl in H; auto|].
    rewrite U.
    apply (Path_end _ _ p).
    assert (V : exists b, exists p',exists H,
              Path_obj _ _ p = Path_obj _ _ (path_cons a' b c p' H)).
    exists (head A l).
    exists (mkPath _ _ l P_R P_start P_end).
    assert (H : R a' (head A l)).
    assert (H' := Path_R _ _ p).
    rewrite <- U in H'.
    apply (path_relation_cons a' l) in H'.
    elim H'; clear H'; intros H H'.
    auto.
    exists H.
    unfold path_cons. simpl.
    auto. auto.
  Qed.



  Lemma path_cons_length : forall a b c p H, path_length (path_cons a b c p H) = S (path_length p).
  Proof.
    unfold path_length.
    unfold path_cons.
    simpl.
    auto.
  Qed.



We can now define the relation Rn : A -> A -> Prop.

  Definition Rn (n:nat) (a b:A) :=
       exists p:(Path a b), path_length p = S n.


  Lemma Rn0 : forall s t, (Rn 0 s t) -> s = t.
  Proof.
    unfold Rn.
    unfold path_length.
    intros a b.
    intro H. elim H. clear H. intro p. intro H.
    assert (H' := length_1 _ _ H). clear H.
    elim H'; clear H'; intro c.
    intro H.
    assert (H_left := p.(Path_start a b)).
    assert (H_right := p.(Path_end a b)).
    rewrite H in H_left.
    rewrite H in H_right.
    simpl in *.
    rewrite H_left in H_right.
    auto.
  Qed.

  Lemma Rn_0 : forall a, (Rn 0 a a).
  Proof.
    intros.
    unfold Rn.
    exists (path_end a).
    unfold path_end.
    unfold path_length.
    simpl.
    reflexivity.
  Qed.


  Lemma RnSn : forall a c, forall n,
                Rn (S n) a c -> exists b, R a b /\ Rn n b c.
  Proof.
    unfold Rn.
    unfold path_length.
    intros a c n H.
    elim H; clear H.
    intros p H.
    assert (exists l, l = Path_obj a c p);
      [exists (Path_obj a c p); reflexivity
      | elim H0; clear H0; intros l H1].
    rewrite <- H1 in H.
    induction l; [|clear IHl]; simpl in H.
    assert (1 <> S (S n)); [auto|contradiction].
    assert (H2 := Path_start _ _ p).
    rewrite <- H1 in H2; simpl in H2.
    rewrite H2 in H1. clear H2 a0.
    assert (H2 := Path_R _ _ p).
    rewrite <- H1 in H2. simpl in H2.
    induction l; [|clear IHl].
    exists a0.
    split; [auto|].
    simpl in H.
    assert (H' := eq_add_S _ _ H); clear H.
    assert (H := eq_add_S _ _ H'); clear H'.
    rewrite <- H.
    assert (H' := Path_end a c p).
    rewrite <- H1 in H'.
    simpl in H'.
    rewrite H' in *.
    assert (P_R : let fix P p := match p with
            | lne_end a => True
            | lne_cons a q => match q with
                 | lne_end b => (R a b)
                 | lne_cons b r => R a b /\ P q
                 end
            end in P (lne_end A c));[simpl;auto|].
    assert (P_start : head A (lne_end A c) = c);[simpl;auto|].
    assert (P_end : last A (lne_end A c) = c);[simpl;auto|].
    exists (mkPath c c (lne_end A c) P_R P_start P_end).
    simpl. reflexivity.
    elim H2. clear H2. intros H2 H3.
    exists a0.
    split; [auto|]; clear H2.
    assert (P_R : let fix P p := match p with
            | lne_end a => True
            | lne_cons a q => match q with
                 | lne_end b => (R a b)
                 | lne_cons b r => R a b /\ P q
                 end
            end in P (lne_cons A a0 l)); [simpl;auto|]; clear H3.
    assert (P_start : head A (lne_cons A a0 l) = a0);[simpl;auto|].
    assert (P_end : last A (lne_cons A a0 l) = c).
    cut (last A (Path_obj a c p) = c);
      [rewrite <- H1; auto | apply (Path_end a c p)].
    exists (mkPath _ _ (lne_cons A a0 l) P_R P_start P_end).
    simpl.
    auto.
  Qed.


  Lemma RnSn_left : forall a c, forall n,
           (exists b, R a b /\ Rn n b c) -> Rn (S n) a c.
  Proof.
    intros a c n H.
    elim H; clear H; intros b H; elim H; clear H;
      unfold Rn; unfold path_length; intros H1 H2;
      elim H2; clear H2; intros p H2.
    assert (P_R : let fix P p := match p with
            | lne_end a => True
            | lne_cons a q => match q with
                 | lne_end b => (R a b)
                 | lne_cons b r => R a b /\ P q
                 end
            end in P (lne_cons A a (Path_obj _ _ p))).
    simpl.
    cut (exists p', p' = Path_obj b c p);
      [intro H;elim H; clear H; intros p' H
      | exists (Path_obj b c p); auto].
    rewrite <- H.
    induction p'.
    cut (a0 = b);
      [ intro U; rewrite U
      | assert (U := Path_start _ _ p);
        rewrite <- H in U;
        simpl in U];
    auto.
    split;
      [ assert (U := Path_start _ _ p)
      | assert (U := Path_R _ _ p) ];
      rewrite <- H in U; simpl in U;
      auto.
    rewrite U; auto.
    assert (P_start : head A (lne_cons A a (Path_obj _ _ p)) = a).
    simpl. reflexivity.
    assert (P_end : last A (lne_cons A a (Path_obj _ _ p)) = c).
    simpl. apply (Path_end _ _ p).
    exists (mkPath a c (lne_cons A a (Path_obj _ _ p)) P_R P_start P_end).
    simpl. auto.
  Qed.

  Lemma Rn_trans : forall m n a b c,
                       Rn m a b -> Rn n b c -> Rn (m + n) a c.
  Proof.
    intro m.
    induction m; intros n a b c H1 H2.
    simpl.
    assert (H3 := Rn0 a b H1).
    rewrite H3. apply H2.
    assert (H3 := RnSn a b m H1).
    elim H3; intro a'.
    intro H4; elim H4; clear H4; intros H4 H5.
    cut (Rn (m+n) a' c);
      [ intro;
        apply (RnSn_left a c (m + n));
        exists a';
        auto
      | apply (IHm n a' b c H5 H2)].
  Qed.



The reflexive transitive closure Rstar of R is defined using Rn.

  Definition Rstar (a b : A) := exists n, Rn n a b.

  Lemma Rstar_trans : forall a b c,
            (Rstar a b) /\ (Rstar b c) -> (Rstar a c).
  Proof.
    unfold Rstar.
    intros.
    elim H; clear H; intros H H'.
    elim H; clear H; intros m H.
    elim H'; clear H'; intros n H'.
    exists (m+n).
    apply (Rn_trans m n a b c H H').
  Qed.


Strong normalization is defined using Path.

  Definition R_finite (n:nat) (a:A) :=
        forall b, forall p:Path a b, path_length p <= S n.

  Lemma Rfin0 : forall a, (R_finite 0 a) -> (EndPoint a).
  Proof.
    unfold R_finite. unfold EndPoint. unfold path_length.
    intros a H b H'.
    specialize (H b).
    assert (P_R : let fix P p := match p with
            | lne_end a => True
            | lne_cons a q => match q with
                 | lne_end b => (R a b)
                 | lne_cons b r => R a b /\ P q
                 end
            end in P (lne_cons A a (lne_end A b))); auto.
    assert (P_start : head A (lne_cons A a (lne_end A b)) = a); auto.
    assert (P_end : last A (lne_cons A a (lne_end A b)) = b); auto.
    specialize (H (mkPath a b (lne_cons A a (lne_end A b)) P_R P_start P_end)).
    simpl in H.
    assert (~ (2 <= 1)); auto with arith.
  Qed.

  Lemma RfinSn : forall n a b, R_finite (S n) a -> R a b -> (R_finite n b).
  Proof.
    unfold R_finite.
    intros n a b H H' c p.
    specialize (H c).
    specialize (H (path_cons a b c p H')).
    unfold path_cons in H.
    unfold path_length in *.
    simpl in H.
    auto with arith.
  Qed.

  Lemma RfinSn_equal : forall n a b, R_finite n a -> R a b -> (R_finite n b).
  Proof.
    unfold R_finite.
    intros n a b H H' c p.
    specialize (H c).
    specialize (H (path_cons a b c p H')).
    unfold path_cons in H.
    unfold path_length in *.
    simpl in H.
    auto with arith.
  Qed.

  Lemma RfinSn2 : forall n m a b, R_finite n a -> Rn m a b -> (R_finite n b).
  Proof.
    intros n m; generalize n; clear n; induction m; intros n a c H H'.
    apply (Rn0 a) in H'.
    rewrite <- H'; auto.
    apply (RnSn a c) in H'.
    elim H'; clear H'; intros b H'.
    elim H'; clear H'; intros H1 H2.
    apply (RfinSn_equal n a b) in H.
    apply (IHm n b c H H2). auto.
  Qed.

  Lemma Rfin_0 : forall n a, (EndPoint a) -> (R_finite n a).
  Proof.
    unfold R_finite.
    intros n a H b p.
    assert (H' := endpoint_length_path a H b p).
    induction n; [rewrite H'|]; auto with arith.
  Qed.

  Lemma Rfin_Sn : forall n a,
           (forall b, (R a b) /\ (R_finite n b)) -> (R_finite (S n) a).
  Proof.
    unfold R_finite.
    intros n a H c p.
    assert (U := path_case a c p).
    elim U; clear U; intro U.
    elim U. clear U. intros U V.
    rewrite V.
    auto with arith.
    elim U. clear U. intros b U.
    elim U. clear U. intros p' U.
    elim U. clear U. intros H' U.
    unfold path_length.
    rewrite U.
    simpl.
    specialize (H b).
    elim H. intros H0 H1.
    specialize (H1 c p').
    auto with arith.
  Qed.



Finally, definition of termination, confluence and local confluence.

  Definition Terminating := exists n, forall a, R_finite n a.

  Definition Confluent :=
     forall a b b', (Rstar a b) /\ (Rstar a b')
        -> exists c, (Rstar b c) /\ (Rstar b' c).

  Definition Local_confluent :=
     forall a b b', (R a b) /\ (R a b')
        -> exists c, (Rstar b c) /\ (Rstar b' c).

  Theorem local_conf_term : Local_confluent /\ Terminating -> Confluent.
  Proof.
    unfold Local_confluent.
    unfold Terminating.
    unfold Confluent.
    unfold Rstar.
    intro.
    elim H. clear H. intro. intro. intro. intro. intro. intro.
    elim H1. clear H1. intros.
    elim H1. clear H1. intro m. intros.
    elim H2. clear H2. intro m'. intros.
    generalize H1 H2.
    elim H0. clear H0. intro n. intro.
    assert (Z := H0 a).
    generalize Z. generalize a b b'.
    clear Z H0. clear H1 H2. clear a b b'.
    generalize m m'. clear m m'.
    induction n;
    intros.
    induction m.
    assert (U := (Rn0 a b H1)).
    rewrite <- U.
    exists b'.
    split; [exists m'; auto | exists 0; apply (Rn_0 b')].
    induction m'.
    assert (U := (Rn0 a b' H2)).
    rewrite <- U.
    exists b.
    split; [exists 0; apply (Rn_0 b) | exists (S m); auto].
    assert (U := (RnSn a b m H1)).
    elim U. intros. elim H0. intros.
    assert (V := Rfin0 a).
    assert (W := V Z).
    clear V.
    unfold EndPoint in W.
    assert (V := W x).
    contradiction.
    induction m.
    assert (U := (Rn0 a b H1)).
    rewrite <- U.
    exists b'.
    split; [exists m'; auto | exists 0; apply (Rn_0 b')].
    induction m'.
    assert (U := (Rn0 a b' H2)).
    rewrite <- U.
    exists b.
    split; [exists 0; apply (Rn_0 b) | exists (S m); auto].
    assert (U := (RnSn a b m H1)).
    assert (V := (RnSn a b' m' H2)).
    clear H1 H2.
    elim U.
    elim V.
    clear U V.
    intro c'. intro H1'. intro c. intro H1.
    elim H1'. elim H1. clear H1' H1.
    intros.
    cut (R a c /\ R a c'); [intro | auto].
    assert (W := H a c c' H4). clear H4.
    elim W. intro d. intros. elim H4. clear H4 W. intros.
    elim H4. elim H5. clear H5 H4.
    intro l'. intro. intro l. intro.
    assert (U := RfinSn n a c' Z H2).
    assert (V := RfinSn n a c Z H0).
    assert (W := (IHn m' l' c' b' d U) H3 H4).
    elim W; intro e'. intros. elim H6; intros.
    elim H7; intro n_b'e'. intros. elim H8; intro n_de'. intros.
    assert (W1 := (IHn m l c b d V) H1 H5).
    elim W1. intro e. intros. elim H11; intros.
    elim H12; intro n_be; intros.
    elim H13; intro n_de; intros.
    assert (V1 := (RfinSn2 n l c d V H5)).
    assert (W2 := (IHn n_de n_de' d e e' V1) H15 H10).
    elim W2; intro f; intros. elim H16; intros.
    elim H17; intro n_ef; intros.
    elim H18; intro n_e'f; intros.
    assert (SOL1 := (Rn_trans n_be n_ef b e f H14 H19)).
    assert (SOL2 := (Rn_trans n_b'e' n_e'f b' e' f H9 H20)).
    exists f.
    split; [ exists (n_be + n_ef) | exists (n_b'e' + n_e'f) ] ; auto.
  Qed.

End RW_sec.