proposition: Theorem fundamental_lemma_h : forall (A : Set)(eqda : EqDec A)(c1 c2 : Comp (A * bool)), (evalDist (Bind c1 (fun x => ret snd x)) true == evalDist (Bind c2 (fun x => ret snd x)) true) -> (forall a, evalDist c1 (a, false) == evalDist c2 (a, false)) -> forall a, ratDistance (evalDist (Bind c1 (fun x => ret (fst x))) a) (evalDist (Bind c2 (fun x => ret (fst x))) a) <= evalDist (Bind c1 (fun x => ret snd x)) true.
proof: Proof. intuition. simpl in *. rewrite (sumList_filter_partition (@snd A bool)). rewrite (sumList_filter_partition (@snd A bool) (getSupport c2)). rewrite ratDistance_add_same_r_gen. eapply leRat_trans. eapply ratDistance_le_max_triv. eapply maxRat_leRat_same. eapply leRat_trans. 2:{ eapply sumList_filter_le. } eapply sumList_le; intuition. apply filter_In in H1. intuition. eapply ratMult_leRat_compat; intuition. destruct a0. simpl in *. subst. destruct (EqDec_dec bool_EqDec true true); try congruence. destruct (EqDec_dec eqda a0 a); intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H. } eapply leRat_trans. 2:{ eapply sumList_filter_le. } eapply sumList_le; intuition. apply filter_In in H1. intuition. eapply ratMult_leRat_compat; intuition. destruct a0. simpl in *. subst. destruct (EqDec_dec bool_EqDec true true); try congruence. destruct (EqDec_dec eqda a0 a); intuition. assert (eq_dec (A * bool)). unfold eq_dec. eapply (EqDec_dec (pair_EqDec _ _)). assert (NoDup (filter (fun a0 : A * bool => negb (snd a0)) (intersect H1 (getSupport c1) (getSupport c2)))). eapply filter_NoDup. eapply filter_NoDup; eapply getSupport_NoDup. eapply eqRat_trans. symmetry. eapply sumList_subset'. trivial. eapply H2. eapply filter_NoDup. eapply getSupport_NoDup. intuition. apply filter_In in H3. intuition. eapply filter_In. split. eapply in_intersect. eapply Permutation_in. eapply intersect_comm. eapply getSupport_NoDup. 2:{ eauto. } eapply getSupport_NoDup. trivial. intuition. apply filter_In in H3. intuition. destruct a0. simpl in *. destruct (EqDec_dec eqda a0 a); subst. rewrite ratMult_1_r. destruct b; simpl in *; try discriminate. rewrite H0. eapply getSupport_not_In_evalDist. intuition. eapply H4. eapply filter_In. intuition. eapply in_intersect. intuition. apply ratMult_0_r. symmetry. eapply eqRat_trans. symmetry. eapply sumList_subset'. trivial. eapply H2. eapply filter_NoDup. eapply getSupport_NoDup. intuition. apply filter_In in H3. intuition. eapply filter_In. split. eapply in_intersect. eauto. trivial. intuition. apply filter_In in H3. intuition. destruct a0. simpl in *. destruct (EqDec_dec eqda a0 a); subst. rewrite ratMult_1_r. destruct b; simpl in *; try discriminate. rewrite <- H0. eapply getSupport_not_In_evalDist. intuition. eapply H4. eapply filter_In. intuition. eapply in_intersect. intuition. apply ratMult_0_r. eapply sumList_body_eq. intuition. apply filter_In in H3. intuition. destruct a0; simpl in *. destruct b; simpl in *; try discriminate. rewrite H0. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia