proposition: Theorem correct: DFA.eval NFA_to_DFA == NFA.eval A.
proof: Proof. pose proof positive_size as Hpositive_size. pose proof theta_below as Htheta_below. pose proof delta'_below as Hdelta'_below. pose proof theta_delta' as Htheta_delta'. pose proof mem_table_finals as Hmem_table_finals. unfold NFA_to_DFA. destruct build_store as [[t d] n]. Opaque equal. simpl in *. Transparent equal. apply mx_to_scal_compat. apply right_filter with (mx_bool tt (nat_of_state n) size (fun s j => StateSet.mem j (theta (state_of_nat s))): KMX _ _). Opaque dot one zero equal. simpl. Transparent dot one zero equal. rewrite mx_point_one_left by num_lia. mx_intros i j Hi Hj. Opaque eq_nat_bool. simpl. bool_simpl. simpl. fold_regex. Transparent eq_nat_bool. rewrite theta_0. reflexivity. mx_intros i j Hi Hj; simpl. fold_regex. unfold labelling. setoid_rewrite sum_distr_left. rewrite sum_inversion. setoid_rewrite sum_distr_right. rewrite sum_inversion. apply sum_compat. intros a Ha. setoid_rewrite dot_xif_zero. simpl; fold_regex. setoid_rewrite dot_neutral_left. setoid_rewrite dot_neutral_right. apply leq_antisym; apply compare_sum_xif_zero; intros u Hu; bool_connectors; intros [Hu' Hu'']; simpl in *. exists (nat_of_state (delta' d a i)); auto. specialize (Hdelta'_below a i). num_lia. bool_connectors. num_prop. rewrite id_num. split; trivial. rewrite Htheta_delta' by num_lia. StateSetProps.mem_prop. apply <- in_delta_set. exists (state_of_nat u); auto. num_prop. rewrite Hu' in Hu''. clear u Hu Hu'. simpl in Hi. rewrite Htheta_delta', <- StateSetProps.mem_iff in Hu'' by num_lia. apply -> in_delta_set in Hu''. destruct Hu'' as [k [? ?]]. exists (nat_of_state k). apply Htheta_below, proj2 in H. clear - H. num_lia. rewrite id_num. bool_connectors. StateSetProps.mem_prop. rewrite id_num. auto. mx_intros i j Hi Hj; simpl in *. fold_regex. setoid_rewrite dot_xif_zero. rewrite Hmem_table_finals. case_eq (StateSet.exists_ (fun x => StateSet.mem x finaux) (theta (statesetelt_of_nat i))); intro H; simpl; fold_regex. rewrite <- StateSetProps.exists_iff in H by trivial. destruct H as [u [Hu Hu']]. rewrite (sum_fixed_xif_zero (v:=nat_of_state u)). auto with algebra. StateSetProps.mem_prop. apply HA in Hu'. apply Htheta_below, proj2 in Hu. num_lia. rewrite id_num. bool_connectors. StateSetProps.mem_prop. auto. apply sum_zero. intros m Hm. apply xif_false. simpl. rewrite <- H. rewrite bool_prop_iff. bool_connectors. rewrite H. StateSetProps.mem_prop. intuition auto with exfalso; try discriminate. rewrite <- H. rewrite <- StateSetProps.exists_iff by trivial. eexists; StateSetProps.mem_prop; eauto. 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) ATBR(DKA_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)