Theory /Cortex /Pulse /Fact

Cortex.Pulse.Fact

proofs

On this page

Overview
Context
Theorem Split
Worker Outcomes
Durable Node Facts
Invariant Preservation
Frontier-Fold Accumulation
Disjoint-Key Accumulation

Imports

import Cortex.Pulse.Frontier
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Perm.Basic

Overview

Frontier workers produce node-local facts. The fixed-topology kernel only needs the node key, the resulting status, and an optional output; payload and failure detail contents remain abstract.

Context

The runtime applies a wave of frontier results by folding node-local updates into a graph state. The theorem-level fact this page needs is that two results for distinct nodes commute because they update disjoint keys.

Theorem Split

The page defines abstract worker outcomes, packages them as durable node results, and proves the disjoint-key commutativity lemma used by later frontier-fold proofs. Arbitrary node facts are not assumed safe: the Admissible predicate records the frontier precondition needed by preservation theorems.

namespace Cortex.Pulse

Worker Outcomes

NodeOutcome payload is the abstract worker outcome for a single node.

inductive NodeOutcome (payload : Type v) : Type v where
  | succeeded : payload → NodeOutcome payload
  | skipped : NodeOutcome payload
  | suspended : NodeOutcome payload
  | failed : NodeOutcome payload
  | timedOut : NodeOutcome payload
  | cancelled : NodeOutcome payload
  | shutdown : NodeOutcome payload
  | runCancelled : NodeOutcome payload
  | rewritten : payload → NodeOutcome payload
  deriving Repr

namespace NodeOutcomevariable {payload : Type v}

NodeOutcome.status outcome is the status contributed by an outcome.

def status : NodeOutcome payload → NodeStatus
  | succeeded _ => NodeStatus.completed
  | skipped => NodeStatus.skipped
  | suspended => NodeStatus.waiting
  | failed => NodeStatus.failed
  | timedOut => NodeStatus.failed
  | cancelled => NodeStatus.interrupted
  | shutdown => NodeStatus.interrupted
  | runCancelled => NodeStatus.interrupted
  | rewritten _ => NodeStatus.rewritten

NodeOutcome.output outcome is the optional output contributed by an outcome.

def output : NodeOutcome payload → Option payload
  | succeeded value => some value
  | rewritten value => some value
  | skipped => none
  | suspended => none
  | failed => none
  | timedOut => none
  | cancelled => none
  | shutdown => none
  | runCancelled => none

output_respects_status says emitted outputs match statuses that own payloads.

theorem output_respects_status
    (outcome : NodeOutcome payload)
    (value : payload)
    (hOutput : output outcome = some value) :
    NodeStatus.mayHaveOutput (status outcome) := bypayload:Type voutcome:NodeOutcome payloadvalue:payloadhOutput:outcome.output = some value⊢ outcome.status.mayHaveOutput
  cases outcomesucceededpayload:Type vvalue:payloada✝:payloadhOutput:(succeeded a✝).output = some value⊢ (succeeded a✝).status.mayHaveOutputskippedpayload:Type vvalue:payloadhOutput:skipped.output = some value⊢ skipped.status.mayHaveOutputsuspendedpayload:Type vvalue:payloadhOutput:suspended.output = some value⊢ suspended.status.mayHaveOutputfailedpayload:Type vvalue:payloadhOutput:failed.output = some value⊢ failed.status.mayHaveOutputtimedOutpayload:Type vvalue:payloadhOutput:timedOut.output = some value⊢ timedOut.status.mayHaveOutputcancelledpayload:Type vvalue:payloadhOutput:cancelled.output = some value⊢ cancelled.status.mayHaveOutputshutdownpayload:Type vvalue:payloadhOutput:shutdown.output = some value⊢ shutdown.status.mayHaveOutputrunCancelledpayload:Type vvalue:payloadhOutput:runCancelled.output = some value⊢ runCancelled.status.mayHaveOutputrewrittenpayload:Type vvalue:payloada✝:payloadhOutput:(rewritten a✝).output = some value⊢ (rewritten a✝).status.mayHaveOutput <;>succeededpayload:Type vvalue:payloada✝:payloadhOutput:(succeeded a✝).output = some value⊢ (succeeded a✝).status.mayHaveOutputskippedpayload:Type vvalue:payloadhOutput:skipped.output = some value⊢ skipped.status.mayHaveOutputsuspendedpayload:Type vvalue:payloadhOutput:suspended.output = some value⊢ suspended.status.mayHaveOutputfailedpayload:Type vvalue:payloadhOutput:failed.output = some value⊢ failed.status.mayHaveOutputtimedOutpayload:Type vvalue:payloadhOutput:timedOut.output = some value⊢ timedOut.status.mayHaveOutputcancelledpayload:Type vvalue:payloadhOutput:cancelled.output = some value⊢ cancelled.status.mayHaveOutputshutdownpayload:Type vvalue:payloadhOutput:shutdown.output = some value⊢ shutdown.status.mayHaveOutputrunCancelledpayload:Type vvalue:payloadhOutput:runCancelled.output = some value⊢ runCancelled.status.mayHaveOutputrewrittenpayload:Type vvalue:payloada✝:payloadhOutput:(rewritten a✝).output = some value⊢ (rewritten a✝).status.mayHaveOutput simp [output, status, NodeStatus.mayHaveOutput] at hOutput ⊢All goals completed! 🐙

status_ne_running says durable worker outcomes never write running.

theorem status_ne_running
    (outcome : NodeOutcome payload) :
    status outcome ≠ NodeStatus.running := bypayload:Type voutcome:NodeOutcome payload⊢ outcome.status ≠ NodeStatus.running
  cases outcomesucceededpayload:Type va✝:payload⊢ (succeeded a✝).status ≠ NodeStatus.runningskippedpayload:Type v⊢ skipped.status ≠ NodeStatus.runningsuspendedpayload:Type v⊢ suspended.status ≠ NodeStatus.runningfailedpayload:Type v⊢ failed.status ≠ NodeStatus.runningtimedOutpayload:Type v⊢ timedOut.status ≠ NodeStatus.runningcancelledpayload:Type v⊢ cancelled.status ≠ NodeStatus.runningshutdownpayload:Type v⊢ shutdown.status ≠ NodeStatus.runningrunCancelledpayload:Type v⊢ runCancelled.status ≠ NodeStatus.runningrewrittenpayload:Type va✝:payload⊢ (rewritten a✝).status ≠ NodeStatus.running <;>succeededpayload:Type va✝:payload⊢ (succeeded a✝).status ≠ NodeStatus.runningskippedpayload:Type v⊢ skipped.status ≠ NodeStatus.runningsuspendedpayload:Type v⊢ suspended.status ≠ NodeStatus.runningfailedpayload:Type v⊢ failed.status ≠ NodeStatus.runningtimedOutpayload:Type v⊢ timedOut.status ≠ NodeStatus.runningcancelledpayload:Type v⊢ cancelled.status ≠ NodeStatus.runningshutdownpayload:Type v⊢ shutdown.status ≠ NodeStatus.runningrunCancelledpayload:Type v⊢ runCancelled.status ≠ NodeStatus.runningrewrittenpayload:Type va✝:payload⊢ (rewritten a✝).status ≠ NodeStatus.running simp [status]All goals completed! 🐙

end NodeOutcome

Durable Node Facts

NodeResult ν payload is the durable fact emitted for one node.

structure NodeResult (ν : Type u) (payload : Type v) where

node is the state key updated by this fact.

node : ν

outcome is the abstract result for the node.

outcome : NodeOutcome payloadnamespace NodeResultvariable {ν : Type u} {payload : Type v}

InTopology G result says a durable node fact targets a topology node.

def InTopology (G : DAG ν) (result : NodeResult ν payload) : Prop :=
  result.node ∈ G.nodes

Admissible G state result says a node fact came from the executable frontier.

def Admissible
    (G : DAG ν)
    (state : GraphState ν payload)
    (result : NodeResult ν payload) : Prop :=
  InTopology G result ∧ DirectReady G state result.node

admissible_inTopology extracts the topology target precondition.

theorem admissible_inTopology
    {G : DAG ν}
    {state : GraphState ν payload}
    {result : NodeResult ν payload}
    (hResult : Admissible G state result) :
    InTopology G result :=
  hResult.1

admissible_directReady extracts the executable-frontier precondition.

theorem admissible_directReady
    {G : DAG ν}
    {state : GraphState ν payload}
    {result : NodeResult ν payload}
    (hResult : Admissible G state result) :
    DirectReady G state result.node :=
  hResult.2

admissible_ready turns an admissible runtime fact into proof-level readiness.

theorem admissible_ready
    (G : DAG ν)
    (state : GraphState ν payload)
    (result : NodeResult ν payload)
    (hCausal : CausalHistoryClosed G state)
    (hResult : Admissible G state result) :
    Ready G state result.node :=
  directReady_ready_of_causalHistoryClosed G state hCausal hResult.2

applyNodeFact result state applies a node-local fact to the graph state.

def applyNodeFact [DecidableEq ν]
    (result : NodeResult ν payload)
    (state : GraphState ν payload) : GraphState ν payload where
  status := fun n =>
    if n = result.node then result.outcome.status else state.status n
  output := fun n =>
    if n = result.node then result.outcome.output else state.output n

Invariant Preservation

applyNodeFact_preserves_topologyDomain preserves off-topology absence.

theorem applyNodeFact_preserves_topologyDomain [DecidableEq ν]
    (G : DAG ν)
    (result : NodeResult ν payload)
    (state : GraphState ν payload)
    (hDomain : GraphState.topologyDomain G state)
    (hResult : InTopology G result) :
    GraphState.topologyDomain G (applyNodeFact result state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G result⊢ GraphState.topologyDomain G (result.applyNodeFact state)
  intro node hNotMemν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodes⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = none
  by_cases hNode : node = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:node = result.node⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = nonenegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.node⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = none
  ·posν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:node = result.node⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = none subst nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resulthNotMem:result.node ∉ G.nodes⊢ (result.applyNodeFact state).status result.node = NodeStatus.pending ∧
  (result.applyNodeFact state).output result.node = none
    exact False.elim (hNotMem hResult)All goals completed! 🐙
  ·negν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.node⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = none rcases hDomain node hNotMem with ⟨hStatus, hOutput⟩negν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.nodehStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (result.applyNodeFact state).status node = NodeStatus.pending ∧ (result.applyNodeFact state).output node = none
    constructorneg.leftν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.nodehStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (result.applyNodeFact state).status node = NodeStatus.pendingneg.rightν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.nodehStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (result.applyNodeFact state).output node = none
    ·neg.leftν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.nodehStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (result.applyNodeFact state).status node = NodeStatus.pending simp [applyNodeFact, hNode, hStatus]All goals completed! 🐙
    ·neg.rightν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:InTopology G resultnode:νhNotMem:node ∉ G.nodeshNode:¬node = result.nodehStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (result.applyNodeFact state).output node = none simp [applyNodeFact, hNode, hOutput]All goals completed! 🐙

applyNodeFact_preserves_outputsRespectStatuses preserves output ownership.

theorem applyNodeFact_preserves_outputsRespectStatuses [DecidableEq ν]
    (result : NodeResult ν payload)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsRespectStatuses state) :
    GraphState.outputsRespectStatuses (applyNodeFact result state) := byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatuses⊢ (result.applyNodeFact state).outputsRespectStatuses
  intro node valueν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payload⊢ (result.applyNodeFact state).output node = some value → ((result.applyNodeFact state).status node).mayHaveOutput hOutputν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some value⊢ ((result.applyNodeFact state).status node).mayHaveOutput
  by_cases hNode : node = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some valuehNode:node = result.node⊢ ((result.applyNodeFact state).status node).mayHaveOutputnegν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some valuehNode:¬node = result.node⊢ ((result.applyNodeFact state).status node).mayHaveOutput
  ·posν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some valuehNode:node = result.node⊢ ((result.applyNodeFact state).status node).mayHaveOutput subst nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesvalue:payloadhOutput:(result.applyNodeFact state).output result.node = some value⊢ ((result.applyNodeFact state).status result.node).mayHaveOutput
    simp [applyNodeFact] at hOutput ⊢posν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesvalue:payloadhOutput:result.outcome.output = some value⊢ result.outcome.status.mayHaveOutput
    exact NodeOutcome.output_respects_status result.outcome value hOutputAll goals completed! 🐙
  ·negν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some valuehNode:¬node = result.node⊢ ((result.applyNodeFact state).status node).mayHaveOutput have hOriginalOutput : state.output node = some value := byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatuses⊢ (result.applyNodeFact state).outputsRespectStatuses
      simpa [applyNodeFact, hNode] using hOutputAll goals completed! 🐙
    have hMayHaveOutput : NodeStatus.mayHaveOutput (state.status node) :=
      hOutputs node value hOriginalOutputnegν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(result.applyNodeFact state).output node = some valuehNode:¬node = result.nodehOriginalOutput:state.output node = some valuehMayHaveOutput:(state.status node).mayHaveOutput⊢ ((result.applyNodeFact state).status node).mayHaveOutput
    simpa [applyNodeFact, hNode] using hMayHaveOutputAll goals completed! 🐙

applyNodeFact_preserves_outputsCompleteForStatuses preserves required outputs.

