proposition: Lemma eval_left: forall (A B: DFA.t), bounded A -> eval (change_initial (merge_DFAs A B) (pi0 (initial A))) == eval A.
proof: Proof. intros A B HA. apply mx_to_scal_compat. simpl. set (s := nat_of_state (max (pi0 (size A)) (pi1 (size B)))). apply left_filter with (box (size A) s (fun i j => xif (eq_state_bool (state_of_nat j) (pi0 (state_of_nat i)) && lt_state_bool i (size A)) (1: regex) (0: regex))). mx_intros i j Hi Hj. Transparent dot. simpl. fold_regex. Opaque dot. apply bounded_initial in HA. setoid_rewrite xif_dot. rewrite (sum_collapse (n:=initial A)). 2: num_lia. bool_simpl. simpl. rewrite dot_neutral_left. apply xif_compat; auto. rewrite id_num. rewrite bool_prop_iff. bool_connectors. num_prop. nat_prop. intuition; num_lia. simpl. intros x Hx. nat_analyse; simpl; auto with algebra. mx_intros i j Hi Hj. Transparent dot. simpl. fold_regex. Opaque dot. unfold labelling. setoid_rewrite xif_dot. setoid_rewrite dot_ann_left. setoid_rewrite dot_neutral_left. setoid_rewrite xif_sum_zero. rewrite sum_inversion. setoid_rewrite sum_distr_left. rewrite sum_inversion. apply sum_compat. intros a Ha. simpl. setoid_rewrite dot_xif_zero. setoid_rewrite dot_neutral_right. setoid_rewrite xif_xif_and. rewrite sum_collapse'. setoid_rewrite <- andb_assoc. rewrite sum_collapse'. apply xif_compat; auto. rewrite 2id_num. rewrite match_pi0. rewrite bool_prop_iff. bool_connectors. num_prop. intuition. num_lia. apply (bounded_delta HA). unfold s. rewrite <- lt_nat_spec. apply below_max_pi0. num_lia. apply -> lt_nat_spec. apply (bounded_delta HA). mx_intros i j Hi Hj. Transparent dot. simpl. fold_regex. Opaque dot. setoid_rewrite dot_xif_zero. setoid_rewrite dot_neutral_left. setoid_rewrite <- andb_assoc. rewrite sum_collapse'. apply xif_compat; auto. rewrite id_num. rewrite bool_prop_iff. bool_connectors. num_prop. StateSetProps.mem_prop. rewrite and_neutral_left by num_lia. generalize (finaux A). rapply StateSetProps.set_induction_above. intros t H. rewrite H at 1. StateSetProps.set_iff. rewrite StateSetProps.Props.fold_1b by auto with set. apply StateSetProps.Props.fold_rec_nodep. StateSetProps.setdec. intros. StateSetProps.set_iff. intuition. discriminate. intros p x IHx H2 H t H1. Transparent NumSet.add. rewrite H1 at 1. rewrite (StateSetProps.fold_equal _ compare_compat _ H1); auto. rewrite StateSetProps.fold_add_above; ti_auto. StateSetProps.set_iff. rewrite <- IHx. intuition (try subst; auto using pi0_inj). repeat intro. psubst. rewrite H3. reflexivity. apply -> lt_nat_spec. apply below_max_pi0. num_lia. Opaque NumSet.add. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions)