proposition: Lemma l4_not_regular_v2: ~ Regular Turing.Lang.Examples.L4.
proof: Proof. apply not_regular_ex. intros p Hge. exists (pow1 "a" p ++ pow1 "b" p) . repeat split. - unfold Examples.L4, In. exists p. apply app_in_eq. + apply pow_char_in. + apply pow_char_in. - Search (length (_ ++ _)). rewrite app_length. Search (length (pow1 _ _)). rewrite pow1_length. lia. - intros x y z Ha Hneq Hlen. exists 2. intros N. destruct N as (n, N). simpl in N. Search (_ ++ []). rewrite app_nil_r in N. apply xyz_rw_ex in Ha; auto. destruct Ha as (b, (Hz, (_,(Hb,(Hc,Hd))))). rewrite Hz in Hd; clear Hz. rewrite Hb in N; clear Hb. rewrite Hc in N; clear Hc. rewrite Hd in N; clear Hd. repeat rewrite app_assoc in *. repeat rewrite pow1_plus in N. assert ("a" <> "b") by (intros M; inversion M). Search (In _ (_ >> _)). apply pow_pow_in_inv in N. apply pow1_a_b_inv_eq in N; auto. destruct N as (L, R). subst. rewrite app_length in *. repeat rewrite <- Nat.add_assoc in *. apply plus_inv_eq_r in R. apply plus_inv_eq_r in R. assert (X: length y = 0). { lia. } destruct y. { contradiction. } inversion X. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util