theorem applyNodeFact_preserves_outputsCompleteForStatuses [DecidableEq ν]
    (result : NodeResult ν payload)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsCompleteForStatuses state) :
    GraphState.outputsCompleteForStatuses (applyNodeFact result state) := byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses⊢ (result.applyNodeFact state).outputsCompleteForStatuses
  intro node hRequiresOutputν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutput⊢ ∃ value, (result.applyNodeFact state).output node = some value
  by_cases hNode : node = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:node = result.node⊢ ∃ value, (result.applyNodeFact state).output node = some valuenegν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:¬node = result.node⊢ ∃ value, (result.applyNodeFact state).output node = some value
  ·posν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:node = result.node⊢ ∃ value, (result.applyNodeFact state).output node = some value subst nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutput⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
    cases hOutcome : result.outcome with
    | succeeded value =>pos.succeededν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputvalue:payloadhOutcome:result.outcome = NodeOutcome.succeeded value⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        exact ⟨value, byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputvalue:payloadhOutcome:result.outcome = NodeOutcome.succeeded value⊢ (result.applyNodeFact state).output result.node = some value simp [applyNodeFact, NodeOutcome.output, hOutcome]All goals completed! 🐙⟩
    | skipped =>pos.skippedν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.skipped⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | suspended =>pos.suspendedν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.suspended⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | failed =>pos.failedν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.failed⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | timedOut =>pos.timedOutν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.timedOut⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | cancelled =>pos.cancelledν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.cancelled⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | shutdown =>pos.shutdownν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.shutdown⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | runCancelled =>pos.runCancelledν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputhOutcome:result.outcome = NodeOutcome.runCancelled⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        simp
          [ applyNodeFact
          , NodeOutcome.status
          , NodeStatus.requiresOutput
          , hOutcome
          ] at hRequiresOutputAll goals completed! 🐙
    | rewritten value =>pos.rewrittenν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputvalue:payloadhOutcome:result.outcome = NodeOutcome.rewritten value⊢ ∃ value, (result.applyNodeFact state).output result.node = some value
        exact ⟨value, byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshRequiresOutput:((result.applyNodeFact state).status result.node).requiresOutputvalue:payloadhOutcome:result.outcome = NodeOutcome.rewritten value⊢ (result.applyNodeFact state).output result.node = some value simp [applyNodeFact, NodeOutcome.output, hOutcome]All goals completed! 🐙⟩
  ·negν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:¬node = result.node⊢ ∃ value, (result.applyNodeFact state).output node = some value have hOriginalRequires : NodeStatus.requiresOutput (state.status node) := byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses⊢ (result.applyNodeFact state).outputsCompleteForStatuses
      simpa [applyNodeFact, hNode] using hRequiresOutputAll goals completed! 🐙
    rcases hOutputs node hOriginalRequires with ⟨value, hOutput⟩negν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:¬node = result.nodehOriginalRequires:(state.status node).requiresOutputvalue:payloadhOutput:state.output node = some value⊢ ∃ value, (result.applyNodeFact state).output node = some value
    exact ⟨value, byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((result.applyNodeFact state).status node).requiresOutputhNode:¬node = result.nodehOriginalRequires:(state.status node).requiresOutputvalue:payloadhOutput:state.output node = some value⊢ (result.applyNodeFact state).output node = some value simpa [applyNodeFact, hNode] using hOutputAll goals completed! 🐙⟩

applyNodeFact_preserves_noRunning preserves the absence of running nodes.

theorem applyNodeFact_preserves_noRunning [DecidableEq ν]
    (result : NodeResult ν payload)
    (state : GraphState ν payload)
    (hNoRunning : GraphState.noRunningNodes state) :
    GraphState.noRunningNodes (applyNodeFact result state) := byν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodes⊢ (result.applyNodeFact state).noRunningNodes
  intro nodeν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:ν⊢ (result.applyNodeFact state).status node ≠ NodeStatus.running
  by_cases hNode : node = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhNode:node = result.node⊢ (result.applyNodeFact state).status node ≠ NodeStatus.runningnegν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhNode:¬node = result.node⊢ (result.applyNodeFact state).status node ≠ NodeStatus.running
  ·posν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhNode:node = result.node⊢ (result.applyNodeFact state).status node ≠ NodeStatus.running subst nodeposν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodes⊢ (result.applyNodeFact state).status result.node ≠ NodeStatus.running
    simpa [applyNodeFact] using NodeOutcome.status_ne_running result.outcomeAll goals completed! 🐙
  ·negν:Type upayload:Type vinst✝:DecidableEq νresult:NodeResult ν payloadstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhNode:¬node = result.node⊢ (result.applyNodeFact state).status node ≠ NodeStatus.running simpa [applyNodeFact, hNode] using hNoRunning nodeAll goals completed! 🐙

applyNodeFact_preserves_causalHistoryClosed preserves causal history for admissible facts.

