LanglibLogical tickets for persistent compressed indices #
Physical index owners are drawn from the reusable generic bank. A second, ghost-only ticket
ledger gives every live physical owner a distinct element of Fin (6 * |input|). Keeping the
association in a function, rather than in ScheduleIndex, lets the scheduler change physical
owners without changing the finite machine alphabet or the block-layout API.
The important distinction is that the ticket ledger is inductive: allocation extends the association at one fresh physical owner and demands a genuinely fresh logical ticket. Thus the cardinality bound below cannot be manufactured merely by assuming a scalar inequality.
@[reducible, inline]
The logical ticket carrier. Primary productive tickets occupy the first 2|input|-1
values, shadow tickets the next 2|input|-1, the next two values are emergency scratch and
transient tickets, and the upper 2|input| values form an outside-window parking bank.
The parking bank is as large as the complete physical owner pool. Consequently a live core
ticket and the global 6|input| index bound certify that some parking ticket is absent, even
while parking tickets belonging to nested protected calls remain live.
Equations
- IndexedGrammar.Aho.IndexTicket input = Fin (6 * input.length)
Instances For
def
IndexedGrammar.Aho.IndexTicket.scratch
{T : Type}
{input : List T}
(hinput : 0 < input.length)
:
IndexTicket input
The one-step emergency logical scratch ticket.
Instances For
def
IndexedGrammar.Aho.IndexTicket.transient
{T : Type}
{input : List T}
(hinput : 0 < input.length)
:
IndexTicket input
The distinguished last logical transient ticket.
Instances For
def
IndexedGrammar.Aho.IndexTicket.parking
{T : Type}
{input : List T}
(slot : Fin (2 * input.length))
:
IndexTicket input
One logical parking ticket. Parking tickets lie above both productive semantic banks.
Instances For
def
IndexedGrammar.Aho.IndexTicket.parkingRange
{T : Type}
(input : List T)
:
List (IndexTicket input)
The complete finite parking bank.
Equations
- IndexedGrammar.Aho.IndexTicket.parkingRange input = List.ofFn fun (slot : Fin (2 * input.length)) => IndexedGrammar.Aho.IndexTicket.parking slot
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicket.parkingRange_nodup
{T : Type}
(input : List T)
:
(parkingRange input).Nodup
def
IndexedGrammar.Aho.IndexTicket.Nonparking
{T : Type}
{input : List T}
(ticket : IndexTicket input)
:
A ticket is nonparking when it is distinct from every member of the upper parking bank.
Equations
- ticket.Nonparking = ∀ (slot : Fin (2 * input.length)), ticket ≠ IndexedGrammar.Aho.IndexTicket.parking slot
Instances For
theorem
IndexedGrammar.Aho.IndexTicket.nonparking_of_core
{T : Type}
{input : List T}
{ticket : IndexTicket input}
(hcore : ↑ticket < 4 * input.length)
:
ticket.Nonparking
Every core ticket lies strictly below, and hence outside, the parking bank.
theorem
IndexedGrammar.Aho.IndexTicket.scratch_nonparking
{T : Type}
{input : List T}
(hinput : 0 < input.length)
:
(scratch hinput).Nonparking
The reserved scratch ticket is nonparking.
theorem
IndexedGrammar.Aho.IndexTicket.transient_nonparking
{T : Type}
{input : List T}
(hinput : 0 < input.length)
:
(transient hinput).Nonparking
The distinguished transient ticket is nonparking.
def
IndexedGrammar.Aho.IndexTicket.semanticOwner
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(ticket : IndexTicket input)
:
Interpret a logical ticket in the semantic-owner carrier. All ticket values, including the complete parking bank, are retained by the embedding.
Equations
- ticket.semanticOwner = ⟨↑ticket, ⋯⟩
Instances For
theorem
IndexedGrammar.Aho.IndexTicket.semanticOwner_injective
{T : Type}
{g : IndexedGrammar T}
{input : List T}
:
The semantic interpretation of logical tickets is injective.
def
IndexedGrammar.Aho.IndexTicket.ofProductiveOwner
{T : Type}
{input : List T}
(owner : Fin (10 * input.length))
(hprimary : ↑owner < 2 * input.length - 1)
:
IndexTicket input
Turn a semantic productive owner into its corresponding logical ticket.
Equations
- IndexedGrammar.Aho.IndexTicket.ofProductiveOwner owner hprimary = ⟨↑owner, ⋯⟩
Instances For
def
IndexedGrammar.Aho.IndexTicket.ofSemanticOwner
{T : Type}
{input : List T}
(owner : Fin (10 * input.length))
(hbank : ↑owner < 4 * input.length - 2)
:
IndexTicket input
Any semantic primary-or-shadow owner below the two temporary slots is a logical ticket.
Equations
- IndexedGrammar.Aho.IndexTicket.ofSemanticOwner owner hbank = ⟨↑owner, ⋯⟩
Instances For
theorem
IndexedGrammar.Aho.IndexTicket.ofProductiveOwner_nonparking
{T : Type}
{input : List T}
(owner : Fin (10 * input.length))
(hprimary : ↑owner < 2 * input.length - 1)
:
(ofProductiveOwner owner hprimary).Nonparking
Every primary productive-owner ticket is nonparking.
theorem
IndexedGrammar.Aho.IndexTicket.ofSemanticOwner_nonparking
{T : Type}
{input : List T}
(owner : Fin (10 * input.length))
(hbank : ↑owner < 4 * input.length - 2)
:
(ofSemanticOwner owner hbank).Nonparking
Every primary-or-shadow semantic-owner ticket is nonparking.
@[simp]
theorem
IndexedGrammar.Aho.IndexTicket.semanticOwner_scratch
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
@[simp]
theorem
IndexedGrammar.Aho.IndexTicket.semanticOwner_transient
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
@[simp]
theorem
IndexedGrammar.Aho.IndexTicket.semanticOwner_transient_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
(hinput : 0 < input.length)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChildEventTicketOne
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
(hone : 1 ∈ rest.eventDepths)
:
IndexTicket input
The logical ticket of the child depth-one event exposed by a unary push.
Equations
- window.pushChildEventTicketOne hone = IndexedGrammar.Aho.IndexTicket.ofProductiveOwner (window.pushChild.eventOwner 1 hone) ⋯
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.semanticOwner_pushChildEventTicketOne
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
(hone : 1 ∈ rest.eventDepths)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.pushChildEventTicketOne_nonparking
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A B : g.nt}
{f : g.flag}
{stack : List g.flag}
{w : List T}
{r : IRule T g.nt g.flag}
{hr : r ∈ g.rules}
{hlhs : r.lhs = A}
{hc : r.consume = none}
{hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]}
{rest : g.NFParse B (f :: stack) w}
(window : ProductiveOwnerWindow (NFParse.push hr hlhs hc hrhs rest))
(hone : 1 ∈ rest.eventDepths)
:
(window.pushChildEventTicketOne hone).Nonparking
The child depth-one productive-event ticket lies below the parking bank.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventTicket
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
IndexTicket input
The logical shadow ticket attached to one productive event.
Equations
- window.shadowEventTicket d hd = IndexedGrammar.Aho.IndexTicket.ofSemanticOwner (window.shadowEventOwner d hd) ⋯
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.semanticOwner_shadowEventTicket
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.shadowEventTicket_nonparking
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
(d : ℕ)
(hd : d ∈ parse.eventDepths)
:
(window.shadowEventTicket d hd).Nonparking
Every shadow-event ticket lies below the parking bank.
def
IndexedGrammar.Aho.ProductiveOwnerWindow.parkingSlot
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
:
The canonical parking slot of a productive window is its root-relative base.
Equations
- window.parkingSlot = ⟨window.base, ⋯⟩
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.parkingSlot_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
:
def
IndexedGrammar.Aho.ProductiveOwnerWindow.parkingTicket
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
:
IndexTicket input
The canonical logical parking ticket associated with a productive window.
Equations
- window.parkingTicket = IndexedGrammar.Aho.IndexTicket.parking window.parkingSlot
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ProductiveOwnerWindow.parkingTicket_val
{T : Type}
{g : IndexedGrammar T}
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
(window : ProductiveOwnerWindow parse)
:
def
IndexedGrammar.Aho.ScheduleCursor.indexTickets
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
(ticketOf : Fin (10 * input.length) → IndexTicket input)
:
List (IndexTicket input)
Logical tickets currently present on the work tape, read through an owner-to-ticket association.
Equations
- cursor.indexTickets ticketOf = List.map ticketOf cursor.indexOwners
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.indexTickets_length
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
(ticketOf : Fin (10 * input.length) → IndexTicket input)
:
Ghost-only semantic projection #
def
IndexedGrammar.Aho.ScheduleIndex.withTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
(owner : Fin (10 * input.length))
:
ScheduleIndex g input
Replace only the owner annotation of a compressed index. This local copy deliberately
does not import the later physical-owner relabelling module, so ticket resources remain usable
by Scheduler.Resources.RunResources without an import cycle.
Equations
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleIndex.withTicketOwner_owner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(idx : ScheduleIndex g input)
(owner : Fin (10 * input.length))
:
def
IndexedGrammar.Aho.ScheduleAtom.relabelTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(f : Fin (10 * input.length) → Fin (10 * input.length))
:
ScheduleAtom g input → ScheduleAtom g input
Relabel index and matching frame annotations for the semantic ticket view.
Equations
- IndexedGrammar.Aho.ScheduleAtom.relabelTicketOwner f (IndexedGrammar.Aho.ScheduleAtom.index idx) = IndexedGrammar.Aho.ScheduleAtom.index (idx.withTicketOwner (f idx.owner))
- IndexedGrammar.Aho.ScheduleAtom.relabelTicketOwner f (IndexedGrammar.Aho.ScheduleAtom.close owner) = IndexedGrammar.Aho.ScheduleAtom.close (f owner)
- IndexedGrammar.Aho.ScheduleAtom.relabelTicketOwner f x✝ = x✝
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleAtom.indexOwner?_relabelTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(f : Fin (10 * input.length) → Fin (10 * input.length))
(atom : ScheduleAtom g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleAtom.closeOwner?_relabelTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(f : Fin (10 * input.length) → Fin (10 * input.length))
(atom : ScheduleAtom g input)
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleAtom.filterMap_indexOwner_relabelTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(f : Fin (10 * input.length) → Fin (10 * input.length))
(word : List (ScheduleAtom g input))
:
List.filterMap indexOwner? (List.map (relabelTicketOwner f) word) = List.map f (List.filterMap indexOwner? word)
@[simp]
theorem
IndexedGrammar.Aho.ScheduleAtom.filterMap_closeOwner_relabelTicketOwner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(f : Fin (10 * input.length) → Fin (10 * input.length))
(word : List (ScheduleAtom g input))
:
List.filterMap closeOwner? (List.map (relabelTicketOwner f) word) = List.map f (List.filterMap closeOwner? word)
def
IndexedGrammar.Aho.ScheduleCursor.relabelTicketOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
(f : Fin (10 * input.length) → Fin (10 * input.length))
:
ScheduleCursor g input
A virtual cursor whose owner annotations are the semantic images of logical tickets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.relabelTicketOwners_indexOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
(f : Fin (10 * input.length) → Fin (10 * input.length))
:
@[simp]
theorem
IndexedGrammar.Aho.ScheduleCursor.relabelTicketOwners_frameOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
(f : Fin (10 * input.length) → Fin (10 * input.length))
:
structure
IndexedGrammar.Aho.IndexTicketLedger
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
(cursor : ScheduleCursor g input)
:
An injective logical-ticket assignment for all persistent physical owners in a cursor.
- ticketOf : Fin (10 * input.length) → IndexTicket input
- tickets_nodup : (cursor.indexTickets self.ticketOf).Nodup
- scratch_fresh (hinput : 0 < input.length) : IndexTicket.scratch hinput ∉ cursor.indexTickets self.ticketOf
Instances For
def
IndexedGrammar.Aho.IndexTicketLedger.swapTickets
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(left right : IndexTicket input)
(hleft : ∀ (hinput : 0 < input.length), left ≠ IndexTicket.scratch hinput)
(hright : ∀ (hinput : 0 < input.length), right ≠ IndexTicket.scratch hinput)
:
IndexTicketLedger cursor
Apply one logical-ticket transposition to every persistent index. This is a ghost-only operation: injectivity is preserved by the permutation, and the explicit side conditions say that the reserved scratch ticket is fixed.
Equations
- ledger.swapTickets left right hleft hright = { ticketOf := fun (owner : Fin (10 * input.length)) => (Equiv.swap left right) (ledger.ticketOf owner), tickets_nodup := ⋯, scratch_fresh := ⋯ }
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.swapTickets_ticketOf
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(left right : IndexTicket input)
(hleft : ∀ (hinput : 0 < input.length), left ≠ IndexTicket.scratch hinput)
(hright : ∀ (hinput : 0 < input.length), right ≠ IndexTicket.scratch hinput)
(owner : Fin (10 * input.length))
:
(ledger.swapTickets left right hleft hright).ticketOf owner = (Equiv.swap left right) (ledger.ticketOf owner)
def
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(window : ProductiveOwnerWindow parse)
:
Every live parking ticket has a slot strictly below the active productive-window base.
Equations
- ledger.ParkingBelow window = ∀ (slot : Fin (2 * input.length)), IndexedGrammar.Aho.IndexTicket.parking slot ∈ cursor.indexTickets ledger.ticketOf → ↑slot < window.base
Instances For
def
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(window : ProductiveOwnerWindow parse)
:
Every live parking ticket has a slot at or below the active productive-window base.
Equations
- ledger.ParkingAtOrBelow window = ∀ (slot : Fin (2 * input.length)), IndexedGrammar.Aho.IndexTicket.parking slot ∈ cursor.indexTickets ledger.ticketOf → ↑slot ≤ window.base
Instances For
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.toAtOrBelow
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbelow : ledger.ParkingBelow window)
:
ledger.ParkingAtOrBelow window
A strict parking bound also supplies the corresponding non-strict bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.parkingTicket_fresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbelow : ledger.ParkingBelow window)
:
window.parkingTicket ∉ cursor.indexTickets ledger.ticketOf
The canonical window-base parking ticket is fresh under a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.mono
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbelow : ledger.ParkingBelow oldWindow)
(hbase : oldWindow.base ≤ newWindow.base)
:
ledger.ParkingBelow newWindow
Increasing the productive-window base preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.mono
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbound : ledger.ParkingAtOrBelow oldWindow)
(hbase : oldWindow.base ≤ newWindow.base)
:
ledger.ParkingAtOrBelow newWindow
Increasing the productive-window base preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.toBelow_of_base_lt
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbound : ledger.ParkingAtOrBelow oldWindow)
(hbase : oldWindow.base < newWindow.base)
:
ledger.ParkingBelow newWindow
A strict increase of the productive-window base turns AtOrBelow back into Below.
def
IndexedGrammar.Aho.IndexTicketLedger.ofEmpty
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(hinput : 0 < input.length)
(hempty : cursor.indexOwners = [])
:
IndexTicketLedger cursor
The unique useful ticket state for an owner-free cursor. The association away from live owners is deliberately arbitrary; choosing the transient ticket makes the root construction uniform.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IndexedGrammar.Aho.IndexTicketLedger.parkingBelow_ofEmpty
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
(hinput : 0 < input.length)
(hempty : cursor.indexOwners = [])
(window : ProductiveOwnerWindow parse)
:
(ofEmpty hinput hempty).ParkingBelow window
The owner-free ledger satisfies every strict window-relative parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ticketOf_injectiveOn
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
{left right : Fin (10 * input.length)}
(hleft : left ∈ cursor.indexOwners)
(hright : right ∈ cursor.indexOwners)
(heq : ledger.ticketOf left = ledger.ticketOf right)
:
Live physical owners inherit injectivity from the duplicate-free ticket image.
def
IndexedGrammar.Aho.IndexTicketLedger.semanticOwnerOf
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
:
Interpret one physical owner through the ledger's logical ticket.
Equations
- ledger.semanticOwnerOf owner = (ledger.ticketOf owner).semanticOwner
Instances For
def
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
ScheduleCursor g input
The virtual cursor on which the existing productive-owner ledger can be reused unchanged. Both compressed indices and their matching frame closes are projected.
Equations
- ledger.semanticCursor = cursor.relabelTicketOwners ledger.semanticOwnerOf
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_indexOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
ledger.semanticCursor.indexOwners = List.map IndexTicket.semanticOwner (cursor.indexTickets ledger.ticketOf)
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_frameOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_right
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
ledger.semanticCursor.right = List.map (ScheduleAtom.relabelTicketOwner ledger.semanticOwnerOf) cursor.right
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_left
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
ledger.semanticCursor.left = List.map (ScheduleAtom.relabelTicketOwner ledger.semanticOwnerOf) cursor.left
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_right_indexOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
List.filterMap ScheduleAtom.indexOwner? ledger.semanticCursor.right = List.map ledger.semanticOwnerOf (List.filterMap ScheduleAtom.indexOwner? cursor.right)
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticCursor_focus_indexOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
List.filterMap ScheduleAtom.indexOwner? [ledger.semanticCursor.focus] = List.map ledger.semanticOwnerOf (List.filterMap ScheduleAtom.indexOwner? [cursor.focus])
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticOwner_mem_indexOwners_iff
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(ticket : IndexTicket input)
:
ticket.semanticOwner ∈ ledger.semanticCursor.indexOwners ↔ ticket ∈ cursor.indexTickets ledger.ticketOf
Membership in the virtual semantic cursor is exactly membership of the corresponding logical ticket in the physical cursor.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ticket_not_mem_of_semanticOwner_not_mem
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
{ticket : IndexTicket input}
(hfresh : ticket.semanticOwner ∉ ledger.semanticCursor.indexOwners)
:
ticket ∉ cursor.indexTickets ledger.ticketOf
Negative form used directly after an existing productive-owner freshness theorem.
def
IndexedGrammar.Aho.IndexTicketLedger.semanticOwners
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owners : List (Fin (10 * input.length)))
:
Map an aligned physical-owner list into its productive-owner ticket view.
Equations
- ledger.semanticOwners owners = List.map ledger.semanticOwnerOf owners
Instances For
@[reducible, inline]
abbrev
IndexedGrammar.Aho.IndexTicketLedger.EventTicketLayout
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
Reuse the existing event-owned block layout on the semantic ticket projection.
Equations
- IndexedGrammar.Aho.IndexTicketLedger.EventTicketLayout parse window ledger blocks owners = IndexedGrammar.Aho.EventOwnedLayout parse window blocks (ledger.semanticOwners owners)
Instances For
@[reducible, inline]
abbrev
IndexedGrammar.Aho.IndexTicketLedger.ShadowTicketLayout
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(blocks : List (List g.flag))
(owners : List (Fin (10 * input.length)))
:
Reuse the existing shadow-start layout on the semantic ticket projection.
Equations
- IndexedGrammar.Aho.IndexTicketLedger.ShadowTicketLayout parse window ledger blocks owners = IndexedGrammar.Aho.ShadowStartLayout parse window blocks (ledger.semanticOwners owners)
Instances For
@[reducible, inline]
abbrev
IndexedGrammar.Aho.IndexTicketLedger.SemanticScheduleOwnerLedger
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
Reuse the complete cursor-level productive-owner ledger on the semantic ticket cursor.
Equations
- IndexedGrammar.Aho.IndexTicketLedger.SemanticScheduleOwnerLedger parse window ledger = IndexedGrammar.Aho.ScheduleOwnerLedger parse window ledger.semanticCursor
Instances For
@[reducible, inline]
abbrev
IndexedGrammar.Aho.IndexTicketLedger.SemanticShadowOwnerLedger
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
(parse : g.NFParse A stack w)
(window : ProductiveOwnerWindow parse)
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
Reuse the complete cursor-level shadow ledger on the semantic ticket cursor.
Equations
- IndexedGrammar.Aho.IndexTicketLedger.SemanticShadowOwnerLedger parse window ledger = IndexedGrammar.Aho.ShadowOwnerLedger parse window ledger.semanticCursor
Instances For
def
IndexedGrammar.Aho.IndexTicketLedger.insertTicket
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
:
Fin (10 * input.length) → IndexTicket input
The owner-to-ticket association used after allocating one physical owner.
Equations
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.insertTicket_self
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
:
theorem
IndexedGrammar.Aho.IndexTicketLedger.insertTicket_eq_of_mem
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
{candidate : Fin (10 * input.length)}
(hcandidate : candidate ∈ cursor.indexOwners)
(hfresh : owner ∉ cursor.indexOwners)
:
def
IndexedGrammar.Aho.IndexTicketLedger.allocate
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
Allocate a fresh physical owner and attach a fresh logical ticket to it.
Equations
- ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices = { ticketOf := ledger.insertTicket owner ticket, tickets_nodup := ⋯, scratch_fresh := ⋯ }
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.allocate_ticketOf_self
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
:
theorem
IndexedGrammar.Aho.IndexTicketLedger.allocate_ticket_eq_of_mem_of_fresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(ticket fresh : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hfresh : fresh ∉ old.indexTickets ledger.ticketOf)
(hmem :
fresh ∈ new.indexTickets (ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ticketOf)
:
If a ticket absent from the old cursor appears after one fresh-owner allocation, it must be the ticket assigned to the new owner.
theorem
IndexedGrammar.Aho.IndexTicketLedger.allocate_preserves_fresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(ticket fresh : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hfresh : fresh ∉ old.indexTickets ledger.ticketOf)
(hne : fresh ≠ ticket)
:
fresh ∉ new.indexTickets (ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ticketOf
Allocating a different ticket preserves freshness of every ticket absent from the old cursor.
def
IndexedGrammar.Aho.IndexTicketLedger.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(hindices : new.indexOwners.Perm old.indexOwners)
:
Transport tickets across a cursor change which preserves physical owners up to permutation.
Equations
Instances For
def
IndexedGrammar.Aho.IndexTicketLedger.release
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
Releasing one physical owner preserves injectivity on the remaining owners.
Equations
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.release_ticketOf
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.release_semanticOwnerOf
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{old new : ScheduleCursor g input}
(ledger : IndexTicketLedger old)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
(candidate : Fin (10 * input.length))
:
def
IndexedGrammar.Aho.IndexTicketLedger.reticket
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
:
IndexTicketLedger cursor
Reticket one live physical owner by swapping its old logical ticket with a fresh target. Because live tickets are duplicate-free and the target is absent, only that owner changes on the projected cursor; applying the same map to frame closes keeps owner matching coherent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IndexedGrammar.Aho.IndexTicketLedger.reticket_ticketOf_owner
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
:
theorem
IndexedGrammar.Aho.IndexTicketLedger.reticket_ticketOf_eq_of_mem_ne
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
{candidate : Fin (10 * input.length)}
(hcandidate : candidate ∈ cursor.indexOwners)
(hne : candidate ≠ owner)
:
Reticketing one live owner leaves every other live owner association unchanged.
theorem
IndexedGrammar.Aho.IndexTicketLedger.reticket_old_fresh
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
:
ledger.ticketOf owner ∉
cursor.indexTickets (ledger.reticket owner target howner htargetFresh htargetNotScratch).ticketOf
After reticketing to a fresh target, the old ticket is absent from the live cursor.
Preservation of window-relative parking bounds #
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.swapTickets_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(left right : IndexTicket input)
(hleft : ∀ (hinput : 0 < input.length), left ≠ IndexTicket.scratch hinput)
(hright : ∀ (hinput : 0 < input.length), right ≠ IndexTicket.scratch hinput)
(hleftNonparking : left.Nonparking)
(hrightNonparking : right.Nonparking)
:
(ledger.swapTickets left right hleft hright).ParkingBelow window
Swapping two nonparking tickets preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.swapTickets_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(left right : IndexTicket input)
(hleft : ∀ (hinput : 0 < input.length), left ≠ IndexTicket.scratch hinput)
(hright : ∀ (hinput : 0 < input.length), right ≠ IndexTicket.scratch hinput)
(hleftNonparking : left.Nonparking)
(hrightNonparking : right.Nonparking)
:
(ledger.swapTickets left right hleft hright).ParkingAtOrBelow window
Swapping two nonparking tickets preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(hindices : new.indexOwners.Perm old.indexOwners)
:
(ledger.transport hindices).ParkingBelow window
Transport across a physical-owner permutation preserves strict parking bounds.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.transport
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(hindices : new.indexOwners.Perm old.indexOwners)
:
(ledger.transport hindices).ParkingAtOrBelow window
Transport across a physical-owner permutation preserves non-strict parking bounds.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.transport_mono
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbound : ledger.ParkingBelow oldWindow)
(hindices : new.indexOwners.Perm old.indexOwners)
(hbase : oldWindow.base ≤ newWindow.base)
:
(ledger.transport hindices).ParkingBelow newWindow
Transport followed by a weak base increase preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.transport_mono
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbound : ledger.ParkingAtOrBelow oldWindow)
(hindices : new.indexOwners.Perm old.indexOwners)
(hbase : oldWindow.base ≤ newWindow.base)
:
(ledger.transport hindices).ParkingAtOrBelow newWindow
Transport followed by a weak base increase preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.transport_toBelow_of_base_lt
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A₁ A₂ : g.nt}
{stack₁ stack₂ : List g.flag}
{w₁ w₂ : List T}
{parse₁ : g.NFParse A₁ stack₁ w₁}
{parse₂ : g.NFParse A₂ stack₂ w₂}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{oldWindow : ProductiveOwnerWindow parse₁}
{newWindow : ProductiveOwnerWindow parse₂}
(hbound : ledger.ParkingAtOrBelow oldWindow)
(hindices : new.indexOwners.Perm old.indexOwners)
(hbase : oldWindow.base < newWindow.base)
:
(ledger.transport hindices).ParkingBelow newWindow
A strict base increase after transport restores a strict bound from AtOrBelow.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.release
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
(ledger.release owner hindices).ParkingBelow window
Releasing one physical owner preserves strict parking bounds.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.release
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(owner : Fin (10 * input.length))
(hindices : old.indexOwners.Perm (owner :: new.indexOwners))
:
(ledger.release owner hindices).ParkingAtOrBelow window
Releasing one physical owner preserves non-strict parking bounds.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.allocate_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hnonparking : ticket.Nonparking)
:
(ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ParkingBelow window
Allocating a nonparking ticket preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.allocate_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hnonparking : ticket.Nonparking)
:
(ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ParkingAtOrBelow window
Allocating a nonparking ticket preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.allocate_core
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hcore : ↑ticket < 4 * input.length)
:
(ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ParkingBelow window
Allocating a core ticket preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.allocate_core
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{old new : ScheduleCursor g input}
{ledger : IndexTicketLedger old}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(owner : Fin (10 * input.length))
(ticket : IndexTicket input)
(hownerFresh : owner ∉ old.indexOwners)
(hticketFresh : ticket ∉ old.indexTickets ledger.ticketOf)
(hticketNotScratch : ∀ (hinput : 0 < input.length), ticket ≠ IndexTicket.scratch hinput)
(hindices : new.indexOwners.Perm (owner :: old.indexOwners))
(hcore : ↑ticket < 4 * input.length)
:
(ledger.allocate owner ticket hownerFresh hticketFresh hticketNotScratch hindices).ParkingAtOrBelow window
Allocating a core ticket preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.reticket_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
(hnonparking : target.Nonparking)
:
(ledger.reticket owner target howner htargetFresh htargetNotScratch).ParkingBelow window
Reticketing one owner to a fresh nonparking target preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.reticket_nonparking
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
(hnonparking : target.Nonparking)
:
(ledger.reticket owner target howner htargetFresh htargetNotScratch).ParkingAtOrBelow window
Reticketing one owner to a fresh nonparking target preserves a non-strict bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.reticket_core
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
(hcore : ↑target < 4 * input.length)
:
(ledger.reticket owner target howner htargetFresh htargetNotScratch).ParkingBelow window
Reticketing one owner to a fresh core target preserves a strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingAtOrBelow.reticket_core
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingAtOrBelow window)
(owner : Fin (10 * input.length))
(target : IndexTicket input)
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : target ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), target ≠ IndexTicket.scratch hinput)
(hcore : ↑target < 4 * input.length)
:
(ledger.reticket owner target howner htargetFresh htargetNotScratch).ParkingAtOrBelow window
Reticketing one owner to a fresh core target preserves a non-strict parking bound.
theorem
IndexedGrammar.Aho.IndexTicketLedger.ParkingBelow.reticket_parkingTicket
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{A : g.nt}
{stack : List g.flag}
{w : List T}
{parse : g.NFParse A stack w}
{cursor : ScheduleCursor g input}
{ledger : IndexTicketLedger cursor}
{window : ProductiveOwnerWindow parse}
(hbound : ledger.ParkingBelow window)
(owner : Fin (10 * input.length))
(howner : owner ∈ cursor.indexOwners)
(htargetFresh : window.parkingTicket ∉ cursor.indexTickets ledger.ticketOf)
(htargetNotScratch : ∀ (hinput : 0 < input.length), window.parkingTicket ≠ IndexTicket.scratch hinput)
:
(ledger.reticket owner window.parkingTicket howner htargetFresh htargetNotScratch).ParkingAtOrBelow window
Parking one owner at the canonical window-base ticket weakens Below only to
AtOrBelow.
theorem
IndexedGrammar.Aho.IndexTicketLedger.index_count_le
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
Logical ticket injectivity bounds physical persistent indices by the complete
6|input| logical carrier.
theorem
IndexedGrammar.Aho.IndexTicketLedger.index_count_lt
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(hinput : 0 < input.length)
:
The permanently reserved scratch ticket leaves strict room in the complete logical carrier. This is deliberately not a bound for the smaller physical owner pool.
theorem
IndexedGrammar.Aho.IndexTicketLedger.pool_free_ne_nil
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
(pool : IndexOwnerPool cursor)
(hcapacity : cursor.indexOwners.length < 6 * input.length)
:
An explicit strict physical-capacity bound implies that the physical owner pool is nonempty. Logical-ticket cardinality alone does not imply this after adding parking tickets.
theorem
IndexedGrammar.Aho.IndexTicketLedger.semanticOwners_nodup
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{cursor : ScheduleCursor g input}
(ledger : IndexTicketLedger cursor)
:
(List.map IndexTicket.semanticOwner (cursor.indexTickets ledger.ticketOf)).Nodup
Semantic-owner images of live tickets are also duplicate-free.