internlm/Lean-Github huggingface dataset:
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ i₂ ∈ s.rtr[Component.rcn] →
    (dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
      dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress)
Tactic:
intro _
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
    dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
    dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
Tactic:
constructor <;> intro ⟨hd, hp⟩
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress

case mpr
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress

case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ i₂ ∉ Set.insert i₁ s.progress
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
Tactic:
exact hd.trans $ Set.subset_insert i₁ s.progress
Proof state after:
no goals
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ i₂ ∉ Set.insert i₁ s.progress
Tactic:
exact Set.mem_insert_iff.not.mpr $ not_or.mpr ⟨hi.not_eq.symm, hp⟩
Proof state after:
no goals
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress

case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ i₂ ∉ s.progress
Theorem: Execution.State.Allows.iff_record_indep
Proof state before:
case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ i₂ ∉ s.progress
Tactic:
exact not_or.mp (Set.mem_insert_iff.not.mp hp) |>.right
Proof state after:
no goals
Theorem: Execution.State.Triggers.congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : autoParam (s₁.rtr = s₂.rtr) _auto✝
ht : autoParam (s₁.tag = s₂.tag) _auto✝
⊢ Triggers s₁ i ↔ Triggers s₂ i
Tactic:
simp [Triggers.def, hr, input_congr hr ht]
Proof state after:
no goals
Theorem: Execution.State.NextTag.isLeast
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ g ∈ lowerBounds {g' | g' ∈ scheduledTags s ∧ s.tag < g'}
Tactic:
simp [lowerBounds]
Proof state after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ ∀ ⦃a : Time.Tag⦄, a ∈ scheduledTags s → s.tag < a → g ≤ a
Theorem: Execution.State.NextTag.isLeast
Proof state before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ ∀ ⦃a : Time.Tag⦄, a ∈ scheduledTags s → s.tag < a → g ≤ a
Tactic:
exact n.least
Proof state after:
no goals
Theorem: Execution.State.Closed.progress_nonempty
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : Closed s
⊢ Set.Nonempty s.progress
Tactic:
simp_all [Closed, ←Partial.Nonempty.iff_ids_nonempty]
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : s.progress = Partial.ids (s.rtr[Component.rcn])
⊢ Partial.Nonempty (s.rtr[Component.rcn])
Theorem: Execution.State.Closed.progress_nonempty
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : s.progress = Partial.ids (s.rtr[Component.rcn])
⊢ Partial.Nonempty (s.rtr[Component.rcn])
Tactic:
exact n
Proof state after:
no goals
Theorem: Execution.State.Nontrivial.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e : s₁.rtr ≈ s₂.rtr
n : Nontrivial s₁
⊢ Nontrivial s₂
Tactic:
simp_all [Nontrivial, Equivalent.obj?_rcn_eq e]
Proof state after:
no goals
Theorem: Execution.State.Terminal.not_elim
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
⊢ ¬Closed s ∨ ∃ g, NextTag s g
Tactic:
by_contra h
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : ¬(¬Closed s ∨ ∃ g, NextTag s g)
⊢ False
Theorem: Execution.State.Terminal.not_elim
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : ¬(¬Closed s ∨ ∃ g, NextTag s g)
⊢ False
Tactic:
push_neg at h
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : Closed s ∧ ∀ (g : Time.Tag), ¬NextTag s g
⊢ False
Theorem: Execution.State.Terminal.not_elim
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : Closed s ∧ ∀ (g : Time.Tag), ¬NextTag s g
⊢ False
Tactic:
exact t ⟨h.left, h.right⟩
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ List.Forall (fun x => ¬Change.Targets x cpt i) (output s i₁)
Tactic:
apply List.forall_iff_forall_mem.mpr
Proof state after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ ∀ x ∈ output s i₁, ¬Change.Targets x cpt i
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ ∀ x ∈ output s i₁, ¬Change.Targets x cpt i
Tactic:
intro c hc
Proof state after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc : c ∈ output s i₁
⊢ ¬Change.Targets c cpt i
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc : c ∈ output s i₁
⊢ ¬Change.Targets c cpt i
Tactic:
simp [output] at hc
Proof state after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc :
  c ∈
    match s.rtr[Component.rcn][i₁], [], fun x => x.body (input s i₁) with
    | some x, x_1, f => f x
    | none, y, x => y
⊢ ¬Change.Targets c cpt i
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc :
  c ∈
    match s.rtr[Component.rcn][i₁], [], fun x => x.body (input s i₁) with
    | some x, x_1, f => f x
    | none, y, x => y
⊢ ¬Change.Targets c cpt i
Tactic:
split at hc <;> try contradiction
Proof state after:
case h_1
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝³ : Option (Component.type α Component.rcn)
x✝² : Reaction.Output
x✝¹ : Component.type α Component.rcn → Reaction.Output
x✝ : Component.type α Component.rcn
heq✝ : s.rtr[Component.rcn][i₁] = some x✝
hc : c ∈ (fun x => x.body (input s i₁)) x✝
⊢ ¬Change.Targets c cpt i
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ ¬Change.Targets c cpt i
Tactic:
case _ rcn₁ h₁ =>
  cases cpt
  all_goals
    intro ⟨⟩
    apply absurd hd
  case stv =>
    exact hi.no_shared_state_deps h₁ h₂ hc
  all_goals
    exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
case h_2
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
heq✝ : s.rtr[Component.rcn][i₁] = none
hc : c ∈ []
⊢ ¬Change.Targets c cpt i
Tactic:
contradiction
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ ¬Change.Targets c cpt i
Tactic:
cases cpt
Proof state after:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.inp i

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.out i

case stv
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.stv i

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.act i
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.stv
hc : Change.norm { cpt := Component.Valued.stv, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.stv, id := i } ∉ rcn₂.deps Kind.in
Tactic:
case stv =>
  exact hi.no_shared_state_deps h₁ h₂ hc
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.inp
hc : Change.norm { cpt := Component.Valued.inp, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.inp, id := i } ∉ rcn₂.deps Kind.in

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.out
hc : Change.norm { cpt := Component.Valued.out, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.out, id := i } ∉ rcn₂.deps Kind.in

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
Tactic:
all_goals
  exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.act i
Tactic:
intro ⟨⟩
Proof state after:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ False
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ False
Tactic:
apply absurd hd
Proof state after:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.stv
hc : Change.norm { cpt := Component.Valued.stv, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.stv, id := i } ∉ rcn₂.deps Kind.in
Tactic:
exact hi.no_shared_state_deps h₁ h₂ hc
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
Tactic:
exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
Proof state after:
no goals
Theorem: Execution.State.target_not_mem_indep_output
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i }.cpt ≠ Component.Valued.stv
Tactic:
simp [Change.Normal.target]
Proof state after:
no goals