proposition: Theorem repeat_unroll_eq: forall (A : Set)(eqd : EqDec A)(c : Comp A)(P : A -> bool) v, well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> evalDist (Repeat c P) v == evalDist (x <-$ c; if (P x) then ret x else (Repeat c P)) v.
proof: Proof. intuition. eapply det_eq_impl_dist_sem_eq; trivial. destruct H0. eapply well_formed_Repeat; trivial. unfold eq_dec. intuition. eapply (EqDec_dec _). eauto. econstructor; intuition. destruct (P b). econstructor. destruct H0. econstructor. unfold eq_dec. intuition. eapply (EqDec_dec _). trivial. eauto. unfold DetSem.evalDet_equiv. intuition. inversion H1; clear H1; subst. inversion H2; clear H2; subst. simpl in *. eapply evalDet_steps_bind_done_inv in H6. destruct H6. destruct H1. intuition. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. destruct (P x). inversion H3; clear H3; subst. simpl in *. inversion H7; clear H7; subst. econstructor. eauto. simpl. 2:eassumption. constructor. inversion H2; clear H2; subst. simpl in *. apply evalDet_steps_bind_eof_inv in H6. intuition. econstructor. eapply evalDet_bind_eof. trivial. destruct H1. destruct H1. intuition. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. destruct (P x). inversion H3; clear H3; subst. simpl in *. inversion H7. trivial. inversion H1; clear H1; subst. eapply evalDet_steps_bind_done_inv in H2. destruct H2. destruct H1. intuition. econstructor. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. destruct (P x). inversion H3; clear H3; subst. simpl in *. inversion H7; clear H7; subst. econstructor. eauto. simpl. 2:eassumption. constructor. apply evalDet_steps_bind_eof_inv in H2. intuition. econstructor. econstructor. eauto. simpl. eapply evalDet_bind_eof. trivial. destruct H1. destruct H1. intuition. econstructor. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. destruct (P x). inversion H3; clear H3; subst. simpl in *. inversion H7. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia