code please$-(*$

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

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

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

$*)$

Set Default Goal Selector $"!".$

Require Import Coq.Strings.Ascii.

Require Import Coq.Lists.List.

Import ListNotations.

Open Scope char$\_$scope.

Require Import Hw$5$Util.

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

$(**$

Use $`$yield$\_$def$`.$

$*)$

Theorem yield$\_$eq:

forall G A w$,$ List.In $($A$,$ w$)($Hw$5$Util.grammar$\_$rules G$)->$ Hw$5$Util.Yield G $[$A$]$ w$.$

Proof.

Admitted.

$(**$

Use $`$yield$\_$def$`$ and $`$app$\_$assoc$`$ to correct the parenthesis.

$*)$

Theorem yield$\_$right:

forall G w$1$ w$2$ r w$3$ w$4,$ Hw$5$Util.Yield G w$1$ w$2->$ w$3=$ w$1++$ r $->$ w$4=$ w$2++$ r $->$ Hw$5$Util.Yield G w$3$ w$4.$

Proof.

Admitted.

$(**$

Similar proof than $`$yield$\_$right$`,$ but you should rewrite with

$`$app$\_$assoc$`$ after using $`$yield$\_$def$`,$ not before.

$*)$

Theorem yield$\_$left:

forall G w$1$ w$2$ l w$3$ w$4,$ Hw$5$Util.Yield G w$1$ w$2->$ w$3=$ l $++$ w$1->$ w$4=$ l $++$ w$2->$ Hw$5$Util.Yield G w$3$ w$4.$

Proof.

Admitted.

$(**$

Consider using one of the lemmas you have just proved.

When your goal is $`$In $("$C$",...)($grammar$\_$rules g$1)`,`$simpl; auto$`$

should solve it$.$

$*)$

Theorem g$1\_$rule$\_1$:

Hw$5$Util.Yield g$1["$C$"]["\{"$; $"$C$"$; $"\}"].$

Proof.

Admitted.

$(**$

Consider using one of the lemmas you have just proved.

When your goal is $`$In $("$C$",...)($grammar$\_$rules g$1)`,`$simpl; auto$`$

should solve it$.$

$*)$

Theorem g$1\_$rule$\_2$:

Hw$5$Util.Yield g$1["$C$"]["$C$"$; $"$C$"].$

Proof.

Admitted.

$(**$

Consider using one of the lemmas you have just proved.

When your goal is $`$In $("$C$",...)($grammar$\_$rules g$1)`,`$simpl; auto$`$

should solve it$.$

$*)$

Theorem g$1\_$rule$\_3$:

Hw$5$Util.Yield g$1["$C$"][].$

Proof.

Admitted.

$(**$

The proof should proceed by inversion and then case analysis on

string $`$u$`.$

$*)$

Theorem yield$\_$inv$\_$start:

forall G w$,$ Hw$5$Util.Yield G $[$Hw$5$Util.grammar$\_$start G$]$ w $->$ In $($Hw$5$Util.grammar$\_$start G$,$ w$)($Hw$5$Util.grammar$\_$rules G$).$

Proof.

Admitted.

$(**$

You will want to use $`$yield$\_$inv$\_$start$`.$ Recall that that $`$List$.$In$`$

simplifies to a series of disjunctions.

$*)$

Theorem g$1\_$ex$1$:

~ Hw$5$Util.Yield g$1["$C$"]["\{"].$

Proof.

Admitted.

$(**$

The idea is to use either: $`$yield$\_$left$`,`$yield$\_$right$`,$ or $`$yield$\_$def$`.$

$*)$

Theorem g$1\_$step$\_1$:

Hw$5$Util.Yield g$1["$C$"$; $"$C$"]["\{"$; $"$C$"$; $"\}"$; $"$C$"].$

Proof.

Admitted.

$(**$

The idea is to use either: $`$yield$\_$left$`,`$yield$\_$right$`,$ or $`$yield$\_$def$`.$

$*)$

Theorem g$1\_$step$\_2$:

Hw$5$Util.Yield g$1["\{"$; $"$C$"$; $"\}"$; $"$C$"]["\{"$; $"\}"$; $"$C$"].$

Proof.

Admitted.

$(**$

The idea is to use either: $`$yield$\_$left$`,`$yield$\_$right$`,$ or $`$yield$\_$def$`.$

$*)$

Theorem g$1\_$step$\_3$:

Hw$5$Util.Yield g$1["\{"$; $"\}"$; $"$C$"]["\{"$; $"\}"$; $"\{"$; $"$C$"$; $"\}"].$

Proof.

Admitted.

$(**$

The idea is to use either: $`$yield$\_$left$`,`$yield$\_$right$`,$ or $`$yield$\_$def$`.$

$*)$

Theorem g$1\_$step$\_4$:

Hw$5$Util.Yield g$1["\{"$; $"\}"$; $"\{"$; $"$C$"$; $"\}"]["\{"$; $"\}"$; $"\{"$; $"\}"].$

Proof.

Admitted.

$(**$

Use either $`$derivation$\_$nil$`$ or $`$derivation$\_$cons$`.$

$*)$

Theorem g$1\_$der$\_1$:

Hw$5$Util.Derivation g$1[["$C$"]].$

Proof.

Admitted.

$(**$

Use either $`$derivation$\_$nil$`$ or $`$derivation$\_$cons$`.$

$*)$

Theorem g$1\_$der$\_2$:

Hw$5$Util.Derivation g$1[["$C$"$; $"$C$"]$; $["$C$"]].$

Proof.

Admitted.

$(**$

Use either $`$derivation$\_$nil$`$ or $`$derivation$\_$cons$`.$

$*)$

Theorem g$1\_$der$\_3$:

Hw$5$Util.Derivation g$1[["\{"$; $"$C$"$; $"\}"$; $"$C$"]$; $["$C$"$; $"$C$"]$; $["$C$"]].$

Proof.

Admitted.

Theorem g$1\_$der$\_4$:

Hw$5$Util.Derivation g$1[$

$["\{"$; $"\}"$; $"$C$"]$;

$["\{"$; $"$C$"$; $"\}"$; $"$C$"]$;

$["$C$"$; $"$C$"]$;

$["$C$"]$

$].$

Proof.

Admitted.

Theorem g$1\_$der$\_5$:

Hw$5$Util.Derivation g$1[$

$["\{"$; $"\}"$; $"\{"$; $"$C