proposition: Lemma CompileBinopOrTest_right_inPlace_tel_generalized: forall {av} op vret varg (val1 val2: W) env ext (tenv tenv': Telescope av) pCoda, PreconditionSet tenv ext [[[vret; varg]]] -> {{ [[`vret ->> (eval_binop op val1 val2) as _]]::[[`varg ->> val2 as _]]::tenv }} pCoda {{ [[`vret ->> (eval_binop op val1 val2) as _]]::tenv' }} ∪ {{ ext }} // env -> {{ [[`vret ->> val1 as _]]::[[`varg ->> val2 as _]]::tenv }} (Seq (Assign vret (WrapOpInExpr op (Var vret) (Var varg))) pCoda) {{ [[`vret ->> (eval_binop op val1 val2) as _]]::tenv' }} ∪ {{ ext }} // env.
proof: Proof. repeat hoare. move_to_front varg. apply ProgOk_Chomp_Some; try compile_do_side_conditions. intros; apply CompileBinopOrTest_right_inPlace; try compile_do_side_conditions. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics