Module ErasureSimulationValues

Set Implicit Arguments.
Require Import MyTactics.
Require Import Layers.
Require Import Programs.
Require Import RawPrograms.
Require Import Erasure.
Require Import SemanticsValues.
Require Import PathSemantics.

-------------------------------------------------------------------------

Value reduction is invisible up to erasure.

Lemma values_stutter:
  forall v1 v2,
  redv v1 v2 ->
  erase_value v1 = erase_value v2.

Proof.

induction 1; simpl; layers; eauto using plugging_respects_erasure;

RedCoStarCommutative and RedCoStarAssociative: destruct disjunctions of hypotheses about layers

  repeat match goal with h: _ \/ _ |- _ => destruct h end;
  simpl in *;
  intuition congruence.
Qed.

Lemma values_stutter_yup:
  forall vs1 vs2,
  redvs vs1 vs2 ->
  pwe vs1 vs2.

Proof.

induction 1; eauto using values_stutter, pwe_reflexive.
Qed.