Sequences of Atomic Steps

A sequence is a list of operators applied in order, each as one atomic step. StateModel.SequenceStep M ops s t says that t is reached from s by applying the operators of ops in order, through some intermediate configurations.

sequenceFootprintUpperBound ops is the union of the footprints of the operators in ops. It is the set of dimensions that may be touched somewhere in the sequence.

It is not the set of dimensions on which the final configuration may differ from the initial one. A later step may restore a dimension that an earlier step changed. The theorems below keep the two notions apart:

• a dimension outside the bound is preserved throughout the sequence, so the initial, every intermediate, and the final configurations agree on it;
• a dimension inside the bound may still agree at the end, as sequenceFootprintUpperBound_not_net_change shows.

Net effects, restoration, and inverse behavior are not defined here.

def SE.Transformation.sequenceFootprintUpperBound (ops : List OperatorCode) : List Dimension

The dimensions that may be touched somewhere in a sequence of operators: the union of the footprints of its operators.

This is an upper bound on where change may occur. It says nothing about which dimensions differ between the initial and final configurations.

Equations

• SE.Transformation.sequenceFootprintUpperBound ops = List.flatMap SE.Transformation.footprint ops

theorem SE.Transformation.mem_sequenceFootprintUpperBound_iff {ops : List OperatorCode} {d : Dimension} : d ∈ sequenceFootprintUpperBound ops ↔ ∃ (op : OperatorCode), op ∈ ops ∧ d ∈ footprint op

A dimension is in the bound exactly when some operator of the sequence has it in its footprint.

theorem SE.Transformation.sequenceFootprintUpperBound_nil : sequenceFootprintUpperBound [] = []

The empty sequence touches no dimension.

theorem SE.Transformation.sequenceFootprintUpperBound_cons (op : OperatorCode) (ops : List OperatorCode) : sequenceFootprintUpperBound (op :: ops) = footprint op ++ sequenceFootprintUpperBound ops

The bound of a sequence with a first operator is that operator's footprint together with the bound of the rest.

theorem SE.Transformation.sequenceFootprintUpperBound_append (xs ys : List OperatorCode) : sequenceFootprintUpperBound (xs ++ ys) = sequenceFootprintUpperBound xs ++ sequenceFootprintUpperBound ys

The bound of a concatenation is the concatenation of the bounds.

inductive SE.Transformation.StateModel.SequenceStep (M : StateModel) : List OperatorCode → M.State → M.State → Prop

M.SequenceStep ops s t: t is reached from s by applying the operators of ops in order, each as one atomic step.

• nil {M : StateModel} (s : M.State) : M.SequenceStep [] s s

  The empty sequence leaves the configuration as it is.

• cons {M : StateModel} {op : OperatorCode} {ops : List OperatorCode} {s t u : M.State} : M.step op s t → M.SequenceStep ops t u → M.SequenceStep (op :: ops) s u

  A first atomic step followed by a sequence.

theorem SE.Transformation.StateModel.SequenceStep.singleton_iff {M : StateModel} {op : OperatorCode} {s t : M.State} : M.SequenceStep [op] s t ↔ M.step op s t

A one-operator sequence is exactly one atomic step.

theorem SE.Transformation.StateModel.SequenceStep.append_iff {M : StateModel} {xs ys : List OperatorCode} {s u : M.State} : M.SequenceStep (xs ++ ys) s u ↔ ∃ (m : M.State), M.SequenceStep xs s m ∧ M.SequenceStep ys m u

A sequence of two parts passes through an intermediate configuration.

theorem SE.Transformation.StateModel.SequenceStep.agree_of_untouched {M : StateModel} {ops : List OperatorCode} {s t : M.State} {d : Dimension} (h : M.SequenceStep ops s t) (hd : ¬d ∈ sequenceFootprintUpperBound ops) : M.agree d s t

A dimension outside the sequence bound is preserved: the initial and final configurations agree on it.

theorem SE.Transformation.StateModel.SequenceStep.preserves {M : StateModel} {D : List Dimension} {P : M.State → M.State → Prop} {ops : List OperatorCode} {s t : M.State} (hP : M.AgreementSuffices D P) (hD : ∀ (d : Dimension), d ∈ D → ¬d ∈ sequenceFootprintUpperBound ops) (h : M.SequenceStep ops s t) : P s t

Frame-based preservation lifts to sequences: if agreement on D suffices for P and the sequence bound avoids D, a sequence of steps preserves P.

theorem SE.Transformation.StateModel.SequenceStep.agree_through_of_untouched {M : StateModel} {xs ys : List OperatorCode} {s u : M.State} {d : Dimension} (h : M.SequenceStep (xs ++ ys) s u) (hd : ¬d ∈ sequenceFootprintUpperBound (xs ++ ys)) : ∃ (m : M.State), M.SequenceStep xs s m ∧ M.SequenceStep ys m u ∧ M.agree d s m ∧ M.agree d m u

Preservation throughout a history: if a dimension is outside the bound of a two-part sequence, the initial configuration agrees on it with the intermediate configuration and the intermediate with the final one.

theorem SE.Transformation.StateModel.SequenceStep.touched_of_not_agree {M : StateModel} {ops : List OperatorCode} {s t : M.State} {d : Dimension} (h : M.SequenceStep ops s t) (hne : ¬M.agree d s t) : d ∈ sequenceFootprintUpperBound ops

A difference between initial and final configurations lies inside the sequence bound.

theorem SE.Transformation.sequenceFootprintUpperBound_not_net_change : ∃ (s : maximalModel.State), ∃ (t : maximalModel.State), maximalModel.SequenceStep [OperatorCode.BD, OperatorCode.UB] s t ∧ Dimension.binding ∈ sequenceFootprintUpperBound [OperatorCode.BD, OperatorCode.UB] ∧ maximalModel.agree Dimension.binding s t

Touched is not net change. In the maximal model, the sequence BD, UB may touch binding, which is in its bound, while the initial and final configurations still agree on binding.