ContextFreeGrammar

📁 Source: Mathlib/Computability/ContextFreeGrammar.lean

Statistics

Metric	Count
Definitions `ContextFreeGrammar`, `Generates`, `NT`, `Produces`, `initial`, `language`, `reverse`, `rules`, `ContextFreeRule`, `Rewrites`, `input`, `output`, `reverse`, `IsContextFree`, `instDecidableEqContextFreeRule`, `decEq`, `instReprContextFreeRule`, `repr`	18
Theorems `append_left`, `append_right`, `eq_or_head`, `eq_or_tail`, `refl`, `reverse`, `trans`, `trans_produces`, `reverse`, `append_left`, `append_right`, `exists_nonterminal_input_mem`, `reverse`, `single`, `trans_derives`, `derives_iff_eq_or_head`, `derives_iff_eq_or_tail`, `derives_nonterminal`, `derives_reverse`, `derives_reverse_comm`, `generates_reverse`, `generates_reverse_comm`, `language_eq_zero_of_forall_input_ne_initial`, `language_reverse`, `mem_language_iff`, `produces_reverse`, `produces_reverse_comm`, `reverse_NT`, `reverse_bijective`, `reverse_initial`, `reverse_injective`, `reverse_involutive`, `reverse_reverse`, `reverse_rules`, `reverse_surjective`, `append_left`, `append_right`, `exists_parts`, `input_output`, `nonterminal_input_mem`, `reverse`, `ext`, `ext_iff`, `reverse_bijective`, `reverse_comp_reverse`, `reverse_injective`, `reverse_involutive`, `reverse_reverse`, `reverse_surjective`, `rewrites_iff`, `rewrites_of_exists_parts`, `rewrites_reverse`, `rewrites_reverse_comm`, `reverse`	54
Total	72

ContextFreeGrammar

Definitions

Name	Category	Theorems
`Generates` 📖	MathDef	3 math math: `generates_reverse_comm`, `generates_reverse`, `Generates.reverse`
`NT` 📖	CompOp	22 math math: `Derives.eq_or_tail`, `Derives.append_right`, `reverse_NT`, `Produces.append_left`, `produces_reverse_comm`, `Derives.reverse`, `reverse_rules`, `generates_reverse_comm`, `produces_reverse`, `Produces.exists_nonterminal_input_mem`, `mem_language_iff`, `Derives.append_left`, `Derives.eq_or_head`, `derives_reverse_comm`, `generates_reverse`, `Produces.append_right`, `derives_iff_eq_or_tail`, `Generates.reverse`, `derives_reverse`, `derives_iff_eq_or_head`, `derives_nonterminal`, `Produces.reverse`
`Produces` 📖	MathDef	9 math math: `Derives.eq_or_tail`, `Produces.append_left`, `produces_reverse_comm`, `produces_reverse`, `Derives.eq_or_head`, `Produces.append_right`, `derives_iff_eq_or_tail`, `derives_iff_eq_or_head`, `Produces.reverse`
`initial` 📖	CompOp	2 math math: `reverse_initial`, `mem_language_iff`
`language` 📖	CompOp	3 math math: `language_reverse`, `mem_language_iff`, `language_eq_zero_of_forall_input_ne_initial`
`reverse` 📖	CompOp	18 math math: `reverse_NT`, `reverse_initial`, `produces_reverse_comm`, `Derives.reverse`, `reverse_surjective`, `reverse_reverse`, `reverse_rules`, `generates_reverse_comm`, `language_reverse`, `produces_reverse`, `reverse_involutive`, `derives_reverse_comm`, `generates_reverse`, `Generates.reverse`, `derives_reverse`, `reverse_injective`, `reverse_bijective`, `Produces.reverse`
`rules` 📖	CompOp	2 math math: `reverse_rules`, `Produces.exists_nonterminal_input_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derives_iff_eq_or_head` 📖	mathematical	—	`Derives` `Symbol` `NT` `Produces`	—	`Relation.ReflTransGen.cases_head_iff`
`derives_iff_eq_or_tail` 📖	mathematical	—	`Derives` `Symbol` `NT` `Produces`	—	`Relation.ReflTransGen.cases_tail_iff`
`derives_nonterminal` 📖	mathematical	—	`Derives` `Symbol` `NT` `Symbol.nonterminal`	—	`derives_iff_eq_or_head` `Mathlib.Tactic.Push.not_and_eq` `Produces.exists_nonterminal_input_mem`
`derives_reverse` 📖	mathematical	—	`Derives` `reverse` `Symbol` `NT`	—	`reverse_reverse` `Derives.reverse`
`derives_reverse_comm` 📖	mathematical	—	`Derives` `reverse` `Symbol` `NT`	—	`derives_reverse`
`generates_reverse` 📖	mathematical	—	`Generates` `reverse` `Symbol` `NT`	—	—
`generates_reverse_comm` 📖	mathematical	—	`Generates` `reverse` `Symbol` `NT`	—	—
`language_eq_zero_of_forall_input_ne_initial` 📖	mathematical	—	`language` `Language` `Language.instZero`	—	`Language.ext`
`language_reverse` 📖	mathematical	—	`language` `reverse` `Language.reverse`	—	`Language.ext`
`mem_language_iff` 📖	mathematical	—	`Language` `Language.instMembershipList` `language` `Derives` `Symbol` `NT` `Symbol.nonterminal` `initial` `Symbol.terminal`	—	—
`produces_reverse` 📖	mathematical	—	`Produces` `reverse` `Symbol` `NT`	—	`Equiv.exists_congr` `ContextFreeRule.reverse_bijective` `Function.Involutive.eq_iff` `ContextFreeRule.reverse_involutive`
`produces_reverse_comm` 📖	mathematical	—	`Produces` `reverse` `Symbol` `NT`	—	`Equiv.exists_congr` `ContextFreeRule.reverse_bijective` `Function.Involutive.eq_iff` `ContextFreeRule.reverse_involutive`
`reverse_NT` 📖	mathematical	—	`NT` `reverse`	—	—
`reverse_bijective` 📖	mathematical	—	`Function.Bijective` `ContextFreeGrammar` `reverse`	—	`Function.Involutive.bijective` `reverse_involutive`
`reverse_initial` 📖	mathematical	—	`initial` `reverse`	—	—
`reverse_injective` 📖	mathematical	—	`ContextFreeGrammar` `reverse`	—	`Function.Bijective.injective` `reverse_bijective`
`reverse_involutive` 📖	mathematical	—	`Function.Involutive` `ContextFreeGrammar` `reverse`	—	`reverse_reverse`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	`Finset.map_map` `ContextFreeRule.reverse_comp_reverse` `Finset.map_refl`
`reverse_rules` 📖	mathematical	—	`rules` `reverse` `Finset.map` `ContextFreeRule` `NT` `ContextFreeRule.reverse`	—	—
`reverse_surjective` 📖	mathematical	—	`ContextFreeGrammar` `reverse`	—	`Function.Bijective.surjective` `reverse_bijective`

