Documentation

Linglib.Tactics.NgeFS

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 #

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

source
theorem 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.

source
theorem 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.

source
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
Instances For
    source
    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
    Instances For
      source
      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
      Instances For
        source
        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
        Instances For
          source
          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
          Instances For
            source
            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
            Instances For
              source
              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
              Instances For
                source
                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
                Instances For
                  source
                  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
                  Instances For