Library compcertx.common.ValuesX

Require Export compcert.common.Values.
Import Coqlib.

Lemma val_inject_lessdef_compose:
  ∀ j v1 v2, val_inject j v1 v2 → ∀ v3, Val.lessdef v2 v3 → val_inject j v1 v3.
Proof.
  inversion 1; subst; inversion 1; subst; auto.
Qed.

Lemma val_lessdef_inject_compose:
  ∀ v1 v2, Val.lessdef v1 v2 → ∀ j v3, val_inject j v2 v3 → val_inject j v1 v3.
Proof.
  inversion 1; subst; inversion 1; subst; auto.
Qed.

Lemma val_inject_incr_recip :
  ∀ j1 v v1,
    val_inject j1 v v1 →
    ∀ j2 v2,
      val_inject j2 v v2 →
      inject_incr j2 j1 →
      val_inject j2 v v1.
Proof.
  inversion 1; subst; try (constructor; fail).
  inversion 1; subst.
  intro INCR. exploit INCR; eauto. intro.
  econstructor.
  2: reflexivity.
  congruence.
Qed.