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.

@[reducible, inline]

abbrev Lean.Meta.ElimEmptyInductive.M (α : Type) : Type

Equations

• Lean.Meta.ElimEmptyInductive.M = StateRefT' IO.RealWorld Nat Lean.MetaM

instance Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM : MonadBacktrack SavedState M

Equations

• Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM = { saveState := liftM Lean.Meta.saveState, restoreState := fun (s : Lean.Meta.SavedState) => liftM s.restore }

partial def Lean.Meta.ElimEmptyInductive.elim (mvarId : MVarId) (fvarId : FVarId) : M Bool

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

• Lean.Meta.mkGenDiseqMask e = Lean.Meta.mkGenDiseqMask.go e #[]

def Lean.Meta.mkGenDiseqMask.go (e : Expr) (acc : Array Bool) : Array Bool

Equations

• Lean.Meta.mkGenDiseqMask.go (Lean.Expr.forallE binderName d b binderInfo) acc = Lean.Meta.mkGenDiseqMask.go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
• Lean.Meta.mkGenDiseqMask.go e acc = acc

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.

def Lean.MVarId.contradiction (mvarId : MVarId) (config : Meta.Contradiction.Config := { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := false }) : 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

• mvarId.contradiction config = do let __do_lift ← mvarId.contradictionCore config if __do_lift = true then pure PUnit.unit else Lean.Meta.throwTacticEx `contradiction mvarId