proposition: Theorem dce_simulation: forall c s c' s', red (c, s) (c', s') -> forall L s1, agree (live c L) s s1 -> (exists s1', red (dce c L, s1) (dce c' L, s1') /\ agree (live c' L) s' s1') \/ ((measure c' < measure c)%nat /\ dce c L = dce c' L /\ agree (live c' L) s' s1).
proof: Proof. intros until s'; intros STEP. dependent induction STEP; intros. Abort. Section RENAMING. Variable f: ident -> ident. Fixpoint rename_aexp (a: aexp) : aexp := match a with | CONST n => CONST n | VAR x => VAR (f x) | PLUS a1 a2 => PLUS (rename_aexp a1) (rename_aexp a2) | MINUS a1 a2 => MINUS (rename_aexp a1) (rename_aexp a2) end. Fixpoint rename_bexp (b: bexp) : bexp := match b with | TRUE => TRUE | FALSE => FALSE | EQUAL a1 a2 => EQUAL (rename_aexp a1) (rename_aexp a2) | LESSEQUAL a1 a2 => LESSEQUAL (rename_aexp a1) (rename_aexp a2) | NOT b1 => NOT (rename_bexp b1) | AND b1 b2 => AND (rename_bexp b1) (rename_bexp b2) end. Definition expr_is_var (a: aexp): option ident := match a with VAR x => Some x | _ => None end. Lemma expr_is_var_correct: forall a x, expr_is_var a = Some x -> a = VAR x. Proof. unfold expr_is_var; intros. destruct a; congruence. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)