RegularExpressions

📁 Source: Mathlib/Computability/RegularExpressions.lean

Statistics

Metric	Count
Definitions `RegularExpression`, `deriv`, `instAdd`, `instDecidablePredListMemLanguageMatches'`, `instInhabited`, `instMul`, `instOne`, `instPowNat`, `instZero`, `map`, `matchEpsilon`, `matches'`, `rmatch`	13
Theorems `add_rmatch_iff`, `char_rmatch_iff`, `comp_def`, `deriv_add`, `deriv_char_of_ne`, `deriv_char_self`, `deriv_one`, `deriv_star`, `deriv_zero`, `map_id`, `map_map`, `map_pow`, `matches'_add`, `matches'_char`, `matches'_epsilon`, `matches'_map`, `matches'_mul`, `matches'_pow`, `matches'_star`, `matches'_zero`, `mul_rmatch_iff`, `one_def`, `one_rmatch_iff`, `plus_def`, `rmatch_iff_matches'`, `star_rmatch_iff`, `zero_def`, `zero_rmatch`	28
Total	41

RegularExpression

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	6 math math: `deriv_add`, `deriv_char_of_ne`, `deriv_char_self`, `deriv_star`, `deriv_one`, `deriv_zero`
`instAdd` 📖	CompOp	3 math, 1 bridge math: `deriv_add`, `matches'_add`, `plus_def` bridge: `add_rmatch_iff`
`instDecidablePredListMemLanguageMatches'` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMul` 📖	CompOp	3 math, 1 bridge math: `matches'_mul`, `deriv_star`, `comp_def` bridge: `mul_rmatch_iff`
`instOne` 📖	CompOp	4 math, 1 bridge math: `deriv_char_self`, `deriv_one`, `one_def`, `matches'_epsilon` bridge: `one_rmatch_iff`
`instPowNat` 📖	CompOp	2 math math: `matches'_pow`, `map_pow`
`instZero` 📖	CompOp	5 math, 1 bridge math: `deriv_char_of_ne`, `deriv_one`, `matches'_zero`, `deriv_zero`, `zero_def` bridge: `zero_rmatch`
`map` 📖	CompOp	4 math math: `map_map`, `map_id`, `matches'_map`, `map_pow`
`matchEpsilon` 📖	CompOp	—
`matches'` 📖	CompOp	8 math, 1 bridge math: `matches'_mul`, `matches'_add`, `matches'_star`, `matches'_pow`, `matches'_zero`, `matches'_map`, `matches'_epsilon`, `matches'_char` bridge: `rmatch_iff_matches'`
`rmatch` 📖	CompOp	7 bridge bridge: `char_rmatch_iff`, `star_rmatch_iff`, `add_rmatch_iff`, `mul_rmatch_iff`, `one_rmatch_iff`, `zero_rmatch`, `rmatch_iff_matches'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_rmatch_iff` 📖	bridging (iff)	—	`rmatch` `RegularExpression` `instAdd`	`rmatch`	`rmatch.eq_2` `deriv_add`
`char_rmatch_iff` 📖	bridging (iff)	—	`rmatch` `char`	`rmatch`	`rmatch.eq_2` `deriv.eq_3` `rmatch.congr_simp` `zero_rmatch`
`comp_def` 📖	mathematical	—	`comp` `RegularExpression` `instMul`	—	—
`deriv_add` 📖	mathematical	—	`deriv` `RegularExpression` `instAdd`	—	—
`deriv_char_of_ne` 📖	mathematical	—	`deriv` `char` `RegularExpression` `instZero`	—	—
`deriv_char_self` 📖	mathematical	—	`deriv` `char` `RegularExpression` `instOne`	—	—
`deriv_one` 📖	mathematical	—	`deriv` `RegularExpression` `instOne` `instZero`	—	—
`deriv_star` 📖	mathematical	—	`deriv` `star` `RegularExpression` `instMul`	—	—
`deriv_zero` 📖	mathematical	—	`deriv` `RegularExpression` `instZero`	—	—
`map_id` 📖	mathematical	—	`map`	—	—
`map_map` 📖	mathematical	—	`map`	—	—
`map_pow` 📖	mathematical	—	`map` `RegularExpression` `instPowNat`	—	`map.eq_def`
`matches'_add` 📖	mathematical	—	`matches'` `RegularExpression` `instAdd` `Language` `Language.instAdd`	—	—
`matches'_char` 📖	mathematical	—	`matches'` `char` `Language` `Language.instSingletonList`	—	—
`matches'_epsilon` 📖	mathematical	—	`matches'` `RegularExpression` `instOne` `Language` `Language.instOne`	—	—
`matches'_map` 📖	mathematical	—	`matches'` `map` `DFunLike.coe` `RingHom` `Language` `Semiring.toNonAssocSemiring` `Language.instSemiring` `RingHom.instFunLike` `Language.map`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `Set.image_singleton` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Language.map_kstar`
`matches'_mul` 📖	mathematical	—	`matches'` `RegularExpression` `instMul` `Language` `Language.instMul`	—	—
`matches'_pow` 📖	mathematical	—	`matches'` `RegularExpression` `instPowNat` `Language` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Language.instSemiring`	—	`matches'_epsilon` `matches'_mul` `pow_succ`
`matches'_star` 📖	mathematical	—	`matches'` `star` `KStar.kstar` `Language` `Language.instKStar`	—	—
`matches'_zero` 📖	mathematical	—	`matches'` `RegularExpression` `instZero` `Language` `Language.instZero`	—	—
`mul_rmatch_iff` 📖	bridging (iff)	—	`rmatch` `RegularExpression` `instMul`	`rmatch`	`rmatch.eq_1` `rmatch.eq_2` `rmatch.congr_simp` `add_rmatch_iff`
`one_def` 📖	mathematical	—	`epsilon` `RegularExpression` `instOne`	—	—
`one_rmatch_iff` 📖	bridging (iff)	—	`rmatch` `RegularExpression` `instOne`	`rmatch`	`zero_rmatch`
`plus_def` 📖	mathematical	—	`plus` `RegularExpression` `instAdd`	—	—
`rmatch_iff_matches'` 📖	bridging (iff)	—	`rmatch` `Language` `Language.instMembershipList` `matches'`	`rmatch`	`zero_def` `zero_rmatch` `one_def` `one_rmatch_iff` `matches'_epsilon` `Language.mem_one` `char_rmatch_iff` `plus_def` `add_rmatch_iff`
`star_rmatch_iff` 📖	bridging (iff)	—	`rmatch` `star`	`rmatch`	`rmatch.eq_2` `deriv.eq_6` `mul_rmatch_iff`
`zero_def` 📖	mathematical	—	`zero` `RegularExpression` `instZero`	—	—
`zero_rmatch` 📖	bridging (complete)	—	`rmatch` `RegularExpression` `instZero`	`rmatch`	—

(root)

Definitions

Name	Category	Theorems
`RegularExpression` 📖	CompData	16 math, 4 bridge math: `RegularExpression.deriv_add`, `RegularExpression.matches'_mul`, `RegularExpression.deriv_char_of_ne`, `RegularExpression.deriv_char_self`, `RegularExpression.deriv_star`, `RegularExpression.matches'_add`, `RegularExpression.comp_def`, `RegularExpression.deriv_one`, `RegularExpression.plus_def`, `RegularExpression.matches'_pow`, `RegularExpression.one_def`, `RegularExpression.matches'_zero`, `RegularExpression.matches'_epsilon`, `RegularExpression.deriv_zero`, `RegularExpression.map_pow`, `RegularExpression.zero_def` bridge: `RegularExpression.add_rmatch_iff`, `RegularExpression.mul_rmatch_iff`, `RegularExpression.one_rmatch_iff`, `RegularExpression.zero_rmatch`

---

← Back to Index