Documentation

Lean.Meta.Tactic.Contradiction

source
structure Lean.Meta.Contradiction.Config :
Type
  • 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.

source
@[reducible, inline]
abbrev Lean.Meta.ElimEmptyInductive.M (α : Type) :
Type
Equations
Instances For
source
instance Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM :
MonadBacktrack SavedState M
Equations
source
partial def Lean.Meta.ElimEmptyInductive.elim (mvarId : MVarId) (fvarId : FVarId) :
M Bool
source
def Lean.Meta.mkGenDiseqMask (e : Expr) :
Array Bool

Given e s.t. isGenDiseq e, generate a bit-mask mask s.t. mask[i] = true iff the i-th binder is an equality without forward dependencies.

See processGenDiseq

Equations
source
def Lean.Meta.mkGenDiseqMask.go (e : Expr) (acc : Array Bool) :
Array Bool
Equations
source
def Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Meta.Contradiction.Config) :
MetaM Bool

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.
source
def Lean.MVarId.contradiction (mvarId : MVarId) (config : Meta.Contradiction.Config := { }) :
MetaM Unit

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