Module BTL_SEsimplifyproof

Require Import Op.
Require Import BTL_SEtheory BTL_SEsimuref BTL_SEsimplify.

Import SvalNotations.

Local Open Scope impure_scope.


Lemma rewrite_ops_correct RRULES ctx op lsv iinfo l hlsv fsv pre args: forall
   (H: rewrite_ops RRULES op lsv iinfo = Some (fsv, pre))
   (LMAP: lmap_sv (fun sv => Some sv) lsv = Some l)
   (ELSVEQ: list_sval_equiv ctx l hlsv)
   (OK: eval_list_sval ctx hlsv = Some args)
   (PRE: Forall (eval_okclause ctx) pre),
   eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm1 ctx).
Global Opaque rewrite_ops.

Theorem rewrite_cbranches_correct RRULES c1 l1 iinfo ctx c2 l2 pre: forall
  (H : rewrite_cbranches RRULES c1 l1 iinfo = Some ((c2, l2), pre))
  (PRE : Forall (eval_okclause ctx) pre)
  (AARGS : Forall (fun sv => alive (eval_sval ctx sv)) l1),
  eval_scondition ctx c2 l2 =
  eval_scondition ctx c1 (lsv_of_list l1).
Global Opaque rewrite_cbranches.