$(*$

$$ #####################################################

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

From Turing Require Import Regex.

Import Lang.Examples.

Import LangNotations.

Import ListNotations.

Import RegexNotations.

Open Scope lang$\_$scope.

Open Scope char$\_$scope.

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

$(**$

Show that 'aba' is accepted the the following regular expression.

$*)$

Theorem ex$1$:

$["$a$"$; $"$b$"$; $"$a$"]\backslash$in $($r$\_$star $"$a$"$ ;; $("$b$"||"$c$")$ ;; r$\_$star $"$a$").$

Proof.

Admitted.

$(**$

Show that $\text{'}$bb$\text{'}$ is rejected by the following regular expression.

$*)$

Theorem ex$2$:

$$ ~ $(["$b$"$; $"$b$"]\backslash$in $($r$\_$star $"$a$"$ ;; $("$b$"||"$c$")$ ;; r$\_$star $"$a$")).$

Proof.

Admitted.

$(**$

Function size counts how many operators were used in a regular

expression. Show that $($c ;; $\{\})*$ can be written using a single

regular expression constructor.

$*)$

Theorem ex$3$:

$$ exists r$,$ size r $=1/\backslash ($r$\_$star $("$c$"$ ;; r$\_$void $)<==>$ r$).$

Proof.

Admitted.

$(**$

Given that the following regular expression uses $530$ constructors

$($because size r$\_$all $=514).$

Show that you can find an equivalent regular expression that uses

at most $6$ constructors.

$*)$

Theorem ex$4$:

$$ exists r$,$ size r $<=6/\backslash (($r$\_$star $(($r$\_$all $||$ r$\_$star $"$c$")$ ;; r$\_$void$)$ ;; r$\_$star $("$a$"||"$b$"))$ ;; r$\_$star r$\_$nil;; $"$c$"<==>$ r$).$

Proof.

Admitted.

$(**$

The following code implements a function that given a string

it returns a regular expression that only accepts that string.

$$ Fixpoint r$\_$word' l :$=$

$$ match l with

$|$ nil $=>$ r$\_$nil

$|$ x :: l $=>($r$\_$char x$)$ ;; r$\_$word' l

$$ end.

Prove that function $`$r$\_$word'$`$ is correct.

Note that you must copy$/$paste the function to outside of the comment

and in your proof state: exists r$\_$word'.

The proof must proceed by induction.

$*)$

Theorem ex$5$:

$$ forall l$,$ exists $($r$\_$word:list ascii $->$ regex$),$ Accept $($r$\_$word l$)==$ fun w $=>$ w $=$ l$.$

Proof.

Admitted.

$(**$

Show that there exists a regular expression with $5$ constructs that

recognizes the following language. The idea is to find the smallest

regular expression that recognizes the language.

$*)$

Theorem ex$6$:

$$ exists r$,($Accept r $==$ fun w $=>$ w $=["$a$"$; $"$c$"]\backslash /$ w $=["$b$"$; $"$c$"])/\backslash$ size r $=5.$

Proof.

Admitted.