proposition: Lemma CompileWhileTrue: forall {av} (env : GLabelMap.t (FuncSpec av)) (ext : StringMap.t (Value av)) (tenv : Telescope av) tenv' tenv'' test body, Lifted_is_true ext tenv test -> {{ tenv }} body {{ tenv' }} ∪ {{ ext }} // env -> {{ tenv' }} (DFacade.While test body) {{ tenv'' }} ∪ {{ ext }} // env -> {{ tenv }} (DFacade.While test body) {{ tenv'' }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | [ H: forall st, st ≲ _ ∪ _ -> _, H': ?st ≲ _ ∪ _ |- _ ] => learn (H _ H') | [ H: is_true ?t ?st, H': is_false ?t ?st |- _ ] => exfalso; exact (is_true_is_false_contradiction H H') | _ => SameValues_Facade_t_step | _ => facade_cleanup_call | _ => LiftPropertyToTelescope_t | _ => apply SafeWhileTrue | [ H: RunsTo _ (DFacade.While _ _) _ _ |- _ ] => inversion H; unfold_and_subst; clear H end. Qed.
imports: CertifiedExtraction.Extraction.DeallocSCA CertifiedExtraction.Extraction.External.Core