internlm/Lean-Github huggingface dataset:
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
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
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₁
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
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
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₂
⊢ False
Tactic:
have hc := Proper.wellformed rtr |>.shared_state_local hc₁ hc₂ hr₁ hr₂ hd₁ 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
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✝¹
⊢ 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
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✝¹
⊢ False
Tactic:
injection hc₂ ▸ hc ▸ hc₁ with hc
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₁
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✝²
⊢ 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
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✝²
⊢ False
Tactic:
cases Dependency.hazard hc₁ hr₁ (hc ▸ hr₂) hi.not_eq hd₁ hd₂ (.inl rfl)
Proof state after:
case inl
α : 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₁
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✝²
h✝ : i₁ <[rtr] i₂
⊢ False

case inr
α : 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₁
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✝²
h✝ : i₂ <[rtr] i₁
⊢ False
Theorem: Independent.no_shared_state_deps
Proof state before:
case inl
α : 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₁
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✝²
h✝ : i₁ <[rtr] i₂
⊢ False

case inr
α : 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₁
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✝²
h✝ : i₂ <[rtr] i₁
⊢ False
Tactic:
all_goals simp [hi.left, hi.right] at *
Proof state after:
no goals
Theorem: Independent.no_shared_state_deps
Proof state before:
case inr
α : 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₁
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✝²
h✝ : i₂ <[rtr] i₁
⊢ False
Tactic:
simp [hi.left, hi.right] at *
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
⊢ c₁ = c₂
Tactic:
by_cases hi : i₁ = i₂
Proof state after:
case pos
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂

case neg
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ c₁ = c₂
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂
Tactic:
case pos => exact get?_some_rtr_eq hc₁ hc₂ (hi ▸ hr₁) hr₂
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ c₁ = c₂
Tactic:
case neg =>
  have hv₁ := wf.valid_deps hc₁ hr₁ hd₁
  have hv₂ := wf.valid_deps hc₂ hr₂ hd₂
  cases k <;> cases cpt <;> try cases ‹Kind› 
  have := obj?_some_extend hc₁ hr₁
  case out.inp => 
    have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
    exact absurd hd₂ hd₂'
  case in.out =>
    cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
    case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
      have hc₁' := obj?_some_extend hc₁ hn₁
      have hc₂' := obj?_some_extend hc₂ hn₂
      have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
      injection hj with hj
      exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂ 
  all_goals 
    cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
    all_goals exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂
Tactic:
exact get?_some_rtr_eq hc₁ hc₂ (hi ▸ hr₁) hr₂
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ c₁ = c₂
Tactic:
have hv₁ := wf.valid_deps hc₁ hr₁ hd₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
⊢ c₁ = c₂
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
⊢ c₁ = c₂
Tactic:
have hv₂ := wf.valid_deps hc₂ hr₂ hd₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k { cpt := cpt, id := j }
⊢ c₁ = c₂
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂
Tactic:
case out.inp => 
  have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
  exact absurd hd₂ hd₂'
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.out, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.out, id := j }
⊢ c₁ = c₂
Tactic:
case in.out =>
  cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
  case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
    have hc₁' := obj?_some_extend hc₁ hn₁
    have hc₂' := obj?_some_extend hc₂ hn₂
    have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
    injection hj with hj
    exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂
Tactic:
have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.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
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
hd₂' : { cpt := Component.Valued.inp, id := j } ∉ rcn₂.deps Kind.out
⊢ c₁ = c₂