Dependent rewrite tactic

theorem Mathlib.Tactic.DepRewrite.dcongrArg {α : Sort u} {a a' : α} {β : (a' : α) → a = a' → Sort v} (h : a = a') (f : (a' : α) → (h : a = a') → β a' h) : f a ⋯ = ⋯ ▸ f a' h

theorem Mathlib.Tactic.DepRewrite.nddcongrArg {α : Sort u} {a a' : α} {β : Sort v} (h : a = a') (f : (a' : α) → a = a' → β) : f a ⋯ = f a' h

theorem Mathlib.Tactic.DepRewrite.heqL {α β : Sort u} {a : α} {b : β} (h : a ≍ b) : a = cast ⋯ b

theorem Mathlib.Tactic.DepRewrite.heqR {α β : Sort u} {a : α} {b : β} (h : a ≍ b) : cast ⋯ a = b

inductive Mathlib.Tactic.DepRewrite.CastMode : Type

See Config.castMode.

• proofs : CastMode

  Only insert casts on proofs.

  In this mode, it is not permitted to cast subterms of proofs that are not themselves proofs.

• all : CastMode

  Insert casts whenever necessary.

instance Mathlib.Tactic.DepRewrite.instBEqCastMode : BEq CastMode

instance Mathlib.Tactic.DepRewrite.instToStringCastMode : ToString CastMode

def Mathlib.Tactic.DepRewrite.CastMode.toNat : CastMode → Nat

Embedding of CastMode into naturals.

instance Mathlib.Tactic.DepRewrite.instLECastMode : LE CastMode

instance Mathlib.Tactic.DepRewrite.instDecidableLECastMode : DecidableLE CastMode

structure Mathlib.Tactic.DepRewrite.Config : Type

Configures the behavior of the rewrite! and rw! tactics.

• transparency : Lean.Meta.TransparencyMode

  Which transparency level to use when unifying the rewrite rule's LHS against subterms of the term being rewritten.

• occs : Lean.Meta.Occurrences

  Which occurrences to rewrite.

• castMode : CastMode

  The cast mode specifies when rw! is permitted to insert casts in order to correct subterms that become type-incorect as a result of rewriting.

  For example, given P : Nat → Prop, f : (n : Nat) → P n → Nat and h : P n₀, rewriting f n₀ h by eq : n₀ = n₁ produces f n₁ h, where h does not typecheck at P n₁. The tactic will cast h to eq ▸ h : P n₁ iff .proofs ≤ castMode.

structure Mathlib.Tactic.DepRewrite.Context : Type

ReaderT context for M.

• cfg : Config

  Configuration.

• p : Lean.Expr

  The pattern to generalize over.

• x : Lean.Expr

  The free variable to substitute for p.

• h : Lean.Expr

  A proof of p = x. Must be an fvar.

• Δ : Array (Lean.FVarId × Lean.Expr)

  The list of value-less binders (cdecls and nondependent ldecls) that we have introduced. Together with each binder, we store its type abstracted over x and h, and with all occurrences of previous entries in Δ casted along the abstracting equation.

  E.g., if the local context is a : T, b : U, we store (a, Ma) where Ma := fun (x' : α) (h' : x = x') => T[x'/x, h'/h] and (b, fun (x' : α) (h' : x = x') => U[x'/x, h'/h, (Eq.rec (motive := Ma) a h)/a]) See the docstring on visitAndCast.

• δ : Std.HashSet Lean.FVarId

  The set of all dependent ldecls that we have introduced.

• pHeadIdx : Lean.HeadIndex

  Cached p.toHeadIndex.

• pNumArgs : Nat

  Cached p.toNumArgs.

def Mathlib.Tactic.DepRewrite.canUseCache (cacheOcc dCacheOcc currOcc : Nat) : Lean.Meta.Occurrences → Bool

We use a cache entry iff the upcoming traversal would abstract exactly the same occurrences as the cached traversal.

@[reducible, inline]

abbrev Mathlib.Tactic.DepRewrite.M (α : Type) : Type

Monad for computing dabstract.

The Nat state tracks which occurrence of the pattern we are about to see, 1-indexed (so the initial value is 1).

The cache stores results of visit together with

• the Nat state before the cached call; and
• the difference in the state resulting from the call. We store these because even if the cache hits, we must update the state as if the call had been made. Storing the difference suffices because the state increases monotonically. See also canUseCache.

def Mathlib.Tactic.DepRewrite.checkCastAllowed (e t : Lean.Expr) (castMode : CastMode) : Lean.MetaM Unit

Check that casting e : t is allowed in the current mode. (We don't need to know what type e is cast to: we only check the sort of t, and it cannot change.)

def Mathlib.Tactic.DepRewrite.zetaDelta (e : Lean.Expr) (fvars : Std.HashSet Lean.FVarId) : Lean.MetaM Lean.Expr

In e, inline the values of those ldecls that appear in fvars.

def Mathlib.Tactic.DepRewrite.castBack? (e te x h : Lean.Expr) (Δ : Array (Lean.FVarId × Lean.Expr)) (δ : Std.HashSet Lean.FVarId) : Lean.MetaM (Option Lean.Expr)

If e : te is a term whose type mentions x, h (the generalization variables) or entries in Δ/δ, return h.symm ▸ e : te[p/x, rfl/h, …]. Otherwise return none.

def Mathlib.Tactic.DepRewrite.castBack?.motive (te x h : Lean.Expr) (Δ : Array (Lean.FVarId × Lean.Expr)) (δ : Std.HashSet Lean.FVarId) : Lean.MetaM Lean.Expr

Compute the motive that casts e back to te[p/x, rfl/h, …].

def Mathlib.Tactic.DepRewrite.castFwd (e te p x h : Lean.Expr) (Δ : Array (Lean.FVarId × Lean.Expr)) (δ : Std.HashSet Lean.FVarId) : Lean.MetaM Lean.Expr

Cast e : te[p/x, rfl/h, ...] to h ▸ e : te.

partial def Mathlib.Tactic.DepRewrite.visitAndCast (e : Lean.Expr) (et? : Option Lean.Expr) : M Lean.Expr

Given e, return e' where e' has had

• the occurrences of p in ctx.cfg.occs replaced by x; and
• subterms cast as appropriate in order to make e' type-correct.

If et? is not none, the output is guaranteed to have type (defeq to) et?.

We do not assume that e is well-typed. We use this when processing binders: to traverse ∀ (x : α), β, we obtain α' ← visit α, add x : α' to the local context and continue traversing β. Although x : α' ⊢ β may not hold, the output β' should have x : α' ⊢ β' (otherwise we have a bug).

To achieve this, we maintain the invariant that all entries in the local context that we have introduced can be translated back to their original (pre-visit) types using the motive computed by castBack?.motive. (But we have not attempted to prove this.)

partial def Mathlib.Tactic.DepRewrite.visit (e : Lean.Expr) (et? : Option Lean.Expr) : M Lean.Expr

Like visitAndCast, but does not insert casts at the top level. The expected types of certain subterms are computed from et?.

partial def Mathlib.Tactic.DepRewrite.visitInner (e : Lean.Expr) (et? : Option Lean.Expr) : M Lean.Expr

See visit.

def Mathlib.Tactic.DepRewrite.dabstract (e p : Lean.Expr) (cfg : Config) : Lean.MetaM Lean.Expr

Analogue of kabstract with support for inserting casts.

def Lean.MVarId.depRewrite (mvarId : MVarId) (e heq : Expr) (symm : Bool := false) (config : Mathlib.Tactic.DepRewrite.Config := { }) : MetaM Meta.RewriteResult

Analogue of Lean.MVarId.rewrite with support for inserting casts.

def Mathlib.Tactic.DepRewrite.depRewriteSeq : Lean.ParserDescr

rewrite! is like rewrite, but can also insert casts to adjust types that depend on the LHS of a rewrite. It is available as an ordinary tactic and a conv tactic.

The sort of casts that are inserted is controlled by the castMode configuration option. By default, only proof terms are casted; by proof irrelevance, this adds no observable complexity.

With rewrite! +letAbs (castMode := .all), casts are inserted whenever necessary. This means that the 'motive is not type correct' error never occurs, at the expense of creating potentially complicated terms.

def Mathlib.Tactic.DepRewrite.depRwSeq : Lean.ParserDescr

rw! is like rewrite!, but also calls dsimp to simplify the result after every substitution. It is available as an ordinary tactic and a conv tactic.

def Mathlib.Tactic.DepRewrite.depRewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : Config := { }) : Lean.Elab.Tactic.TacticM Unit

Apply rewrite! to the goal.

def Mathlib.Tactic.DepRewrite.depRewriteLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : Config := { }) : Lean.Elab.Tactic.TacticM Unit

Apply rewrite! to a local declaration.

def Mathlib.Tactic.DepRewrite.elabDepRewriteConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Elaborate DepRewrite.Config.

def Mathlib.Tactic.DepRewrite.evalDepRewriteSeq : Lean.Elab.Tactic.Tactic

rewrite! is like rewrite, but can also insert casts to adjust types that depend on the LHS of a rewrite. It is available as an ordinary tactic and a conv tactic.

The sort of casts that are inserted is controlled by the castMode configuration option. By default, only proof terms are casted; by proof irrelevance, this adds no observable complexity.

With rewrite! +letAbs (castMode := .all), casts are inserted whenever necessary. This means that the 'motive is not type correct' error never occurs, at the expense of creating potentially complicated terms.

def Mathlib.Tactic.DepRewrite.evalDepRwSeq : Lean.Elab.Tactic.Tactic

rw! is like rewrite!, but also calls dsimp to simplify the result after every substitution. It is available as an ordinary tactic and a conv tactic.

def Mathlib.Tactic.DepRewrite.Conv.depRewrite : Lean.ParserDescr

rewrite! is like rewrite, but can also insert casts to adjust types that depend on the LHS of a rewrite. It is available as an ordinary tactic and a conv tactic.

The sort of casts that are inserted is controlled by the castMode configuration option. By default, only proof terms are casted; by proof irrelevance, this adds no observable complexity.

With rewrite! +letAbs (castMode := .all), casts are inserted whenever necessary. This means that the 'motive is not type correct' error never occurs, at the expense of creating potentially complicated terms.

def Mathlib.Tactic.DepRewrite.Conv.depRw : Lean.ParserDescr

rw! is like rewrite!, but also calls dsimp to simplify the result after every substitution. It is available as an ordinary tactic and a conv tactic.

def Mathlib.Tactic.DepRewrite.Conv.depRewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : Config := { }) : Lean.Elab.Tactic.TacticM Unit

Apply rewrite! to the goal.

def Mathlib.Tactic.DepRewrite.Conv.depRwTarget (stx : Lean.Syntax) (symm : Bool) (config : Config := { }) : Lean.Elab.Tactic.TacticM Unit

Apply rw! to the goal.

def Mathlib.Tactic.DepRewrite.Conv.depRwLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : Config := { }) : Lean.Elab.Tactic.TacticM Unit

Apply rw! to a local declaration.

def Mathlib.Tactic.DepRewrite.Conv.evalDepRewriteSeq : Lean.Elab.Tactic.Tactic

rewrite! is like rewrite, but can also insert casts to adjust types that depend on the LHS of a rewrite. It is available as an ordinary tactic and a conv tactic.

The sort of casts that are inserted is controlled by the castMode configuration option. By default, only proof terms are casted; by proof irrelevance, this adds no observable complexity.

With rewrite! +letAbs (castMode := .all), casts are inserted whenever necessary. This means that the 'motive is not type correct' error never occurs, at the expense of creating potentially complicated terms.

def Mathlib.Tactic.DepRewrite.Conv.evalDepRwSeq : Lean.Elab.Tactic.Tactic

rw! is like rewrite!, but also calls dsimp to simplify the result after every substitution. It is available as an ordinary tactic and a conv tactic.