Lean.Meta.Tactic.SplitIf

Equations

Lean.Meta.SplitIf.getSimpContext = Lean.LazyInitExtension.get Lean.Meta.SplitIf.ext

source

def Lean.Meta.SplitIf.discharge? (useDecide : optParam Bool false) :

Lean.Meta.Simp.Discharge

Equations

Lean.Meta.SplitIf.discharge? useDecide prop = do let prop ← liftM (Lean.Meta.instantiateMVars prop) let cls : Lean.Name := `Meta.Tactic.splitIf let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM (Option Lean.Expr) := fun y => let _do_jp := fun y => do let a ← Lean.getLCtx Lean.LocalContext.findDeclRevM? a fun localDecl => if Lean.LocalDecl.isAuxDecl localDecl = true then pure none else do let a ← liftM (Lean.Meta.isDefEq prop (Lean.LocalDecl.type localDecl)) if a = true then pure (some (Lean.LocalDecl.toExpr localDecl)) else match Lean.Expr.notNot? prop with | none => pure none | some arg => do let a ← liftM (Lean.Meta.isDefEq arg (Lean.LocalDecl.type localDecl)) if a = true then pure (some (Lean.mkApp2 (Lean.mkConst `not_not_intro) arg (Lean.LocalDecl.toExpr localDecl))) else pure none; if useDecide = true then do let prop ← liftM (Lean.Meta.instantiateMVars prop) if (!Lean.Expr.hasFVar prop && !Lean.Expr.hasMVar prop) = true then do let d ← liftM (Lean.Meta.mkDecide prop) let r ← Lean.Meta.withDefault (liftM (Lean.Meta.whnf d)) if Lean.Expr.isConstOf r `Bool.true = true then do let a ← liftM (Lean.Meta.mkEqRefl (Lean.mkConst `Bool.true)) pure (some (Lean.mkApp3 (Lean.mkConst `of_decide_eq_true) prop (Lean.Expr.appArg! d) a)) else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "discharge? " ++ Lean.toMessageData prop ++ Lean.toMessageData ", " ++ Lean.toMessageData (Lean.Expr.notNot? prop) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

partial def Lean.Meta.SplitIf.findIfToSplit? (e : Lean.Expr) :

Option Lean.Expr

source

def Lean.Meta.SplitIf.splitIfAt? (mvarId : Lean.MVarId) (e : Lean.Expr) (hName? : Option Lean.Name) :

Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))

Equations

Lean.Meta.SplitIf.splitIfAt? mvarId e hName? = match Lean.Meta.SplitIf.findIfToSplit? e with | some cond => let _do_jp := fun hName => let cls := `Meta.Tactic.splitIf; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)) := fun y => do let a ← Lean.Meta.byCases mvarId cond hName pure (some a) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "splitting on " ++ Lean.toMessageData cond ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; match hName? with | none => do let y ← liftM (Lean.mkFreshUserName `h) _do_jp y | some hName => do let y ← pure hName _do_jp y | x => pure none

source

def Lean.Meta.simpIfTarget (mvarId : Lean.MVarId) (useDecide : optParam Bool false) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.simpIfTarget mvarId useDecide = do let ctx ← Lean.Meta.SplitIf.getSimpContext let a ← Lean.Meta.simpTarget mvarId ctx (some (Lean.Meta.SplitIf.discharge? useDecide)) match a with | some mvarId' => pure mvarId' | x => panicWithPosWithDecl "Lean.Meta.Tactic.SplitIf" "Lean.Meta.simpIfTarget" 87 4 "unreachable code has been reached"

source

def Lean.Meta.simpIfLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.simpIfLocalDecl mvarId fvarId = do let ctx ← Lean.Meta.SplitIf.getSimpContext let a ← Lean.Meta.simpLocalDecl mvarId fvarId ctx (some (Lean.Meta.SplitIf.discharge? false)) match a with | some (x, mvarId') => pure mvarId' | x => panicWithPosWithDecl "Lean.Meta.Tactic.SplitIf" "Lean.Meta.simpIfLocalDecl" 94 4 "unreachable code has been reached"

source

def Lean.Meta.splitIfTarget? (mvarId : Lean.MVarId) (hName? : optParam (Option Lean.Name) none) :

Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))

Equations

Lean.Meta.splitIfTarget? mvarId hName? = Lean.commitWhenSome? do let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.SplitIf.splitIfAt? mvarId a hName? match a with | some (s₁, s₂) => do let mvarId₁ ← Lean.Meta.simpIfTarget s₁.mvarId false let mvarId₂ ← Lean.Meta.simpIfTarget s₂.mvarId false if (s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂) = true then pure none else pure (some ({ mvarId := mvarId₁, fvarId := s₁.fvarId }, { mvarId := mvarId₂, fvarId := s₂.fvarId })) | x => pure none

source

def Lean.Meta.splitIfLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (hName? : optParam (Option Lean.Name) none) :

Lean.MetaM (Option (Lean.MVarId × Lean.MVarId))

Equations

Lean.Meta.splitIfLocalDecl? mvarId fvarId hName? = Lean.commitWhenSome? (Lean.Meta.withMVarContext mvarId do let a ← Lean.Meta.inferType (Lean.mkFVar fvarId) let a ← Lean.Meta.SplitIf.splitIfAt? mvarId a hName? match a with | some (s₁, s₂) => do let mvarId₁ ← Lean.Meta.simpIfLocalDecl s₁.mvarId fvarId let mvarId₂ ← Lean.Meta.simpIfLocalDecl s₂.mvarId fvarId if (s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂) = true then pure none else pure (some (mvarId₁, mvarId₂)) | x => pure none)