structure DY.ReachabilityConfig [ExecTraceTypes] : Type 1

• Input : Type
• PreCond : self.Input → ExecTrace → Prop
• step : self.Input → (Output : Type) × Traceful Output

@[reducible, inline]

abbrev DY.ReachabilityConfig.make [ExecTraceTypes] {α β : Type} (step : α → Traceful β) : ReachabilityConfig

Equations

• DY.ReachabilityConfig.make step = { Input := α, PreCond := fun (x : α) (x_1 : DY.ExecTrace) => True, step := fun (x : α) => ⟨β, step x⟩ }

def DY.ReachabilityConfig.combine [ExecTraceTypes] {α : Type} (configs : α → ReachabilityConfig) : ReachabilityConfig

Equations

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

class DY.ReachabilityConfig.HasStep [ExecTraceTypes] (config1 : ReachabilityConfig) (config2 : semiOutParam ReachabilityConfig) : Type

• inj : config1.Input → config2.Input
• pf_pre (input : config1.Input) (tr : ExecTrace) : config1.PreCond input tr = config2.PreCond (inj input) tr
• pf_step (input : config1.Input) : config1.step input = config2.step (inj input)

class DY.ReachabilityConfig.Has [ExecTraceTypes] (config1 config2 : ReachabilityConfig) : Type

• inj : config1.Input → config2.Input
• pf_pre (input : config1.Input) (tr : ExecTrace) : config1.PreCond input tr = config2.PreCond (inj input) tr
• pf_step (input : config1.Input) : config1.step input = config2.step (inj input)

@[instance_reducible]

instance DY.instReachabilityConfigHasItself [ExecTraceTypes] (config : ReachabilityConfig) : config.Has config

Equations

• DY.instReachabilityConfigHasItself config = { inj := fun (x : config.Input) => x, pf_pre := ⋯, pf_step := ⋯ }

@[instance_reducible]

instance DY.instReachabilityConfigHasStep [ExecTraceTypes] (config1 config2 config3 : ReachabilityConfig) [inst12 : config1.HasStep config2] [inst23 : config2.Has config3] : config1.Has config3

Equations

• DY.instReachabilityConfigHasStep config1 config2 config3 = { inj := fun (x : config1.Input) => DY.ReachabilityConfig.Has.inj (DY.ReachabilityConfig.HasStep.inj x), pf_pre := ⋯, pf_step := ⋯ }

@[instance_reducible]

instance DY.instReachabilityConfigCombineHasStep [ExecTraceTypes] {n : Nat} (configs : Fin n → ReachabilityConfig) (id : Fin n) : (configs id).HasStep (ReachabilityConfig.combine configs)

Equations

• DY.instReachabilityConfigCombineHasStep configs id = { inj := fun (x : (configs id).Input) => ⟨id, x⟩, pf_pre := ⋯, pf_step := ⋯ }

inductive DY.Trace.Reachable [ExecTraceTypes] (config : ReachabilityConfig) : ExecTrace → Prop

• Base [ExecTraceTypes] {config : ReachabilityConfig} : Reachable config nil
• Step [ExecTraceTypes] {config : ReachabilityConfig} {tr : ExecTrace} (input : config.Input) : config.PreCond input tr → Reachable config tr → Reachable config ((config.step input).snd.run tr).snd.val

def DY.Traceful.PreservesReachabilityFrom [ExecTraceTypes] {a : Type} (config : ReachabilityConfig) (f : Traceful a) (post : a → ExecTrace → Prop) (tr : ExecTrace) : Prop

Equations

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

def DY.Traceful.PreservesReachability [ExecTraceTypes] {a : Type} (config : ReachabilityConfig) (f : Traceful a) (pre : ExecTrace → Prop) (post : a → ExecTrace → Prop) : Prop

Equations

• DY.Traceful.PreservesReachability config f pre post = ∀ (tr : DY.ExecTrace), DY.Trace.Reachable config tr → pre tr → DY.Traceful.PreservesReachabilityFrom config f post tr

theorem DY.Traceful.PreservesReachabilityFrom_bind [ExecTraceTypes] {a b : Type} (config : ReachabilityConfig) (x : Traceful a) (f : a → Traceful b) (postF : b → ExecTrace → Prop) (preX : ExecTrace → Prop) (postX : a → ExecTrace → Prop) (tr : ExecTrace) (h_x : PreservesReachability config x preX postX) (h_tr_reachable : Trace.Reachable config tr) (h_pre_x : preX tr) (h_f : ∀ (x' : a) (trMid : ExecTrace), postX x' trMid → Trace.Reachable config trMid → tr ≤ trMid → PreservesReachabilityFrom config (f x') postF trMid) : PreservesReachabilityFrom config (x >>= f) postF tr

theorem DY.Traceful.PreservesReachability_base [ExecTraceTypes] (subConfig config : ReachabilityConfig) [subConfig.Has config] (input : subConfig.Input) : PreservesReachability config (subConfig.step input).snd (subConfig.PreCond input) fun (x : (subConfig.step input).fst) (x_1 : ExecTrace) => True

theorem DY.Traceful.PreservesReachabilityFrom_pure [ExecTraceTypes] {α : Type} (config : ReachabilityConfig) (x : α) (tr : ExecTrace) (post : α → ExecTrace → Prop) : Trace.Reachable config tr → post x tr → PreservesReachabilityFrom config (pure x) post tr

theorem DY.Traceful.PreservesReachability_to_Reachable [ExecTraceTypes] {a : Type} {config : ReachabilityConfig} {f : Traceful a} {pre : ExecTrace → Prop} {post : a → ExecTrace → Prop} (h : PreservesReachability config f pre post) : pre Trace.nil → Trace.Reachable config (f.run Trace.nil).snd.val