Documentation

Lean.Meta.Tactic.Contradiction

  • useDecide : Bool
  • emptyType : Bool

    Check whether any of the hypotheses is an empty type.

  • searchFuel : Nat

    When checking for empty types, searchFuel specifies the number of goals visited.

  • genDiseq : Bool

    Support for hypotheses such as

    h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
    

    This kind of hypotheses appear when proving conditional equation theorems for match expressions.

Instances For

    Return true if goal mvarId has contradictory hypotheses. See MVarId.contradiction for the list of tests performed by this method.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.MVarId.contradiction (mvarId : Lean.MVarId) (config : optParam Lean.Meta.Contradiction.Config { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := false }) :

      Try to close the goal using "contradictions" such as

      • Contradictory hypotheses h₁ : p and h₂ : ¬ p.
      • Contradictory disequality h : x ≠ x.
      • Contradictory equality between different constructors, e.g., h : List.nil = List.cons x xs.
      • Empty inductive types, e.g., x : Fin 0.
      • Decidable propositions that evaluate to false, i.e., a hypothesis h : p s.t. decide p reduces to false. This is only tried if Config.useDecide = true.

      Throw exception if goal failed to be closed.

      Equations
      Instances For