proposition: Theorem evalDet_evalDist_equiv : forall (A : Set)(c : Comp A), well_formed_comp c -> forall a, rat_inf_limit (lowDistApprox c a) (evalDist c a).
proof: Proof. induction 1; intuition. unfold rat_inf_limit, inf_limit in *; intuition. exists O. intuition. simpl. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (ratIdentityIndiscernables a'). eapply lowDistApprox_Ret_inv. eauto. eapply rat0_le_all. eapply (@rat_inf_limit_squeeze (fun n => lowDistApprox_bind c1 c2 a (Nat.div2 n)) (lowDistApprox_bind c1 c2 a)); intuition. eapply rat_inf_limit_div_2. eapply lowDistApprox_bind_evalDist_limit; eauto. eapply lowDistApprox_bind_evalDist_limit; eauto. eapply lowDistApprox_bind_le_div2; eauto. eapply lowDistApprox_le_bind; eauto. eapply lowDistApprox_bind_div2_left_total; trivial. eapply lowDistApprox_bind_left_total; trivial. exists n. intuition. simpl. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (ratIdentityIndiscernables a'). assert (exists n'', n' = n + n'')%nat. exists (n' - n). lia. destruct H2. subst. rewrite lowDistApprox_Rnd. eapply eqRat_terms; intuition. eauto. eapply rat0_le_all. eapply lowDistApprox_limit_repeat. trivial. econstructor; eauto. trivial. Unshelve. eapply O. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat