Metatheory of semantic stores

List-level definedness laws, store-substitution symmetry, and generated-name reservation properties for the definitions in Store.

Key results:

• isDefinedCons / isDefinedApp and the corresponding SemanticStore.varsUndefined* laws compose and decompose list-level definedness.
• substStoresFlip, substDefinedFlip, invStoresComm, and invStoresExceptComm establish substitution and invariance symmetry.
• SemanticStore.isReserved.gen_slot_none, SemanticStore.isReserved.storeWith_gen, and SemanticStore.isReserved.mono establish and preserve generated-name reservations.

theorem Imperative.isDefinedCons {self✝ : PureExpr} {v : self✝.Ident} {σ : SemanticStore self✝} {vs2 : List self✝.Ident} : SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ [v]) σ → SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ vs2) σ → SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ v :: vs2) σ

Definedness of a singleton and a tail implies definedness of their cons.

theorem Imperative.isDefinedApp {P : PureExpr} {σ : SemanticStore P} {vs1 vs2 : List P.Ident} : SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ vs1) σ → SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ vs2) σ → SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ vs1 ++ vs2) σ

Definedness of two lists implies definedness of their concatenation.

theorem Imperative.isDefinedCons' {self✝ : PureExpr} {h : self✝.Ident} {t : List self✝.Ident} {σ : SemanticStore self✝} : SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ h :: t) σ → SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ [h]) σ ∧ SemanticStore.varsDefined (fun (x : self✝.Ident) => x ∈ t) σ

Definedness of a cons list implies definedness of its head and tail.

theorem Imperative.isDefinedApp' {P : PureExpr} {σ : SemanticStore P} {t1 t2 : List P.Ident} : SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ t1 ++ t2) σ → SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ t1) σ ∧ SemanticStore.varsDefined (fun (x : P.Ident) => x ∈ t2) σ

Definedness of a concatenation implies definedness of both component lists.

theorem Imperative.isNotDefinedCons {self✝ : PureExpr} {v : self✝.Ident} {σ : SemanticStore self✝} {vs2 : List self✝.Ident} : SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ [v]) σ → SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ vs2) σ → SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ v :: vs2) σ

Undefinedness of a singleton and a tail implies undefinedness of their cons.

theorem Imperative.isNotDefinedApp {P : PureExpr} {σ : SemanticStore P} {vs1 vs2 : List P.Ident} : SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ vs1) σ → SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ vs2) σ → SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ vs1 ++ vs2) σ

Undefinedness of two lists implies undefinedness of their concatenation.

theorem Imperative.isNotDefinedCons' {self✝ : PureExpr} {h : self✝.Ident} {t : List self✝.Ident} {σ : SemanticStore self✝} : SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ h :: t) σ → SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ [h]) σ ∧ SemanticStore.varsUndefined (fun (x : self✝.Ident) => x ∈ t) σ

Undefinedness of a cons list implies undefinedness of its head and tail.

theorem Imperative.isNotDefinedApp' {P : PureExpr} {σ : SemanticStore P} {t1 t2 : List P.Ident} : SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ t1 ++ t2) σ → SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ t1) σ ∧ SemanticStore.varsUndefined (fun (x : P.Ident) => x ∈ t2) σ

Undefinedness of a concatenation implies undefinedness of both components.

Store substitution

theorem Imperative.substSwapId (P : PureExpr) (substs : List (P.Ident × P.Ident)) : substSwap (substSwap substs) = substs

Swapping both sides of every substitution pair twice is the identity.

theorem Imperative.substStoresFlip {P✝ : PureExpr} {σ₁ σ₂ : SemanticStore P✝} {substs : List (P✝.Ident × P✝.Ident)} : substStores σ₁ σ₂ substs → substStores σ₂ σ₁ (substSwap substs)

Store substitution can be read in the reverse direction after swapping its identifier pairs.

theorem Imperative.substStoresFlip' {P✝ : PureExpr} {σ₂ σ₁ : SemanticStore P✝} {substs : List (P✝.Ident × P✝.Ident)} : substStores σ₂ σ₁ (substSwap substs) → substStores σ₁ σ₂ substs

Reverse-direction store substitution can be flipped back.

theorem Imperative.substDefinedFlip {P✝ : PureExpr} {σ₁ σ₂ : SemanticStore P✝} {substs : List (P✝.Ident × P✝.Ident)} : substDefined σ₁ σ₂ substs → substDefined σ₂ σ₁ (substSwap substs)

Pairwise definedness is symmetric after swapping substitution pairs.

theorem Imperative.substDefinedFlip' {P✝ : PureExpr} {σ₂ σ₁ : SemanticStore P✝} {substs : List (P✝.Ident × P✝.Ident)} : substDefined σ₂ σ₁ (substSwap substs) → substDefined σ₁ σ₂ substs

Swapped pairwise definedness can be flipped back.

theorem Imperative.invStoresComm {P✝ : PureExpr} {σ₁ σ₂ : SemanticStore P✝} {ks : List P✝.Ident} : invStores σ₁ σ₂ ks → invStores σ₂ σ₁ ks

Store invariance is symmetric.

theorem Imperative.invStoresExceptComm {P✝ : PureExpr} {σ₁ σ₂ : SemanticStore P✝} {ks : List P✝.Ident} : invStoresExcept σ₁ σ₂ ks → invStoresExcept σ₂ σ₁ ks

Store invariance outside a key set is symmetric.

Generated-name reservations

theorem Imperative.SemanticStore.isReserved.gen_slot_none {P : PureExpr} [HasIdent P] {Q : String → Prop} {state : StringGenState} {store : SemanticStore P} (pfx : String) (hreserved : isReserved Q state store) (hwf : state.WF) (hQ : Q (StringGenState.gen pfx state).fst) : store (HasIdent.ident (StringGenState.gen pfx state).fst) = none

The freshly generated name's slot is undefined in a reserved store, given a well-formed generator state and classification of the generated name.

theorem Imperative.SemanticStore.isReserved.storeWith_gen {P : PureExpr} [HasIdent P] [DecidableEq P.Ident] [LawfulHasIdent P] {Q : String → Prop} {state : StringGenState} {store : SemanticStore P} (pfx : String) (value : P.Val) (hreserved : isReserved Q state store) : isReserved Q (StringGenState.gen pfx state).snd (store.update (HasIdent.ident (StringGenState.gen pfx state).fst) value)

Defining the freshly generated name and advancing the generator preserves reserved-name freshness.

theorem Imperative.SemanticStore.isReserved.mono {P : PureExpr} [HasIdent P] {Q : String → Prop} {state state' : StringGenState} {store : SemanticStore P} (hstep : state.GenStep state') (hreserved : isReserved Q state store) : isReserved Q state' store

Advancing the generator weakens the set of ungenerated names, so reserved name freshness remains true.