theorem applyNodeFact_preserves_causalHistoryClosed [DecidableEq ν]
    (G : DAG ν)
    (result : NodeResult ν payload)
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state)
    (hResult : Admissible G state result) :
    CausalHistoryClosed G (applyNodeFact result state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state result⊢ CausalHistoryClosed G (result.applyNodeFact state)
  classical
  have hReady : Ready G state result.node :=
    admissible_ready G state result hCausal hResultν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.node⊢ CausalHistoryClosed G (result.applyNodeFact state)
  intro node hUnblocksν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessors⊢ ∀ (predecessor : ν), G.reaches predecessor node → ((result.applyNodeFact state).status predecessor).terminal predecessorν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:ν⊢ G.reaches predecessor node → ((result.applyNodeFact state).status predecessor).terminal hReachν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor node⊢ ((result.applyNodeFact state).status predecessor).terminal
  by_cases hNode : node = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:node = result.node⊢ ((result.applyNodeFact state).status predecessor).terminalnegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal
  ·posν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:node = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal subst nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.node⊢ ((result.applyNodeFact state).status predecessor).terminal
    by_cases hPred : predecessor = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.nodehPred:predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminalnegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.nodehPred:¬predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal
    ·posν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.nodehPred:predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal subst predecessorposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodehUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches result.node result.node⊢ ((result.applyNodeFact state).status result.node).terminal
      exact False.elim (G.not_reaches_self result.node hReach)All goals completed! 🐙
    ·negν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.nodehPred:¬predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal have hOriginalTerminal : NodeStatus.terminal (state.status predecessor) :=
        hReady.2.2 predecessor hReachnegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodepredecessor:νhUnblocks:((result.applyNodeFact state).status result.node).unblocksSuccessorshReach:G.reaches predecessor result.nodehPred:¬predecessor = result.nodehOriginalTerminal:(state.status predecessor).terminal⊢ ((result.applyNodeFact state).status predecessor).terminal
      simpa [applyNodeFact, hPred] using hOriginalTerminalAll goals completed! 🐙
  ·negν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal have hOriginalUnblocks : NodeStatus.unblocksSuccessors (state.status node) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state result⊢ CausalHistoryClosed G (result.applyNodeFact state)
      simpa [applyNodeFact, hNode] using hUnblocksAll goals completed! 🐙
    by_cases hPred : predecessor = result.nodeposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshPred:predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminalnegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshPred:¬predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal
    ·posν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshPred:predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal subst predecessorposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorshNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshReach:G.reaches result.node node⊢ ((result.applyNodeFact state).status result.node).terminal
      have hOriginalTerminal : NodeStatus.terminal (state.status result.node) :=
        hCausal node hOriginalUnblocks result.node hReachposν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorshNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshReach:G.reaches result.node nodehOriginalTerminal:(state.status result.node).terminal⊢ ((result.applyNodeFact state).status result.node).terminal
      have hPendingTerminal : NodeStatus.terminal NodeStatus.pending := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state result⊢ CausalHistoryClosed G (result.applyNodeFact state)
        simpa [hReady.2.1] using hOriginalTerminalAll goals completed! 🐙
      exact False.elim (NodeStatus.pending_not_terminal hPendingTerminal)All goals completed! 🐙
    ·negν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshPred:¬predecessor = result.node⊢ ((result.applyNodeFact state).status predecessor).terminal have hOriginalTerminal : NodeStatus.terminal (state.status predecessor) :=
        hCausal node hOriginalUnblocks predecessor hReachnegν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthReady:Ready G state result.nodenode:νhUnblocks:((result.applyNodeFact state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehNode:¬node = result.nodehOriginalUnblocks:(state.status node).unblocksSuccessorshPred:¬predecessor = result.nodehOriginalTerminal:(state.status predecessor).terminal⊢ ((result.applyNodeFact state).status predecessor).terminal
      simpa [applyNodeFact, hPred] using hOriginalTerminalAll goals completed! 🐙

Frontier-Fold Accumulation

applyNodeFacts results state folds node-local facts in list order.

def applyNodeFacts [DecidableEq ν]
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload) : GraphState ν payload :=
  results.foldl (fun current result => applyNodeFact result current) state

AllAdmissibleFold G state results requires each folded fact to be frontier-admissible.

def AllAdmissibleFold [DecidableEq ν]
    (G : DAG ν) : GraphState ν payload → List (NodeResult ν payload) → Prop
  | _state, [] => True
  | state, result :: rest =>
      Admissible G state result ∧
        AllAdmissibleFold G (applyNodeFact result state) rest

applyNodeFacts_preserves_topologyDomain preserves off-topology absence.

theorem applyNodeFacts_preserves_topologyDomain [DecidableEq ν]
    (G : DAG ν)
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload)
    (hDomain : GraphState.topologyDomain G state)
    (hResults : AllAdmissibleFold G state results) :
    GraphState.topologyDomain G (applyNodeFacts results state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresults:List (NodeResult ν payload)state:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResults:AllAdmissibleFold G state results⊢ GraphState.topologyDomain G (applyNodeFacts results state)
  induction results generalizing state with
  | nil =>nilν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResults:AllAdmissibleFold G state []⊢ GraphState.topologyDomain G (applyNodeFacts [] state) simpa [applyNodeFacts] using hDomainAll goals completed! 🐙
  | cons result rest ih =>consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  GraphState.topologyDomain G state →
    AllAdmissibleFold G state rest → GraphState.topologyDomain G (applyNodeFacts rest state)state:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResults:AllAdmissibleFold G state (result :: rest)⊢ GraphState.topologyDomain G (applyNodeFacts (result :: rest) state)
      rcases hResults with ⟨hResult, hRest⟩consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  GraphState.topologyDomain G state →
    AllAdmissibleFold G state rest → GraphState.topologyDomain G (applyNodeFacts rest state)state:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) rest⊢ GraphState.topologyDomain G (applyNodeFacts (result :: rest) state)
      have hStep : GraphState.topologyDomain G (applyNodeFact result state) :=
        applyNodeFact_preserves_topologyDomain G result state hDomain hResult.1consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  GraphState.topologyDomain G state →
    AllAdmissibleFold G state rest → GraphState.topologyDomain G (applyNodeFacts rest state)state:GraphState ν payloadhDomain:GraphState.topologyDomain G statehResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) resthStep:GraphState.topologyDomain G (result.applyNodeFact state)⊢ GraphState.topologyDomain G (applyNodeFacts (result :: rest) state)
      simpa [applyNodeFacts] using ih (applyNodeFact result state) hStep hRestAll goals completed! 🐙

applyNodeFacts_preserves_outputsRespectStatuses preserves output ownership.

theorem applyNodeFacts_preserves_outputsRespectStatuses [DecidableEq ν]
    (G : DAG ν)
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsRespectStatuses state)
    (hResults : AllAdmissibleFold G state results) :
    GraphState.outputsRespectStatuses (applyNodeFacts results state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresults:List (NodeResult ν payload)state:GraphState ν payloadhOutputs:state.outputsRespectStatuseshResults:AllAdmissibleFold G state results⊢ (applyNodeFacts results state).outputsRespectStatuses
  induction results generalizing state with
  | nil =>nilν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatuseshResults:AllAdmissibleFold G state []⊢ (applyNodeFacts [] state).outputsRespectStatuses simpa [applyNodeFacts] using hOutputsAll goals completed! 🐙
  | cons result rest ih =>consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsRespectStatuses → AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsRespectStatusesstate:GraphState ν payloadhOutputs:state.outputsRespectStatuseshResults:AllAdmissibleFold G state (result :: rest)⊢ (applyNodeFacts (result :: rest) state).outputsRespectStatuses
      rcases hResults with ⟨_hResult, hRest⟩consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsRespectStatuses → AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsRespectStatusesstate:GraphState ν payloadhOutputs:state.outputsRespectStatuses_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) rest⊢ (applyNodeFacts (result :: rest) state).outputsRespectStatuses
      have hStep :
          GraphState.outputsRespectStatuses (applyNodeFact result state) :=
        applyNodeFact_preserves_outputsRespectStatuses result state hOutputsconsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsRespectStatuses → AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsRespectStatusesstate:GraphState ν payloadhOutputs:state.outputsRespectStatuses_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) resthStep:(result.applyNodeFact state).outputsRespectStatuses⊢ (applyNodeFacts (result :: rest) state).outputsRespectStatuses
      simpa [applyNodeFacts] using ih (applyNodeFact result state) hStep hRestAll goals completed! 🐙

applyNodeFacts_preserves_outputsCompleteForStatuses preserves required outputs.

theorem applyNodeFacts_preserves_outputsCompleteForStatuses [DecidableEq ν]
    (G : DAG ν)
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsCompleteForStatuses state)
    (hResults : AllAdmissibleFold G state results) :
    GraphState.outputsCompleteForStatuses (applyNodeFacts results state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresults:List (NodeResult ν payload)state:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshResults:AllAdmissibleFold G state results⊢ (applyNodeFacts results state).outputsCompleteForStatuses
  induction results generalizing state with
  | nil =>nilν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshResults:AllAdmissibleFold G state []⊢ (applyNodeFacts [] state).outputsCompleteForStatuses simpa [applyNodeFacts] using hOutputsAll goals completed! 🐙
  | cons result rest ih =>consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsCompleteForStatuses →
    AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsCompleteForStatusesstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuseshResults:AllAdmissibleFold G state (result :: rest)⊢ (applyNodeFacts (result :: rest) state).outputsCompleteForStatuses
      rcases hResults with ⟨_hResult, hRest⟩consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsCompleteForStatuses →
    AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsCompleteForStatusesstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) rest⊢ (applyNodeFacts (result :: rest) state).outputsCompleteForStatuses
      have hStep :
          GraphState.outputsCompleteForStatuses (applyNodeFact result state) :=
        applyNodeFact_preserves_outputsCompleteForStatuses result state hOutputsconsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.outputsCompleteForStatuses →
    AllAdmissibleFold G state rest → (applyNodeFacts rest state).outputsCompleteForStatusesstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) resthStep:(result.applyNodeFact state).outputsCompleteForStatuses⊢ (applyNodeFacts (result :: rest) state).outputsCompleteForStatuses
      simpa [applyNodeFacts] using ih (applyNodeFact result state) hStep hRestAll goals completed! 🐙

applyNodeFacts_preserves_noRunning preserves the absence of running nodes.

theorem applyNodeFacts_preserves_noRunning [DecidableEq ν]
    (G : DAG ν)
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload)
    (hNoRunning : GraphState.noRunningNodes state)
    (hResults : AllAdmissibleFold G state results) :
    GraphState.noRunningNodes (applyNodeFacts results state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresults:List (NodeResult ν payload)state:GraphState ν payloadhNoRunning:state.noRunningNodeshResults:AllAdmissibleFold G state results⊢ (applyNodeFacts results state).noRunningNodes
  induction results generalizing state with
  | nil =>nilν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodeshResults:AllAdmissibleFold G state []⊢ (applyNodeFacts [] state).noRunningNodes simpa [applyNodeFacts] using hNoRunningAll goals completed! 🐙
  | cons result rest ih =>consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.noRunningNodes → AllAdmissibleFold G state rest → (applyNodeFacts rest state).noRunningNodesstate:GraphState ν payloadhNoRunning:state.noRunningNodeshResults:AllAdmissibleFold G state (result :: rest)⊢ (applyNodeFacts (result :: rest) state).noRunningNodes
      rcases hResults with ⟨_hResult, hRest⟩consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.noRunningNodes → AllAdmissibleFold G state rest → (applyNodeFacts rest state).noRunningNodesstate:GraphState ν payloadhNoRunning:state.noRunningNodes_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) rest⊢ (applyNodeFacts (result :: rest) state).noRunningNodes
      have hStep : GraphState.noRunningNodes (applyNodeFact result state) :=
        applyNodeFact_preserves_noRunning result state hNoRunningconsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  state.noRunningNodes → AllAdmissibleFold G state rest → (applyNodeFacts rest state).noRunningNodesstate:GraphState ν payloadhNoRunning:state.noRunningNodes_hResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) resthStep:(result.applyNodeFact state).noRunningNodes⊢ (applyNodeFacts (result :: rest) state).noRunningNodes
      simpa [applyNodeFacts] using ih (applyNodeFact result state) hStep hRestAll goals completed! 🐙

