MatchingLogic.EntryIII.Generated

@[instance_reducible]

noncomputable def MatchingLogic.instDecidableEqPatternNatGenerated {S : Signature} : DecidableEq (Pattern S ℕ)

Local decidable equality used by the generated-submodel construction.

Equations

• MatchingLogic.instDecidableEqPatternNatGenerated = Classical.decEq (MatchingLogic.Pattern S ℕ)

Application-context composition

def MatchingLogic.AppCtx.comp {S : Signature} {Var : Type} (outer inner : AppCtx S Var) : AppCtx S Var

Context composition: outer.comp inner plugs inner into outer.

Equations

• MatchingLogic.AppCtx.hole.comp inner = inner
• (MatchingLogic.AppCtx.node sigma i args tail).comp inner = MatchingLogic.AppCtx.node sigma i args (tail.comp inner)

@[simp]

theorem MatchingLogic.AppCtx.plug_comp {S : Signature} {Var : Type} (outer inner : AppCtx S Var) (p : Pattern S Var) : (outer.comp inner).plug p = outer.plug (inner.plug p)

Definition 74: generated canonical model

def MatchingLogic.canonicalStep {S : Signature} (parent child : CanonicalCarrier S) : Prop

One backwards canonical step, from an output world to one component world of a tuple producing it.

Equations

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

@[simp]

theorem MatchingLogic.canonicalStep_iff {S : Signature} (parent child : CanonicalCarrier S) : canonicalStep parent child ↔ ∃ (sigma : S.Sym) (components : Fin (S.arity sigma) → CanonicalCarrier S) (i : Fin (S.arity sigma)), parent ∈ canonicalInterp sigma components ∧ child = components i

def MatchingLogic.Generated {S : Signature} (root world : CanonicalCarrier S) : Prop

The smallest set of canonical worlds containing root and closed under backwards canonical symbol steps.

Equations

• MatchingLogic.Generated root world = Relation.ReflTransGen MatchingLogic.canonicalStep root world

@[reducible, inline]

abbrev MatchingLogic.GeneratedCarrier {S : Signature} (root : CanonicalCarrier S) : Type

The carrier of the submodel generated by root.

Equations

• MatchingLogic.GeneratedCarrier root = { world : MatchingLogic.CanonicalCarrier S // MatchingLogic.Generated root world }

theorem MatchingLogic.GeneratedCarrier.isMCS {S : Signature} {root : CanonicalCarrier S} (world : GeneratedCarrier root) : IsMCS ↑↑world

A generated point still carries its canonical MCS proof.

theorem MatchingLogic.GeneratedCarrier.witnessed {S : Signature} {root : CanonicalCarrier S} (world : GeneratedCarrier root) : Witnessed ↑↑world

A generated point still carries its canonical witnessedness proof.

def MatchingLogic.generatedRoot {S : Signature} (root : CanonicalCarrier S) : GeneratedCarrier root

The root as a point of its generated carrier.

Equations

• MatchingLogic.generatedRoot root = ⟨root, ⋯⟩

def MatchingLogic.generatedInterp {S : Signature} (root : CanonicalCarrier S) (sigma : S.Sym) (components : Fin (S.arity sigma) → GeneratedCarrier root) : Set (GeneratedCarrier root)

The canonical interpretation restricted to generated inputs and outputs.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.generatedModel {S : Signature} (root : CanonicalCarrier S) : Model S

The submodel generated backwards from root.

Equations

• MatchingLogic.generatedModel root = { carrier := MatchingLogic.GeneratedCarrier root, nonempty := ⋯, interp := MatchingLogic.generatedInterp root }

@[simp]

theorem MatchingLogic.mem_generatedInterp {S : Signature} {root : CanonicalCarrier S} {sigma : S.Sym} {components : Fin (S.arity sigma) → GeneratedCarrier root} {world : GeneratedCarrier root} : world ∈ generatedInterp root sigma components ↔ ↑world ∈ canonicalInterp sigma fun (i : Fin (S.arity sigma)) => ↑(components i)

@[simp]

theorem MatchingLogic.generatedModel_interp {S : Signature} (root : CanonicalCarrier S) (sigma : S.Sym) (components : Fin (S.arity sigma) → GeneratedCarrier root) : (generatedModel root).interp sigma components = generatedInterp root sigma components

theorem MatchingLogic.mem_generatedModel_interp {S : Signature} {root : CanonicalCarrier S} {sigma : S.Sym} {components : Fin (S.arity sigma) → GeneratedCarrier root} {world : GeneratedCarrier root} : world ∈ (generatedModel root).interp sigma components ↔ ↑world ∈ canonicalInterp sigma fun (i : Fin (S.arity sigma)) => ↑(components i)

Definitions 75--76: generating paths and their contexts

inductive MatchingLogic.GeneratingPath {S : Signature} (root : CanonicalCarrier S) : CanonicalCarrier S → List (Coord S) → Prop

The source's explicit generating-path relation. A new coordinate is appended when an output world is followed to one of its argument worlds.

• root {S : Signature} {root : CanonicalCarrier S} : GeneratingPath root root []
• tail {S : Signature} {root parent : CanonicalCarrier S} {path : List (Coord S)} {sigma : S.Sym} {components : Fin (S.arity sigma) → CanonicalCarrier S} {i : Fin (S.arity sigma)} : GeneratingPath root parent path → parent ∈ canonicalInterp sigma components → GeneratingPath root (components i) (path ++ [⟨sigma, i⟩])

def MatchingLogic.generatingStepContext {S : Signature} (e : Coord S) : AppCtx S ℕ

The one-step context for a generating coordinate, with top in all sibling positions as required by source Definition 76.

Equations

• MatchingLogic.generatingStepContext e = MatchingLogic.AppCtx.node e.fst e.snd (fun (x : Fin (S.arity e.fst)) => MatchingLogic.Pattern.tp) MatchingLogic.AppCtx.hole

@[simp]

theorem MatchingLogic.generatingStepContext_plug {S : Signature} (e : Coord S) (p : Pattern S ℕ) : (generatingStepContext e).plug p = Pattern.app e.fst (Function.update (fun (x : Fin (S.arity e.fst)) => Pattern.tp) e.snd p)

def MatchingLogic.generatingContext {S : Signature} (path : List (Coord S)) : AppCtx S ℕ

The symbol context C_path, obtained by nesting one-step contexts in path order.

Equations

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

@[simp]

theorem MatchingLogic.generatingContext_nil {S : Signature} : generatingContext [] = AppCtx.hole

theorem MatchingLogic.generatingContext_append {S : Signature} (path : List (Coord S)) (e : Coord S) : generatingContext (path ++ [e]) = (generatingContext path).comp (generatingStepContext e)

theorem MatchingLogic.CanonicalCarrier.top_mem {S : Signature} (world : CanonicalCarrier S) : Pattern.tp ∈ ↑world

Every canonical MCS contains top.

theorem MatchingLogic.GeneratingPath.generated {S : Signature} {root world : CanonicalCarrier S} {path : List (Coord S)} (hpath : GeneratingPath root world path) : Generated root world

A source generating path witnesses membership in the reachability closure.

theorem MatchingLogic.Generated.exists_generatingPath {S : Signature} {root world : CanonicalCarrier S} (hgen : Generated root world) : ∃ (path : List (Coord S)), GeneratingPath root world path

Reachability and the paper's explicit generating-path relation agree.

theorem MatchingLogic.GeneratingPath.plug_mem_root {S : Signature} {root world : CanonicalCarrier S} {path : List (Coord S)} (hpath : GeneratingPath root world path) {p : Pattern S ℕ} (hp : p ∈ ↑world) : (generatingContext path).plug p ∈ ↑root

Source Lemma 77: a generating context transports every member of its end world back into the root MCS.

theorem MatchingLogic.Generated.exists_generatingContext {S : Signature} {root world : CanonicalCarrier S} (hgen : Generated root world) : ∃ (C : AppCtx S ℕ), ∀ p ∈ ↑world, C.plug p ∈ ↑root

Every reachable world has a context transporting all of its members into the root.

Lemma 78: Singleton Variables

theorem MatchingLogic.generated_singleton_variables {S : Signature} (root : CanonicalCarrier S) {left right : CanonicalCarrier S} (hleft : Generated root left) (hright : Generated root right) {x : ℕ} (hxleft : Pattern.var x ∈ ↑left) (hxright : Pattern.var x ∈ ↑right) : left = right

Source Lemma 78: a variable pattern belongs to at most one reachable canonical world.

theorem MatchingLogic.GeneratedCarrier.eq_of_var_mem {S : Signature} {root : CanonicalCarrier S} (left right : GeneratedCarrier root) {x : ℕ} (hxleft : Pattern.var x ∈ ↑↑left) (hxright : Pattern.var x ∈ ↑↑right) : left = right

Carrier form of Singleton Variables, used by the later completed valuation.