proposition: Theorem Repeat_unroll_n : forall n (A : Set)(eqda : EqDec A)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> (exists x, In x (filter P (getSupport c))) -> evalDist (Repeat c P) a == evalDist (x <-$ compMap _ (fun _ => c) (forNats n); match (hd_error (filter P x)) with | None => Repeat c P | Some z => ret z end) a.
proof: Proof. induction n; intuition. unfold forNats. unfold compMap. comp_simp. simpl. intuition. unfold forNats. fold forNats. unfold compMap. fold compMap. inline_first. rewrite repeat_unroll_eq. comp_skip. inline_first. case_eq (P x); intuition. comp_irr_r. eapply compMap_wf. intuition. comp_simp. simpl. rewrite H2. simpl. reflexivity. rewrite IHn. comp_skip. reflexivity. comp_simp. simpl. rewrite H2. intuition. trivial. trivial. trivial. trivial. Qed.
imports: FCF.FCF Permutation