proposition: Lemma CompileBinopOrTest_full: forall {av} name var1 var2 (val1 val2: W) env ext op p1 p2 (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> var1 ∉ ext -> var2 ∉ ext -> var1 <> var2 -> var1 <> name -> var2 <> name -> {{ tenv }} p1 {{ [[`var1 ->> val1 as _]]::tenv }} ∪ {{ ext }} // env -> {{ [[`var1 ->> val1 as _]]::tenv }} p2 {{ [[`var1 ->> val1 as _]]::[[`var2 ->> val2 as _]]::tenv }} ∪ {{ ext }} // env -> {{ tenv }} (Seq p1 (Seq p2 (Assign name ((match op with inl o => Binop o | inr o => TestE o end) (Var var1) (Var var2))))) {{ [[`name ->> (eval_binop op val1 val2) as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat hoare. destruct op; SameValues_Facade_t. apply (SameValues_Pop_Both (H := FacadeWrapper_SCA)); eauto 2. apply SameValues_not_In_Telescope_not_in_Ext_remove; eauto 2. eapply SameValues_forget_Ext. 2:eapply SameValues_forget_Ext; try eassumption. eauto with SameValues_db. eauto with SameValues_db. apply (SameValues_Pop_Both (H := FacadeWrapper_SCA)); eauto 2. apply SameValues_not_In_Telescope_not_in_Ext_remove; eauto 2. eapply SameValues_forget_Ext. 2:eapply SameValues_forget_Ext; try eassumption. eauto with SameValues_db. eauto with SameValues_db. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics