Documentation

LeanCert.Tactic.IntervalAuto.Norm

Goal Normalization for Interval Tactics #

This module provides utilities for normalizing goal structure before parsing:

Bridge Theorems #

source
theorem LeanCert.Tactic.Auto.forall_arrow_of_Icc {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} :
(∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), lo ≤ x → x ≤ hi → P x

Bridge: Set.Icc bound to arrow chain (lo ≤ x → x ≤ hi).

source
theorem LeanCert.Tactic.Auto.forall_arrow_of_Icc_rev {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} :
(∀ x ∈ Set.Icc lo hi, P x) → ∀ x ≤ hi, lo ≤ x → P x

Bridge: Set.Icc bound to reversed arrow chain (x ≤ hi → lo ≤ x).

source
theorem LeanCert.Tactic.Auto.forall_and_of_Icc {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} :
(∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), lo ≤ x ∧ x ≤ hi → P x

Bridge: Set.Icc bound to conjunctive domain (lo ≤ x ∧ x ≤ hi).

source
theorem LeanCert.Tactic.Auto.forall_and_of_Icc_rev {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} :
(∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), x ≤ hi ∧ lo ≤ x → P x

Bridge: Set.Icc bound to reversed conjunctive domain (x ≤ hi ∧ lo ≤ x).

Goal Structure Detection #

source
def LeanCert.Tactic.Auto.tryNormalizeGoalToIcc :
Lean.Elab.Tactic.TacticM Bool

Try to normalize goal to Set.Icc form

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

    Main Normalization #

    source
    def LeanCert.Tactic.Auto.intervalNormCore :
    Lean.Elab.Tactic.TacticM Unit

    Normalize common goal patterns for interval tactics.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanCert.Tactic.Auto.intervalNormTac :
      Lean.ParserDescr

      The interval_norm tactic.

      Normalizes inequalities, subtraction, rational division, and domain syntax to reduce goal-shape variation before parsing.

      Equations
      Instances For
        source
        def LeanCert.Tactic.Auto.elabIntervalNorm :
        Lean.Elab.Tactic.Tactic
        Equations
        Instances For