ContextFreeGrammar.Derives

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_left` 📖	mathematical	`ContextFreeGrammar.Derives`	`ContextFreeGrammar.Derives` `Symbol` `ContextFreeGrammar.NT`	—	`trans_produces` `ContextFreeGrammar.Produces.append_left`
`append_right` 📖	mathematical	`ContextFreeGrammar.Derives`	`ContextFreeGrammar.Derives` `Symbol` `ContextFreeGrammar.NT`	—	`trans_produces` `ContextFreeGrammar.Produces.append_right`
`eq_or_head` 📖	mathematical	`ContextFreeGrammar.Derives`	`Symbol` `ContextFreeGrammar.NT` `ContextFreeGrammar.Produces` `ContextFreeGrammar.Derives`	—	`Relation.ReflTransGen.cases_head`
`eq_or_tail` 📖	mathematical	`ContextFreeGrammar.Derives`	`Symbol` `ContextFreeGrammar.NT` `ContextFreeGrammar.Derives` `ContextFreeGrammar.Produces`	—	`Relation.ReflTransGen.cases_tail`
`refl` 📖	mathematical	—	`ContextFreeGrammar.Derives`	—	—
`reverse` 📖	mathematical	`ContextFreeGrammar.Derives`	`ContextFreeGrammar.Derives` `ContextFreeGrammar.reverse` `Symbol` `ContextFreeGrammar.NT`	—	`trans_produces` `ContextFreeGrammar.Produces.reverse`
`trans` 📖	mathematical	`ContextFreeGrammar.Derives`	`ContextFreeGrammar.Derives`	—	`Relation.ReflTransGen.trans`
`trans_produces` 📖	mathematical	`ContextFreeGrammar.Derives` `ContextFreeGrammar.Produces`	`ContextFreeGrammar.Derives`	—	`trans` `ContextFreeGrammar.Produces.single`

ContextFreeGrammar.Generates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reverse` 📖	mathematical	`ContextFreeGrammar.Generates`	`ContextFreeGrammar.Generates` `ContextFreeGrammar.reverse` `Symbol` `ContextFreeGrammar.NT`	—	`ContextFreeGrammar.generates_reverse`

ContextFreeGrammar.Produces

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_left` 📖	mathematical	`ContextFreeGrammar.Produces`	`ContextFreeGrammar.Produces` `Symbol` `ContextFreeGrammar.NT`	—	`ContextFreeRule.Rewrites.append_left`
`append_right` 📖	mathematical	`ContextFreeGrammar.Produces`	`ContextFreeGrammar.Produces` `Symbol` `ContextFreeGrammar.NT`	—	`ContextFreeRule.Rewrites.append_right`
`exists_nonterminal_input_mem` 📖	mathematical	`ContextFreeGrammar.Produces`	`ContextFreeRule` `ContextFreeGrammar.NT` `Finset` `SetLike.instMembership` `Finset.instSetLike` `ContextFreeGrammar.rules` `Symbol` `Symbol.nonterminal` `ContextFreeRule.input`	—	`ContextFreeRule.Rewrites.nonterminal_input_mem`
`reverse` 📖	mathematical	`ContextFreeGrammar.Produces`	`ContextFreeGrammar.Produces` `ContextFreeGrammar.reverse` `Symbol` `ContextFreeGrammar.NT`	—	`ContextFreeGrammar.produces_reverse`
`single` 📖	mathematical	`ContextFreeGrammar.Produces`	`ContextFreeGrammar.Derives`	—	`Relation.ReflTransGen.single`
`trans_derives` 📖	mathematical	`ContextFreeGrammar.Produces` `ContextFreeGrammar.Derives`	`ContextFreeGrammar.Derives`	—	`ContextFreeGrammar.Derives.trans` `single`

ContextFreeRule

Definitions

Name	Category	Theorems
`Rewrites` 📖	CompData	8 math math: `rewrites_of_exists_parts`, `rewrites_reverse_comm`, `rewrites_iff`, `rewrites_reverse`, `Rewrites.reverse`, `Rewrites.input_output`, `Rewrites.append_right`, `Rewrites.append_left`
`input` 📖	CompOp	7 math math: `ext_iff`, `rewrites_of_exists_parts`, `ContextFreeGrammar.Produces.exists_nonterminal_input_mem`, `Rewrites.exists_parts`, `rewrites_iff`, `Rewrites.input_output`, `Rewrites.nonterminal_input_mem`
`output` 📖	CompOp	5 math math: `ext_iff`, `rewrites_of_exists_parts`, `Rewrites.exists_parts`, `rewrites_iff`, `Rewrites.input_output`
`reverse` 📖	CompOp	10 math math: `ContextFreeGrammar.reverse_rules`, `reverse_comp_reverse`, `reverse_reverse`, `reverse_injective`, `rewrites_reverse_comm`, `rewrites_reverse`, `Rewrites.reverse`, `reverse_surjective`, `reverse_bijective`, `reverse_involutive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`input` `output`	—	—	—
`ext_iff` 📖	mathematical	—	`input` `output`	—	`ext`
`reverse_bijective` 📖	mathematical	—	`Function.Bijective` `ContextFreeRule` `reverse`	—	`Function.Involutive.bijective` `reverse_involutive`
`reverse_comp_reverse` 📖	mathematical	—	`ContextFreeRule` `reverse`	—	`reverse_reverse`
`reverse_injective` 📖	mathematical	—	`ContextFreeRule` `reverse`	—	`Function.Bijective.injective` `reverse_bijective`
`reverse_involutive` 📖	mathematical	—	`Function.Involutive` `ContextFreeRule` `reverse`	—	`reverse_reverse`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	—
`reverse_surjective` 📖	mathematical	—	`ContextFreeRule` `reverse`	—	`Function.Bijective.surjective` `reverse_bijective`
`rewrites_iff` 📖	mathematical	—	`Rewrites` `Symbol` `Symbol.nonterminal` `input` `output`	—	`Rewrites.exists_parts` `rewrites_of_exists_parts`
`rewrites_of_exists_parts` 📖	mathematical	—	`Rewrites` `Symbol` `Symbol.nonterminal` `input` `output`	—	—
`rewrites_reverse` 📖	mathematical	—	`Rewrites` `reverse` `Symbol`	—	`reverse_reverse` `Rewrites.reverse`
`rewrites_reverse_comm` 📖	mathematical	—	`Rewrites` `reverse` `Symbol`	—	`rewrites_reverse` `reverse_reverse`