applyNodeFacts_preserves_causalHistoryClosed preserves causal history.

theorem applyNodeFacts_preserves_causalHistoryClosed [DecidableEq ν]
    (G : DAG ν)
    (results : List (NodeResult ν payload))
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state)
    (hResults : AllAdmissibleFold G state results) :
    CausalHistoryClosed G (applyNodeFacts results state) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresults:List (NodeResult ν payload)state:GraphState ν payloadhCausal:CausalHistoryClosed G statehResults:AllAdmissibleFold G state results⊢ CausalHistoryClosed G (applyNodeFacts results state)
  induction results generalizing state with
  | nil =>nilν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statehResults:AllAdmissibleFold G state []⊢ CausalHistoryClosed G (applyNodeFacts [] state) simpa [applyNodeFacts] using hCausalAll goals completed! 🐙
  | cons result rest ih =>consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  CausalHistoryClosed G state → AllAdmissibleFold G state rest → CausalHistoryClosed G (applyNodeFacts rest state)state:GraphState ν payloadhCausal:CausalHistoryClosed G statehResults:AllAdmissibleFold G state (result :: rest)⊢ CausalHistoryClosed G (applyNodeFacts (result :: rest) state)
      rcases hResults with ⟨hResult, hRest⟩consν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  CausalHistoryClosed G state → AllAdmissibleFold G state rest → CausalHistoryClosed G (applyNodeFacts rest state)state:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) rest⊢ CausalHistoryClosed G (applyNodeFacts (result :: rest) state)
      have hStep : CausalHistoryClosed G (applyNodeFact result state) :=
        applyNodeFact_preserves_causalHistoryClosed G result state hCausal hResultconsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νresult:NodeResult ν payloadrest:List (NodeResult ν payload)ih:∀ (state : GraphState ν payload),
  CausalHistoryClosed G state → AllAdmissibleFold G state rest → CausalHistoryClosed G (applyNodeFacts rest state)state:GraphState ν payloadhCausal:CausalHistoryClosed G statehResult:Admissible G state resulthRest:AllAdmissibleFold G (result.applyNodeFact state) resthStep:CausalHistoryClosed G (result.applyNodeFact state)⊢ CausalHistoryClosed G (applyNodeFacts (result :: rest) state)
      simpa [applyNodeFacts] using ih (applyNodeFact result state) hStep hRestAll goals completed! 🐙

Disjoint-Key Accumulation

applyNodeFact_comm proves facts for distinct nodes commute.

theorem applyNodeFact_comm [DecidableEq ν]
    (r1 r2 : NodeResult ν payload)
    (state : GraphState ν payload)
    (hDistinct : r1.node ≠ r2.node) :
    applyNodeFact r1 (applyNodeFact r2 state) =
      applyNodeFact r2 (applyNodeFact r1 state) := byν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.node⊢ r1.applyNodeFact (r2.applyNodeFact state) = r2.applyNodeFact (r1.applyNodeFact state)
  have hDistinctSymm : r2.node ≠ r1.node := byν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.node⊢ r1.applyNodeFact (r2.applyNodeFact state) = r2.applyNodeFact (r1.applyNodeFact state)
    intro hEqν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehEq:r2.node = r1.node⊢ False
    exact hDistinct hEq.symmAll goals completed! 🐙
  ext nhStatusν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:ν⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status nhOutput.aν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payload⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝
  ·hStatusν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:ν⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n by_cases h1 : n = r1.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status nnegν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n
    ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n by_cases h2 : n = r2.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status nnegν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n
      ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n exact False.elim (hDistinct (byν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.nodeh2:n = r2.node⊢ r1.node = r2.node rw [← h1, ← h2]All goals completed! 🐙))
      ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n simp [applyNodeFact, h1, hDistinct]All goals completed! 🐙
    ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n by_cases h2 : n = r2.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status nnegν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n
      ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n simp [applyNodeFact, h2, hDistinctSymm]All goals completed! 🐙
      ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νh1:¬n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).status n = (r2.applyNodeFact (r1.applyNodeFact state)).status n simp [applyNodeFact, h1, h2]All goals completed! 🐙
  ·hOutput.aν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payload⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ by_cases h1 : n = r1.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝
    ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ by_cases h2 : n = r2.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝
      ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ exact False.elim (hDistinct (byν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.nodeh2:n = r2.node⊢ r1.node = r2.node rw [← h1, ← h2]All goals completed! 🐙))
      ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ simp [applyNodeFact, h1, hDistinct]All goals completed! 🐙
    ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ by_cases h2 : n = r2.nodeposν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝
      ·posν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.nodeh2:n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ simp [applyNodeFact, h2, hDistinctSymm]All goals completed! 🐙
      ·negν:Type upayload:Type vinst✝:DecidableEq νr1:NodeResult ν payloadr2:NodeResult ν payloadstate:GraphState ν payloadhDistinct:r1.node ≠ r2.nodehDistinctSymm:r2.node ≠ r1.noden:νa✝:payloadh1:¬n = r1.nodeh2:¬n = r2.node⊢ (r1.applyNodeFact (r2.applyNodeFact state)).output n = some a✝ ↔
  (r2.applyNodeFact (r1.applyNodeFact state)).output n = some a✝ simp [applyNodeFact, h1, h2]All goals completed! 🐙

