SEq.Tactic.DepRewrite

source

theorem SEq.Tactic.DRewrite.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

source

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

f a ⋯ = f a' h

source

theorem SEq.Tactic.DRewrite.heqL {α β : Sort u} {a : α} {b : β} (h : HEq a b) :

a = cast ⋯ b

source

theorem SEq.Tactic.DRewrite.heqR {α β : Sort u} {a : α} {b : β} (h : HEq a b) :

cast ⋯ a = b

source

inductive SEq.Tactic.DRewrite.CastMode :

Type

Determines which, if any, type-incorrect subterms should be casted along the equality that drewrite is rewriting by.

none : CastMode
Don't insert any casts.
proofs : CastMode
Only insert casts on proofs.
In this mode, it is not permitted to cast subterms of proofs that are not themselves proofs. For example, given y : Fin n, P : Fin n → Prop, p : (x : Fin n) → P x and eq : n = m, we will not rewrite p y : P y to p (eq ▸ y) : P (eq ▸ y).
all : CastMode
Insert as many Eq.recs as necessary.

Instances For

source

instance SEq.Tactic.DRewrite.instBEqCastMode :

BEq CastMode

Equations

SEq.Tactic.DRewrite.instBEqCastMode = { beq := SEq.Tactic.DRewrite.beqCastMode✝ }

source

instance SEq.Tactic.DRewrite.instToStringCastMode :

ToString CastMode

Equations

One or more equations did not get rendered due to their size.

source

def SEq.Tactic.DRewrite.CastMode.toNat :

CastMode → Nat

Equations

Instances For

source

instance SEq.Tactic.DRewrite.instLECastMode :

LE CastMode

Equations

SEq.Tactic.DRewrite.instLECastMode = { le := fun (a b : SEq.Tactic.DRewrite.CastMode) => a.toNat ≤ b.toNat }

source

instance SEq.Tactic.DRewrite.instDecidableLECastMode :

DecidableLE CastMode

Equations

SEq.Tactic.DRewrite.instDecidableLECastMode a b = inferInstanceAs (Decidable (a.toNat ≤ b.toNat))

source

structure SEq.Tactic.DRewrite.Config :

Type

transparency : Lean.Meta.TransparencyMode
offsetCnstrs : Bool
occs : Lean.Meta.Occurrences
castMode : CastMode

Instances For

source

structure SEq.Tactic.DRewrite.Context :

Type

cfg : Config
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.
pHeadIdx : Lean.HeadIndex
pNumArgs : Nat
subst : Lean.Meta.FVarSubst

Instances For

source

@[reducible, inline]

abbrev SEq.Tactic.DRewrite.M (α : Type) :

Type

Monad for computing dabstract. The cache is for visit (not visitAndCast, which has two arguments), and the Nat tracks which occurrence of the pattern we are currently seeing.

Equations

SEq.Tactic.DRewrite.M = ReaderT SEq.Tactic.DRewrite.Context (Lean.MonadCacheT Lean.ExprStructEq Lean.Expr (StateRefT' IO.RealWorld Nat Lean.MetaM))

Instances For

source

def SEq.Tactic.DRewrite.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.)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SEq.Tactic.DRewrite.castBack? (e te x h : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SEq.Tactic.DRewrite.withSubst? {α : Type} (x tx : Lean.Expr) (k : M α) :

M α

Equations

One or more equations did not get rendered due to their size.

Instances For

source

partial def SEq.Tactic.DRewrite.visitAndCast (e : Lean.Expr) (et? : Option Lean.Expr) :

M Lean.Expr

Given e, return e[x/p] (i.e., e with occurrences of p replaced by x). If et? is not none, the output is guaranteed to have type (defeq to) et?.

Does not assume that e is well-typed, but assumes that for all subterms e' of e, e'[x/p] is well-typed. We use this when processing lambdas: to traverse fun (x : α) => b, we add x : α[x/p] to the local context and continue traversing b. x : α[x/p] ⊢ b may be ill-typed, but the output x : α[x/p] ⊢ b[x/p] is well-typed.

source

partial def SEq.Tactic.DRewrite.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?.

source

def SEq.Tactic.DRewrite.dabstract (e p : Lean.Expr) (cfg : Config) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.MVarId.depRewrite (mvarId : MVarId) (e heq : Expr) (symm : Bool := false) (config : SEq.Tactic.DRewrite.Config := { transparency := Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Meta.Occurrences.all, castMode := SEq.Tactic.DRewrite.CastMode.proofs }) :

MetaM Meta.RewriteResult

Rewrite goal mvarId dependently.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SEq.Tactic.DRewrite.depRewriteSeq :

Lean.ParserDescr

rewrite! is like rewrite, but can also rewrite inside types by inserting casts. This means that the 'motive is not type correct' error never occurs, at the expense of potentially creating complicated terms. It is also available as 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.

Equations