ContextFreeRule.Rewrites

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_left` 📖	mathematical	`ContextFreeRule.Rewrites`	`ContextFreeRule.Rewrites` `Symbol`	—	`ContextFreeRule.rewrites_iff`
`append_right` 📖	mathematical	`ContextFreeRule.Rewrites`	`ContextFreeRule.Rewrites` `Symbol`	—	`ContextFreeRule.rewrites_iff`
`exists_parts` 📖	mathematical	`ContextFreeRule.Rewrites`	`Symbol` `Symbol.nonterminal` `ContextFreeRule.input` `ContextFreeRule.output`	—	—
`input_output` 📖	mathematical	—	`ContextFreeRule.Rewrites` `Symbol` `Symbol.nonterminal` `ContextFreeRule.input` `ContextFreeRule.output`	—	—
`nonterminal_input_mem` 📖	mathematical	`ContextFreeRule.Rewrites`	`Symbol` `Symbol.nonterminal` `ContextFreeRule.input`	—	—
`reverse` 📖	mathematical	`ContextFreeRule.Rewrites`	`ContextFreeRule.Rewrites` `ContextFreeRule.reverse` `Symbol`	—	`append_left` `input_output` `append_right`

Language

Definitions

Name	Category	Theorems
`IsContextFree` 📖	MathDef	1 math math: `IsContextFree.reverse`

Language.IsContextFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reverse` 📖	mathematical	`Language.IsContextFree`	`Language.IsContextFree` `Language.reverse`	—	`ContextFreeGrammar.language_reverse`

(root)

Definitions

Name	Category	Theorems
`ContextFreeGrammar` 📖	CompData	4 math math: `ContextFreeGrammar.reverse_surjective`, `ContextFreeGrammar.reverse_involutive`, `ContextFreeGrammar.reverse_injective`, `ContextFreeGrammar.reverse_bijective`
`ContextFreeRule` 📖	CompData	7 math math: `ContextFreeGrammar.reverse_rules`, `ContextFreeRule.reverse_comp_reverse`, `ContextFreeGrammar.Produces.exists_nonterminal_input_mem`, `ContextFreeRule.reverse_injective`, `ContextFreeRule.reverse_surjective`, `ContextFreeRule.reverse_bijective`, `ContextFreeRule.reverse_involutive`
`instDecidableEqContextFreeRule` 📖	CompOp	—
`instReprContextFreeRule` 📖	CompOp	—

instDecidableEqContextFreeRule

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

instReprContextFreeRule

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index