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] A Simple Grammar

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

``S -> | aSb``

It is easy to see that this grammar produces exactly the language L of all words of the form anbn for n ≥ 0. Prove this property, i.e. L = G!

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"
| a_b: "w ∈ G ⟹ a # w @ ''b'' ∈ G"

definition
"L = {w. ∃n. w = replicate n a @ replicate n b}"

end```

### Template File

```theory Submission
imports Defs
begin

theorem L_eq_G:
"L = G"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem L_eq_G:
"L = G"
by (rule Submission.L_eq_G)

end```

### Definitions File

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

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

def L : set (list char) :=
{w | ∃ (n : ℕ), w = list.repeat 'a' n ++ list.repeat 'b' n}

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

### Template File

```import .defs

lemma problem (l : list char) : G l ↔ L l :=
sorry```

### Check File

```import .defs
import .submission

lemma goal : GOAL :=
begin
assume l,
exact problem l
end```

### Definitions File

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

Inductive letter := a | b.

Inductive G : list letter -> Prop :=
| G_empty : G []
| G_ab : forall g, G g -> G (a :: g ++ [b]).

Definition L : list letter -> Prop :=
fun w => exists n, w = repeat a n ++ repeat b n.```

### Template File

```Require Import Defs.

Lemma L_eq_G (l: list letter) : L l <-> G l.

### 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"
| a_b: "w ∈ G ⟹ a # w @ ''b'' ∈ G"

definition
"L = {w. ∃n. w = replicate n a @ replicate n b}"

end```

### Template File

```theory Submission
imports Defs
begin

theorem L_eq_G:
"L = G"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem L_eq_G:
"L = G"
by (rule Submission.L_eq_G)

end```

### Definitions File

```-- Lean version: 3.16.2
-- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955
import tactic.basic

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

def L : set (list char) :=
{w | ∃ (n : ℕ), w = list.repeat 'a' n ++ list.repeat 'b' n}

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

### Template File

```import .defs

lemma problem (l : list char) : G l ↔ L l :=
sorry```

### Check File

```import .defs
import .submission

lemma goal : GOAL :=
problem```

Terms and Conditions