Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Balanced Words Grammar

You are given the following context-free grammar that produces a language G:

``S -> | SS | aSb | bSa``

It is easy to see that this grammar produces exactly the language L of all balanced words over a, b, i.e. that contain the same number of a's and b's. Can you prove this property, i.e. L = G?

We split the problem in two tasks:

1. Show G ⊆ L.
2. Show L ⊆ G.

Here is an informal proof sketch for task (2): Assume w ∈ L. We define h(u)=|u|b − |u|a, i.e. h(u)=0 ↔ u ∈ L. We show w ∈ G by (complete) induction on the length of w. For the induction step, we consider five cases: w = ϵ, w = bua, w = aub, w = aua, w = bub. The first three are simple. Thus assume w = aua (w = bub is symmetric). We have h(w)=0 and can deduce that there are x and y s.t. u = xy and h(x)=1 and h(y)=1, by analyzing the values of h for prefixes of w (*). We can thus apply the IH to get ax ∈ G and ya ∈ G, and derive w ∈ G.

(*) We propose the following lemma to help you here: Assume h(u)=k, k > 1, and u ∈ {a, b}*. Then there are x and y such that u = xy, h(x)=k − 1, and h(y)=1.

Thanks to Simon Wimmer for stating the problem. Thanks to Armaël Guéneau, Maximilian P. L. Haslbeck and Kevin Kappelmann for translating.

## Resources

### Definitions File

```theory Defs
imports Main
begin

text ‹‹#w⇘c⇙› denotes the number of times the character ‹c› occurs in word ‹w››
abbreviation count :: "'a list ⇒ 'a ⇒ nat" ("#_⇘_⇙") where
"count xs x ≡ count_list xs x"

abbreviation
"a ≡ CHR ''a''"

abbreviation
"b ≡ CHR ''b''"

lemma count_append[simp]:
"count (u @ v) c = count u c + count v c"
by (induction u) auto

inductive_set G :: "string set" where
empty: "[] ∈ G"
| append: "u@v ∈ G" if "u ∈ G" "v ∈ G"
| a_b: "a#u@[b] ∈ G" if "u ∈ G"
| b_a: "b#u@[a] ∈ G" if "u ∈ G"

definition
"L = {w. #w⇘a⇙ = #w⇘b⇙ ∧ set w ⊆ {a, b}}"

end
```

### Template File

```theory Submission
imports Defs
begin

theorem G_L:
"G ⊆ L"
sorry

theorem L_G:
"L ⊆ G"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem G_L:
"G ⊆ L"
by (rule Submission.G_L)

theorem L_G:
"L ⊆ G"
by (rule Submission.L_G)

end
```

### Definitions File

```-- Lean version: 3.4.2
-- Mathlib version: 2019-09-11

import data.list

inductive G : (list char) → Prop
| empty : G []
| append (g1 g2 : list char) : G g1 → G g2 → G (g1 ++ g2)
| a_b (g : list char) : G g → G (['a'] ++ g ++ ['b'])
| b_a (g : list char) : G g → G (['b'] ++ g ++ ['a'])

def L : set (list char) :=
{ w |  w ⊆ ['a', 'b'] ∧ w.count 'a' = w.count 'b' }

notation `GOAL` := ∀ (l:list char) , G l ↔ L l```

### Template File

```import .defs
import tactic.find
import tactic.ring

-- 1/10 points
theorem G_L (w : list char): G w → L w :=
sorry

-- 9/10 points
theorem L_G (w : list char): L w → G w :=
sorry```

### Check File

```import .defs
import .submission

-- 1/10 points
theorem GOAL1 (w : list char): G w → L w :=
G_L w

-- 9/10 points
theorem GOAL2 (w : list char): L w → G w :=
L_G w```

### Definitions File

```Require Export List.
Require Export Arith ZArith Lia.
Export ListNotations.

Inductive letter := a | b.

Inductive G : list letter -> Prop :=
| G_emp : G []
| G_app : forall g1 g2, G g1 -> G g2 -> G (g1 ++ g2)
| G_ab : forall g, G g -> G (a :: g ++ [b])
| G_ba : forall g, G g -> G (b :: g ++ [a]).

Definition letter_dec (x y : letter) : { x = y } + { x <> y }.
Proof. destruct x; destruct y; firstorder. Qed.

(* [#{c} w] denotes the number of times the character [c] occurs in the word [w]. *)
Notation "'#' '{' c '}'" := (fun w => count_occ letter_dec w c) (at level 1).

Definition L : list letter -> Prop :=
fun w => #{a} w = #{b} w.```

### Template File

```Require Import Defs.

(* 1/10 points *)
Lemma G_L (w : list letter) : G w -> L w.

(* 9/10 points *)
Lemma L_G (w : list letter) : L w -> G w.

### Definitions File

```theory Defs
imports Main
begin

text ‹‹#w⇘c⇙› denotes the number of times the character ‹c› occurs in word ‹w››
abbreviation count :: "'a list ⇒ 'a ⇒ nat" ("#_⇘_⇙") where
"count xs x ≡ count_list xs x"

abbreviation
"a ≡ CHR ''a''"

abbreviation
"b ≡ CHR ''b''"

lemma count_append[simp]:
"count (u @ v) c = count u c + count v c"
by (induction u) auto

inductive_set G :: "string set" where
empty: "[] ∈ G"
| append: "u@v ∈ G" if "u ∈ G" "v ∈ G"
| a_b: "a#u@[b] ∈ G" if "u ∈ G"
| b_a: "b#u@[a] ∈ G" if "u ∈ G"

definition
"L = {w. #w⇘a⇙ = #w⇘b⇙ ∧ set w ⊆ {a, b}}"

end
```

### Template File

```theory Submission
imports Defs
begin

theorem G_L:
"G ⊆ L"
sorry

theorem L_G:
"L ⊆ G"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem G_L:
"G ⊆ L"
by (rule Submission.G_L)

theorem L_G:
"L ⊆ G"
by (rule Submission.L_G)

end
```

### Definitions File

```-- Lean version: 3.16.2
-- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955

import tactic.basic
import data.list

inductive G : (list char) → Prop
| empty : G []
| append (g1 g2 : list char) : G g1 → G g2 → G (g1 ++ g2)
| a_b (g : list char) : G g → G (['a'] ++ g ++ ['b'])
| b_a (g : list char) : G g → G (['b'] ++ g ++ ['a'])

def L : set (list char) :=
{ w |  w ⊆ ['a', 'b'] ∧ w.count 'a' = w.count 'b' }

notation `GOAL1` := ∀ (l:list char) , G l → L l
notation `GOAL2` := ∀ (l:list char) , L l → G l```

### Template File

```import .defs
import tactic.find
import tactic.ring

-- 1/10 points
theorem G_L (w : list char): G w → L w :=
sorry

-- 9/10 points
theorem L_G (w : list char): L w → G w :=
sorry```

### Check File

```import .defs
import .submission

-- 1/10 points
theorem goal1 : GOAL1 :=
G_L

-- 9/10 points
theorem goal2 : GOAL2 :=
L_G```

### Definitions File

```theory Defs
imports Main
begin

text ‹‹#w⇘c⇙› denotes the number of times the character ‹c› occurs in word ‹w››
abbreviation count :: "'a list ⇒ 'a ⇒ nat" ("#_⇘_⇙") where
"count xs x ≡ count_list xs x"

abbreviation
"a ≡ CHR ''a''"

abbreviation
"b ≡ CHR ''b''"

lemma count_append[simp]:
"count (u @ v) c = count u c + count v c"
by (induction u) auto

inductive_set G :: "string set" where
empty: "[] ∈ G"
| append: "u@v ∈ G" if "u ∈ G" "v ∈ G"
| a_b: "a#u@[b] ∈ G" if "u ∈ G"
| b_a: "b#u@[a] ∈ G" if "u ∈ G"

definition
"L = {w. #w⇘a⇙ = #w⇘b⇙ ∧ set w ⊆ {a, b}}"

end
```

### Template File

```theory Submission
imports Defs
begin

theorem G_L:
"G ⊆ L"
sorry

theorem L_G:
"L ⊆ G"
sorry

end
```

### Check File

```theory Check
imports Submission
begin