Documentation

theorem IRw.iff_trans_eq {p q r : Prop} (h : p ↔ q) (e : q = r) :

p ↔ r

Compose an iff with an equality on its right side.

theorem IRw.imp_congr_of_left {a a' b b' : Prop} (ha : a ↔ a') (hb : a → (b ↔ b')) :

a → b ↔ a' → b'

Transport an implication when the consequent equivalence may use the source antecedent as a logical support fact.

theorem IRw.eq_congr_equiv {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) (x y : α) :

x = y ↔ e x = e y

Transport equality through an equivalence.

theorem IRw.mem_congr_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (x : α) (S : Set α) :

x ∈ S ↔ e x ∈ ⇑e '' S

Transport membership through an equivalence.

theorem IRw.subset_congr_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (S T : Set α) :

S ⊆ T ↔ ⇑e '' S ⊆ ⇑e '' T

Transport subset through an equivalence.

Coherence cleanup for structural binder equivalences #

When recursion enters a binder transported by a structural equivalence E, the source body is instantiated at E.symm y. Atomic rules then transport the pieces of that source value again. For a bare value this produces e (e.symm y), handled by Equiv.apply_symm_apply. Product projections and sets hide that same cancellation behind their constructors. Forward structural transport can also hide a payload beneath a constructor, as in optionCongr e (some x), or beneath function transport. The equations below expose both kinds of structure to the small irw cleanup simp set so normalization can continue recursively through arbitrary compositions.

These are deliberately not global [simp] lemmas. They belong to the normalization protocol of irw's internally constructed structural equivalences.

theorem IRw.prodCongr_symm_apply_fst {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (p : α₂ × β₂) :

((e₁.prodCongr e₂).symm p).1 = e₁.symm p.1

First projection of the inverse product transport.

theorem IRw.prodCongr_symm_apply_snd {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (p : α₂ × β₂) :

((e₁.prodCongr e₂).symm p).2 = e₂.symm p.2

Second projection of the inverse product transport.

theorem IRw.prodCongr_apply_mk {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (x : α₁) (y : β₁) :

(e₁.prodCongr e₂) (x, y) = (e₁ x, e₂ y)

Forward product transport acts componentwise on a constructor.

theorem IRw.sumCongr_apply_inl {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (x : α₁) :

(e₁.sumCongr e₂) (Sum.inl x) = Sum.inl (e₁ x)

Forward sum transport preserves the left constructor and transports its payload.

theorem IRw.sumCongr_apply_inr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (y : β₁) :

(e₁.sumCongr e₂) (Sum.inr y) = Sum.inr (e₂ y)

Forward sum transport preserves the right constructor and transports its payload.

theorem IRw.image_setCongr_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (S : Set β) :

⇑e '' e.setCongr.symm S = S

Equiv.setCongr transports a set by image. Applying the element transport to the inverse transport of a set therefore cancels. This is the set-level analogue of Equiv.apply_symm_apply.

theorem IRw.setCongr_apply_eq_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (S : Set α) :

e.setCongr S = ⇑e '' S

Expose the image representation used by set-valued naturality rules.

theorem IRw.apply_arrowCongr_symm_apply {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (f : α₂ → β₂) (x : α₂) :

eβ ((eα.arrowCongr eβ).symm f (eα.symm x)) = f x

Applying a function transported backwards by arrowCongr to an argument transported backwards, then transporting the result forwards, recovers ordinary target-side application.

theorem IRw.arrowCongr_symm_apply {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (f : α₂ → β₂) (x : α₁) :

(eα.arrowCongr eβ).symm f x = eβ.symm (f (eα x))

Pointwise action of the inverse function-space transport.

theorem IRw.arrowCongr_apply_fun {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (f : α₁ → β₁) :

(eα.arrowCongr eβ) f = fun (x : α₂) => eβ (f (eα.symm x))

Forward function-space transport is conjugation by the domain and codomain equivalences. Stating this at function level lets cleanup descend beneath structural constructors containing a transported function.

theorem IRw.optionCongr_none {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

e.optionCongr none = none

Structural transport preserves Option.none.

theorem IRw.optionCongr_some {α : Type u_1} {β : Type u_2} (e : α ≃ β) (x : α) :

e.optionCongr (some x) = some (e x)

Forward option transport preserves some and transports its payload.

theorem IRw.optionCongr_some_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (x : β) :

e.optionCongr (some (e.symm x)) = some x

Forward transport cancels inverse transport beneath Option.some.

theorem IRw.forall_congr_equiv {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {P : α → Prop} {Q : β → Prop} (h : ∀ (y : β), P (e.symm y) ↔ Q y) :

(∀ (x : α), P x) ↔ ∀ (y : β), Q y

Rewrite a universally quantified proposition using an equivalence of binder types.

theorem IRw.exists_congr_equiv {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {P : α → Prop} {Q : β → Prop} (h : ∀ (y : β), P (e.symm y) ↔ Q y) :

(∃ (x : α), P x) ↔ ∃ (y : β), Q y

Rewrite an existentially quantified proposition using an equivalence of binder types.

theorem IRw.exists_and_left_explicit {α : Sort u} (b : Prop) (p : α → Prop) :

(∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x

Explicit-argument form of exists_and_left, used by the existential guard normalizer.

theorem IRw.forall_guard_to_subtype {α : Sort u_1} {S P : α → Prop} :

(∀ (x : α), S x → P x) ↔ ∀ (x : { x : α // S x }), P ↑x

Turn an implication-guarded universal quantifier into a subtype quantifier.

theorem IRw.exists_guard_to_subtype {α : Sort u_1} {S P : α → Prop} :

(∃ (x : α), S x ∧ P x) ↔ ∃ (x : { x : α // S x }), P ↑x

Turn a conjunction-guarded existential quantifier into a subtype quantifier.

theorem IRw.forall_guard_congr_equiv {α : Sort u_1} {β : Sort u_2} {S : α → Prop} {T : β → Prop} (e : { x : α // S x } ≃ { y : β // T y }) {P : (x : α) → S x → Prop} {Q : (y : β) → T y → Prop} (h : ∀ (y : β) (hy : T y), P ↑(e.symm ⟨y, hy⟩) ⋯ ↔ Q y hy) :

(∀ (x : α) (hx : S x), P x hx) ↔ ∀ (y : β) (hy : T y), Q y hy

Transport a guarded universal directly, preserving ordinary bounded-quantifier syntax.

theorem IRw.exists_guard_congr_equiv {α : Sort u_1} {β : Sort u_2} {S : α → Prop} {T : β → Prop} (e : { x : α // S x } ≃ { y : β // T y }) {P : α → Prop} {Q : β → Prop} (h : ∀ (y : β) (hy : T y), P ↑(e.symm ⟨y, hy⟩) ↔ Q y) :

(∃ (x : α), S x ∧ P x) ↔ ∃ (y : β), T y ∧ Q y

Transport a conjunction-guarded existential directly. The target body is proof-independent, which is the form produced by ordinary bounded-existential notation.

Transport-domain descriptors #

structure IRw.TotalDomain (A : Sort u) (B : Sort v) :

Sort (max (max 1 u) v)

A domain on which the chosen transformation acts everywhere.

equiv : A ≃ B

Instances For

structure IRw.SupportedDomain (A : Type u) (B : Type v) :

Type (max u v)

A domain on which the chosen transformation acts only after establishing support.

sourceSupport : A → Prop
targetSupport : B → Prop
equiv : { a : A // self.sourceSupport a } ≃ { b : B // self.targetSupport b }

Instances For

theorem IRw.eq_congr_supported {α : Type u_1} {β : Type u_2} (d : SupportedDomain α β) (x y : α) (hx : d.sourceSupport x) (hy : d.sourceSupport y) :

x = y ↔ ↑(d.equiv ⟨x, hx⟩) = ↑(d.equiv ⟨y, hy⟩)

Transport an equality of ambient values when both values are known to lie in a supported domain. The target equality is stated on ambient values as well, so support proofs remain an internal implementation detail.

def IRw.supportedSetEquiv {A : Type u} (S : A → Prop) :

{ X : Set A // ∀ ⦃x : A⦄, x ∈ X → S x } ≃ Set { x : A // S x }

Ambient sets supported by S are equivalent to sets of the support subtype.

Equations

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

Instances For

def IRw.SupportedDomain.set {A : Type u} {B : Type v} (d : SupportedDomain A B) :

SupportedDomain (Set A) (Set B)

Supported domains lift structurally to ambient sets whose elements are supported.

Equations

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

Instances For

theorem IRw.forall_iff_forall_guard {A : Sort u} {S P : A → Prop} (outside : ∀ (x : A), ¬S x → P x) :

(∀ (x : A), P x) ↔ ∀ (x : A), S x → P x

Restrict a universal quantifier to a supported domain when its body is automatic outside that domain.

theorem IRw.exists_iff_exists_guard {A : Sort u} {S P : A → Prop} (supported : ∀ (x : A), P x → S x) :

(∃ (x : A), P x) ↔ ∃ (x : A), S x ∧ P x

Restrict an existential quantifier to a supported domain when every witness is supported.

The tactic itself #

Everything below is compile-time code, so it lives in a meta section.

Registries #

@[reducible, inline]

abbrev IRw.SystemId :

Identifier of a registered change-of-coordinates system. Phase 1 uses the head declaration of the supplied isomorphism type; later registry entries are indexed by this identifier.

Equations

IRw.SystemId = Lean.Name

Instances For

structure IRw.Registration :

A system-indexed IRw registration. Higher priorities are considered first, but priorities only resolve otherwise-overlapping rules; exact matches always outrank definitional matches.

system : SystemId
declName : Lean.Name
priority : ℕ

Instances For

@[instance_reducible]

instance IRw.instInhabitedRegistration :

Inhabited Registration

Equations

IRw.instInhabitedRegistration = { default := IRw.instInhabitedRegistration.default }

@[instance_reducible]

instance IRw.instBEqRegistration :

BEq Registration

Equations

IRw.instBEqRegistration = { beq := IRw.instBEqRegistration.beq }

def IRw.instBEqRegistration.beq :

Registration → Registration → Bool

Equations

IRw.instBEqRegistration.beq { system := a, declName := a_1, priority := a_2 } { system := b, declName := b_1, priority := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
IRw.instBEqRegistration.beq x✝¹ x✝ = false

Instances For

Lean.SimpleScopedEnvExtension Lean.Name (Array Lean.Name)

opaque IRw.systemExt :

Transformation/type constructors recognized by irw (for example Graph.Iso and Matroid.Iso).

Lean.SimpleScopedEnvExtension Registration (Array Registration)

opaque IRw.equivExt :

Binder-type equivalence rules used by irw.

Lean.SimpleScopedEnvExtension Registration (Array Registration)

opaque IRw.domainExt :

Primitive total or supported transport-domain rules used by irw.

Lean.SimpleScopedEnvExtension Registration (Array Registration)

opaque IRw.naturalityExt :

Canonicalization rules used only by IRw's private, system-indexed normalizer.

def IRw.registeredSystemForType? (type : Lean.Expr) :

Lean.CoreM (Option SystemId)

Return the registered system whose type constructor is the head of type, if any.

Equations

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

Instances For

def IRw.inferRegistrationSystem (declName : Lean.Name) :

Lean.MetaM SystemId

Infer the unique transformation system mentioned by a registration theorem's telescope.

Equations

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

Instances For

def IRw.validateSystem (declName : Lean.Name) :

Equations

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

Instances For

def IRw.validateEquiv (declName : Lean.Name) :

Equations

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

Instances For

def IRw.validateDomain (declName : Lean.Name) :

Equations

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

Instances For

def IRw.validateNaturality (declName : Lean.Name) :

Equations

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

Instances For

def IRw.naturalitySides (declName : Lean.Name) :

Lean.MetaM (Lean.Expr × Lean.Expr)

Instantiate a naturality theorem and return its oriented left- and right-hand sides.

Equations

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

Instances For

def IRw.validateNaturalityOverlap (system : SystemId) (priority : ℕ) (declName : Lean.Name) :

Reject equal-priority naturality rules whose left sides overlap but whose proposed canonical forms disagree. This makes import/declaration order irrelevant and reports the problem at the second attribute rather than during an unrelated later proof.

Equations

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

Instances For

def IRw.irwEquivAttr :

Equations

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

Instances For

def IRw.irwSystemAttr :

Equations

IRw.irwSystemAttr = Lean.ParserDescr.node `IRw.irwSystemAttr 1024 (Lean.ParserDescr.nonReservedSymbol "irw_system" false)

Instances For

def IRw.irwDomainAttr :

Equations

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

Instances For

def IRw.irwNaturalityAttr :

Equations

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

Instances For

Metaprogramming core #

The engine lives in IRw.Core rather than IRw.Meta: an inner namespace called Meta would be ambiguous with Lean.Meta, which this file has open.

structure IRw.Core.LocalTransport :

A source-side local datum and its target-side representative, together with the equivalence and kernel-checked coherence theorem used to normalize that correspondence.

source : Lean.Expr
target : Lean.Expr
sourceType : Lean.Expr
targetType : Lean.Expr
equiv : Lean.Expr
coherence : Lean.Expr

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedLocalTransport :

Inhabited LocalTransport

Equations

IRw.Core.instInhabitedLocalTransport = { default := IRw.Core.instInhabitedLocalTransport.default }

structure IRw.Core.TransportContext :

Runtime state shared by every IRw subsystem.

system : SystemId
iso : Lean.Expr
locals : Array LocalTransport

Instances For

Inhabited TransportContext

@[instance_reducible]

instance IRw.Core.instInhabitedTransportContext :

Equations

IRw.Core.instInhabitedTransportContext = { default := IRw.Core.instInhabitedTransportContext.default }

def IRw.Core.TransportContext.sourceObject (ctx : TransportContext) :

The source object is the penultimate argument of a registered binary transformation system. Carrier and universe parameters may precede it; the target object is the final argument.

Equations

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

Instances For

Lean.MetaM TransportContext

def IRw.Core.mkTransportContext (iso : Lean.Expr) :

Build the initial context and reject unregistered transformation notions early.

Equations

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

Instances For

inductive IRw.Core.MatchQuality :

exact : MatchQuality
defEq : MatchQuality

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedMatchQuality :

Inhabited MatchQuality

Equations

IRw.Core.instInhabitedMatchQuality = { default := IRw.Core.instInhabitedMatchQuality.default }

def IRw.Core.instBEqMatchQuality.beq :

MatchQuality → MatchQuality → Bool

Equations

IRw.Core.instBEqMatchQuality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[instance_reducible]

instance IRw.Core.instBEqMatchQuality :

BEq MatchQuality

Equations

IRw.Core.instBEqMatchQuality = { beq := IRw.Core.instBEqMatchQuality.beq }

def IRw.Core.instReprMatchQuality.repr :

MatchQuality → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance IRw.Core.instReprMatchQuality :

Repr MatchQuality

Equations

IRw.Core.instReprMatchQuality = { reprPrec := IRw.Core.instReprMatchQuality.repr }

structure IRw.Core.PropResult :

target : Lean.Expr
proof : Lean.Expr

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedPropResult :

Inhabited PropResult

Equations

IRw.Core.instInhabitedPropResult = { default := IRw.Core.instInhabitedPropResult.default }

structure IRw.Core.EquivResult :

target : Lean.Expr
equiv : Lean.Expr

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedEquivResult :

Inhabited EquivResult

Equations

IRw.Core.instInhabitedEquivResult = { default := IRw.Core.instInhabitedEquivResult.default }

structure IRw.Core.SupportedResult :

target : Lean.Expr
sourceSupport : Lean.Expr
targetSupport : Lean.Expr
equiv : Lean.Expr
descriptor : Lean.Expr

Instances For

Inhabited SupportedResult

@[instance_reducible]

instance IRw.Core.instInhabitedSupportedResult :

Equations

IRw.Core.instInhabitedSupportedResult = { default := IRw.Core.instInhabitedSupportedResult.default }

inductive IRw.Core.DomainResult :

total (result : EquivResult) : DomainResult
supported (result : SupportedResult) : DomainResult

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedDomainResult :

Inhabited DomainResult

Equations

IRw.Core.instInhabitedDomainResult = { default := IRw.Core.instInhabitedDomainResult.default }

def IRw.Core.iffSides? (e : Lean.Expr) :

Equations

IRw.Core.iffSides? e = do let e ← Lean.Meta.whnf e if e.isAppOfArity `Iff 2 = true then have args := e.getAppArgs; pure (some (args[0]!, args[1]!)) else pure none

Instances For

def IRw.Core.equivSides? (e : Lean.Expr) :

Equations

IRw.Core.equivSides? e = do let e ← Lean.Meta.whnf e if e.isAppOfArity `Equiv 2 = true then have args := e.getAppArgs; pure (some (args[0]!, args[1]!)) else pure none

Instances For

def IRw.Core.subtypeParts? (e : Lean.Expr) :

Split a Subtype type into its carrier and predicate.

Equations

IRw.Core.subtypeParts? e = do let e ← Lean.Meta.whnf e if e.isAppOfArity `Subtype 2 = true then have args := e.getAppArgs; pure (some (args[0]!, args[1]!)) else pure none

Instances For

def IRw.Core.mkIffRefl (p : Lean.Expr) :

Equations

IRw.Core.mkIffRefl p = Lean.Meta.mkAppM `Iff.refl #[p]

Instances For

def IRw.Core.mkEquivApply (e x : Lean.Expr) :

Apply an Equiv to an argument. An Equiv is not a function, so the application has to go through the FunLike coercion; mkApp on the bare equivalence produces an ill-typed term.

Equations

IRw.Core.mkEquivApply e x = Lean.Meta.mkAppM `DFunLike.coe #[e, x]

Instances For

def IRw.Core.mkEquivSymmApply (e x : Lean.Expr) :

Apply the inverse of an Equiv to an argument.

Equations

IRw.Core.mkEquivSymmApply e x = do let __do_lift ← Lean.Meta.mkAppM `Equiv.symm #[e] IRw.Core.mkEquivApply __do_lift x

Instances For

Lean.MetaM TransportContext

def IRw.Core.TransportContext.pushTotal (ctx : TransportContext) (source target sourceType targetType equiv : Lean.Expr) :

Record the source representative e.symm target introduced beneath a transported binder. The stored coherence theorem is a local normalization rule e source = target.

Equations

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

Instances For

def IRw.Core.checkedPropResult (source : Lean.Expr) (r : PropResult) :

Check every proof produced by the tactic before it can be installed into a goal. This is intentionally more defensive than most tactics: failures in metaprograms are otherwise liable to surface only much later as kernel errors.

Equations

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

Instances For

def IRw.Core.checkedEquivResult (source : Lean.Expr) (r : EquivResult) :

Lean.MetaM EquivResult

Equations

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

Instances For

Lean.MetaM SupportedResult

def IRw.Core.checkedSupportedResult (source : Lean.Expr) (r : SupportedResult) :

Equations

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

Instances For

Lean.MetaM SupportedResult

def IRw.Core.supportedResultFromDescriptor (source descriptor : Lean.Expr) :

Equations

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

Instances For

def IRw.Core.tryRule (declName : Lean.Name) (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Option (MatchQuality × PropResult))

Try a registered theorem by applying the supplied isomorphism as its first explicit argument, then using unification against source to infer all remaining theorem arguments. Failed attempts are backtracked completely.

Equations

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

Instances For

def IRw.Core.tryEquivRule (declName : Lean.Name) (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Option (MatchQuality × EquivResult))

Equations

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

Instances For

def IRw.Core.tryRegisteredEquiv (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Option EquivResult)

Equations

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

Instances For

def IRw.Core.tryCoherentRegisteredEquiv (ctx : TransportContext) (source equiv : Lean.Expr) :

Lean.MetaM (Option EquivResult)

Find the registered binder equivalence which is definitionally the equivalence stored in a supported-domain descriptor. Unlike ordinary binder lookup, coherence with the descriptor can disambiguate two roles whose support subtypes are definitionally equal.

Equations

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

Instances For

Lean.MetaM SupportedResult

def IRw.Core.canonicalizeSupportedResult (ctx : TransportContext) (result : SupportedResult) :

Replace the implementation field of a supported-domain descriptor by a registered, named equivalence when the two are definitionally equal. Naturality rules can then state their target using the public equivalence and the cleanup pass sees the syntactic e (e.symm x) cancellation. This applies equally to primitive supported domains and to structurally derived ones such as supported sets.

Equations

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

Instances For

def IRw.Core.tryDomainRule (declName : Lean.Name) (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Option (MatchQuality × DomainResult))

Equations

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

Instances For

def IRw.Core.registeredDomainCandidates (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Array (Lean.Name × DomainResult))

Equations

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

Instances For

def IRw.Core.tryRegisteredDomain (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM (Option DomainResult)

Equations

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

Instances For

def IRw.Core.tryRegisteredNaturalityProp (ctx : TransportContext) (source : Lean.Expr) :

Try proposition-valued naturality declarations as atomic transport facts. Equality-valued declarations are ignored here and remain private-normalizer rules.

Equations

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

Instances For

def IRw.Core.mkReflEquiv (α : Lean.Expr) :

Lean.MetaM EquivResult

Equations

IRw.Core.mkReflEquiv α = do let e ← Lean.Meta.mkAppM `Equiv.refl #[α] IRw.Core.checkedEquivResult α { target := α, equiv := e }

Instances For

def IRw.Core.isConstApp (e : Lean.Expr) (n : Lean.Name) (arity : ℕ) :

Equations

IRw.Core.isConstApp e n arity = e.isAppOfArity n arity

Instances For

partial def IRw.Core.deriveEquiv (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM EquivResult

Derive an equivalence for a quantified binder type. Domain-specific equivalences are tried first; afterwards the routine structurally closes under elementary type constructors. A final reflexive fallback is intentional: genuinely object-independent binder types (Nat, a fixed index type, etc.) should remain unchanged.

partial def IRw.Core.findDomain (ctx : TransportContext) (source : Lean.Expr) :

Lean.MetaM DomainResult

Resolve a primitive supported/total domain first, then fall back to the legacy total-domain engine and its structural closure.

def IRw.Core.cleanupLemmas :

List Lean.Name

Lemmas used to tidy up the transported proposition.

This must stay a small, targeted list. Running the full default simp set here is actively harmful: lemmas such as Set.image_subset_image_iff and Set.mem_image_equiv rewrite a transported ⇑e '' S ⊆ ⇑e '' T straight back to S ⊆ T, so irw would faithfully build a transport proof and then throw it away, leaving the goal untouched.

Equations

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

Instances For

def IRw.Core.simplifyTarget (ctx : TransportContext) (source : Lean.Expr) (r : PropResult) :

Equations

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

Instances For

def IRw.Core.mkBinaryCongr (ctx : TransportContext) (source : Lean.Expr) (lemmaName : Lean.Name) (rl rr : PropResult) :

Equations

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

Instances For

def IRw.Core.mkNotCongr (ctx : TransportContext) (source : Lean.Expr) (r : PropResult) :

Equations

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

Instances For

def IRw.Core.isNondependentForall (body : Lean.Expr) :

Equations

IRw.Core.isNondependentForall body = !body.hasLooseBVar 0

Instances For

partial def IRw.Core.occursFVar (id : Lean.FVarId) :

Lean.Expr → Bool

partial def IRw.Core.occursExpr (needle : Lean.Expr) :

Lean.Expr → Bool

Syntactic occurrence of an arbitrary expression, rather than only a free variable.

partial def IRw.Core.dependsOnExpr (needle e : Lean.Expr) (seen : Array Lean.FVarId := #[]) :

Check dependency through both an expression and the types of the free variables it contains. The latter matters for an opaque Q x: the term does not spell the source object, but the types of Q and x do.

def IRw.Core.isFixedAtom (ctx : TransportContext) (source : Lean.Expr) :

An opaque proposition is fixed only when it is independent of both the source object and every source-side representative introduced beneath transported binders.

Equations

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

Instances For

partial def IRw.Core.supportProofFromHyp? (goal h : Lean.Expr) (depth : ℕ) :

def IRw.Core.setSubsetSides? (e : Lean.Expr) :

Recognize a set-subset proposition without unfolding it to a dependent function type.

Equations

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

Instances For

partial def IRw.Core.proveSubset? (left right : Lean.Expr) (depth : ℕ) :

Close set support obligations under transitivity of locally available subset hypotheses.

partial def IRw.Core.proveSupport? (ctx : TransportContext) (goal : Lean.Expr) (depth : ℕ := 16) :

Small initial support prover. It intentionally uses only local hypotheses and elementary propositional decomposition; Phase 6 can replace the backend with restricted grind without changing this interface.

def IRw.Core.supportGrindConfig :

Lean.Grind.Config

Resource-bounded grind configuration for support certificates. Arithmetic, extensionality, congruence-closure extras, and the global @[grind] theorem database are deliberately disabled.

Equations

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

Instances For

Lean.MetaM Lean.Meta.Grind.Params

def IRw.Core.mkSupportGrindParams :

Equations

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

Instances For

def IRw.Core.proveSupportWithGrind? (goal : Lean.Expr) :

Try the restricted support-specific grind database and the current local context.

Equations

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

Instances For

def IRw.Core.proveSupport (ctx : TransportContext) (goal : Lean.Expr) :

Equations

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

Instances For

partial def IRw.Core.subtypePropertiesIn (term : Lean.Expr) :

Lean.MetaM (Array Lean.Expr)

Collect support proofs carried by subtype-valued subterms. This exposes facts such as the IsWalk proof bundled into a supported walk when proving support for one of its endpoints.

def IRw.Core.proveSupportUsingTerm (ctx : TransportContext) (goal term : Lean.Expr) :

Prove support using a genuine subtype property contained in term as an explicit premise, then discharge that premise with its bundled proof.

Equations

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

Instances For

def IRw.Core.transportSupportedEquality? (ctx : TransportContext) (source α x y : Lean.Expr) :

Try to transport an equality on an ambient carrier through a supported domain. A candidate is usable only when support for both operands follows from the local context.

Equations

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

Instances For

def IRw.Core.universalSupportCertificate (ctx : TransportContext) (n : Lean.Name) (bi : Lean.BinderInfo) (domain body sourceSupport : Lean.Expr) :

Equations

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

Instances For

def IRw.Core.existentialSupportCertificate (ctx : TransportContext) (n : Lean.Name) (bi : Lean.BinderInfo) (domain pred sourceSupport : Lean.Expr) :

Equations

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

Instances For

def IRw.Core.mkSubtypeType (pred : Lean.Expr) :

Equations

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

Instances For

def IRw.Core.guardedEquivForSubtype? (ctx : TransportContext) (domain sourceSubtype : Lean.Expr) :

Lean.MetaM (Option EquivResult)

Prefer the canonical equivalence supplied by a supported domain when a syntactic guard is definitionally that domain's support predicate. This keeps bounded and inferred-supported quantifiers on one coherence path.

Equations

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

Instances For

Reordering batched guarded universal quantifiers #

Lean elaborates

∀ I J K, gI → gJ → gK → P

as one forallE telescope. The bounded-quantifier transporter, intentionally, only consumes the local shape ∀ I, gI → .... Rather than teach bounded transport a second semantics for batched guards, we normalize a leading universal telescope by moving any registered unary guard directly after the binder it guards. The normalization is accompanied by an explicit iff proof, the ordinary recursive transporter is run on the normalized proposition, and the transported telescope is then permuted back to the source ordering.

This layer is deliberately only a telescope permutation. It neither invents a transport nor interprets arbitrary propositions as bounds: a guard is movable only if bundling it with its binder produces a subtype accepted by @[irw_equiv].

structure IRw.Core.GuardMove :

binderIdx : ℕ
guardIdx : ℕ

Instances For

@[instance_reducible]

instance IRw.Core.instInhabitedGuardMove :

Inhabited GuardMove

Equations

IRw.Core.instInhabitedGuardMove = { default := IRw.Core.instInhabitedGuardMove.default }

def IRw.Core.isMovedGuard (moves : Array GuardMove) (idx : ℕ) :

Equations

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

Instances For

def IRw.Core.guardForBinder? (moves : Array GuardMove) (idx : ℕ) :

Option ℕ

Equations

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

Instances For

def IRw.Core.dependsOnLaterTelescopeFVar (guardTy : Lean.Expr) (fvars : Array Lean.Expr) (i : ℕ) :

A candidate guard may be moved directly after binder i only when its type does not mention a later telescope variable. This is slightly conservative (a later variable may itself eventually be moved earlier), but it makes the permutation criterion local and prevents us from manufacturing an ill-scoped dependent telescope.

Equations

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

Instances For

def IRw.Core.findGuardForBinder (ctx : TransportContext) (fvars : Array Lean.Expr) (moves : Array GuardMove) (i : ℕ) :

Lean.MetaM (Option ℕ)

Find a later proposition binder which is a registered guard for fvars[i].

Equations

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

Instances For

def IRw.Core.findGuardMoves (ctx : TransportContext) (fvars : Array Lean.Expr) :

Lean.MetaM (Array GuardMove)

Discover all independent registered guards in a universal telescope. A proof binder is used at most once.

Equations

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

Instances For

def IRw.Core.guardNormalizationOrder (size : ℕ) (moves : Array GuardMove) :

Array ℕ

Remove moved guards from their original positions and insert each immediately after its guarded binder. All other binders keep their relative order.

Equations

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

Instances For

def IRw.Core.isIdentityOrder (order : Array ℕ) :

Equations

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

Instances For

def IRw.Core.invertOrder (order : Array ℕ) :

Array ℕ

Invert an array representation of a permutation.

Equations

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

Instances For

def IRw.Core.telescopeOrderValid (fvars : Array Lean.Expr) (order : Array ℕ) :

Check that reordering the local declarations according to order respects all telescope dependencies. The result is checked again by the kernel when the permutation proof is built; this pre-check exists to turn a scope problem into a useful trace instead of an opaque abstraction failure.

Equations

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

Instances For

def IRw.Core.permuteForallTelescope (source : Lean.Expr) (fvars : Array Lean.Expr) (tail : Lean.Expr) (order : Array ℕ) :

Permute the first fvars.size universal/implication binders of source according to order. fvars and tail must come from opening that prefix of source. Both directions are constructed by pure lambda/application reshuffling and then kernel-checked.

Equations

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

Instances For

def IRw.Core.hasLeadingForallSupportGuard (r : PropResult) (sr : SupportedResult) :

Whether a transported result still exposes the candidate domain's support immediately after its leading data binder. When role candidates share a raw source carrier, eliminating this guard is useful evidence that the body actually identifies the candidate's intended role.

Equations

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

Instances For

def IRw.Core.hasLeadingExistsSupportGuard (r : PropResult) (sr : SupportedResult) :

Existential analogue of hasLeadingForallSupportGuard.

Equations

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

Instances For

partial def IRw.Core.guardAfterExists? (body : Lean.Expr) (crossed : Array Lean.FVarId := #[]) :

Lean.MetaM (Option (Lean.Expr × ℕ))

Find the first conjunct after a nonempty leading existential telescope. The conjunct is returned only when it is independent of every witness crossed on the way.

partial def IRw.Core.insertGuardAfterExists (guard body : Lean.Expr) :

Insert guard as the first conjunct after a leading existential telescope.

partial def IRw.Core.hoistGuardAcrossExists (guard body : Lean.Expr) :

Hoist a fixed first conjunct from the end of a leading existential telescope. Every step is an explicit exists_congr_equiv followed by exists_and_left_explicit, so the returned equivalence is kernel checked rather than justified by a syntactic rewrite.

partial def IRw.Core.transportBoundedForall (ctx : TransportContext) (source : Lean.Expr) (n : Lean.Name) (domain body : Lean.Expr) (bi : Lean.BinderInfo) :

Transport a bounded universal ∀ x, guard x → body x through an equivalence between the corresponding guarded subtypes. The generated target is again an ordinary guarded forall.

partial def IRw.Core.transportBoundedExists (ctx : TransportContext) (source domain pred : Lean.Expr) :

Transport a bounded existential ∃ x, guard x ∧ body x through an equivalence between the corresponding guarded subtypes.

partial def IRw.Core.transportSupportedForall (ctx : TransportContext) (source : Lean.Expr) (n : Lean.Name) (domain body : Lean.Expr) (bi : Lean.BinderInfo) (sr : SupportedResult) :

Transport an unguarded universal through a supported domain after proving that its body is automatic outside the source support. The first supported normal form deliberately exposes the target guard.

partial def IRw.Core.transportSupportedExists (ctx : TransportContext) (source domain pred : Lean.Expr) (sr : SupportedResult) :

Transport an unguarded existential through a supported domain after proving that every source witness is supported. The first supported normal form deliberately exposes the target guard.

partial def IRw.Core.transportAmbiguousSupportedForall? (ctx : TransportContext) (source : Lean.Expr) (n : Lean.Name) (domain body : Lean.Expr) (bi : Lean.BinderInfo) :

When several exact supported domains share the same raw carrier, use the quantified body as delayed role evidence. A candidate is committed only if both its support certificate and recursive proposition transport succeed.

partial def IRw.Core.transportAmbiguousSupportedExists? (ctx : TransportContext) (source domain pred : Lean.Expr) :

Existential counterpart of transportAmbiguousSupportedForall?.

partial def IRw.Core.transportBatchedForall (ctx : TransportContext) (source : Lean.Expr) :

Normalize non-adjacent registered guards in a leading universal telescope, recurse through the already-existing bounded-forall path, and restore the transported telescope to the original binder ordering. This handles batched syntax such as

∀ I J K, I ⊆ E → J ⊆ E → K ⊆ E → P I J K

without duplicating bounded-quantifier transport logic.

partial def IRw.Core.transportBatchedExists (ctx : TransportContext) (source : Lean.Expr) :

Hoist the first guard in a batched existential across all later witnesses, transport the resulting adjacent guarded existential, and restore the batched target shape. Recursion handles the remaining guards after the first supported witness is entered.

partial def IRw.Core.transportProp (ctx : TransportContext) (source : Lean.Expr) :