Automation for ¬ge and ¬geFS derivations

The nge_close tactic automatically derives negated ordering facts (¬sys.ge A B) from hypotheses in the local context. It handles compositions of monotonicity, transitivity, and positivity lemmas up to depth 3, with backtracking over hypothesis assignments.

Supported patterns

• 0-step: direct assumption
• 1-step: nge_of_mono_right_set, nge_of_mono_left_set, nge_of_trans_left_set, nge_of_trans_right_set, nge_via_hpos_set
• 2-step: compositions like mono_right ∘ trans_left, etc.
• 3-step: mono_right ∘ trans_left ∘ trans_left, etc.

Subset obligations (C ⊆ B) on Sets are closed by intro x hx; fin_cases x <;> simp_all. On Finsets, by decide.

theorem Tactics.NgeFS.ngeFS_of_mono_right' {n : ℕ} (sys : Core.Scale.EpistemicSystemFA (Fin n)) {A C B : Finset (Fin n)} (hng : ¬sys.geFS A C) (h : C ⊆ B) : ¬sys.geFS A B

Variant of ngeFS_of_mono_right without autoParam, suitable for apply.

theorem Tactics.NgeFS.ngeFS_of_mono_left' {n : ℕ} (sys : Core.Scale.EpistemicSystemFA (Fin n)) {C B A : Finset (Fin n)} (hng : ¬sys.geFS C B) (h : A ⊆ C) : ¬sys.geFS A B

Variant of ngeFS_of_mono_left without autoParam, suitable for apply.

def tacticNge_close : Lean.ParserDescr

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.

Equations

• tacticNge_close = Lean.ParserDescr.node `tacticNge_close 1024 (Lean.ParserDescr.nonReservedSymbol "nge_close" false)

def tacticHlt_assumption : Lean.ParserDescr

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.

Equations

• tacticHlt_assumption = Lean.ParserDescr.node `tacticHlt_assumption 1024 (Lean.ParserDescr.nonReservedSymbol "hlt_assumption" false)

def tacticNge_overlap : Lean.ParserDescr

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.

Equations

• tacticNge_overlap = Lean.ParserDescr.node `tacticNge_overlap 1024 (Lean.ParserDescr.nonReservedSymbol "nge_overlap" false)

def tacticNge_double_additive : Lean.ParserDescr

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.

Equations

• tacticNge_double_additive = Lean.ParserDescr.node `tacticNge_double_additive 1024 (Lean.ParserDescr.nonReservedSymbol "nge_double_additive" false)

def tacticGe_via_additive : Lean.ParserDescr

Derive ge B A via one additive step + one trans step, or two additive steps. Mirrors nge_double_additive but for positive ge facts:

1. 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.
2. Double additive: as above, then also check if ge (C\A) (A\C) is in context.

Equations

• tacticGe_via_additive = Lean.ParserDescr.node `tacticGe_via_additive 1024 (Lean.ParserDescr.nonReservedSymbol "ge_via_additive" false)

def tacticSaturate_singleton_ge : Lean.ParserDescr

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.

Equations

• tacticSaturate_singleton_ge = Lean.ParserDescr.node `tacticSaturate_singleton_ge 1024 (Lean.ParserDescr.nonReservedSymbol "saturate_singleton_ge" false)

def tacticHlt_nge_close : Lean.ParserDescr

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.

Equations

• tacticHlt_nge_close = Lean.ParserDescr.node `tacticHlt_nge_close 1024 (Lean.ParserDescr.nonReservedSymbol "hlt_nge_close" false)

def tacticHge_assumption : Lean.ParserDescr

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.

Equations

• tacticHge_assumption = Lean.ParserDescr.node `tacticHge_assumption 1024 (Lean.ParserDescr.nonReservedSymbol "hge_assumption" false)

def tacticHge_trans : Lean.ParserDescr

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.

Equations

• tacticHge_trans = Lean.ParserDescr.node `tacticHge_trans 1024 (Lean.ParserDescr.nonReservedSymbol "hge_trans" false)