proposition: Lemma Rev_correct (char : finType) (e : regexp char) w : w \in Rev e = (rev w \in e).
proof: Proof. elim: e w => [||a|e IH|e1 IH1 e2 IH2|e1 IH1 e2 IH2] w //. - rewrite !inE. apply/eqP/idP; first by move->. elim/last_ind: w => //= s a _. by rewrite rev_rcons. - rewrite !inE. apply/eqP/eqP; first by move->. do 2 elim/last_ind: w => //= w ? _. by rewrite !rev_rcons. - rewrite /=; apply/idP/idP; case/starP => vv /allP /= H. + move->. rewrite rev_flatten. apply: starI => v'. rewrite mem_rev => /mapP [v V1 ->]. rewrite -IH. by case/andP: (H _ V1). + rewrite -{2}[w]revK => ->. rewrite rev_flatten. apply: starI => v'. rewrite mem_rev => /mapP [v V1 ->]. rewrite IH revK. by case/andP: (H _ V1). - by rewrite /= !inE -!/(re_lang _) IH1 IH2. - rewrite /=. apply/concP/concP => [] [w1] [w2]; rewrite -!/(re_lang _). + move => [-> [A B]]. exists (rev w2), (rev w1). by rewrite rev_cat -IH1 -IH2. + rewrite -{2}[w]revK. move => [-> [A B]]. exists (rev w2), (rev w1). by rewrite rev_cat IH1 IH2 !revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)