# Constructor Theorems on Languages

If you have a $*$goal$*$ that is a language membership,

eg$,`$In w $($L$1>>$ L$2)`,$ then you'll need to use a

constructor theorem, eg$,`$app$\_$in$`$

There is one constructor theorem per language:

$-`$char$\_$in$`$

$-`$nil$\_$in$`$

$-`$union$\_$in$\_$l$`$

$-`$union$\_$in$\_$r$`$

$-`$app$\_$in$`$

$**$Solve:$**[`$tutorial$1.$v$`]($tutorial$1.$v$)$

# Inversion Theorems on Languages

If you have an $*$assumption$*$ that is a language membership

in one of the assumptions, eg$,`$In w $($L$1>>$ L$2)`,$

then you'll need to use an inversion theorem, eg$,`$app$\_$in$\_$inv$`.$

There is one inversion theorem per language:

$-$ char$\_$in$\_$inv for $`"$a$"`$

$-$ app$\_$in$\_$inv for $`$L$1>>$ L$2`$

$-$ union$\_$in$\_$inv for $`$L$1$ U L$2`$

$-$ use $`$inversion H; subst; clear H$`$ for Pow

$-$ use star$\_$to$\_$pow for $`$L$1*`$

$**$Solve:$**[`$tutorial$2.$v$`]($tutorial$2.$v$)$

# Exercise $1$

$*$Objective:$*$ If w is in Language, then conclude

something about Language.

The technical point of this exercise is to remember

Inversion Theorems on Languages.

Any equivalence exercises where you show that a language

is equal to "fun w $=>..."$ is a more general case.

For a guiding example, look at l$1\_$spec, in one

of the directions you have that $"$w is in L$1"$

and you have to show that "exists w$\text{'},$ w $=$ w$\text{'}++["$a$"].$

## Recommended exercises

$-$ l$1\_$spec

$-$ l$4\_$spec

$-$ abb$\_$not$\_$in$\_$l$4$

# Exercise $2$

$*$Objective:$*$ Show that a word in in a language.

The language itself is composed of multiple language

combinators. The goal is to use Constructor Theorems.

## Recommended exercises

$-$ l$1\_$spec

$-$ l$4\_$spec

$-$ aabb$\_$in$\_$l$4$

# Exercise $3$

$*$Objective:$*$ If w is $**$not$**$ in Language, then

assume that w $**$is$*$ in the language, and then

reach a contradiction.

Similarly to exercise $1,$ you'll need Inversion

Theorems on Languages.

In terms of proof technique, you'll always try

to favor $($start by$)$ assumptions that lead to

an impossibility. You'll probably need to use

tactics such as inversion $($explosion principle$),$

intuition, and contradiction.

## Recommended exercises

$-$ car$\_$not$\_$in$\_$l$4$

$-$ abb$\_$not$\_$in$\_$l$4$

# Exercise $4$

$*$Objective:$*$ show language equivalence through

rewriting rules.

In this case, because both languages consist

of combinators, you'll want to use theorems

for rewriting equalities. These theorems end

with $"\_$rw$".$

$`$Search$`$ is your friend.

For instance, $`$Search $(\_==\{\})`$ searches

for any rewrite rule that ends with the void

language $`\{\}`.$

Do $**$not$**$ open Equiv and do not use $`$split$`.$

## Recommended exercises

$-`$Goal $(("$a$">>\{\})*$ U $"$a$")*=="$a$"*.`$

# Exercise $5$

Same as $4.$

# Exercise $6$

$**$Objective:$**$ language equivalence combines

showing that a word is in a language $($Exercise $2),$

and concluding something from knowing that a word is

in a language $($Exercise $1).$

Open $**$Equiv$**.$ You will want to use the theorems

$`$app$\_$l$\_$char$\_$in$\_$inv$`$ and $`$app$\_$l$\_$char$\_$in$`$

Practice Exercises $1,2,$ and $3.$

# Exercise $7$

Same as $4.$

# Exercise $8$

Same as $4$