proposition: Lemma ProdIntegrableSimplifyDisjoint : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)), ProdIntegrableSimple (ProdIntegrableSimplify hn).
proof: Proof. intros. apply (forall_disjoint_pairs_equiv _ _ (ProdSubsetIntersect hn (fst (nil,@nil bool)) (snd (@nil bool, nil)))). intros. unfold ProdIntegrableSimplify in H0. rewrite map_length, prod_length in H0. assert (0 < length (FreeSubsets (length hn)))%nat as lenPos. { destruct (length (FreeSubsets (length hn))). exfalso; inversion H0. apply le_n_S, Nat.le_0_l. } unfold ProdIntegrableSimplify. do 2 rewrite (map_nth (fun xy => ProdSubsetIntersect hn (fst xy) (snd xy)) _ (@nil bool, @nil bool)). rewrite (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil i (Nat.lt_trans _ _ _ H H0)). rewrite (nth_list_prod (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil j H0). unfold fst, snd. remember (i / length (FreeSubsets (length hn)))%nat as a. remember (i mod (length (FreeSubsets (length hn))))%nat as b. remember (j / length (FreeSubsets (length hn)))%nat as c. remember (j mod (length (FreeSubsets (length hn))))%nat as d. intros x y z. simpl in z. destruct z as [xH [xK [yH yK]]]. destruct (Nat.eq_dec a c). - assert (b <> d). { intro abs. subst d. subst b. subst c. subst a. rewrite (nat_euclid_unique _ _ _ lenPos e abs) in H. exact (Nat.lt_irrefl j H). } assert (d < length (FreeSubsets (length hn)))%nat as din. { subst d. apply Nat.mod_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl _ lenPos). } apply (ProdIntegrableSubsetsDisjoint (map prodint_g hn) (nth d (FreeSubsets (length hn)) nil) (nth b (FreeSubsets (length hn)) nil) y). 4: split; assumption. rewrite (FreeSubsetsLength (length hn)). rewrite (FreeSubsetsLength (length hn)). reflexivity. apply nth_In. subst b. apply Nat.mod_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl _ lenPos). apply nth_In. exact din. rewrite (FreeSubsetsLength (length hn)). rewrite map_length. reflexivity. apply nth_In. exact din. apply FreeSubsetsDifferent. intro abs. apply H1. symmetry. exact abs. exact din. subst b. apply Nat.mod_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl _ lenPos). - assert (c < length (FreeSubsets (length hn)))%nat as cin. { subst c. apply Nat.div_lt_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl 0 lenPos). exact H0. } apply (ProdIntegrableSubsetsDisjoint (map prodint_f hn) (nth c (FreeSubsets (length hn)) nil) (nth a (FreeSubsets (length hn)) nil) x). 4: split; assumption. clear xH xK yH yK. rewrite (FreeSubsetsLength (length hn)). rewrite (FreeSubsetsLength (length hn)). reflexivity. apply nth_In. subst a. apply Nat.div_lt_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl 0 lenPos). exact (Nat.lt_trans _ _ _ H H0). apply nth_In. exact cin. rewrite (FreeSubsetsLength (length hn)). rewrite map_length. reflexivity. apply nth_In. exact cin. apply FreeSubsetsDifferent. intro abs. apply n. symmetry. exact abs. exact cin. subst a. apply Nat.div_lt_upper_bound. intro abs. rewrite abs in lenPos. exact (Nat.lt_irrefl 0 lenPos). exact (Nat.lt_trans _ _ _ H H0). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile