Cookies disclaimer

I agree 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.

[Proof Ground 2019] 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

Download Files

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

text ‹Task definitions›
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

text ‹Task 1 (1/10 points)›
theorem G_L:
  "G ⊆ L"
  sorry

text ‹Task 2  (9/10 points)›
theorem L_G:
  "L ⊆ G"
  sorry

end

Check File 

theory Check
  imports Submission
begin

text ‹Task 1›
theorem G_L:
  "G ⊆ L"
  by (rule Submission.G_L)

text ‹Task 2›
theorem L_G:
  "L ⊆ G"
  by (rule Submission.L_G)

end
Download Files

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
Download Files

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.
Admitted.


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

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

text ‹Task definitions›
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

text ‹Task 1 (1/10 points)›
theorem G_L:
  "G ⊆ L"
  sorry

text ‹Task 2  (9/10 points)›
theorem L_G:
  "L ⊆ G"
  sorry

end

Check File 

theory Check
  imports Submission
begin

text ‹Task 1›
theorem G_L:
  "G ⊆ L"
  by (rule Submission.G_L)

text ‹Task 2›
theorem L_G:
  "L ⊆ G"
  by (rule Submission.L_G)

end
Download Files

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
Download Files

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

text ‹Task definitions›
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

text ‹Task 1 (1/10 points)›
theorem G_L:
  "G ⊆ L"
  sorry

text ‹Task 2  (9/10 points)›
theorem L_G:
  "L ⊆ G"
  sorry

end

Check File 

theory Check
  imports Submission
begin

text ‹Task 1›
theorem G_L:
  "G ⊆ L"
  by (rule Submission.G_L)

text ‹Task 2›
theorem L_G:
  "L ⊆ G"
  by (rule Submission.L_G)

end
Terms and Conditions