Trying to prove things about a definition can be extremely tedious. Sometimes it might be worth defining an inductive and proving it equivalent to some definition just to have the proofs be so much easier.
Having None in literal is cool, but
maybe unnecessary. It gives life to the optimization of rejecting a
regex completely, but that could be a separate analysis on the regex. At
the moment None can arise only with the CdEmpty character
class.
Leaving things not proven is a better way to progress. Proving small simple but very time consuming lemmas is wasting time and not progressing the theory. However, on the other hand I did leave a lemma unproven once, and realized only later that it was actually not a true lemma despite me relying on that lemma in other proofs.
LazyPrefix.v. Some proofs there might be
very useful.Move onto proving equivalence of first_leaf on trees that are pruned if the string search does not find a match in this position of the haystack.