I was able to do ex$2,$ ex$3,$ ex$4,$ ex$5.$ please do the rest.

$(*$

#####################################################

### PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY ###

#####################################################

$*)$

Set Default Goal Selector $"!".$

Require Import Coq.Strings.Ascii.

Require Import Coq.Lists.List.

From Turing Require Import Lang.

From Turing Require Import Util.

Import LangNotations.

Import ListNotations.

Import Lang.Examples.

Open Scope lang$\_$scope.

Open Scope char$\_$scope.

$(*---------------------------------------------------------------------------*)$

$(**$

Show that any word that is in L$4$ is either empty or starts with $"$a$".$

$*)$

Theorem ex$1$:

forall w$,$ L$4$ w $->$ w $=[]\backslash /$ exists w$\text{'},$ w $="$a$"$ :: w$\text{'}.$

Proof.

Admitted.

$(**$

Show that the following word is accepted by the given language.

$*)$

Lemma b$\_$in$\_$b:

Char $"$b$"["$b$"].$

Proof.

unfold Char.

reflexivity.

Qed.

Lemma in$\_$bb:

In $["$b$"$; $"$b$"]($Pow $($Char $"$b$")2).$

Proof.

unfold In$.$

$(*\{$ a $\}*)$

apply pow$\_$cons with $($w$1$:$=["$b$"])($w$2$:$=["$b$"]).$

$-$ apply pow$\_$cons with $($w$1$:$=["$b$"])($w$2$:$=[]).$

$*$ apply pow$\_$nil.

$*$ apply b$\_$in$\_$b$.$

$*$ reflexivity.

$-$ apply b$\_$in$\_$b$.$

$-$ reflexivity.

Qed.

Theorem ex$2$: In $["$a$"$; $"$b$"$; $"$b$"$; $"$a$"]("$a$">>"$b$"*>>"$a$").$

Proof.

unfold Star.

unfold In$.$

unfold App.

exists $["$a$"$; $"$b$"$; $"$b$"],["$a$"].$

split.

$-$ simpl. reflexivity.

$-$ split.

$--$ exists $["$a$"],["$b$"$;$"$b$"].$ split.

$\{$ reflexivity. $\}$

$\{$ split. $-$ reflexivity. $-$ exists $2.$ apply in$\_$bb$.\}$

$--$ reflexivity.

Qed.

$(**$

Show that the following word is rejected by the given language.

$*)$

Theorem ex$3$: ~ In $["$b$"$; $"$b$"]("$a$">>"$b$"*>>"$a$").$

Proof.

unfold not.

intros.

unfold In$,$ App in H$.$

destruct H as $($w$1,($w$2,$ H$)).$

destruct H as $($Ha$,($Hb$,$ Hc$)).$

destruct Hb as $($Hd$,($He$,$ Hf$)).$

destruct Hf$.$

destruct H$0.$

unfold Char in H$0.$

subst.

inversion Ha$.$

Qed.

$(**$

Show that the following language is empty.

$*)$

Theorem ex$4$: $"0"*>>\{\}==\{\}.$

Proof.

apply app$\_$r$\_$void$\_$rw$.$

Qed.

$(**$

Rearrange the following terms. Hint use the distribution and absorption laws.

$*)$

Theorem ex$5$: $("0"$ U Nil$)>>("1"*)==("0">>"1"*)$ U $("1"*).$

Proof.

Admitted.

$(**$

Show that the following langue only accepts two words.

$*)$

Theorem ex$6$: $("0">>"1"$ U $"1">>"0")==$ fun w $=>($w $=["0"$; $"1"]\backslash /$ w $=["1"$; $"0"]).$

Proof.

Admitted.

Theorem ex$7$: $"$b$">>("$a$"$ U $"$b$"$ U Nil$)*>>$ Nil $=="$b$">>("$b$"$ U $"$a$")*.$

Proof.

Admitted.

Theorem ex$8$: $(("$b$">>("$a$"$ U $\{\}))$ U $($Nil $>>\{\}>>"$c$")*)*==("$b$">>"$a$")*.$

Proof.

Admitted.