internlm/Lean-Github huggingface dataset:
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
by_cases hi₂ : i = i₂ <;> try subst hi₂
Proof state after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : i = i₂
⊢ o₁✝ = o₂✝
Tactic:
subst hi₂
Proof state after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝
Tactic:
have h₁ := u₁.obj?_preserved (.inl hc₁) ▸ u₂.obj?_updated
Proof state after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have h₂ := u₁'.obj?_updated ▸ u₂'.obj?_preserved (.inl hc₁)
Proof state after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
injection ho₁ ▸ h₂.trans h₁.symm ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (.inl hc₁) ▸ u₂.obj?_preserved (.inr hi₂)
Proof state after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (.inr hi₂) ▸ u₂'.obj?_preserved (.inl hc₁)
Proof state after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (j := i) (.inl hc₁) ▸ u₂.obj?_preserved  (.inl hc₂)
Proof state after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (j := i) (.inl hc₂) ▸ u₂'.obj?_preserved (.inl hc₁)
Proof state after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Theorem: Reactor.LawfulUpdate.ne_comm
Proof state before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: Execution.Grouped.Tail.closed_to_none
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : Tail s₁ s₂
⊢ s₁ = s₂
Tactic:
cases e
Proof state after:
case none
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁

case some
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
a✝ : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂
Theorem: Execution.Grouped.Tail.closed_to_none
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁
Tactic:
case none => rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Tail.closed_to_none
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
case some e => exact absurd h e.not_closed
Proof state after:
no goals
Theorem: Execution.Grouped.Tail.closed_to_none
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Grouped.Tail.closed_to_none
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
exact absurd h e.not_closed
Proof state after:
no goals
Theorem: Execution.Grouped.Tail.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁✝ s₂ s₁ : State α
e : s ↓ᵢ+ s₁
hp : s₁.progress = s.progress
⊢ s.progress = s₁.progress
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: Reaction.Output.mem_targets_cons
Proof state before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
⊢ t ∈ targets (hd :: tl)
Tactic:
have ⟨c, hm, _⟩ := h
Proof state after:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ t ∈ targets (hd :: tl)
Theorem: Reaction.Output.mem_targets_cons
Proof state before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ t ∈ targets (hd :: tl)
Tactic:
exists c, by simp [hm]
Proof state after:
no goals
Theorem: Reaction.Output.mem_targets_cons
Proof state before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ c ∈ hd :: tl
Tactic:
simp [hm]
Proof state after:
no goals
Theorem: Reaction.Output.target_mem_targets
Proof state before:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ t ∈ targets out
Tactic:
exists c, hc
Proof state after:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ Change.Targets c t.1 t.2
Theorem: Reaction.Output.target_mem_targets
Proof state before:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ Change.Targets c t.1 t.2
Tactic:
cases c <;> simp [Change.target] at *
Proof state after:
case norm
out : Output
t : Component.Valued × ID
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
ht : (a✝.cpt, a✝.id) = t
⊢ Change.Targets (Change.norm a✝) t.1 t.2
Theorem: Reaction.Output.target_mem_targets
Proof state before:
case norm
out : Output
t : Component.Valued × ID
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
ht : (a✝.cpt, a✝.id) = t
⊢ Change.Targets (Change.norm a✝) t.1 t.2
Tactic:
subst ht
Proof state after:
case norm
out : Output
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
⊢ Change.Targets (Change.norm a✝) (a✝.cpt, a✝.id).1 (a✝.cpt, a✝.id).2
Theorem: Reaction.Output.target_mem_targets
Proof state before:
case norm
out : Output
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
⊢ Change.Targets (Change.norm a✝) (a✝.cpt, a✝.id).1 (a✝.cpt, a✝.id).2
Tactic:
constructor
Proof state after:
no goals
Theorem: Reactor.equiv_eq_dependencies
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
⊢ dependencies rtr₁ = dependencies rtr₂
Tactic:
ext i j
Proof state after:
case h.h
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
i j : ID
⊢ j ∈ dependencies rtr₁ i ↔ j ∈ dependencies rtr₂ i
Theorem: Reactor.equiv_eq_dependencies
Proof state before:
case h.h
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
i j : ID
⊢ j ∈ dependencies rtr₁ i ↔ j ∈ dependencies rtr₂ i
Tactic:
exact ⟨.equiv $ .symm e, .equiv e⟩
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
⊢ rtr₁ = rtr₂
Tactic:
have e := Equivalent.trans (Equivalent.symm rf₁.equiv) rf₂.equiv
Proof state after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ rtr₁ = rtr₂
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ rtr₁ = rtr₂
Tactic:
apply ext_obj? e
Proof state after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
Tactic:
intro cpt _ _ _ ho₁ ho₂
Proof state after:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
cpt : Component.Valued
i✝ : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₁[Component.val cpt][i✝] = some o₁✝
ho₂ : rtr₂[Component.val cpt][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
cpt : Component.Valued
i✝ : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₁[Component.val cpt][i✝] = some o₁✝
ho₂ : rtr₂[Component.val cpt][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
cases cpt
Proof state after:
case inp
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case out
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case stv
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case act
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case stv => injection (rf₁.eq_state ▸ ho₁) ▸ rf₂.eq_state ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case act => injection (rf₁.acts     ▸ ho₁) ▸ rf₂.acts     ▸ ho₂
Proof state after:
no goals
Theorem: Reactor.Refresh.deterministic
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
case inp => injection (rf₁.inputs   ▸ ho₁) ▸ rf₂.inputs   ▸ ho₂
Proof state after:
no goals