Lean.Meta.Tactic.Contradiction

source

structure Lean.Meta.Contradiction.Config :

Type

useDecide : Bool
searchFuel : Nat
genDiseq : Bool

source

@[inline]

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

Type

Equations

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

source

instance Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM :

Lean.MonadBacktrack Lean.Meta.SavedState Lean.Meta.ElimEmptyInductive.M

Equations

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

source

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

Lean.Meta.ElimEmptyInductive.M Bool

source

def Lean.Meta.contradictionCore (mvarId : Lean.MVarId) (config : Lean.Meta.Contradiction.Config) :

Lean.MetaM Bool

Equations

Lean.Meta.contradictionCore mvarId config = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `contradiction let a ← Lean.getLCtx let r ← let col := a; forIn col { fst := none, snd := PUnit.unit } fun localDecl r => let r := r.snd; if Lean.LocalDecl.isAuxDecl localDecl = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do let a ← Lean.Meta.matchNot? (Lean.LocalDecl.type localDecl) let _do_jp : PUnit → Lean.MetaM (ForInStep (MProd (Option Bool) PUnit)) := fun y => do let a ← Lean.Meta.matchNe? (Lean.LocalDecl.type localDecl) let _do_jp : PUnit → Lean.MetaM (ForInStep (MProd (Option Bool) PUnit)) := fun y => let isEq := false; do let a ← Lean.Meta.matchEq? (Lean.LocalDecl.type localDecl) let _do_jp : Bool → PUnit → Lean.MetaM (ForInStep (MProd (Option Bool) PUnit)) := fun isEq y => let _do_jp := fun y => let _do_jp := fun y => if isEq = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do let a ← Lean.Meta.elimEmptyInductive mvarId (Lean.LocalDecl.fvarId localDecl) config.searchFuel if a = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }); if (config.genDiseq && Lean.Meta.isGenDiseq (Lean.LocalDecl.type localDecl)) = true then do let a ← Lean.Meta.processGenDiseq mvarId localDecl if a = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y; if (config.useDecide && !Lean.Expr.hasFVar (Lean.LocalDecl.type localDecl)) = true then do let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) if (!Lean.Expr.hasMVar type && !Lean.Expr.hasFVar type) = true then do let r ← tryCatch (do let d ← Lean.Meta.mkDecide (Lean.LocalDecl.type localDecl) let r ← Lean.Meta.withDefault (Lean.Meta.whnf d) if Lean.Expr.isConstOf r `Bool.false = true then do let a ← Lean.Meta.mkEqRefl d let hn : Lean.Expr := Lean.mkAppN (Lean.mkConst `of_decide_eq_false) (Array.push (Lean.Expr.getAppArgs d) a) let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.mkAbsurd a (Lean.LocalDecl.toExpr localDecl) hn Lean.Meta.assignExprMVar mvarId a pure (DoResultPR.return true PUnit.unit) else do let y ← pure PUnit.unit pure (DoResultPR.pure y PUnit.unit)) fun x => do let y ← pure () pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; do let y ← pure a _do_jp y | DoResultPR.return b u => let x := u; pure (ForInStep.done { fst := some b, snd := PUnit.unit }) else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y match a with | some (x, lhs, rhs) => let isEq := true; do let a ← Lean.Meta.matchConstructorApp? lhs match a with | some lhsCtor => do let a ← Lean.Meta.matchConstructorApp? rhs match a with | some rhsCtor => if (lhsCtor.toConstantVal.name != rhsCtor.toConstantVal.name) = true then do let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.mkNoConfusion a (Lean.LocalDecl.toExpr localDecl) Lean.Meta.assignExprMVar mvarId a pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do let y ← pure PUnit.unit _do_jp isEq y | x => do let y ← pure PUnit.unit _do_jp isEq y | x => do let y ← pure PUnit.unit _do_jp isEq y | x => do let y ← pure PUnit.unit _do_jp isEq y match a with | some (x, lhs, rhs) => do let a ← Lean.Meta.isDefEq lhs rhs if a = true then do let a ← Lean.Meta.getMVarType mvarId let a_1 ← Lean.Meta.mkEqRefl lhs let a ← Lean.Meta.mkAbsurd a a_1 (Lean.LocalDecl.toExpr localDecl) Lean.Meta.assignExprMVar mvarId a pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y match a with | some p => do let a ← Lean.Meta.findLocalDeclWithType? p match a with | some pFVarId => do let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.mkAbsurd a (Lean.mkFVar pFVarId) (Lean.LocalDecl.toExpr localDecl) Lean.Meta.assignExprMVar mvarId a pure (ForInStep.done { fst := some true, snd := PUnit.unit }) | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => pure false match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

def Lean.Meta.contradiction (mvarId : Lean.MVarId) (config : optParam Lean.Meta.Contradiction.Config { useDecide := true, searchFuel := 16, genDiseq := false }) :

Lean.MetaM Unit

Equations

Lean.Meta.contradiction mvarId config = do let a ← Lean.Meta.contradictionCore mvarId config if a = true then pure PUnit.unit else Lean.Meta.throwTacticEx `contradiction mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "") Lean.Syntax.missing