internlm/Lean-Github huggingface dataset:
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ (∃ x, x <[rtr] x) ↔ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
constructor <;> intro ⟨d, h⟩
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x

case mpr
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
case mp  => exact ⟨_, h.mem₁, h⟩
Proof state after:
no goals
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x
Tactic:
case mpr => exact ⟨_, h.right⟩
Proof state after:
no goals
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
exact ⟨_, h.mem₁, h⟩
Proof state after:
no goals
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x
Tactic:
exact ⟨_, h.right⟩
Proof state after:
no goals
Theorem: Dependency.Acyclic.of_trivial
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ Acyclic rtr
Tactic:
simp_all [Dependency.Acyclic.iff_mem_acyclic, triv]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ ∀ i ∈ ∅, ¬i <[rtr] i
Theorem: Dependency.Acyclic.of_trivial
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ ∀ i ∈ ∅, ¬i <[rtr] i
Tactic:
intros _ h
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
i✝ : Component.idType Component.rcn
h : i✝ ∈ ∅
⊢ ¬i✝ <[rtr] i✝
Theorem: Dependency.Acyclic.of_trivial
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
i✝ : Component.idType Component.rcn
h : i✝ ∈ ∅
⊢ ¬i✝ <[rtr] i✝
Tactic:
exact absurd h Partial.not_mem_empty
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
by_cases hm₁ : rcn₁.Mutates <;> by_cases hm₂ : rcn₂.Mutates
Proof state after:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case neg
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inl $ .mutNorm hc h₁ h₂ hm₁ (by simp_all [Reaction.Mutates])
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ Reaction.Normal rcn₂
Tactic:
simp_all [Reaction.Mutates]
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inr $ .mutNorm hc h₂ h₁ hm₂ (by simp_all [Reaction.Mutates])
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ Reaction.Normal rcn₁
Tactic:
simp_all [Reaction.Mutates]
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case pos
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
cases Proper.wellformed rtr |>.ordered_prio hc h₁ h₂ hn hp
Proof state after:
case pos.inl
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos.inr
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case pos.inl
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inr $ .prio hc h₂ h₁ (by simp_all) ‹_›
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₁.prio < rcn₂.prio
⊢ Reaction.Mutates rcn₂ ↔ Reaction.Mutates rcn₁
Tactic:
simp_all
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case pos.inr
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact .inl $ .prio hc h₁ h₂ (by simp_all) ‹_›
Proof state after:
no goals
Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
h✝ : rcn₂.prio < rcn₁.prio
⊢ Reaction.Mutates rcn₁ ↔ Reaction.Mutates rcn₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: Dependency.shared_out_dep
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have ⟨_, _, hc₁, hr₁⟩ := obj?_some_split h₁
Proof state after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.shared_out_dep
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have ⟨_, _, hc₂, hr₂⟩ := obj?_some_split h₂
Proof state after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.shared_out_dep
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
have hc := Proper.wellformed rtr |>.shared_dep_local hc₁ hc₂ hr₁ hr₂ hd₁ hd₂
Proof state after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc : w✝³ = w✝¹
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.shared_out_dep
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc : w✝³ = w✝¹
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
injection hc₂ ▸ hc ▸ hc₁ with hc
Proof state after:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Theorem: Dependency.shared_out_dep
Proof state before:
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
hc✝ : w✝³ = w✝¹
hc : w✝ = w✝²
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
exact same_con_shared_out_dep hc₁ hr₁ (hc ▸ hr₂) hn hd₁ hd₂
Proof state after:
no goals
Theorem: Independent.no_shared_state_deps
Proof state before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
have hd₁ := rcn₁.target_mem_deps hs
Proof state after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : Change.Normal.target { cpt := Component.Valued.stv, id := j, value := v } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Theorem: Independent.no_shared_state_deps
Proof state before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : Change.Normal.target { cpt := Component.Valued.stv, id := j, value := v } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
simp [Change.Normal.target] at hd₁
Proof state after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Theorem: Independent.no_shared_state_deps
Proof state before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
⊢ { cpt := Component.Valued.stv, id := j } ∉ rcn₂.deps k
Tactic:
by_contra hd₂
Proof state after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
⊢ False
Theorem: Independent.no_shared_state_deps
Proof state before:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
⊢ False
Tactic:
have ⟨_, _, hc₁, hr₁⟩ := obj?_some_split h₁
Proof state after:
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ False