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] 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

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"
| 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

text ‹Your task›
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
Download Files

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

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

text ‹Your task›
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
Download Files

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
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"
| 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

text ‹Your task›
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
Terms and Conditions