proposition: Lemma CompileIf : forall {av A} k tmp (gallinaTest: bool) (gallinaT gallinaF: Comp A) facadeTest facadeT facadeF env (ext: StringMap.t (Value av)) tenv tenv', tmp ∉ ext -> NotInTelescope tmp tenv -> {{ tenv }} facadeTest {{ [[`tmp ->> (bool2w gallinaTest) as _]]::tenv }} ∪ {{ ext }} // env -> {{ [[`tmp ->> (bool2w gallinaTest) as _]]::tenv }} facadeT {{ [[`tmp ->> (bool2w gallinaTest) as _]]::[[k ~~> gallinaT as v]]::tenv' v }} ∪ {{ ext }} // env -> {{ [[`tmp ->> (bool2w gallinaTest) as _]]::tenv }} facadeF {{ [[`tmp ->> (bool2w gallinaTest) as _]]::[[k ~~> gallinaF as v]]::tenv' v }} ∪ {{ ext }} // env -> {{ tenv }} (Seq facadeTest (DFacade.If (isTrueExpr tmp) facadeT facadeF)) {{ [[k ~~> if gallinaTest then gallinaT else gallinaF as v]]::tenv' v }} ∪ {{ ext }} // env.
proof: Proof. intros; hoare. repeat (SameValues_Facade_t_step || facade_if_helper). Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics