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 -> | aSb`

It is easy to see that this grammar produces exactly the language *L* of all words of the form *a*^{n}*b*^{n} 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

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" | a_b: "w ∈ G ⟹ a # w @ ''b'' ∈ G" definition "L = {w. ∃n. w = replicate n a @ replicate n b}" end

theory Submission imports Defs begin text ‹Your task› theorem L_eq_G: "L = G" sorry end

theory Check imports Submission begin theorem L_eq_G: "L = G" by (rule Submission.L_eq_G) end

Download Files
### Definitions File

### Template File

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

import .defs lemma problem (l : list char) : G l ↔ L l := sorry

import .defs import .submission lemma goal : GOAL := begin assume l, exact problem l end

Download Files
### Definitions File

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

Require Import Defs. Lemma L_eq_G (l: list letter) : L l <-> G l. Admitted.

Terms and Conditions