proposition: Lemma dat_correct_repeat_same_h : forall depth repeats (A : Set)(c : Comp A) P ls t a t1, dat_correct_h (Repeat c P) ls depth t -> well_formed_comp c -> In a (filter P (getSupport c)) -> (forall a' n' ls', evalDet_steps (cs_more c (firstn n' ls)) (cs_done a' ls') -> ls' = nil) -> dat_correct_h c ls depth t1 -> repeats >= depth -> datRepeat_depth (dat_correct_h c nil) P repeats depth t1 t.
proof: Proof. induction depth; intuition. inversion H; clear H; subst. inversion H5; clear H5; subst. inversion H6; clear H6; subst. simpl in *. apply evalDet_steps_bind_done_inv in H9. destruct H9. destruct H. intuition. inversion H3; clear H3; subst. inversion H; clear H; subst. case_eq (P x); intuition; rewrite H in H6. inversion H6; clear H6; subst. simpl in *. inversion H11; clear H11; subst. assert (a1 = a0 /\ s'0 = s'). eapply evalDet_steps_done_func; eauto. intuition. subst. econstructor. rewrite H. trivial. assert (x0 = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. inversion H6; clear H6; subst. simpl in *. apply evalDet_steps_bind_done_inv in H11. destruct H11. destruct H3. intuition. assert (x1 = nil). eapply evalDet_nil. eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done x0 (nil ++ ls))). eapply evalDet_steps_app_eq. trivial. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a = x). eapply evalDet_steps_nil_eq; eauto. eapply filter_In; eauto. subst. assert (P x = true). eapply filter_In; eauto. congruence. exfalso. eapply H. econstructor. eauto. inversion H3; clear H3; subst. inversion H; clear H; subst. case_eq (P a0); intuition. exfalso. eapply H5. econstructor. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. rewrite H. econstructor. eauto. simpl. econstructor. eapply datRepeat_depth_0. econstructor. trivial. trivial. econstructor. intuition. inversion H3; clear H3; subst. assert (s'0 = nil). eapply evalDet_nil; eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done a1 (nil ++ ls))). eapply evalDet_steps_app_eq. trivial. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a0 = a1 /\ s' = nil). eapply evalDet_steps_done_func; eauto. intuition. subst. assert (a = a1). eapply evalDet_steps_nil_eq; eauto. eapply filter_In; eauto. subst. assert (P a1 = true). eapply filter_In; eauto. congruence. econstructor. inversion H; clear H; subst. inversion H5; clear H5; subst. inversion H6; clear H6; subst. simpl in *. apply evalDet_steps_bind_done_inv in H9. destruct H9. destruct H. intuition. inversion H3; clear H3; subst. inversion H; clear H; subst. assert (x = a1 /\ x0 = s'0). eapply evalDet_steps_done_func; eauto. intuition; subst. assert (s'0 = nil). eapply H2. rewrite firstn_eq_all_gen. eauto. eauto. subst. case_eq (P a1); intuition. rewrite H in H6. inversion H6; clear H6; subst. simpl in *. inversion H11; clear H11; subst. econstructor. trivial. rewrite H in H6. inversion H6; clear H6; subst. simpl in *. apply evalDet_steps_bind_done_inv in H11. destruct H11. destruct H3. intuition. assert (x0 = nil). eapply evalDet_nil. eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done x (nil ++ ls))). eapply evalDet_steps_app_eq. eauto. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a = a1). eapply evalDet_steps_nil_eq. eauto. eapply filter_In; eauto. subst. assert (P a1 = true). eapply filter_In; eauto. congruence. exfalso. eapply H7. econstructor. eauto. edestruct (dat_exists_h depth (true::nil)); eauto. edestruct (dat_exists_h depth (false::nil)); eauto. inversion H3; clear H3; subst. inversion H9; clear H9; subst. case_eq (P a0); intuition. exfalso. eapply H6. econstructor. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. rewrite H3. econstructor. eauto. simpl. econstructor. destruct repeats. lia. eapply datRepeat_depth_leaf_Some_repeat. trivial. eapply dat_correct_h_internal; simpl. intuition. inversion H9; clear H9; subst. assert (s'0 = nil). eapply evalDet_nil. eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done a1 (nil ++ ls))). eapply evalDet_steps_app_eq. trivial. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a = a0). eapply evalDet_steps_nil_eq. eauto. eapply filter_In; eauto. subst. assert (P a0 = true). eapply filter_In; eauto. congruence. eauto. eauto. assert (s' = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. eapply datRepeat_depth_internal. eapply IHdepth. eapply dat_correct_h_repeat_app. eauto. trivial. eauto. trivial. eauto. intuition. destruct n'; simpl in *. eapply evalDet_nil; eauto. edestruct (@evalDet_dec _ c nil); eauto. destruct H11. inversion H11; clear H11; subst. assert (s' = nil). eapply evalDet_nil. eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done x1 (nil ++ ls))). eapply evalDet_steps_app_eq. trivial. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a = a0). eapply evalDet_steps_nil_eq. eauto. eapply filter_In; eauto. subst. assert (P a0 = true). eapply filter_In; eauto. congruence. rewrite firstn_nil in H9. eapply evalDet_app_nil; eauto. trivial. lia. eapply IHdepth. eapply dat_correct_h_repeat_app. eauto. trivial. eauto. trivial. eauto. intuition. destruct n'; simpl in *. eapply evalDet_nil; eauto. edestruct (@evalDet_dec _ c nil); eauto. destruct H11. inversion H11; clear H11; subst. assert (s' = nil). eapply evalDet_nil. eauto. subst. assert (evalDet_steps (cs_more c (nil ++ ls)) (cs_done x1 (nil ++ ls))). eapply evalDet_steps_app_eq. trivial. simpl in *. assert (ls = nil). eapply H2. rewrite firstn_eq_all_gen; eauto. subst. assert (a = a0). eapply evalDet_steps_nil_eq. eauto. eapply filter_In; eauto. subst. assert (P a0 = true). eapply filter_In; eauto. congruence. rewrite firstn_nil in H9. eapply evalDet_app_nil; eauto. trivial. lia. eapply datRepeat_depth_internal. eapply IHdepth; eauto. intuition. edestruct evalDet_steps_dec; eauto. destruct H9. destruct H9. exfalso. eapply H10. econstructor. eauto. eapply evalDet_app_nil. eauto. econstructor. eauto. destruct (ge_dec n' (length (ls ++ true :: nil))). rewrite firstn_ge_all in H3. eauto. trivial. apply not_ge in n. exfalso. assert (n' <= length ls)%nat. rewrite app_length in n. simpl in *. lia. rewrite firstn_app in H3. assert (ls = firstn n' ls ++ skipn n' ls). symmetry. eapply firstn_skipn. assert (evalDet_steps (cs_more c ((firstn n' ls) ++ (skipn n' ls))) (cs_done a' (ls' ++ (skipn n' ls)))). eapply evalDet_steps_app_eq. trivial. specialize (H10 a'). eapply H10. eapply (@evalDet_done _ _ _ a' (ls' ++ skipn n' ls)). rewrite H14 at 1. eapply H15. trivial. lia. eapply IHdepth; eauto. intuition. edestruct evalDet_steps_dec; eauto. destruct H9. destruct H9. exfalso. eapply H10. econstructor. eauto. eapply evalDet_app_nil. eauto. econstructor. eapply H9. destruct (ge_dec n' (length (ls ++ false :: nil))). rewrite firstn_ge_all in H3. eauto. trivial. apply not_ge in n. exfalso. assert (n' <= length ls)%nat. rewrite app_length in n. simpl in *. lia. rewrite firstn_app in H3. assert (ls = firstn n' ls ++ skipn n' ls). symmetry. eapply firstn_skipn. assert (evalDet_steps (cs_more c ((firstn n' ls) ++ (skipn n' ls))) (cs_done a' (ls' ++ (skipn n' ls)))). eapply evalDet_steps_app_eq. trivial. specialize (H10 a'). eapply H10. eapply (@evalDet_done _ _ _ a' (ls' ++ skipn n' ls)). rewrite H14 at 1. eapply H15. trivial. lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat