Library iris.prelude.relations

This file collects definitions and theorems on abstract rewriting systems. These are particularly useful as we define the operational semantics as a small step semantics. This file defines a hint database ars containing some theorems on abstract rewriting systems.

From Coq Require Import Wf_nat.
From iris.prelude Require Export tactics base.

Definitions

Section definitions.
Context `(R : relation A).

An element is reducible if a step is possible.

Definition red (x : A) := ∃ y, R x y.

An element is in normal form if no further steps are possible.

Definition nf (x : A) := ¬red x.

The reflexive transitive closure.

  Inductive rtc : relation A :=
    | rtc_refl x : rtc x x
    | rtc_l x y z : R x y → rtc y z → rtc x z.

The reflexive transitive closure for setoids.

  Inductive rtcS `{Equiv A} : relation A :=
    | rtcS_refl x y : x ≡ y → rtcS x y
    | rtcS_l x y z : R x y → rtcS y z → rtcS x z.

Reductions of exactly n steps.

  Inductive nsteps : nat → relation A :=
    | nsteps_O x : nsteps 0 x x
    | nsteps_l n x y z : R x y → nsteps n y z → nsteps (S n) x z.

  Inductive nstepsS `{Equiv A}: nat → relation A :=
    | nstepsS_O x y : x ≡ y → nstepsS 0 x y
    | nstepsS_l n x y z : R x y → nstepsS n y z → nstepsS (S n) x z.

Reduction of at most n steps.

  Inductive bsteps : nat → relation A :=
    | bsteps_refl n x : bsteps n x x
    | bsteps_l n x y z : R x y → bsteps n y z → bsteps (S n) x z.

The transitive closure.

  Inductive tc : relation A :=
    | tc_once x y : R x y → tc x y
    | tc_l x y z : R x y → tc y z → tc x z.

An element x is universally looping if all paths starting at x are infinite.

CoInductive all_loop : A → Prop :=
| all_loop_do_step x : red x → (∀ y, R x y → all_loop y ) → all_loop x.

An element x is existentally looping if some path starting at x is infinite.

CoInductive ex_loop : A → Prop :=
| ex_loop_do_step x y : R x y → ex_loop y → ex_loop x.
End definitions.

Hint Unfold nf red.

General theorems

Section rtc.
  Context `{R : relation A}.

  Hint Constructors rtc nsteps bsteps tc.

  Global Instance rtc_reflexive: Reflexive (rtc R).
  Proof. exact (@rtc_refl A R). Qed.
  Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z.
  Proof. induction 1; eauto. Qed.
  Global Instance: Transitive (rtc R).
  Proof. exact rtc_transitive. Qed.
  Lemma rtc_once x y : R x y → rtc R x y.
  Proof. eauto. Qed.
  Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
  Proof. intros. etrans; eauto. Qed.
  Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
  Proof. inversion_clear 1; eauto. Qed.
  Lemma rtc_ind_l (P : A → Prop) (z : A)
    (Prefl : P z) (Pstep : ∀ x y, R x y → rtc R y z → P y → P x) :
    ∀ x, rtc R x z → P x.
  Proof. induction 1; eauto. Qed.
  Lemma rtc_ind_r_weak (P : A → A → Prop)
    (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
    ∀ x z, rtc R x z → P x z.
  Proof.
    cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
    { eauto using rtc_refl. }
    induction 1; eauto using rtc_r.
  Qed.
  Lemma rtc_ind_r (P : A → Prop) (x : A)
    (Prefl : P x) (Pstep : ∀ y z, rtc R x y → R y z → P y → P z) :
    ∀ z, rtc R x z → P z.
  Proof.
    intros z p. revert x z p Prefl Pstep. refine (rtc_ind_r_weak _ _ _); eauto.
  Qed.
  Lemma rtc_inv_r x z : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z.
  Proof. revert z. apply rtc_ind_r; eauto. Qed.

  Lemma nsteps_once x y : R x y → nsteps R 1 x y.
  Proof. eauto. Qed.
  Lemma nsteps_trans n m x y z :
    nsteps R n x y → nsteps R m y z → nsteps R (n + m) x z.
  Proof. induction 1; simpl; eauto. Qed.
  Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z.
  Proof. induction 1; eauto. Qed.
  Lemma nsteps_rtc n x y : nsteps R n x y → rtc R x y.
  Proof. induction 1; eauto. Qed.
  Lemma rtc_nsteps x y : rtc R x y → ∃ n, nsteps R n x y.
  Proof. induction 1; firstorder eauto. Qed.

  Lemma bsteps_once n x y : R x y → bsteps R (S n) x y.
  Proof. eauto. Qed.
  Lemma bsteps_plus_r n m x y :
    bsteps R n x y → bsteps R (n + m) x y.
  Proof. induction 1; simpl; eauto. Qed.
  Lemma bsteps_weaken n m x y :
    n ≤ m → bsteps R n x y → bsteps R m x y.
  Proof.
    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
  Qed.
  Lemma bsteps_plus_l n m x y :
    bsteps R n x y → bsteps R (m + n) x y.
  Proof. apply bsteps_weaken. auto with arith. Qed.
  Lemma bsteps_S n x y : bsteps R n x y → bsteps R (S n) x y.
  Proof. apply bsteps_weaken. lia. Qed.
  Lemma bsteps_trans n m x y z :
    bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
  Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z.
  Proof. induction 1; eauto. Qed.
  Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y.
  Proof. induction 1; eauto. Qed.
  Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y.
  Proof. induction 1; [∃ 0; constructor|]. naive_solver eauto. Qed.
  Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
    (Prefl : ∀ n, P n x)
    (Pstep : ∀ n y z, bsteps R n x y → R y z → P n y → P (S n) z) :
    ∀ n z, bsteps R n x z → P n z.
  Proof.
    cut (∀ m y z, bsteps R m y z → ∀ n,
      bsteps R n x y → (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y ) → P (n + m) z).
    { intros help ?. change n with (0 + n). eauto. }
    induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
    intros n p1 H. rewrite <-plus_n_Sm.
    apply (IH (S n)); [by eauto using bsteps_r |].
    intros [|m'] [??]; [lia |]. apply Pstep with x'.
    - apply bsteps_weaken with n; intuition lia.
    - done.
    - apply H; intuition lia.
  Qed.

  Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z.
  Proof. induction 1; eauto. Qed.
  Global Instance: Transitive (tc R).
  Proof. exact tc_transitive. Qed.
  Lemma tc_r x y z : tc R x y → R y z → tc R x z.
  Proof. intros. etrans; eauto. Qed.
  Lemma tc_rtc_l x y z : rtc R x y → tc R y z → tc R x z.
  Proof. induction 1; eauto. Qed.
  Lemma tc_rtc_r x y z : tc R x y → rtc R y z → tc R x z.
  Proof. intros Hxy Hyz. revert x Hxy. induction Hyz; eauto using tc_r. Qed.
  Lemma tc_rtc x y : tc R x y → rtc R x y.
  Proof. induction 1; eauto. Qed.

  Lemma all_loop_red x : all_loop R x → red R x.
  Proof. destruct 1; auto. Qed.
  Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y.
  Proof. destruct 1; auto. Qed.
  Lemma all_loop_rtc x y : all_loop R x → rtc R x y → all_loop R y.
  Proof. induction 2; eauto using all_loop_step. Qed.
  Lemma all_loop_alt x :
    all_loop R x ↔ ∀ y, rtc R x y → red R y.
  Proof.
    split; [eauto using all_loop_red, all_loop_rtc|].
    intros H. cut (∀ z, rtc R x z → all_loop R z); [eauto|].
    cofix FIX. constructor; eauto using rtc_r.
  Qed.
End rtc.

Hint Constructors rtc nsteps bsteps tc : ars.
Hint Resolve rtc_once rtc_r tc_r rtc_transitive tc_rtc_l tc_rtc_r
  tc_rtc bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.

Section setoid_rel.
  Context `{A_equiv: Equiv A} `{Equivalence _ A_equiv}.

  Lemma rel_proper_iff_impl:
    ∀ (P: A → A → Prop), Proper (equiv ==> equiv ==> iff) P →
                                Proper (equiv ==> equiv ==> impl) P.
  Proof.
    intros P Hpr ? ? Heq ? ? Heq' Hp.
    eapply Hpr; [ | | apply Hp]; eauto.
  Qed.

  Global Instance rel_proper_impl_iff (R: relation A) (resp: Proper (equiv ==> equiv ==> impl) R):
    Proper (equiv ==> equiv ==> iff) R.
  Proof.
    intros x y Heq x' y' Heq'.
    split.
    × intros HR. rewrite <-Heq, <-Heq'; auto.
    × intros HR. rewrite <-Heq, <-Heq' in HR; auto.
  Qed.

  Context `(R : relation A) (resp: Proper (equiv ==> equiv ==> iff) R).

  Existing Instance resp.

  Section union.
    Context `(R' : relation A) (resp': Proper (equiv ==> equiv ==> iff) R').
    Existing Instance resp'.
    Global Instance rel_union_proper: Proper ((≡) ==> (≡) ==> iff) (Relation_Operators.union _ R R').
    Proof.
      intros x y Heq x' y' Heq'.
      split.
      × intros [HR | HR']; [ left | right ]; rewrite <- Heq, <- Heq'; auto.
      × intros [HR | HR']; [ left | right ]; rewrite Heq, Heq'; auto.
    Qed.

  End union.

  Global Instance tc_proper: Proper ((≡) ==> (≡) ==> iff) (tc R).
  Proof.
    intros x y Heq x' y' Heq'.
    split.
    × intros HR. revert HR y Heq y' Heq'.
      induction 1; intros.
      ** eapply tc_once; rewrite <- Heq, <- Heq'; eauto.
      ** eapply tc_l.
         rewrite <- Heq; eauto.
         eauto.
    × intros HR. revert HR x Heq x' Heq'.
      induction 1; intros.
      ** eapply tc_once; rewrite Heq, Heq'; eauto.
      ** eapply tc_l.
         rewrite Heq; eauto.
         eauto.
  Qed.

  Global Instance nstepsS_proper n: Proper ((≡) ==> (≡) ==> iff) (nstepsS R n).
  Proof.
    intros x y Heq x' y' Heq'.
    split.
    × intros HR. revert HR y Heq y' Heq'.
      induction 1; intros.
      ** econstructor; rewrite <- Heq, <- Heq'; eauto.
      ** eapply nstepsS_l.
         rewrite <- Heq; eauto.
         eauto.
    × intros HR. revert HR x Heq x' Heq'.
      induction 1; intros.
      ** econstructor; rewrite Heq, Heq'; eauto.
      ** eapply nstepsS_l.
         rewrite Heq; eauto.
         eauto.
  Qed.

  Lemma nsteps_nstepsS: ∀ n x y, nsteps R n x y → nstepsS R n x y.
  Proof.
    induction 1.
    × econstructor; eauto.
    × eapply nstepsS_l; eauto.
  Qed.

  Lemma nstepsS_nsteps: ∀ n x y, nstepsS R (S n) x y → nsteps R (S n) x y.
  Proof.
    intros ? ? ? Hns. assert (S n ≠ 0) as Hnz by auto.
    revert Hns Hnz.
    induction 1 as [| n'].
    × intros; exfalso; auto.
    × intros. destruct n'.
      ** inversion Hns as [ ? ? Heq|]. subst. econstructor; [|econstructor].
         rewrite <-Heq. auto.
      ** econstructor; eauto.
  Qed.

  Global Instance rtcS_proper: Proper ((≡) ==> (≡) ==> iff) (rtcS R).
  Proof.
    intros x y Heq x' y' Heq'.
    split.
    × intros HR. revert HR y Heq y' Heq'.
      induction 1; intros.
      ** eapply rtcS_refl; rewrite <- Heq, <- Heq'; eauto.
      ** eapply rtcS_l.
         rewrite <- Heq; eauto.
         eauto.
    × intros HR. revert HR x Heq x' Heq'.
      induction 1; intros.
      ** eapply rtcS_refl; rewrite Heq, Heq'; eauto.
      ** eapply rtcS_l.
         rewrite Heq; eauto.
         eauto.
  Qed.

  Global Instance rtcS_reflexive: Reflexive (rtcS R).
  Proof. intros r. eapply rtcS_refl. reflexivity. Qed.
  Lemma rtcS_transitive x y z : rtcS R x y → rtcS R y z → rtcS R x z.
  Proof. induction 1; eauto; try rewrite <-H0; auto.
         intros. eapply rtcS_l; eauto.
  Qed.
  Global Instance: Transitive (rtcS R).
  Proof. exact rtcS_transitive. Qed.

  Lemma rtc_rtcS x y: rtc R x y → rtcS R x y.
  Proof.
    induction 1; subst.
    × eapply rtcS_refl; eauto.
    × eapply rtcS_l; eauto.
  Qed.

  Hint Resolve rtc_rtcS : arsS.

  Lemma rtcS_once x y : R x y → rtcS R x y.
  Proof. eauto with ars arsS. Qed.
  Lemma rtcS_r x y z : rtcS R x y → R y z → rtcS R x z.
  Proof. intros. etransitivity; eauto. eapply rtcS_once; auto. Qed.
  Lemma rtcS_inv x z : rtcS R x z → x ≡ z ∨ ∃ y, R x y ∧ rtcS R y z.
  Proof. inversion_clear 1; eauto. Qed.
  Lemma rtcS_ind_l (P : A → Prop) (Hp: Proper ((≡) ==> iff) P) (z : A)
    (Prefl : P z) (Pstep : ∀ x y, R x y → rtcS R y z → P y → P x) :
    ∀ x, rtcS R x z → P x.
  Proof. induction 1; eauto with ars arsS. eapply Hp; eauto. Qed.
  Lemma rtcS_ind_r_weak (P : A → A → Prop) (Hp: Proper ((≡) ==> (≡) ==> iff) P)
    (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtcS R x y → R y z → P x y → P x z) :
    ∀ x z, rtcS R x z → P x z.
  Proof.
    cut (∀ y z, rtcS R y z → ∀ x, rtcS R x y → P x y → P x z).
    { eauto using rtcS_refl. }
    induction 1; eauto using rtcS_r with ars arsS.
    intros x0 Hr HP; eapply Hp; try eapply HP; eauto.
  Qed.
  Lemma rtcS_ind_r (P : A → Prop) (x : A) (Hp: Proper ((≡) ==> iff) P)
    (Prefl : P x) (Pstep : ∀ y z, rtcS R x y → R y z → P y → P z) :
    ∀ z, rtcS R x z → P z.
  Proof.
    intros z p. revert x z p Prefl Pstep. refine (rtcS_ind_r_weak _ _ _ _); eauto.
    intros x y Heq x' y' Heq'.
    split.
    × intros Himpl1 Hy Himpl2. eapply Hp. symmetry; eauto.
      eapply Himpl1; [ eapply Hp |]; eauto.
      intros. eapply Himpl2; [ rewrite <- Heq; eauto | | ]; eauto.
    × intros Himpl1 Hy Himpl2. eapply Hp. eauto.
      eapply Himpl1. eapply Hp. symmetry. eauto. eauto.
      intros. eapply Himpl2; [ rewrite Heq; eauto | | ]; eauto.
  Qed.
  Lemma rtcS_inv_r x z : rtcS R x z → x ≡ z ∨ ∃ y, rtcS R x y ∧ R y z.
  Proof.
    revert z. apply rtcS_ind_r; eauto with ars arsS.
    intros y z Heq.
    split.
    × rewrite Heq.
      intros [ | [y' (Hrtc&HR) ] ]; eauto. right.
      eexists; split_and?; eauto.
      eapply resp; [reflexivity | symmetry; eapply Heq |]; eauto.
    × rewrite Heq.
      intros [ | [y' (Hrtc&HR) ] ]; eauto. right.
      eexists; split_and?; eauto.
      eapply resp; [reflexivity | eapply Heq |]; eauto.
Qed.

End setoid_rel.

Theorems on sub relations

Section subrel.
  Context {A} (R1 R2 : relation A).
  Notation subrel := (∀ x y, R1 x y → R2 x y).
  Lemma red_subrel x : subrel → red R1 x → red R2 x.
  Proof. intros ? [y ?]; eauto. Qed.
  Lemma nf_subrel x : subrel → nf R2 x → nf R1 x.
  Proof. intros ? H1 H2; destruct H1; by apply red_subrel. Qed.
End subrel.

Theorems on well founded relations

Notation wf := well_founded.

Section wf.
Context `{R : relation A}.

A trick by Thomas Braibant to compute with well-founded recursions: it lazily adds 2^n Acc_intro constructors in front of a well foundedness proof, so that the actual proof is never reached in practise.

  Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R :=
    match n with
    | 0 ⇒ wfR
    | S n ⇒ λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y)
    end.

  Lemma wf_projected `(R2 : relation B) (f : A → B) :
    (∀ x y, R x y → R2 (f x) (f y)) →
    wf R2 → wf R.
  Proof.
    intros Hf Hwf.
    cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R x).
    { intros aux x. apply (aux (f x)); auto. }
    induction 1 as [y _ IH]. intros x ?. subst.
    constructor. intros. apply (IH (f y)); auto.
  Qed.
End wf.

Strategy 100 [wf_guard].