applyNodeFacts_perm_invariant lifts disjoint-key commutativity to fact folds.

theorem applyNodeFacts_perm_invariant [DecidableEq ν]
    {left right : List (NodeResult ν payload)}
    (hPerm : left.Perm right)
    (hDistinct : left.Pairwise (fun first second => first.node ≠ second.node))
    (state : GraphState ν payload) :
    applyNodeFacts left state = applyNodeFacts right state := byν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payload⊢ applyNodeFacts left state = applyNodeFacts right state
  unfold applyNodeFactsν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payload⊢ List.foldl (fun current result => result.applyNodeFact current) state left =
  List.foldl (fun current result => result.applyNodeFact current) state right
  refine hPerm.foldl_eq' ?_ stateν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payload⊢ ∀ x ∈ left,
  ∀ y ∈ left, ∀ (z : GraphState ν payload), y.applyNodeFact (x.applyNodeFact z) = x.applyNodeFact (y.applyNodeFact z)
  intro first hFirstν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ left⊢ ∀ y ∈ left,
  ∀ (z : GraphState ν payload), y.applyNodeFact (first.applyNodeFact z) = first.applyNodeFact (y.applyNodeFact z) secondν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payload⊢ second ∈ left →
  ∀ (z : GraphState ν payload),
    second.applyNodeFact (first.applyNodeFact z) = first.applyNodeFact (second.applyNodeFact z) hSecondν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ left⊢ ∀ (z : GraphState ν payload),
  second.applyNodeFact (first.applyNodeFact z) = first.applyNodeFact (second.applyNodeFact z) currentν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payload⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current)
  by_cases hSame : first = secondposν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:first = second⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current)negν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = second⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current)
  ·posν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:first = second⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current) subst secondposν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftcurrent:GraphState ν payloadhSecond:first ∈ left⊢ first.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (first.applyNodeFact current)
    rflAll goals completed! 🐙
  ·negν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = second⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current) have hSymm :
        Symmetric (fun first second : NodeResult ν payload => first.node ≠ second.node) := byν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payload⊢ applyNodeFacts left state = applyNodeFacts right state
      intro a bν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = seconda:NodeResult ν payloadb:NodeResult ν payload⊢ (fun first second => first.node ≠ second.node) a b → (fun first second => first.node ≠ second.node) b a hDistinctNodesν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = seconda:NodeResult ν payloadb:NodeResult ν payloadhDistinctNodes:a.node ≠ b.node⊢ b.node ≠ a.node hEqν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = seconda:NodeResult ν payloadb:NodeResult ν payloadhDistinctNodes:a.node ≠ b.nodehEq:b.node = a.node⊢ False
      exact hDistinctNodes hEq.symmAll goals completed! 🐙
    have hDistinctNodes : first.node ≠ second.node :=
      List.Pairwise.forall hSymm hDistinct hFirst hSecond hSamenegν:Type upayload:Type vinst✝:DecidableEq νleft:List (NodeResult ν payload)right:List (NodeResult ν payload)hPerm:left.Perm righthDistinct:List.Pairwise (fun first second => first.node ≠ second.node) leftstate:GraphState ν payloadfirst:NodeResult ν payloadhFirst:first ∈ leftsecond:NodeResult ν payloadhSecond:second ∈ leftcurrent:GraphState ν payloadhSame:¬first = secondhSymm:Symmetric fun first second => first.node ≠ second.nodehDistinctNodes:first.node ≠ second.node⊢ second.applyNodeFact (first.applyNodeFact current) = first.applyNodeFact (second.applyNodeFact current)
    exact (applyNodeFact_comm first second current hDistinctNodes).symmAll goals completed! 🐙

end NodeResultend Cortex.Pulse

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Pulse.DAG Next →Cortex.Pulse.Frontier