Cancellation tactics for EpistemicSystemFA (Fin 4)

• cancel_fin4: packages cancellation_from_pairs with explicit pair lists
• solve_cancellation: auto-computes lt_pairs and eq_pairs from integer weights, derives all ¬ge/ge facts via deterministic meta-level strategy selection, then applies cancellation_from_pairs

def tacticCancel_fin4_Lt_pairs_Eq_pairs_ : Lean.ParserDescr

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.

Equations

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

def tacticSc_sdiff : Lean.ParserDescr

Prove a Set (Fin 4) diff equality by reducing to Finset sdiff (decidable).

Equations

• tacticSc_sdiff = Lean.ParserDescr.node `tacticSc_sdiff 1024 (Lean.ParserDescr.nonReservedSymbol "sc_sdiff" false)

def tacticSc_nonempty_ : Lean.ParserDescr

Prove a Set.Nonempty goal by exhibiting a computed witness.

Equations

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

def tacticSolve_cancellation____ : Lean.ParserDescr

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.

Equations

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