proposition: Lemma datRepeat_better_depth: forall (A : Set) n2 (t2 t1 t1' : DistApproxTree A)(rel : nat -> DistApproxTree A -> Prop) reps depth (P : A -> bool), forall n1 (t2' : DistApproxTree A), datRepeat (rel n1) P n2 t2 t2' -> datRepeat_depth rel P reps depth t1 t1' -> dat_better t2 t1 -> n1 >= depth -> n2 >= reps -> (forall (n1 n2: nat) (t3 t4 : DistApproxTree A), rel n1 t3 -> rel n2 t4 -> n1 >= n2 -> dat_better t3 t4) -> (forall a, rel 0%nat (dat_leaf (Some a)) -> P a = true) -> (forall n t, rel n t -> datDepth t <= n)%nat -> dat_better t2' t1'.
proof: Proof. induction n2; induction t2; intuition. assert (reps = O). lia. subst. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. inversion H0; clear H0; subst. inversion H; clear H; subst. econstructor. congruence. econstructor. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. inversion H0; clear H0; subst. inversion H; clear H; subst. econstructor. eapply IHt2_1; eauto; lia. eapply IHt2_2; eauto; lia. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. inversion H0; clear H0; subst. inversion H; clear H; subst. econstructor. congruence. econstructor. inversion H; clear H; subst. congruence. eapply IHn2. eauto. eauto. eapply H4; eauto. trivial. lia. trivial. trivial. trivial. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. inversion H; clear H; subst. inversion H0; clear H0; subst. econstructor. eapply IHt2_1; eauto; lia. eapply IHt2_2; eauto; lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat