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.

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:

- Show
*G*⊆*L*. - 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* = *b**u**a*, *w* = *a**u**b*, *w* = *a**u**a*, *w* = *b**u**b*. The first three are simple. Thus assume *w* = *a**u**a* (*w* = *b**u**b* is symmetric). We have *h*(*w*)=0 and can deduce that there are *x* and *y* s.t. *u* = *x**y* 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 *a**x* ∈ *G* and *y**a* ∈ *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* = *x**y*, *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.

Download Files
### Definitions File

### Template File

### Check 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

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

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

### Template File

### Check 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

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

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

### Template 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.

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.

Terms and Conditions