Custom Tactics for Langlib

This file provides domain-specific tactics that automate common proof patterns in grammar and language theory formalizations.

Main declarations

• no_nonterminal — close goals where a nonterminal appears in a terminal-only list
• count_contra — contradiction from character-counting arguments
• deri_context — strip matching prefix/postfix from a derivation goal

no_nonterminal

Closes goals that are absurd because a symbol.nonterminal appears in a list built from symbol.terminal (typically from List.map symbol.terminal w).

Automates the recurring pattern:

have := congr_arg List.toFinset h
rw [Finset.ext_iff] at this
specialize this (symbol.nonterminal _)
aesop

def tacticNo_nonterminal : Lean.ParserDescr

Close goals where a symbol.nonterminal appears in a terminal-only list.

Variants:

• no_nonterminal — automatically searches for the right hypothesis and symbol (slow)
• no_nonterminal (sym) at hyp — specify the symbol and hypothesis to target (fast), (sym) and at hyp are optional
• no_nonterminal? — like no_nonterminal, but suggests no_nonterminal (sym) at hyp

Falls back to exfalso; simp for membership-based contradictions.

Equations

• tacticNo_nonterminal = Lean.ParserDescr.node `tacticNo_nonterminal 1024 (Lean.ParserDescr.nonReservedSymbol "no_nonterminal" false)

def «tacticNo_nonterminal(_)At_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def tacticNo_nonterminalAt_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «tacticNo_nonterminal(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def tacticNo_nonterminal! : Lean.ParserDescr

Equations

• tacticNo_nonterminal! = Lean.ParserDescr.node `tacticNo_nonterminal! 1024 (Lean.ParserDescr.nonReservedSymbol "no_nonterminal!" false)

def tacticNo_nonterminal? : Lean.ParserDescr

Equations

• tacticNo_nonterminal? = Lean.ParserDescr.node `tacticNo_nonterminal? 1024 (Lean.ParserDescr.nonReservedSymbol "no_nonterminal?" false)

grammar_cases

Given a hypothesis h : CF_transforms g w w', destructure it into the rule, prefix, suffix, and then case-split on which rule was applied. Finishes by simplifying with +decide to substitute concrete rule data.

For grammars defined as named constants, pass the name as an extra simp lemma to unfold the rules: grammar_cases ht [cfg_anbn]

def tacticGrammar_cases_ : Lean.ParserDescr

Core implementation for grammar_cases. Unfolds CF_transforms, destructures the existentials, uses simp_all +decide to resolve concrete rule membership, case-splits on which rule was applied, and simplifies each branch.

For grammars defined as named constants, pass the name as an extra simp lemma to unfold the rules: grammar_cases ht [cfg_anbn]

Equations

• One or more equations did not get rendered due to their size.

def «tacticGrammar_cases_[_,,]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

append_chase

Exhaustively analyze list-append equations in hypotheses.

When you have hypotheses like a ++ b = c ++ d or a ++ [x] ++ b = c ++ [y] ++ d, this tactic repeatedly applies List.append_eq_append_iff, performs case splits, and simplifies with simp_all +decide and omega.

def tacticAppend_chase : Lean.ParserDescr

Equations

• tacticAppend_chase = Lean.ParserDescr.node `tacticAppend_chase 1024 (Lean.ParserDescr.nonReservedSymbol "append_chase" false)

append_chase variant with extra simp lemmas

def «tacticAppend_chase[_,,]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

count_contra

Derive a contradiction from List.count_in equalities/inequalities.

Rewrites all count_in hypotheses using distributivity over append, replicate, and singletons, then invokes omega to find the contradiction. Useful for pumping lemma counterexamples where character counts become inconsistent.

def tacticCount_contra : Lean.ParserDescr

Equations

• tacticCount_contra = Lean.ParserDescr.node `tacticCount_contra 1024 (Lean.ParserDescr.nonReservedSymbol "count_contra" false)

deri_context

When the goal is CF_derives g (pᵣ ++ w₁ ++ pₒ) (pᵣ ++ w₂ ++ pₒ), strip the common prefix and/or postfix, reducing the goal to CF_derives g w₁ w₂.

Also handles goals with only a prefix or only a postfix.

def tacticDeri_context : Lean.ParserDescr

Equations

• tacticDeri_context = Lean.ParserDescr.node `tacticDeri_context 1024 (Lean.ParserDescr.nonReservedSymbol "deri_context" false)