On the three-letter alphabet `{M;I;U}`, we consider the language `L` defined from the following axiom and rules:

- Axiom: `MI ∈ L`

- Rule 1: If `xI ∈ L`, then `xIU ∈ L` (where `x ∈ {M;I;U}*`)

- Rule 2: If `Mx ∈ L`, then `Mxx ∈ L` (where `x ∈ {M;I;U}*`)

- Rule 3: If `xIIIy ∈ L`, then `xUy ∈ L` (where `x,y ∈ {M;I;U}*`)

- Rule 4: If `xUUy ∈ L`, then `xy ∈ L` (where `x,y ∈ {M;I;U}*`)

The question is whether the word `MU` belongs to the language `L` or not.

## Coq formalization ##

To formalize this puzzle in Coq, we introduce the following definitions:

```coq

RequireImportList.

ImportListNotations.

Inductivealpha:=M|I|U.

Definitionword:=listalpha.

Inductivelang:word->Prop:=

|axiom:lang[M;I]

|rule1x:lang(x++[I])->lang(x++[I;U])

|rule2x:lang([M]++x)->lang([M]++x++x)

|rule3xy:lang(x++[I;I;I]++y)->lang(x++[U]++y)

|rule4xy:lang(x++[U;U]++y)->lang(x++y).

```

A word on the `{M;U;I}` alphabet is hence represented in Coq by a list of letters. For instance, the word `MI` corresponds to the list `[M;I]`, this syntaxe being a syntactic shortcut for `M::I::nil`, itself being `cons M (cons I nil)` internally. And the concatenation of words is hence the concatenation on lists `++` (named `app` in Coq). For more explanations on Coq lists, see for instance TD3. Then, membership to language `L` is modeled in Coq via the predicate `lang : word->Prop`.

1. As a warm-up, show in Coq that all words in language `L` start with letter `M`. Be careful, there are (at least) two possible formulations for this statement (by using `exists` or by using `match`). Prove the easiest one directly, then the other one by equivalence.

## Ternary arithmetic ##

We will now show that all the words of this language have a number of occurrences of the letter `I` that cannot be a multiple of 3. For that, we formalize first a little bit of ternary arithmetic (i.e. counting modulo 3, i.e. Z/3Z). We start with the following definition:

```coq

InductiveZ3:=Z0|Z1|Z2.

```

1. Define first the functions `succ:Z3->Z3` and `add:Z3->Z3->Z3` which implement the successor and addition modulo 3. Add then a notation for `add` via `Infix "+" := add`.

2. Show that `add` is commutative and associative and that `Z0` is neutral for `add`.

3. Show that for all `z:Z3`, we have `z<>Z0 -> z+z <> Z0`.

4. Define a function `occurI3 : word -> Z3` that for any word `w:word` computes the number of occurrences of the letter `I` modulo 3 in `w`.

5. Show that for all words `v` and `w` we have `occurI3 (v ++ w) = (occurI3 v)+(occurI3 w)`.

6. Show that for all word `w` in the language `L`, we have `occurI3 w <> Z0`.