Lean.Meta.Tactic.Simp.CongrLemmas

Lean.Meta.mkCongrLemma declName prio = (fun onlyMVarsAt => Lean.Meta.withReducible do let c ← Lean.mkConstWithLevelParams declName let a ← Lean.Meta.inferType c let discr ← Lean.Meta.forallMetaTelescopeReducing a none Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (xs, bis, type) => match Lean.Expr.eq? type with | none => Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, equality expected" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") | some (x, lhs, rhs) => Lean.Expr.withApp lhs fun lhsFn lhsArgs => Lean.Expr.withApp rhs fun rhsFn rhsArgs => let _do_jp := fun y => let foundMVars := ∅; do let r ← forIn lhsArgs foundMVars fun lhsArg r => let foundMVars := r; do let r ← let col := (Lean.Expr.collectMVars { visitedExpr := ∅, result := #[] } lhsArg).result; forIn col foundMVars fun mvarId r => let foundMVars := r; let foundMVars := Std.RBTree.insert foundMVars mvarId; do pure PUnit.unit pure (ForInStep.yield foundMVars) let x : Lean.MVarIdSet := r let foundMVars : Lean.MVarIdSet := x pure PUnit.unit pure (ForInStep.yield foundMVars) let x : Lean.MVarIdSet := r let foundMVars : Lean.MVarIdSet := x let i : Nat := 0 let hypothesesPos : Array Nat := #[] let s : Subarray Lean.BinderInfo := toStream bis let r ← forIn xs { fst := i, snd := { fst := hypothesesPos, snd := { fst := s, snd := foundMVars } } } fun x r => let i := r.fst; let x_1 := r.snd; let hypothesesPos := x_1.fst; let x_2 := x_1.snd; let s := x_2.fst; let foundMVars := x_2.snd; match Stream.next? s with | none => pure (ForInStep.done { fst := i, snd := { fst := hypothesesPos, snd := { fst := s, snd := foundMVars } } }) | some (bi, s') => let s := s'; let _do_jp := fun i hypothesesPos foundMVars y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := i, snd := { fst := hypothesesPos, snd := { fst := s, snd := foundMVars } } }); if (Lean.BinderInfo.isExplicit bi && !Std.RBTree.contains foundMVars (Lean.Expr.mvarId! x)) = true then do let a ← Lean.Meta.inferType x let rhsFn? ← Lean.Meta.forallTelescopeReducing a fun ys xType => match Lean.Expr.eq? xType with | none => pure none | some (x, xLhs, xRhs) => let j := 0; do let r ← forIn ys j fun y r => let j := r; do let yType ← Lean.Meta.inferType y let _do_jp : Nat → PUnit → Lean.MetaM (ForInStep Nat) := fun j y => let j := j + 1; do pure PUnit.unit pure (ForInStep.yield j) if onlyMVarsAt yType foundMVars = true then do let y ← pure PUnit.unit _do_jp j y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, argument #" ++ Lean.toMessageData (j + 1) ++ Lean.toMessageData " of parameter #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData " contains unresolved parameter" ++ Lean.toMessageData (Lean.indentExpr yType) ++ Lean.toMessageData "") _do_jp j y let x : Nat := r let j : Nat := x let _do_jp : PUnit → Lean.MetaM (Option Lean.Expr) := fun y => let xRhsFn := Lean.Expr.getAppFn xRhs; let _do_jp := fun y => let _do_jp := fun y => do let r ← let col := Lean.Expr.getAppArgs xRhs; forIn col PUnit.unit fun arg r => if Lean.Expr.isFVar arg = true then do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, parameter #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData " is not a valid hypothesis, the right-hand-side argument is not local variable" ++ Lean.toMessageData (Lean.indentExpr xRhs) ++ Lean.toMessageData "") pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure (some xRhsFn); if (!Std.RBTree.contains foundMVars (Lean.Expr.mvarId! xRhsFn)) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, parameter #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData " is not a valid hypothesis, the right-hand-side head was already resolved" ++ Lean.toMessageData (Lean.indentExpr xRhs) ++ Lean.toMessageData "") _do_jp y; if Lean.Expr.isMVar xRhsFn = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, parameter #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData " is not a valid hypothesis, the right-hand-side head is not a metavariable" ++ Lean.toMessageData (Lean.indentExpr xRhs) ++ Lean.toMessageData "") _do_jp y if onlyMVarsAt xLhs foundMVars = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, parameter #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData " is not a valid hypothesis, the left-hand-side contains unresolved parameters" ++ Lean.toMessageData (Lean.indentExpr xLhs) ++ Lean.toMessageData "") _do_jp y match rhsFn? with | none => do let y ← pure () _do_jp i hypothesesPos foundMVars y | some rhsFn => let foundMVars := Std.RBTree.insert (Std.RBTree.insert foundMVars (Lean.Expr.mvarId! x)) (Lean.Expr.mvarId! rhsFn); let hypothesesPos := Array.push hypothesesPos i; do let y ← pure PUnit.unit _do_jp i hypothesesPos foundMVars y else do let y ← pure PUnit.unit _do_jp i hypothesesPos foundMVars y let x : MProd Nat (MProd (Array Nat) (MProd (Subarray Lean.BinderInfo) Lean.MVarIdSet)) := r match x with | { fst := i, snd := { fst := hypothesesPos, snd := { fst := s, snd := foundMVars } } } => let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.CongrLemma := fun y => pure { theoremName := declName, funName := Lean.Expr.constName! lhsFn, hypothesesPos := hypothesesPos, priority := prio } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "c: " ++ Lean.toMessageData c ++ Lean.toMessageData " : " ++ Lean.toMessageData type ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if (Lean.Expr.isConst lhsFn && Lean.Expr.isConst rhsFn && Lean.Expr.constName! lhsFn == Lean.Expr.constName! rhsFn && Array.size lhsArgs == Array.size rhsArgs) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y) Lean.Meta.mkCongrLemma.onlyMVarsAt

source

def Lean.Meta.mkCongrLemma.onlyMVarsAt (t : Lean.Expr) (mvarSet : Lean.MVarIdSet) :

Bool

Equations

Lean.Meta.mkCongrLemma.onlyMVarsAt t mvarSet = Option.isNone (Lean.Expr.find? (fun e => Lean.Expr.isMVar e && !Std.RBTree.contains mvarSet (Lean.Expr.mvarId! e)) t)

source

def Lean.Meta.addCongrLemma (declName : Lean.Name) (attrKind : Lean.AttributeKind) (prio : Nat) :

Lean.MetaM Unit

Equations

Lean.Meta.addCongrLemma declName attrKind prio = do let lemma ← Lean.Meta.mkCongrLemma declName prio Lean.ScopedEnvExtension.add Lean.Meta.congrExtension lemma attrKind

source

def Lean.Meta.getCongrLemmas :

Lean.MetaM Lean.Meta.CongrLemmas

Equations

Lean.Meta.getCongrLemmas = do let a ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.congrExtension a)