inductive DY.Trace (α : Type) : Type

• nil {α : Type} : Trace α
• snoc {α : Type} : Trace α → α → Trace α

inductive DY.Trace.le {α : Type} : Trace α → Trace α → Prop

• equal {α : Type} (tr : Trace α) : tr.le tr
• extend {α : Type} (tr1 tr2 : Trace α) (e : α) : tr1.le tr2 → tr1.le (tr2.snoc e)

@[instance_reducible]

instance DY.instLETrace {α : Type} : LE (Trace α)

Equations

• DY.instLETrace = { le := DY.Trace.le }

theorem DY.Trace.induct_le {α : Type} {tr1 : Trace α} {motive : (tr2 : Trace α) → tr1 ≤ tr2 → Prop} {tr2 : Trace α} (t : tr1 ≤ tr2) (equal : motive tr1 ⋯) (extend : ∀ (tr2 : Trace α) (e : α) (a : tr1 ≤ tr2), motive tr2 a → motive (tr2.snoc e) ⋯) : motive tr2 t

theorem DY.Trace.le_refl {α : Type} (tr : Trace α) : tr ≤ tr

theorem DY.Trace.le_trans {α : Type} (tr1 tr2 tr3 : Trace α) : tr1 ≤ tr2 → tr2 ≤ tr3 → tr1 ≤ tr3

class DY.TraceEntryHas (EntryT α : Type) : Type

• inj : EntryT → α
• proj : α → Option EntryT
• inj_proj_eq (x : α) (y : EntryT) : (proj x = some y) = (x = inj y)

def DY.Trace.append {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (entry : EntryT) : Trace α

Equations

• tr.append entry = tr.snoc (DY.TraceEntryHas.inj entry)

theorem DY.Trace.append_le {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (entry : EntryT) : tr ≤ tr.append entry

def DY.Trace.length {α : Type} (tr : Trace α) : Nat

Equations

• DY.Trace.nil.length = 0
• (trBefore.snoc a).length = trBefore.length + 1

theorem DY.Trace.length_le {α : Type} (tr1 tr2 : Trace α) : tr1 ≤ tr2 → tr1.length ≤ tr2.length

def DY.Trace.prefix {α : Type} (tr : Trace α) (i : Nat) : Trace α

Equations

• DY.Trace.nil.prefix i = if DY.Trace.nil.length ≤ i then DY.Trace.nil else DY.Trace.nil
• (trBefore.snoc a).prefix i = if (trBefore.snoc a).length ≤ i then trBefore.snoc a else trBefore.prefix i

theorem DY.Trace.prefix_length {α : Type} (tr : Trace α) (i : Nat) : (tr.prefix i).length = min tr.length i

theorem DY.Trace.prefix_le_self {α : Type} (tr : Trace α) (i : Nat) : tr.prefix i ≤ tr

theorem DY.Trace.prefix_le_prefix {α : Type} (tr : Trace α) (i1 i2 : Nat) : i1 ≤ i2 → tr.prefix i1 ≤ tr.prefix i2

@[simp]

theorem DY.Trace.prefix_length_eq_self {α : Type} (tr : Trace α) : tr.prefix tr.length = tr

theorem DY.Trace.prefix_ge_length_eq_self {α : Type} (tr : Trace α) (i : Nat) : tr.length ≤ i → tr.prefix i = tr

theorem DY.Trace.le_imp_prefix_eq {α : Type} (tr1 tr2 : Trace α) : tr1 ≤ tr2 → tr2.prefix tr1.length = tr1

theorem DY.Trace.le_imp_prefix_le_length_eq {α : Type} (tr1 tr2 : Trace α) (i : Nat) : tr1 ≤ tr2 → i ≤ tr1.length → tr1.prefix i = tr2.prefix i

theorem DY.Trace.prefix_prefix_le {α : Type} (tr1 tr2 : Trace α) (i : Nat) : tr1 ≤ tr2 → tr1.prefix i ≤ tr2.prefix i

def DY.Trace.at {α : Type} (tr : Trace α) (i : Nat) (h_i : i < tr.length) : α

Equations

• DY.Trace.nil.at i h_i_2 = ⋯.elim
• (trBefore.snoc entry).at i h_i_2 = if h : i = trBefore.length then entry else trBefore.at i ⋯

theorem DY.Trace.at_le {α : Type} (tr1 tr2 : Trace α) (i : Nat) (h_i : i < tr1.length) (h_le : tr1 ≤ tr2) : tr1.at i h_i = tr2.at i ⋯

def DY.Trace.at? {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (i : Nat) : Option EntryT

Equations

• tr.at? i = if h_i : i < tr.length then DY.TraceEntryHas.proj (tr.at i h_i) else none

theorem DY.Trace.at?_le {EntryT α : Type} [TraceEntryHas EntryT α] (tr1 tr2 : Trace α) (i : Nat) : tr1 ≤ tr2 → match tr1.at? i with | some res => tr2.at? i = some res | none => True

theorem DY.Trace.at?_append {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (entry : EntryT) : (tr.append entry).at? tr.length = some entry

theorem DY.Trace.at?_eq_some {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (i : Nat) (entry : EntryT) : (tr.at? i = some entry) = ∃ (h_i : i < tr.length), tr.at i h_i = TraceEntryHas.inj entry

theorem DY.Trace.at?_eq_some_implies_length_le {EntryT α : Type} [TraceEntryHas EntryT α] (tr : Trace α) (i : Nat) : match tr.at? i with | some val => i < tr.length | none => True

class DY.ExecTraceTypes : Type 1

• ExecT : Type

def DY.ExecTrace.Entry [ExecTraceTypes] : Type

Equations

• DY.ExecTrace.Entry = DY.ExecTraceTypes.ExecT

@[reducible, inline]

abbrev DY.ExecTrace [ExecTraceTypes] : Type

Equations

• DY.ExecTrace = DY.Trace DY.ExecTrace.Entry

class DY.ExecTraceTypes.Has [ExecTraceTypes] (ExecEntryT : Type) extends DY.TraceEntryHas ExecEntryT DY.ExecTrace.Entry : Type

• inj : ExecEntryT → ExecTrace.Entry
• proj : ExecTrace.Entry → Option ExecEntryT
• inj_proj_eq (x : ExecTrace.Entry) (y : ExecEntryT) : (proj x = some y) = (x = inj y)

class DY.ExecTraceTypes.HasStep (ExecEntryT1 : Type) (ExecEntryT2 : semiOutParam Type) : Type

• inj : ExecEntryT1 → ExecEntryT2
• proj : ExecEntryT2 → Option ExecEntryT1
• inj_proj_eq (x : ExecEntryT2) (y : ExecEntryT1) : (proj x = some y) = (x = inj y)

@[instance_reducible]

instance DY.instExecTraceTypesHasItself [ExecTraceTypes] : ExecTraceTypes.Has ExecTrace.Entry

Equations

• DY.instExecTraceTypesHasItself = { inj := fun (x : DY.ExecTrace.Entry) => x, proj := fun (x : DY.ExecTrace.Entry) => some x, inj_proj_eq := ⋯ }

@[instance_reducible]

instance DY.instExecTraceTypesHasStep [ExecTraceTypes] (ExecEntryT1 ExecEntryT2 : Type) [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] [ExecTraceTypes.Has ExecEntryT2] : ExecTraceTypes.Has ExecEntryT1

Equations

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

@[instance_reducible]

instance DY.instTraceEntryHasEntryOfHas [ExecTraceTypes] (ExecEntryT : Type) [inst : ExecTraceTypes.Has ExecEntryT] : TraceEntryHas ExecEntryT ExecTrace.Entry

Equations

• DY.instTraceEntryHasEntryOfHas ExecEntryT = inst.toTraceEntryHas

theorem DY.TraceEntryHas.inj_injective (EntryT α : Type) [TraceEntryHas EntryT α] : Function.Injective inj

structure DY.ExecTraceTypes.combine {n : Nat} (ExecTypes : Fin n → Type) : Type

• id : Fin n
• entry : ExecTypes self.id

@[instance_reducible]

instance DY.instExecTraceTypesCombineHasStep {n : Nat} (Types : Fin n → Type) (id : Fin n) : ExecTraceTypes.HasStep (Types id) (ExecTraceTypes.combine Types)

Equations

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