proposition: Lemma eval_deriv a e: elang (deriv a e) ≡ lang_deriv a (elang e).
proof: Proof. induction e; simpl deriv; simpl eval; fold_regex; fold_lang. - reflexivity. - now rewrite lang_deriv_1. - rewrite lang_deriv_pls. now apply cup_weq. - generalize (epsilon_iff_lang_nil e1). case epsilon; intro He1. setoid_rewrite dot1x. setoid_rewrite lang_deriv_dot_1. 2: now apply He1. now rewrite <- IHe1, <- IHe2. setoid_rewrite dot0x. setoid_rewrite lang_deriv_dot_2. 2: clear -He1; intuition discriminate. rewrite <- IHe1. apply cupxb. - rewrite lang_deriv_str. now rewrite <- IHe. - case eqb_spec. intros <- w. compute. split. now intros <-. now intro E; injection E. intros D w. compute. split. intros []. intro E. apply D. injection E. congruence. Qed.
imports: syntax kleene boolean lang lset sums normalisation