proposition: Theorem expand' (e: regex') A: vars e ≦ A -> e ≡ eps e + \sum_(a\in A) var a ⋅ deriv a e.
proof: Proof. induction e; simpl vars; intro HA; simpl deriv; fold_regex. + rewrite sup_b, cupxb; ra. + rewrite sup_b, cupxb; ra. + apply cup_spec in HA as [HA1 HA2]. simpl epsilon. setoid_rewrite orb_pls. setoid_rewrite dotxpls. rewrite supcup. rewrite IHe1 at 1 by assumption. rewrite IHe2 at 1 by assumption. simpl. fold_regex. ra. + apply cup_spec in HA as [HA1 HA2]. setoid_rewrite dotxpls. rewrite supcup. rewrite IHe1 at 1 by assumption. rewrite dotplsx. rewrite IHe2 at 1 by assumption. rewrite dotxpls. rewrite dotxsum, dotsumx. simpl epsilon. rewrite andb_dot. setoid_rewrite dot_ofboolx. setoid_rewrite dotA. ra. + specialize (IHe HA). clear HA. simpl epsilon. setoid_rewrite dotA. rewrite <-dotsumx. set (f := \sum_(i\in A) var i ⋅ deriv i e) in *. clearbody f. rewrite IHe. case epsilon; ra_normalise; rewrite ?str_pls1x; apply str_unfold_l. + setoid_rewrite cupbx. apply antisym. rewrite <- (leq_xsup _ _ a) by (apply HA; now left). rewrite eqb_refl. ra. apply leq_supx. intros b _. case eqb_spec; try intros <-; ra. Qed.
imports: syntax kleene boolean lang lset sums normalisation