def
Lean.Meta.Simp.synthesizeArgs
(lemmaName : Lean.Name)
(xs : Array Lean.Expr)
(bis : Array Lean.BinderInfo)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.synthesizeArgs lemmaName xs bis discharge? = (fun synthesizeInstance => let s := toStream bis; do let r ← forIn xs { fst := none, snd := s } fun x r => let r := r.snd; let s := r; match Stream.next? s with | none => pure (ForInStep.done { fst := none, snd := s }) | some (bi, s') => let s := s'; do let type ← liftM (Lean.Meta.inferType x) if Lean.BinderInfo.isInstImplicit bi = true then do let a ← synthesizeInstance x type if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) else pure (ForInStep.done { fst := some false, snd := s }) else do let a ← liftM (Lean.Meta.instantiateMVars x) if Lean.Expr.isMVar a = true then do let a ← liftM (Lean.Meta.isProp type) if a = true then do let a ← liftM (Lean.Meta.instantiateMVars type) let a ← liftM (Lean.Meta.hasAssignableMVar a) let _do_jp : PUnit → Lean.Meta.SimpM (ForInStep (MProd (Option Bool) (Subarray Lean.BinderInfo))) := fun y => do let a ← discharge? type match a with | some proof => do let a ← liftM (Lean.Meta.isDefEq x proof) if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) else let cls := `Meta.Tactic.simp.discharge; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM (ForInStep (MProd (Option Bool) (Subarray Lean.BinderInfo))) := fun y => pure (ForInStep.done { fst := some false, snd := s }) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lemmaName ++ Lean.toMessageData ", failed to assign proof" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | none => let cls := `Meta.Tactic.simp.discharge; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM (ForInStep (MProd (Option Bool) (Subarray Lean.BinderInfo))) := fun y => pure (ForInStep.done { fst := some false, snd := s }) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lemmaName ++ Lean.toMessageData ", failed to discharge hypotheses" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then let cls := `Meta.Tactic.simp.discharge; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM (ForInStep (MProd (Option Bool) (Subarray Lean.BinderInfo))) := fun y => pure (ForInStep.done { fst := some false, snd := s }) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lemmaName ++ Lean.toMessageData ", hypothesis contains metavariables" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let a ← liftM (Lean.Meta.isClass? type) if Option.isSome a = true then do let a ← synthesizeInstance x type if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) else pure (ForInStep.done { fst := some false, snd := s }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := s }) let x : Subarray Lean.BinderInfo := r.snd let s : Subarray Lean.BinderInfo := x let _do_jp : PUnit → Lean.Meta.SimpM Bool := fun y => pure true match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a) (Lean.Meta.Simp.synthesizeArgs.synthesizeInstance lemmaName)
def
Lean.Meta.Simp.synthesizeArgs.synthesizeInstance
(lemmaName : Lean.Name)
(x : Lean.Expr)
(type : Lean.Expr)
:
Equations
- Lean.Meta.Simp.synthesizeArgs.synthesizeInstance lemmaName x type = do let a ← liftM (Lean.Meta.trySynthInstance type none) match a with | Lean.LOption.some val => do let a ← Lean.Meta.withReducibleAndInstances (liftM (Lean.Meta.isDefEq x val)) if a = true then pure true else let cls := `Meta.Tactic.simp.discharge; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM Bool := fun y => pure false if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lemmaName ++ Lean.toMessageData ", failed to assign instance" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "\nsythesized value" ++ Lean.toMessageData (Lean.indentExpr val) ++ Lean.toMessageData "\nis not definitionally equal to" ++ Lean.toMessageData (Lean.indentExpr x) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => let cls := `Meta.Tactic.simp.discharge; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM Bool := fun y => pure false if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lemmaName ++ Lean.toMessageData ", failed to synthesize instance" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.Meta.Simp.tryLemmaWithExtraArgs?
(e : Lean.Expr)
(lemma : Lean.Meta.SimpLemma)
(numExtraArgs : Nat)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.tryLemmaWithExtraArgs? e lemma numExtraArgs discharge? = Lean.Meta.withNewMCtxDepth do let val ← liftM (Lean.Meta.SimpLemma.getValue lemma) let type ← liftM (Lean.Meta.inferType val) let discr ← liftM (Lean.Meta.forallMetaTelescopeReducing type none Lean.MetavarKind.natural) let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (xs, bis, type) => do let a ← liftM (Lean.Meta.instantiateMVars type) let type ← liftM (Lean.Meta.whnf a) let lhs : Lean.Expr := Lean.Expr.appArg! (Lean.Expr.appFn! type) Lean.Meta.Simp.tryLemmaCore lhs xs bis val type e lemma numExtraArgs discharge?
def
Lean.Meta.Simp.tryLemma?
(e : Lean.Expr)
(lemma : Lean.Meta.SimpLemma)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.tryLemma? e lemma discharge? = Lean.Meta.withNewMCtxDepth do let val ← liftM (Lean.Meta.SimpLemma.getValue lemma) let type ← liftM (Lean.Meta.inferType val) let discr ← liftM (Lean.Meta.forallMetaTelescopeReducing type none Lean.MetavarKind.natural) let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (xs, bis, type) => do let a ← liftM (Lean.Meta.instantiateMVars type) let type ← liftM (Lean.Meta.whnf a) let lhs : Lean.Expr := Lean.Expr.appArg! (Lean.Expr.appFn! type) let a ← Lean.Meta.Simp.tryLemmaCore lhs xs bis val type e lemma 0 discharge? match a with | some result => pure (some result) | none => let lhsNumArgs := Lean.Expr.getAppNumArgs lhs; let eNumArgs := Lean.Expr.getAppNumArgs e; if eNumArgs > lhsNumArgs then Lean.Meta.Simp.tryLemmaCore lhs xs bis val type e lemma (eNumArgs - lhsNumArgs) discharge? else pure none
def
Lean.Meta.Simp.rewrite
(e : Lean.Expr)
(s : Lean.Meta.DiscrTree Lean.Meta.SimpLemma)
(erased : Std.PHashSet Lean.Name)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
(tag : String)
:
Equations
- Lean.Meta.Simp.rewrite e s erased discharge? tag = (fun inErasedSet => do let candidates ← liftM (Lean.Meta.DiscrTree.getMatchWithExtra s e) if Array.isEmpty candidates = true then let cls := `Debug.Meta.Tactic.simp; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Meta.SimpM Lean.Meta.Simp.Result := fun y => pure { expr := e, proof? := none } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "no theorems found for " ++ Lean.toMessageData tag ++ Lean.toMessageData "-rewriting " ++ Lean.toMessageData e ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let candidates := Array.insertionSort candidates fun e₁ e₂ => decide (e₁.fst.priority > e₂.fst.priority); do let r ← forIn candidates { fst := none, snd := PUnit.unit } fun x r => match x with | (lemma, numExtraArgs) => let r := r.snd; if inErasedSet lemma = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do let a ← Lean.Meta.Simp.tryLemmaWithExtraArgs? e lemma numExtraArgs discharge? match a with | some result => pure (ForInStep.done { fst := some result, snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.Meta.SimpM Lean.Meta.Simp.Result := fun y => pure { expr := e, proof? := none } match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a) (Lean.Meta.Simp.rewrite.inErasedSet erased)
def
Lean.Meta.Simp.rewrite.inErasedSet
(erased : Std.PHashSet Lean.Name)
(lemma : Lean.Meta.SimpLemma)
:
Equations
- Lean.Meta.Simp.rewrite.inErasedSet erased lemma = match lemma.name? with | none => false | some name => Std.PersistentHashSet.contains erased name
Equations
- Lean.Meta.Simp.rewriteCtorEq? e = Lean.Meta.withReducibleAndInstances (match Lean.Expr.eq? e with | none => pure none | some (x, lhs, rhs) => do let lhs ← Lean.Meta.whnf lhs let rhs ← Lean.Meta.whnf rhs let env ← Lean.getEnv let _discr : Option (Lean.ConstructorVal × Array Lean.Expr) := Lean.Expr.constructorApp? env rhs match Lean.Expr.constructorApp? env lhs, Lean.Expr.constructorApp? env rhs with | some (c₁, x), some (c₂, x_1) => if (c₁.toConstantVal.name != c₂.toConstantVal.name) = true then Lean.Meta.withLocalDeclD `h e fun h => do let a ← Lean.Meta.mkNoConfusion (Lean.mkConst `False) h let a ← Lean.Meta.mkLambdaFVars #[h] a false true let a ← Lean.Meta.mkEqFalse' a pure (some { expr := Lean.mkConst `False, proof? := some a }) else pure none | x, x_1 => pure none)
@[inline]
Equations
- Lean.Meta.Simp.tryRewriteCtorEq e x = do let a ← liftM (Lean.Meta.Simp.rewriteCtorEq? e) match a with | some r => pure (Lean.Meta.Simp.Step.done r) | none => x
Equations
- Lean.Meta.Simp.rewriteUsingDecide? e = Lean.Meta.withReducibleAndInstances (if (Lean.Expr.hasFVar e || Lean.Expr.hasMVar e || Lean.Expr.isConstOf e `True || Lean.Expr.isConstOf e `False) = true then pure none else do let r ← tryCatch (do let d ← Lean.Meta.mkDecide e let r ← Lean.Meta.withDefault (Lean.Meta.whnf d) if Lean.Expr.isConstOf r `Bool.true = true then do let a ← Lean.Meta.mkEqRefl (Lean.mkConst `Bool.true) pure (some { expr := Lean.mkConst `True, proof? := some (Lean.mkAppN (Lean.mkConst `eq_true_of_decide) #[e, Lean.Expr.appArg! d, a]) }) else if Lean.Expr.isConstOf r `Bool.false = true then do let _ ← Lean.Meta.mkEqRefl d let a ← Lean.Meta.mkEqRefl (Lean.mkConst `Bool.false) pure (some { expr := Lean.mkConst `False, proof? := some (Lean.mkAppN (Lean.mkConst `eq_false_of_decide) #[e, Lean.Expr.appArg! d, a]) }) else pure none) fun x => pure none pure r)
@[inline]
def
Lean.Meta.Simp.tryRewriteUsingDecide
(e : Lean.Expr)
(x : Lean.Meta.SimpM Lean.Meta.Simp.Step)
:
Equations
- Lean.Meta.Simp.tryRewriteUsingDecide e x = do let a ← read if a.config.decide = true then do let a ← liftM (Lean.Meta.Simp.rewriteUsingDecide? e) match a with | some r => pure (Lean.Meta.Simp.Step.done r) | none => x else x
def
Lean.Meta.Simp.rewritePre
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.rewritePre e discharge? = do let a ← read let lemmas ← pure a.simpLemmas let a ← Lean.Meta.Simp.rewrite e lemmas.pre lemmas.erased discharge? "pre" pure (Lean.Meta.Simp.Step.visit a)
def
Lean.Meta.Simp.rewritePost
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.rewritePost e discharge? = do let a ← read let lemmas ← pure a.simpLemmas let a ← Lean.Meta.Simp.rewrite e lemmas.post lemmas.erased discharge? "post" pure (Lean.Meta.Simp.Step.visit a)
def
Lean.Meta.Simp.preDefault
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.preDefault e discharge? = Lean.Meta.Simp.tryRewriteCtorEq e (Lean.Meta.Simp.rewritePre e discharge?)
def
Lean.Meta.Simp.postDefault
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Equations
- Lean.Meta.Simp.postDefault e discharge? = Lean.Meta.Simp.tryRewriteCtorEq e (Lean.Meta.Simp.tryRewriteUsingDecide e (Lean.Meta.Simp.rewritePost e discharge?))