Module MoreRelations

Require Import Util.
Import Utf8.
Require Import Smallstep.
Export Relations.

Lemma clos_refl_trans_two_cases {X} {R: relation X} {x x': X}
(RT: clos_refl_trans X R x x') :
x' = x ∨ clos_trans X R x x'.

Proof.

  apply clos_rt_rt1n in RT.
  elim RT. vauto. clear x RT.
  intros x y z Hx Hz [ -> | H ]; right; vauto.
Qed.

Fixpoint iter_rel {X} (n: nat) (R: relation X) (α ω: X) : Prop :=
  match n with
  | O => α = ω
  | S n' => ∃ β, R α β ∧ iter_rel n' R β ω
end.

Lemma iter_rel_trans {X} (m n: nat) (R: relation X) (α μ ω: X) :
  iter_rel m R α μ →
  iter_rel n R μ ω →
  iter_rel (m + n) R α ω.

Proof.

  intros H; revert α H n ω.
  elim m; clear.
  intros α -> ? ?; exact id.
  intros m IH α ( β & H & Hm ) n ω Hn. vauto.
Qed.

Fixpoint iter_rel' {X} (n: nat) (R: relation X) (α ω: X) : Prop :=
  match n with
  | O => α = ω
  | S n' => ∃ ψ, iter_rel' n' R α ψ ∧ R ψ ω
end.

Lemma iter_rel'_rel {X} {n: nat} {R: relation X} {α ω: X} :
  iter_rel' n R α ω →
  iter_rel n R α ω.

Proof.

  revert ω.
  elim n; clear.
  intros ?; exact id.
  intros n IH ω ( ψ & H & Hn ).
  replace (S n) with (n + 1) by Psatz.lia.
  apply (iter_rel_trans n 1 R α ψ ω). auto.
  exists ω. vauto.
Qed.

Lemma iter'_clos_refl_trans {X} (R: relation X) n α ω :
iter_rel' n R α ω →
clos_refl_trans X R α ω.

Proof.

  revert ω.
  elim n; clear. intros ? ->; vauto.
  intros n IH ω (ψ & Hn & H). vauto.
Qed.

Lemma clos_trans_iter {X} (R: relation X) α ω :
  clos_trans X R α ω →
  ∃ n,
    iter_rel (S n) R α ω.

Proof.

  intros H.
  apply clos_trans_t1n in H. elim H; clear H.
  - intros x y H. exists O. simpl. vauto.
  - intros x y z Hiz Hyz (n & Hn). vauto.
Qed.

Corollary clos_refl_trans_iter {X} (R: relation X) α ω :
  clos_refl_trans X R α ω →
  ∃ n,
    iter_rel n R α ω.

Proof.

  intros H.
  apply clos_refl_trans_two_cases in H.
  destruct H as [ -> | H ]. exists O; vauto.
  destruct (clos_trans_iter _ _ _ H); vauto.
Qed.

Lemma iter_rel'_star {genv state} (step: genv → state → Events.trace → state → Prop) n ge α ω :
iter_rel' n (λ s, step ge s nil) α ω →
star step ge α nil ω.

Proof.

  revert ω.
  elim n; clear n; simpl.
  - intros ? <-. vauto.
  - intros n IH ω (ψ & Hn & STEP).
    eapply star_right; eauto.
Qed.

Corollary iter_rel'_plus {genv state} (step: genv → state → Events.trace → state → Prop) n ge α ω :
iter_rel' (S n) (λ s, step ge s nil) α ω →
plus step ge α nil ω.

Proof.

intros (ψ & STAR & STEP).
eapply plus_right. eauto using iter_rel'_star. exact STEP. reflexivity.
Qed.