proposition: Lemma evalDet_lowDistApprox_ls_done: forall (A : Set) (eqd : eq_dec A) (c : Comp A) (s : Blist) (a1 a2 : A) (n : nat), evalDet c s (ca_done a1) -> lowDistApprox_ls c a2 n s (if eqd a2 a1 then 1 else 0).
proof: Proof. unfold lowDistApprox_ls. intuition. exists (listRepeat (ca_done a1) (length (getAllBlists n))). destruct (eqd a1 a2); subst. exists (length (getAllBlists n)). intuition. eapply rel_map_listRepeat. intuition. eapply evalDet_app_eq. trivial. eapply pred_count_eq_all; intuition. symmetry. eapply in_listRepeat_inv. eauto. rewrite listRepeat_length. trivial. destruct (eqd a2 a2); try congruence. rewrite getAllBlists_length. apply num_dem_same_rat1. unfold natToPosnat, posnatToNat. trivial. exists O. intuition. eapply rel_map_listRepeat. intuition. eapply evalDet_app_eq. trivial. eapply pred_count_eq_none; intuition. subst. assert (ca_done a2 = ca_done a1). eapply in_listRepeat_inv. eauto. inversion H1; subst; clear H1. intuition. destruct (eqd a2 a1); subst; try congruence. apply rat_num_0. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat