Library RW

Definitions of the notion of relation and transitivity closure

Libraries

Require Import ssreflect.

Section RW.

The relation is on some terms

Variable term : Set.

It is a binary proposition

Variable R : term -> term -> Prop.

Transitivity closure of the relation

Inductive Rstar : term -> term -> Prop :=
| Rzero : forall r, Rstar r r
| Rcons : forall r t s, (R r s) -> (Rstar s t) -> (Rstar r t).

Trivial lemmas

Lemma R_Rstar : forall s t, R s t -> Rstar s t.
Proof.
move => s t H.
apply (Rcons _ _ t); [apply H | apply Rzero].
Qed.

Lemma Rstar_trans :
  forall r s t, Rstar r s -> Rstar s t -> Rstar r t.
Proof.
move => r s t.
elim.
* by move => ?.
* move => {r s} r s u H K L M.
  apply (Rcons _ _ u).
  * by done.
  * by apply (L M).
Qed.

Congruence of Rstar with respect to congruence of R

Section Rstar_cong.

Variable S : term -> term -> term.
Variable T : term -> term.

Hypothesis C : forall t t':term, R t t' -> R (T t) (T t').
Hypothesis Rh : forall s t t':term, R t t' -> R (S s t) (S s t').
Hypothesis Lh : forall s t t':term, R t t' -> R (S t s) (S t' s).

Lemma Rstar_cong : forall t t':term, Rstar t t' -> Rstar (T t) (T t').
Proof.
move => t t'.
elim.
* by move => ?; apply Rzero.
* move => {t t'} r t t' H _ K.
  apply (Rcons _ _ (T t')).
  * by apply (C _ _ H).
  * by apply K.
Qed.

Lemma Rstar_rcong : forall s t t':term, Rstar t t' -> Rstar (S s t) (S s t').
Proof.
move => s t t'.
elim.
* by move => ?; apply Rzero.
* move => {t t'} r t t' H _ K.
  apply (Rcons _ _ (S s t')).
  * by apply (Rh _ _ _ H).
  * by apply K.
Qed.

Lemma Rstar_lcong : forall s t t':term, Rstar t t' -> Rstar (S t s) (S t' s).
Proof.
move => s t t'.
elim.
* by move => ?; apply Rzero.
* move => {t t'} r t t' H _ K.
  apply (Rcons _ _ (S t' s)).
  * by apply (Lh _ _ _ H).
  * by apply K.
Qed.

End Rstar_cong.

More definitions... In the library we only use local confluence.

Definition local_confluent :=
  forall r s t,
    R r s -> R r t ->
    exists u, Rstar s u /\ Rstar t u.

Definition confluent :=
  forall r s t,
    Rstar r s -> Rstar r t ->
    exists u, Rstar s u /\ Rstar t u.

Definition normal_form s := forall t, ~ R s t.

Definition Rmax s t := Rstar s t /\ normal_form t.

Definition terminating := forall s, exists t, Rmax s t.

End RW.

term is usually implicit

Implicit Arguments Rstar [term].
Implicit Arguments Rzero [term].
Implicit Arguments Rcons [term].

Implicit Arguments R_Rstar [term].
Implicit Arguments Rstar_trans [term].
Implicit Arguments Rstar_cong [term].
Implicit Arguments Rstar_rcong [term].
Implicit Arguments Rstar_lcong [term].
Implicit Arguments local_confluent [term].
Implicit Arguments confluent [term].
Implicit Arguments normal_form [term].
Implicit Arguments Rmax [term].
Implicit Arguments terminating [term].

Tactic stuff

Hint Immediate Rzero.

Use transitivity of Rstar R to solve the goal

Ltac solve_Rstar_trans :=
  match goal with
    | [ H : Rstar ?R ?a ?b, K : Rstar ?R ?b ?c |- Rstar ?R ?a ?c ]
      => apply (Rstar_trans _ _ _ _ H K)
  end.

Given |- Rstar R s t, try to find H : R s t or H : Rstar R s t in hypothesis to solve the goal

Ltac try_Rstar_in_goal :=
  match goal with
    | [ H : Rstar _ _ _ |- _ ] =>
      (try apply H); clear H; try_Rstar_in_goal
    | [ H : ?R ?s ?t |- _ ] =>
      let K := fresh in
        (have K : (Rstar R s t) by apply (R_Rstar _));
        (try apply K); clear K H; try_Rstar_in_goal
    | _ => idtac
  end.