proposition: Lemma RemoveSkips_Safe {av} : forall prog pre env, @Safe av env prog pre -> @Safe av env (RemoveSkips prog) pre.
proof: Proof. intros. eapply (Safe_coind RemoveSkips_Safe_CoInd_Hyp); intros; unfold RemoveSkips_Safe_CoInd_Hyp; lazymatch goal with | [ H: RemoveSkips_Safe_CoInd_Hyp _ _ |- _ ] => destruct H as (prog' & [ eq_rm | eq ] & safe); [ | subst; inversion' safe; intuition eauto ] | _ => solve [eexists; eauto] end. - induction prog'; simpl in eq_rm; try discriminate. + destruct_Is_Skip prog'1. * pose proof (RemoveSkip_left_Safe eq safe). intuition eauto using RemoveSkip_left_Safe. * inversion' safe; destruct_conjs. destruct_Is_Skip prog'2. { intuition. } { inversion' eq_rm; split; eexists; eauto using RemoveSkips_RunsTo. } - induction prog'; simpl in eq_rm; try discriminate. + destruct_Is_Skip prog'1. * pose proof (RemoveSkip_left_Safe eq safe). intuition. * inversion' safe; destruct_conjs. destruct_Is_Skip prog'2. { intuition. } { discriminate. } + inversion' eq_rm; inversion' safe; intuition eauto. - induction prog'; simpl in eq_rm; try discriminate. + destruct_Is_Skip prog'1. * pose proof (RemoveSkip_left_Safe eq safe). intuition. * inversion' safe; destruct_conjs. destruct_Is_Skip prog'2. { intuition. } { discriminate. } + inversion' eq_rm; inversion' safe. * left. intuition eauto. exists (DFacade.While cond prog'); intuition eauto using RemoveSkips_RunsTo. * solve [eauto]. - induction prog'; simpl in eq_rm; try discriminate. + destruct_Is_Skip prog'1. * pose proof (RemoveSkip_left_Safe eq safe). intuition. * inversion' safe; destruct_conjs. destruct_Is_Skip prog'2. { intuition. } { discriminate. } + inversion' eq_rm; inversion' safe; intuition eauto. - induction prog'; simpl in eq_rm; try discriminate. + destruct_Is_Skip prog'1. * pose proof (RemoveSkip_left_Safe eq safe). intuition. * inversion' safe; destruct_conjs. destruct_Is_Skip prog'2. { intuition. } { discriminate. } + inversion' eq_rm; inversion' safe. * intuition; eexists; eauto. * intuition eauto. eexists; split; eauto. right; eexists; intuition eauto. - eexists; eauto. - eexists; intuition eauto. right; eexists; intuition eauto. Qed.
imports: Bedrock.Platform.Facade.DFacade Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations Coq.Program.Program