proposition: Theorem nfa_lang A i: dfa.lang A i ≡ lang ((to_nfa A)^M) ((to_nfa A)^v) (mx_fun (fun _ => i) 1).
proof: Proof. intro w. revert i. induction w; intro i; simpl. - rewrite epsilon_iff_reflexive_eps. rewrite (scal_mx_map (fun e => eps e)). change (mx_dot regex_ops regex_tt) with (@dot (mx_ops regex_ops regex_tt)). rewrite (mx_dot_kfun1 (X:=regex_ops)). unfold mx_map, mx_scal. rewrite <-epsilon_iff_reflexive_eps. case dfa.v; reflexivity. - rewrite IHw. clear IHw. change (mx_dot regex_ops regex_tt) with (@dot (mx_ops regex_ops regex_tt)). rewrite (mx_dot_kfun1 (X:=regex_ops)). unfold mx_fun, epsilon_mx, mx_map. setoid_rewrite mx_sup. setoid_rewrite deriv_sup. setoid_rewrite epsilon_sup. split. + intros [Ha H]. eapply lang_leq. 2: apply H. clear w H. intros _ j. rewrite <-(leq_xsup _ _ a Ha). case eqb_ord. 2: apply leq_bx. simpl. now rewrite eqb_refl. + intros H. split. case (List.in_dec (cmp_dec _) a (dfa.vars A)) as [Ha|Ha]. assumption. apply lang_empty in H. elim H. clear H. intros o j. apply sup_b. intros b Hb. case eqb_ord. 2: reflexivity. simpl. case eqb_spec; simpl. 2: reflexivity. intros <-. elim (Ha Hb). eapply lang_leq. 2: apply H. clear w H. intros _ j. apply leq_supx. intros b _. case eqb_spec. 2: intros; ra. intros ->. simpl. case eqb_spec; simpl. 2: intro; lattice. intros <-. now rewrite eqb_refl. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation