proposition: Lemma lowDistApproxFromTree_datMap_inv : forall (A B : Set)(eqda : eq_dec A)(eqdb : eq_dec B)(tb : DistApproxTree B)(ta : DistApproxTree A)(mapRel : B -> DistApproxTree A -> Prop), datMap mapRel tb ta -> (forall b, In b (getTreeSupport eqdb tb) -> exists t, mapRel b t) -> (forall b t1 t2, mapRel b t1 -> mapRel b t2 -> t1 = t2) -> forall a r, sumList_rel (fun b r' => forall ta', mapRel b ta' -> lowDistApproxFromTree eqdb tb b * lowDistApproxFromTree eqda ta' a == r') (getTreeSupport eqdb tb) r -> lowDistApproxFromTree eqda ta a == r.
proof: Proof. induction 1; intuition; simpl in *. apply sumList_rel_all_0_inv in H1; intuition. simpl in *. intuition. eapply sumList_rel_only_one_inv in H2. rewrite H2. eapply eqRat_refl. unfold getTreeSupport. simpl. eauto. unfold getTreeSupport. simpl. econstructor. intuition. econstructor. intuition. simpl in *. intuition. intuition. rewrite <- H3. destruct (eqdb a a); intuition. rewrite ratMult_1_l. eapply eqRat_refl. intuition. trivial. unfold getTreeSupport in *. simpl in *. assert (sumList_rel (fun (b : B) (r' : Rat) => forall ta' : DistApproxTree A, mapRel b ta' -> ((lowDistApproxFromTree eqdb t1a b * (1 / 2) * lowDistApproxFromTree eqda ta' a) + (lowDistApproxFromTree eqdb t2a b * (1 / 2) * lowDistApproxFromTree eqda ta' a) == r')) (getUnique (getTreeSupport_dups t1a ++ getTreeSupport_dups t2a) eqdb) r). eapply sumList_rel_body_eq. eapply H3. intuition. rewrite <- ratMult_distrib_r. eapply H4; eauto. intuition. trivial. clear H3. remember (fun b r' => forall ta', (mapRel b ta' -> lowDistApproxFromTree eqdb t1a b * lowDistApproxFromTree eqda ta' a == r')) as rel1. remember (fun b r' => forall ta', (mapRel b ta' -> lowDistApproxFromTree eqdb t2a b * lowDistApproxFromTree eqda ta' a == r')) as rel2. edestruct (sumList_rel_left_total rel1). intuition. destruct (H1 a0). eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eapply H3. exists (lowDistApproxFromTree eqdb t1a a0 * lowDistApproxFromTree eqda x a). subst. intuition. assert (x = ta'). eauto. subst. intuition. edestruct (sumList_rel_left_total rel2). intuition. subst. destruct (H1 a0). eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eapply H5. exists (lowDistApproxFromTree eqdb t2a a0 * lowDistApproxFromTree eqda x0 a). intuition. assert (x0 = ta'). eauto. subst. intuition. rewrite IHdatMap1; subst; eauto. rewrite IHdatMap2; subst; eauto. assert (sumList_rel (fun (b : B) (r' : Rat) => forall ta' : DistApproxTree A, mapRel b ta' -> lowDistApproxFromTree eqdb t1a b * lowDistApproxFromTree eqda ta' a == r' * (2/1)) (getUnique (getTreeSupport_dups t1a) eqdb) (x * (1/2))). eapply (sumList_rel_factor_constant (pos 1) (pos 2)). eapply sumList_rel_body_eq. eapply H3. intuition. specialize (H6 ta'). rewrite H6. intuition. rewrite ratMult_assoc. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. rewrite <- ratMult_num_den. symmetry. eapply num_dem_same_rat1. unfold posnatMult, posnatToNat, natToPosnat. trivial. trivial. rewrite ratMult_assoc. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. rewrite <- ratMult_num_den. symmetry. eapply num_dem_same_rat1. trivial. trivial. clear H3. assert (sumList_rel (fun (b : B) (r' : Rat) => forall ta' : DistApproxTree A, mapRel b ta' -> lowDistApproxFromTree eqdb t2a b * lowDistApproxFromTree eqda ta' a == r' * (2/1)) (getUnique (getTreeSupport_dups t2a) eqdb) (x0 * (1/2))). eapply (sumList_rel_factor_constant (pos 1) (pos 2)). eapply sumList_rel_body_eq. eapply H5. intuition. specialize (H3 ta'). intuition. rewrite H8. rewrite ratMult_assoc. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. rewrite <- ratMult_num_den. symmetry. eapply num_dem_same_rat1. unfold posnatMult, posnatToNat, natToPosnat. trivial. rewrite ratMult_assoc. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. rewrite <- ratMult_num_den. symmetry. eapply num_dem_same_rat1. trivial. trivial. clear H5. assert (sumList_rel (fun (b : B) (r' : Rat) => forall ta' : DistApproxTree A, mapRel b ta' -> lowDistApproxFromTree eqdb t1a b * lowDistApproxFromTree eqda ta' a == r' * (2 / 1)) (getUnique (getTreeSupport_dups t1a ++ getTreeSupport_dups t2a) eqdb) (x * (1 / 2))). eapply sumList_rel_ls_intersect. eapply H6. eapply getUnique_NoDup. eapply getUnique_NoDup. trivial. intuition. destruct (H1 a0). eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eauto. assert (r1 * (2/1) == r2 * (2/1)). rewrite <- H7. rewrite <- H8. eapply eqRat_refl. eauto. eauto. eapply ratMult_same_r_inv. eauto. intuition. intuition. exfalso. eapply H7. eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eauto. intuition. rewrite ratMult_0_l. eapply ratMult_0. left. eapply lowDistApproxFromTree_eq_0. unfold getTreeSupport. intuition. clear H6. assert (sumList_rel (fun (b : B) (r' : Rat) => forall ta' : DistApproxTree A, mapRel b ta' -> lowDistApproxFromTree eqdb t2a b * lowDistApproxFromTree eqda ta' a == r' * (2 / 1)) (getUnique (getTreeSupport_dups t1a ++ getTreeSupport_dups t2a) eqdb) (x0 * (1 / 2))). eapply sumList_rel_ls_intersect. eapply H3. eapply getUnique_NoDup. eapply getUnique_NoDup. trivial. intuition. destruct (H1 a0). eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eauto. assert (r1 * (2/1) == r2 * (2/1)). rewrite <- H7. rewrite <- H8. eapply eqRat_refl. eauto. trivial. eapply ratMult_same_r_inv. eauto. intuition. intuition. exfalso. eapply H7. eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eauto. intuition. rewrite ratMult_0_l. eapply ratMult_0. left. eapply lowDistApproxFromTree_eq_0. intuition. clear H3. symmetry. eapply sumList_rel_plus_inv. 3:{ eapply H5. } 3:{ eapply H6. } eapply H4. intuition. destruct (H1 a0). trivial. rewrite <- H7; eauto. specialize (H8 _ H10). specialize (H9 _ H10). eapply ratMult_inverse_nat in H8. eapply ratMult_inverse_nat in H9. eapply ratAdd_eqRat_compat. rewrite ratMult_assoc. rewrite (ratMult_comm (1/2)). rewrite <- ratMult_assoc. eapply H8. rewrite ratMult_assoc. rewrite (ratMult_comm (1/2)). rewrite <- ratMult_assoc. eauto. intuition. destruct (H1 b). eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eauto. econstructor. eauto. intuition. destruct (H1 b). eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eauto. econstructor. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat