proposition: Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistApproxTree A)(rel : nat -> DistApproxTree A -> Prop) reps depth (P : A -> bool), datRepeat_depth rel P reps depth t1 t1' -> forall n1 (t2' : DistApproxTree A), reps >= n2 -> datRepeat (rel n1) P n2 t2 t2' -> dat_better t1 t2 -> depth >= n1 * n2 + datDepth t2 -> (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 t1' t2'.
proof: Proof. induction n2; induction t2; intuition. inversion H2; clear H2; subst. inversion H1; clear H1; subst. econstructor. inversion H1; clear H1; subst. inversion H; clear H; subst. econstructor. congruence. congruence. econstructor. inversion H2; clear H2; subst. inversion H1; clear H1; subst. inversion H; clear H; subst. simpl in *. rewrite Nat.mul_0_r in *. simpl in *. assert (depth0 >= (max (datDepth t2_1) (datDepth t2_2))). lia. econstructor. eapply IHt2_1. eauto. lia. eauto. eauto. rewrite Nat.mul_0_r; simpl. eapply Nat.max_lub_l. eauto. trivial. trivial. trivial. trivial. eapply IHt2_2. eauto. lia. eauto. trivial. rewrite Nat.mul_0_r; simpl. eapply Nat.max_lub_r. eauto. trivial. trivial. trivial. trivial. inversion H2; clear H2; subst. inversion H1; clear H1; subst. econstructor. inversion H1; clear H1; subst. inversion H; clear H; subst. econstructor. congruence. congruence. inversion H; clear H; subst. congruence. lia. rewrite Nat.mul_comm in H3. simpl in *. eapply IHn2. eauto. lia. eauto. eapply H4; eauto. remember (n2 * n1)%nat as x. lia. eapply Nat.le_trans. 2:{ eapply H3. } rewrite Nat.add_0_r. rewrite Nat.add_comm. eapply Nat.add_le_mono. eauto. rewrite Nat.mul_comm. trivial. trivial. trivial. trivial. inversion H2; clear H2; subst. inversion H1; clear H1; subst. inversion H; clear H; subst. simpl in *. econstructor. eapply IHt2_1. eauto. trivial. eauto. trivial. eapply Nat.le_trans. eapply Nat.add_le_mono. eapply Nat.le_refl. eapply (Nat.max_lub_l (datDepth t2_1) (datDepth t2_2)). eapply Nat.le_refl. lia. trivial. trivial. trivial. eapply IHt2_2. eauto. trivial. eauto. trivial. eapply Nat.le_trans. eapply Nat.add_le_mono. eapply Nat.le_refl. eapply (Nat.max_lub_r (datDepth t2_1) (datDepth t2_2)). eapply Nat.le_refl. lia. trivial. trivial. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat