class DY.ErasableProofEntry (ExecEntryT : outParam Type) (ProofEntryT : Type) : Type

• erase : ProofEntryT → ExecEntryT

@[reducible, inline]

abbrev DY.ErasableProofEntry.default (ExecEntryT : Type) : ErasableProofEntry ExecEntryT ExecEntryT

Equations

• DY.ErasableProofEntry.default ExecEntryT = { erase := fun (x : ExecEntryT) => x }

class DY.ExecEntryAssociatedWithProofEntry (ExecEntryT : Type) (ProofEntryT : outParam Type) : Type

class DY.ProofTraceTypes [ExecTraceTypes] : Type 1

• ProofT : Type
• tc : ErasableProofEntry ExecTraceTypes.ExecT ProofT

def DY.ProofTrace.Entry [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.ProofTrace.Entry = DY.ProofTraceTypes.ProofT

@[instance_reducible]

instance DY.instErasableProofEntryEntryEntry [ExecTraceTypes] [ProofTraceTypes] : ErasableProofEntry ExecTrace.Entry ProofTrace.Entry

Equations

• DY.instErasableProofEntryEntryEntry = { erase := fun (entry : DY.ProofTrace.Entry) => DY.ErasableProofEntry.erase entry }

@[reducible, inline]

abbrev DY.ProofTrace [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.ProofTrace = DY.Trace DY.ProofTrace.Entry

def DY.ProofTrace.Entry.erase [ExecTraceTypes] [ProofTraceTypes] (entry : Entry) : ExecTrace.Entry

Equations

• entry.erase = DY.ErasableProofEntry.erase entry

def DY.Trace.erase [ExecTraceTypes] [ProofTraceTypes] (tr : ProofTrace) : ExecTrace

Equations

• DY.Trace.nil.erase = DY.Trace.nil
• (trBefore.snoc entry).erase = DY.Trace.snoc trBefore.erase entry.erase

theorem DY.Trace.erase_le [ExecTraceTypes] [ProofTraceTypes] (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → erase tr1 ≤ erase tr2

@[simp]

theorem DY.Trace.erase_length [ExecTraceTypes] [ProofTraceTypes] (tr : ProofTrace) : length (erase tr) = length tr

theorem DY.Trace.erase_at [ExecTraceTypes] [ProofTraceTypes] (tr : ProofTrace) (i : Nat) (h_i : i < length (erase tr)) : «at» (erase tr) i h_i = («at» tr i ⋯).erase

@[simp]

theorem DY.Trace.prefix_erase [ExecTraceTypes] [ProofTraceTypes] (tr : ProofTrace) (i : Nat) : («prefix» tr i).erase = «prefix» (erase tr) i

class DY.ProofTraceTypes.Has [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT : outParam Type} (ProofEntryT : Type) [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] extends DY.TraceEntryHas ProofEntryT DY.ProofTrace.Entry : Type

• inj : ProofEntryT → ProofTrace.Entry
• proj : ProofTrace.Entry → Option ProofEntryT
• inj_proj_eq (x : ProofTrace.Entry) (y : ProofEntryT) : (proj x = some y) = (x = inj y)
• proj_none_eq_erase (x : ProofTrace.Entry) : (TraceEntryHas.proj x = none) = (TraceEntryHas.proj x.erase = none)
• erase_commutes (entry : ProofEntryT) : (TraceEntryHas.inj entry).erase = TraceEntryHas.inj (ErasableProofEntry.erase entry)

class DY.ProofTraceTypes.HasStep {ExecEntryT1 ExecEntryT2 : outParam Type} (ProofEntryT1 : Type) (ProofEntryT2 : semiOutParam Type) [ErasableProofEntry ExecEntryT1 ProofEntryT1] [ErasableProofEntry ExecEntryT2 ProofEntryT2] [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] : Type

• proofInj : ProofEntryT1 → ProofEntryT2
• proofProj : ProofEntryT2 → Option ProofEntryT1
• proof_inj_proj_eq (x : ProofEntryT2) (y : ProofEntryT1) : (proofProj x = some y) = (x = proofInj y)
• proofProj_none_eq_erase (x : ProofEntryT2) : (proofProj x = none) = (ExecTraceTypes.HasStep.proj (ErasableProofEntry.erase x) = none)
• erase_commutes (entry : ProofEntryT1) : ErasableProofEntry.erase (proofInj entry) = ExecTraceTypes.HasStep.inj (ErasableProofEntry.erase entry)

@[instance_reducible]

instance DY.instProofTraceTypesHasItself [ExecTraceTypes] [ProofTraceTypes] : ProofTraceTypes.Has ProofTrace.Entry

Equations

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

@[instance_reducible]

instance DY.instProofTraceTypesHasStep [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT1 ExecEntryT2 : Type} (ProofEntryT1 ProofEntryT2 : Type) [ErasableProofEntry ExecEntryT1 ProofEntryT1] [ErasableProofEntry ExecEntryT2 ProofEntryT2] [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] [ProofTraceTypes.HasStep ProofEntryT1 ProofEntryT2] [ExecTraceTypes.Has ExecEntryT2] [ProofTraceTypes.Has ProofEntryT2] : ProofTraceTypes.Has ProofEntryT1

Equations

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

structure DY.ProofTraceTypes.combine {n : Nat} (ProofTypes : Fin n → Type) : Type

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

@[instance_reducible]

instance DY.instErasableProofEntryCombine {n : Nat} (ExecTypes ProofTypes : Fin n → Type) [(id : Fin n) → ErasableProofEntry (ExecTypes id) (ProofTypes id)] : ErasableProofEntry (ExecTraceTypes.combine ExecTypes) (ProofTraceTypes.combine ProofTypes)

Equations

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

@[instance_reducible]

instance DY.instProofTraceTypesCombineHasStep {n : Nat} (ExecTypes ProofTypes : Fin n → Type) [(id : Fin n) → ErasableProofEntry (ExecTypes id) (ProofTypes id)] (id : Fin n) : ProofTraceTypes.HasStep (ProofTypes id) (ProofTraceTypes.combine ProofTypes)

Equations

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

theorem DY.ProofTrace.Entry.erase_eq_imp_exists [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT ProofEntryT : Type} [ErasableProofEntry ExecEntryT ProofEntryT] [ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] {entry : Entry} {result : ExecEntryT} : entry.erase = TraceEntryHas.inj result ↔ ∃ (result' : ProofEntryT), entry = TraceEntryHas.inj result' ∧ ErasableProofEntry.erase result' = result

theorem DY.ProofTrace.Entry.at?_eq_none_erase [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT ProofEntryT : Type} [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] (tr : ProofTrace) (i : Nat) : (Trace.at? tr i = none) = (Trace.at? (Trace.erase tr) i = none)

theorem DY.ProofTrace.Entry.at?_eq_some_erase [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT ProofEntryT : Type} [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] (tr : ProofTrace) (i : Nat) (entry : ProofEntryT) : Trace.at? tr i = some entry → Trace.at? (Trace.erase tr) i = some (ErasableProofEntry.erase entry)

theorem DY.Trace.append_erase [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT ProofEntryT : Type} [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] (tr : ProofTrace) (entry : ProofEntryT) : (append tr entry).erase = append (erase tr) (ErasableProofEntry.erase entry)

class DY.SubTraceInvariant [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT : outParam Type} (ProofEntryT : Type) [ErasableProofEntry ExecEntryT ProofEntryT] : Type

• invariant : ProofTrace → ProofEntryT → Prop

class DY.TraceInvariant [ExecTraceTypes] [ProofTraceTypes] : Type

• tc_inv : SubTraceInvariant ProofTrace.Entry

@[instance_reducible]

instance DY.instSubTraceInvariantEntryEntryOfProofTraceTypesOfTraceInvariant [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : SubTraceInvariant ProofTrace.Entry

Equations

• DY.instSubTraceInvariantEntryEntryOfProofTraceTypesOfTraceInvariant = DY.TraceInvariant.tc_inv

def DY.ProofTrace.Entry.Invariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (trBefore : ProofTrace) (entry : Entry) : Prop

Equations

• DY.ProofTrace.Entry.Invariant trBefore entry = DY.SubTraceInvariant.invariant trBefore entry

def DY.Trace.Invariant [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (tr : ProofTrace) : Prop

Equations

• DY.Trace.nil.Invariant = True
• (trBefore.snoc entry).Invariant = (trBefore.Invariant ∧ DY.ProofTrace.Entry.Invariant trBefore entry)

class DY.TraceInvariant.Has [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {ExecEntryT : outParam Type} (ProofEntryT : Type) [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [SubTraceInvariant ProofEntryT] : Prop

• inv_commutes (trBefore : ProofTrace) (entry : ProofEntryT) : ProofTrace.Entry.Invariant trBefore (TraceEntryHas.inj entry) = SubTraceInvariant.invariant trBefore entry

class DY.TraceInvariant.HasStep [ExecTraceTypes] [ProofTraceTypes] {ExecEntryT1 ExecEntryT2 : outParam Type} (ProofEntryT1 ProofEntryT2 : Type) [ErasableProofEntry ExecEntryT1 ProofEntryT1] [ErasableProofEntry ExecEntryT2 ProofEntryT2] [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] [ProofTraceTypes.HasStep ProofEntryT1 ProofEntryT2] [SubTraceInvariant ProofEntryT1] [SubTraceInvariant ProofEntryT2] : Prop

• inv_commutes (trBefore : ProofTrace) (entry : ProofEntryT1) : SubTraceInvariant.invariant trBefore (ProofTraceTypes.HasStep.proofInj entry) = SubTraceInvariant.invariant trBefore entry

instance DY.instTraceInvariantHasItself [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] : TraceInvariant.Has ProofTrace.Entry

instance DY.instTraceInvariantHasStep [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {ExecEntryT1 ProofEntryT1 ExecEntryT2 ProofEntryT2 : Type} [ErasableProofEntry ExecEntryT1 ProofEntryT1] [ErasableProofEntry ExecEntryT2 ProofEntryT2] [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] [ProofTraceTypes.HasStep ProofEntryT1 ProofEntryT2] [ExecTraceTypes.Has ExecEntryT2] [ProofTraceTypes.Has ProofEntryT2] [SubTraceInvariant ProofEntryT1] [SubTraceInvariant ProofEntryT2] [TraceInvariant.HasStep ProofEntryT1 ProofEntryT2] [TraceInvariant.Has ProofEntryT2] : TraceInvariant.Has ProofEntryT1

@[instance_reducible]

instance DY.SubTraceInvariant.combine [ExecTraceTypes] [ProofTraceTypes] {n : Nat} {ExecTypes ProofTypes : Fin n → Type} [(id : Fin n) → ErasableProofEntry (ExecTypes id) (ProofTypes id)] [(id : Fin n) → SubTraceInvariant (ProofTypes id)] : SubTraceInvariant (ProofTraceTypes.combine ProofTypes)

Equations

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

instance DY.instTraceInvariantCombineHasStep [ExecTraceTypes] [ProofTraceTypes] {n : Nat} {ExecTypes : Fin n → Type} (ProofTypes : Fin n → Type) [(id : Fin n) → ErasableProofEntry (ExecTypes id) (ProofTypes id)] [(id : Fin n) → SubTraceInvariant (ProofTypes id)] (id : Fin n) : TraceInvariant.HasStep (ProofTypes id) (ProofTraceTypes.combine ProofTypes)

theorem DY.Trace.invariant_append [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] {ExecEntryT ProofEntryT : Type} [ErasableProofEntry ExecEntryT ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [SubTraceInvariant ProofEntryT] [TraceInvariant.Has ProofEntryT] (tr : ProofTrace) (entry : ProofEntryT) : (append tr entry).Invariant = (Invariant tr ∧ SubTraceInvariant.invariant tr entry)

theorem DY.Trace.invariant_at [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] (tr : ProofTrace) (i : Nat) (h_i : i < length tr) : Invariant tr → ProofTrace.Entry.Invariant («prefix» tr i) («at» tr i h_i)