Logs and compatibility

This module defines logged events and the log of a configuration (events that have a minimal conflict with some event outside the configuration), and the notion of a computation being compatible with a log.

def EventStructures.logged (es : EventStructure) (e : es.Event) : Prop

An event e is logged if there exists some event e' with which it has minimal conflict.

Equations

• EventStructures.logged es e = ∃ (e' : es.Event), es.minimalConflict e e'

def EventStructures.log (es : EventStructure) (c : Conf es) : Set es.Event

The log of a configuration c is the set of events in c that are logged and have a minimal conflict with some event outside c.

Equations

• EventStructures.log es c = {e : es.Event | e ∈ ↑c ∧ ∃ e' ∉ ↑c, es.minimalConflict e e'}

theorem EventStructures.Log.log_subset (es : EventStructure) {c : Conf es} : log es c ⊆ ↑c

If e is in the log of c, then e is in c.

theorem EventStructures.Log.log_logged (es : EventStructure) {c : Conf es} {e : es.Event} (h : e ∈ log es c) : logged es e

If e is in the log of c, then e is logged.

theorem EventStructures.Log.log_mem_iff (es : EventStructure) {c : Conf es} {e : es.Event} : e ∈ log es c ↔ e ∈ ↑c ∧ ∃ e' ∉ ↑c, es.minimalConflict e e'

The log is a subset of the configuration.

theorem EventStructures.Log.logged_iff (es : EventStructure) {e : es.Event} : logged es e ↔ ∃ (e' : es.Event), es.minimalConflict e e'

e is logged if it has minimal conflict with some event.

theorem EventStructures.Log.logged_symm (es : EventStructure) {e e' : es.Event} (h : es.minimalConflict e e') : logged es e'

By symmetry of minimal conflict, if e is logged, then any e' with e ## e' also has minimal conflict with some event.

theorem EventStructures.Log.log_has_conflict_outside (es : EventStructure) {c : Conf es} {e : es.Event} (he : e ∈ log es c) : ∃ e' ∉ ↑c, es.minimalConflict e e'

If e is in the log of c and e' has minimal conflict with e, then either e' is not in c, or there exists another e'' not in c with e ## e''.

def EventStructures.Log.compatibleWithLog (es : EventStructure) (σ : Computations es) (l : Set es.Event) : Prop

A computation σ is compatible with a log l if:

1. All events in l are in σ's target configuration
2. Events in σ are consistent with events in l
3. If an event in σ conflicts with any event, it must be in l

Equations

• EventStructures.Log.compatibleWithLog es σ l = ((∀ e ∈ l, e ∈ ↑σ.fst) ∧ (∀ e ∈ ↑σ.fst, ∀ e' ∈ l, ¬es.conflict e e') ∧ ∀ e ∈ ↑σ.fst, ∀ (e' : es.Event), es.conflict e e' → e ∈ l)

theorem EventStructures.Log.compatibleWithLog_log_subset (es : EventStructure) {σ : Computations es} {l : Set es.Event} (h : compatibleWithLog es σ l) : l ⊆ ↑σ.fst

Extract the first condition: all events in the log are in the computation.

theorem EventStructures.Log.compatibleWithLog_consistent (es : EventStructure) {σ : Computations es} {l : Set es.Event} (h : compatibleWithLog es σ l) {e e' : es.Event} (he : e ∈ ↑σ.fst) (he' : e' ∈ l) : ¬es.conflict e e'

Extract the second condition: events in the computation are consistent with the log.

theorem EventStructures.Log.compatibleWithLog_conflict_in_log (es : EventStructure) {σ : Computations es} {l : Set es.Event} (h : compatibleWithLog es σ l) {e e' : es.Event} (he : e ∈ ↑σ.fst) (hconf : es.conflict e e') : e ∈ l

Extract the third condition: conflicting events in the computation are in the log.

def EventStructures.Log.CompatibleComputations (es : EventStructure) (l : Set es.Event) : Type

The type of all computations compatible with a given log.

Equations

• EventStructures.Log.CompatibleComputations es l = { σ : EventStructures.Computations es // EventStructures.Log.compatibleWithLog es σ l }

def EventStructures.Log.CompatibleComputations.val (es : EventStructure) {l : Set es.Event} (σ : CompatibleComputations es l) : Computations es

Extract the underlying computation from a compatible computation.

Equations

• EventStructures.Log.CompatibleComputations.val es σ = ↑σ

theorem EventStructures.Log.CompatibleComputations.compatible (es : EventStructure) {l : Set es.Event} (σ : CompatibleComputations es l) : compatibleWithLog es (val es σ) l

Extract the compatibility proof.

def EventStructures.Log.compatibleWithConfigLog (es : EventStructure) (c : Conf es) (σ : Computations es) : Prop

A computation is compatible with the log of a configuration.

Equations

• EventStructures.Log.compatibleWithConfigLog es c σ = EventStructures.Log.compatibleWithLog es σ (EventStructures.log es c)

def EventStructures.Log.CompatibleWithConfigLog (es : EventStructure) (c : Conf es) : Type

The type of all computations compatible with the log of a configuration.

Equations

• EventStructures.Log.CompatibleWithConfigLog es c = EventStructures.Log.CompatibleComputations es (EventStructures.log es c)