hw$3.$v

I need the code help please not the explanation to the questions$-(*$

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

### 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.

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

$(*$ I worked with my teammate $(*$ Brandon Siscoe $*)*)$

$(**$

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.

intros.

unfold L$4$ in H$.$

destruct H$.$

apply app$\_$in$\_$inv in H$.$

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

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

subst.

destruct x$.$

$-$ inversion H$2.$

inversion H$3.$

simpl.

left.

reflexivity.

$-$ inversion H$2$; subst; clear H$2.$

inversion H$3$; subst; clear H$3.$

inversion H$1$; subst; clear H$1.$

right.

simpl.

exists $($w$3++$w$1++$w$4).$

reflexivity.

Qed.

$(**$

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

$*)$

Theorem ex$2$:

In $["$a$"$; $"$b$"$; $"$b$"$; $"$a$"]("$a$">>"$b$"*>>"$a$").$

Proof.

apply concat$\_$intro with $($w$1$ :$=["$a$"])($w$2$ :$=["$b$"$; $"$b$"$; $"$a$"]).$

split.

$-$ simpl. left. reflexivity. $(*$ Matches the first $"$a$"*)$

$-$ split.

$+$ apply in$\_$star$\_$app.

$*$ apply repeat$\_$intro. constructor. $(*$ Matches the $"$b$"*$ part containing two $"$b$"$s $*)$

$+$ simpl. right. reflexivity. $(*$ Matches the final $"$a$"*)$

Qed.

$(**$

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

$*)$

Theorem ex$3$:

~ In $["$b$"$; $"$b$"]("$a$">>"$b$"*>>"$a$").$

Proof.

Admitted.

$(**$

Show that the following language is empty.

$*)$

Theorem ex$4$:

$"0"*>>\{\}==\{\}.$

Proof.

Admitted.

$(**$

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.