proposition: Theorem language_DFA_eval: forall A, DFA.bounded A -> regex_language (DFA.eval A) == DFA_language A.
proof: Proof. Opaque leq plus. intros A HA. fold_regex_language. unfold DFA.eval, MAUT.eval, comp. rewrite functor_mx_to_scal. rewrite 2functor_dot. rewrite functor_star. rewrite simpl_regex_language. Opaque eq_nat_bool regex_language_f. simpl. bool_simpl. simpl. fold_langAlg label. Transparent regex_language_f. setoid_rewrite sum_distr_left. setoid_rewrite functor_xif. Transparent regex_language_f. simpl. fold_langAlg label. setoid_rewrite dot_boolxif_right. setoid_rewrite dot_boolxif_left. setoid_rewrite xif_xif_and. rewrite sum_inversion. rewrite (sum_collapse (G:=@lang_Graph label) (n:=DFA.initial A)). 2: apply DFA.bounded_initial in HA; num_lia. 2: simpl; intros; fold_langAlg label. 2: apply sum_zero; intros; apply xif_false. 2: bool_connectors; nat_prop; intuition. simpl Peano.plus. bool_simpl. unfold DFA_language. generalize (DFA.bounded_initial HA) as Hs. generalize (DFA.initial A) as s. intros s Hs. match goal with |- context[box ?n ?m ?f] => set (M:=box n m f) end. apply leq_antisym. apply sum_leq. simpl. fold_langAlg label. intros n _ Hn. rewrite (@mx_star_charac _ M s n); auto. 2: num_lia. simpl. bool_simpl. StateSetProps.mem_analyse; simpl. 2: fold_langAlg label; auto with algebra. rewrite lang_Union_spec. intro m. revert s Hs. induction m; intros s Hs. simpl. nat_analyse. rewrite lang_leq. intros x ->. rewrite id_num in i. split; auto. intros a Ha. inversion Ha. fold_langAlg label; auto with algebra. simpl. fold_langAlg label. rewrite id_num. setoid_rewrite sum_distr_left. rewrite sum_inversion. setoid_rewrite dot_xifzero_left. apply sum_leq. intros a _ Ha. rewrite (sum_collapse (G:=@lang_Graph label) (n:=DFA.delta A a s)). simpl. rewrite id_num. bool_simpl. simpl. rewrite lang_leq. intros w [u -> [v Hv ->]]. simpl. setoid_rewrite lang_leq in IHm. split. eapply IHm; auto. apply (DFA.bounded_delta HA). intros b [<-|Hb]. num_simpl. assumption. eapply (IHm (DFA.delta A a s)); eauto. apply (DFA.bounded_delta HA). specialize (DFA.bounded_delta HA a s). num_lia. intros. simpl in H. num_analyse. elim H. rewrite <- e. num_lia. reflexivity. rewrite lang_leq. cut (forall w: Word, StateSet.In (read A w s) (DFA.finaux A) -> (forall a, In a w -> a < DFA.max_label A) -> exists2 j, StateSet.In j (DFA.finaux A) & !((M:LMX _ _) #) s (nat_of_state j) w). intro C. intros w [Hw Hw']. destruct (C _ Hw Hw') as [j Hj Hj']. rewrite lang_sum. exists (nat_of_state j). apply HA in Hj. num_lia. simpl. bool_simpl. rewrite (StateSet.mem_1 Hj). assumption. intro w. revert s Hs. induction w; simpl; intros s Hs Hw Hw'. assert (Hs': (s < DFA.size A)%nat). num_lia. exists s; auto. rewrite (@mx_star_charac _ M s s Hs' Hs' nil). exists O. simpl. bool_simpl. reflexivity. apply IHw in Hw; try apply (DFA.bounded_delta HA). clear IHw. destruct Hw as [j Hj' Hj]. exists j; auto. rewrite (fun Hs Hj => @mx_star_charac _ M s (nat_of_state j) Hs Hj (a::w)). 2: num_lia. 2: apply HA in Hj'; num_lia. rewrite (fun Hs Hj => @mx_star_charac _ M (DFA.delta A a s) (nat_of_state j) Hs Hj w) in Hj. 2: specialize (DFA.bounded_delta HA a s); num_lia. 2: apply HA in Hj'; num_lia. destruct Hj as [n Hn]. exists (Datatypes.S n). simpl. fold_langAlg label. rewrite lang_sum. exists (DFA.delta A a s). specialize (DFA.bounded_delta HA a s). num_lia. simpl Peano.plus. exists (a::nil). rewrite 2id_num. rewrite lang_sum. simpl. exists a. specialize (Hw' a). num_simpl. auto. bool_simpl. reflexivity. exists w; auto. intros b Hb. auto. Qed.
imports: Coq(List) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(Functors) ATBR(MxFunctors) ATBR(DKA_Definitions) ATBR(Model_Languages)