The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.
cancel_fin4
Convenience macro for calling cancellation_from_pairs with standard proof
obligations. Takes weight vector, lt_pairs list, and eq_pairs list.
Use lt_pairs and eq_pairs keywords to separate arguments.
- Tags:
- Defined in module:
- Linglib.Tactics.CancelFin4
ennreal_arith
Discharge a concrete ℝ≥0∞ arithmetic goal — equality a = b, strict
inequality a < b, or negated strict inequality ¬ a < b — between
nonnegative real numerical expressions built from +, *, /, and
natural-number literals.
Lifts through ENNReal.toReal (with ≠ ⊤ side conditions discharged by
simp [ENNReal.add_eq_top, ENNReal.div_eq_top]) and closes the residual
real-arithmetic goal with norm_num.
- Tags:
- Defined in module:
- Linglib.Tactics.ENNRealArith
ge_via_additive
Derive ge B A via one additive step + one trans step, or two additive steps.
Mirrors nge_double_additive but for positive ge facts:
- One additive + trans: find singleton ge {d} {e} with d ∈ B, e ∉ B, compute C = (B{d})∪{e}, and check if ge C A is in context.
- Double additive: as above, then also check if ge (C\A) (A\C) is in context.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
hge_assumption
Close ∀ pair ∈ eq_pairs, sys.ge ↑pair.1 ↑pair.2 → sys.ge ↑pair.2 ↑pair.1
goals (the heq argument of cancellation_from_pairs). Like hlt_assumption
but with an intro _ step to discharge the antecedent before assumption.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
hge_trans
Like hge_assumption but derives ge facts via transitivity when assumption
fails. Handles eq_pairs where the reverse direction needs transitive closure.
Uses an elab tactic to find the EpistemicSystemFA hypothesis by type and
apply .trans using its actual FVar name, avoiding macro hygiene issues.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
hlt_assumption
Close ∀ pair ∈ pairs, ¬sys.ge ↑pair.1 ↑pair.2 goals by iterating over
list membership, substituting each pair, normalizing Finset→Set coercions,
and closing by assumption. Used in the hlt argument of
cancellation_from_pairs.
Strategy: intro a single pair variable (not destructured), normalize
membership to pair = v₁ ∨ pair = v₂ ∨ ... via simp, then peel
disjuncts with rcases h | hmem. Each subst h substitutes the whole
pair, after which simp reduces Prod projections via iota and normalizes
Finset.coe, and assumption matches a hypothesis. Sequential (not <;>)
composition ensures each subst+close block targets only the first goal
from rcases. The final bare equality is handled after repeat.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
hlt_nge_close
Like hlt_assumption but falls back to nge_close when assumption fails.
Used in the hlt argument of cancellation_from_pairs when not all ¬ge
facts are pre-computed in the context. Processes each pair via rcases,
closing each ¬ge goal via assumption, nge_double_additive, nge_close,
or nge_overlap.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
nge_close
Automatically derive ¬sys.ge A B or ¬sys.geFS A B from hypotheses
via compositions of monotonicity, transitivity, and positivity lemmas
(up to depth 3). Works with both Set-typed and Finset-typed goals.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
nge_double_additive
Derive ¬ge A B via double additive: find hypotheses ge D1 E1 and ¬ge D2 E2
in context such that nge_of_double_additive applies with computed bridge set C.
C is computed as D1 ∪ (A \ E1), then verified against D2, E2, B.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
nge_overlap
Derive ¬ge A B via trans+additive+hpos: find a hypothesis ge C A in context
where C ⊆ B and B\C nonempty. Tries each ge hypothesis × witness pair.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
nonneg_of_forall
Close 0 ≤ f a₁ + f a₂ + ⋯ + f aₙ given ∀ x, 0 ≤ f x in context.
Decomposes sums via add_nonneg (and products via mul_nonneg), then
closes leaf goals by applying forall-quantified non-negativity hypotheses
from the local context.
- Tags:
- Defined in module:
- Linglib.Tactics.NonnegOfForall
pmf_eval_no_decide
This tactic has no documentation.
- Tags:
- Defined in module:
- Linglib.Core.Probability.Eval
rsa_predict
rsa_predict proves RSA prediction goals by RExpr reflection.
The tactic reifies both sides of a comparison to RExpr (rational expression
trees), then proves the comparison via exact ℚ evaluation or tree-based interval
arithmetic. The kernel verifies that RExpr.denote matches the original ℝ
expression via iota-reduction.
- Tags:
- Defined in module:
- Linglib.Tactics.RSAPredict
saturate_singleton_ge
Saturate context with transitively-derived singleton ge facts.
Collects all singleton ge {i} {j} hypotheses, then derives all
transitive consequences ge {i} {k} via sys.trans. Two rounds
for chains up to length 4.
- Tags:
- Defined in module:
- Linglib.Tactics.NgeFS
sc_nonempty
Prove a Set.Nonempty goal by exhibiting a computed witness.
- Tags:
- Defined in module:
- Linglib.Tactics.CancelFin4
sc_sdiff
Prove a Set (Fin 4) diff equality by reducing to Finset sdiff (decidable).
- Tags:
- Defined in module:
- Linglib.Tactics.CancelFin4
set_sdiff_fin
Tactic for proving (A : Set (Fin n)) \ B = C where A, B, C are Set
literals or Set.univ. Normalizes to Finset coercions, computes the sdiff
via kernel reduction, and closes by rfl or decide. Falls back to
ext x; fin_cases x for edge cases.
- Tags:
- Defined in module:
- Linglib.Core.Scales.EpistemicScale.FinsetBridge
solve_cancellation
Auto-compute cancellation from integer weights. Usage: solve_cancellation 7 6 3 2.
Derives all ¬ge/ge facts via deterministic meta-level strategy selection
(no backtracking search), then applies cancellation_from_pairs.
- Tags:
- Defined in module:
- Linglib.Tactics.CancelFin4