This file covers exercises 1 and 2 from exercise sheet 1 (which can be found at https://iccl.inf.tu-dresden.de/w/images/a/a1/FS2025-Blatt-01.pdf). The goal of these exercises is to show some general theorems about formal languages as well as some theorems about particular languages. Definitions and results used in the proofs can be found in lecture1.

The following three theorems show the monotonicity of union, concatenation and kleene star for languages.

theorem a {Sigma : Type u} [DecidableEq Sigma] {L1 L2 L3 L4 : Language Sigma} : L1 ⊆ L3 → L2 ⊆ L4 → L1 ∪ L2 ⊆ L3 ∪ L4

theorem b {Sigma : Type u} [DecidableEq Sigma] {L1 L2 L3 L4 : Language Sigma} : L1 ⊆ L3 → L2 ⊆ L4 → L1 * L2 ⊆ L3 * L4

theorem c {Sigma : Type u} [DecidableEq Sigma] {L1 L3 : Language Sigma} : L1 ⊆ L3 → L1* ⊆ L3*

theorem ex_2_a1 {Sigma : Type u} [DecidableEq Sigma] {L1 L2 L3 : Language Sigma} : L1 * (L2 ∪ L3) = L1 * L2 ∪ L1 * L3

Concatenation of languages is distributive over union.

def L1 : Language Char

Equations

• L1 w = (w = ['a'] ∨ w = ['a', 'b'])

def L2 : Language Char

Equations

• L2 w = (w = ['c'])

def L3 : Language Char

Equations

• L3 w = (w = ['b', 'c'])

theorem ex_2_a2 : L1 * (L2 ∩ L3) ≠ L1 * L2 ∩ (L1 * L3)

Concatenation of languages is not distributive over intersection. We show this by giving a counterexample.

theorem kstar_incl_left {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L* * L ⊆ L*

theorem kstar_incl_right {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L * L* ⊆ L*

In exercise sessions the solution given for 1.2b is usually somewhat informal. We just argue that every word from the languages on the left hand side and the right hand side starts and ends with an a and in between there can be arbitrary chains of a but never two bs in a row.

def L5 : Language Char

Equations

• L5 w = (w = ['a', 'b'] ∨ w = ['a'])

def L8 : Language Char

Equations

• L8 w = (w = ['b', 'a'] ∨ w = ['a'])

def L6 : Language Char

Equations

• L6 w = (w = ['a'])

def L4 : Language Char

Equations

• L4 w = (w ∈ L6 * L8*)

def L7 : Language Char

Equations

• L7 w = (w ∈ L5* * L6)

theorem aux2 : L5 * L6 = L6 * L8

Auxiliary result for exercise 1.2b

theorem ex_2_b : L4 = L7

def L_ab : Language Char

Equations

• L_ab w = (w = ['a'] ∨ w = ['b'])

def L_a : Language Char

Equations

• L_a w = (w = ['a'])

def L_b : Language Char

Equations

• L_b w = (w = ['b'])

theorem ex_2c : L_ab* ≠ L_a* ∪ L_b*

theorem ex_2f_2 {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L* * L* = L*

Concatenating L* with itself results in L*.

In section d of the exercise we show some properties of the kleene star operator:

• ∅* = {ε}
• ({ε} ∪ L)* = L*
• (L*)* = L*

theorem ex_2d_1 {Sigma : Type u} [DecidableEq Sigma] : L_empty* = L_eps

theorem ex_2d_2 {Sigma : Type u} [DecidableEq Sigma] {L : Language Sigma} : (L_eps ∪ L)* = L*

theorem ex_2d_3 {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L** = L*

in the exercise solution the inclusion (L₁* ∪ L₂*)* ⊆ (L₁ ∪ L₂)* is shown by arguing that every Word w from (L₁* ∪ L₂*)* can be seen as a concatenation of words w₁...wₙ where each wᵢ is from (L₁* ∪ L₂*). Then each wᵢ can again be expressed as a sequence of words x₁...xₙ where either each xᵢ is from L₁ or each xᵢ is from L₂. But then the original word w is a sequence of words from L₁ and L₂, so w ∈ (L₁ ∪ L₂). In Lean it is not quite as easy to switch between words and lists of words. A list of words cannot be equal to a word because the type does not match. In lecture1 we have already shown that for a language L every word from L is equal to a flattened list of words from L. The auxiliary result at the beginning of the proof for 2e does something similar, but here we need to flatten the list twice because the language contains two stars.

theorem ex_2e {Sigma : Type u} [DecidableEq Sigma] (L₁ L₂ : Language Sigma) : (L₁* ∪ L₂*)* = (L₁ ∪ L₂)*

theorem ex_2f_1 {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L * L* = L⁺

theorem ex_2f_3 {Sigma : Type u} [DecidableEq Sigma] (L : Language Sigma) : L* ∪ L = L*