internlm/Lean-Github huggingface dataset:
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
exact e.mem_iff (.inr hj)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
intro j _ _ h₁ h₂
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
have h := e (c := .rcn) (j := j) (.inl $ by simp)
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ Component.rcn ≠ Component.rtr
Tactic:
simp
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
intro j' n₁' n₂' h₁' h₂'
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Tactic:
by_cases hj : j' = j <;> try subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'
Tactic:
case pos => simp_all; assumption
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'
Tactic:
case neg => 
  have := e (c := .rtr) (j := j') (.inr hj)
  simp_all
  apply Equivalent.refl
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : j' = j
⊢ Equivalent n₁' n₂'
Tactic:
subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'
Tactic:
simp_all
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
hi : n₁' ≈ n₂'
h₁' : n₁✝ = n₁'
h₂' : n₂✝ = n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁'
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
hi : n₁' ≈ n₂'
h₁' : n₁✝ = n₁'
h₂' : n₂✝ = n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁'
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Tactic:
assumption
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'
Tactic:
have := e (c := .rtr) (j := j') (.inr hj)
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = rtr₂✝{Component.rtr}{j'}
⊢ Equivalent n₁' n₂'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = rtr₂✝{Component.rtr}{j'}
⊢ Equivalent n₁' n₂'
Tactic:
simp_all
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : n₂' = n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₁'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = some n₁'
⊢ Equivalent n₁' n₁'
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : n₂' = n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₁'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = some n₁'
⊢ Equivalent n₁' n₁'
Tactic:
apply Equivalent.refl
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_not_final
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i : ID
cpt : Component
j : ID
o : Component.type (Component.type α Component.rtr) cpt
o' : Component.type α cpt
s : StrictMember Component.rtr i rtr
h : object s{cpt}{j} = some o
hf : rtr{cpt}{j} = some o'
⊢ extend s h ≠ final hf
Tactic:
cases s <;> simp [extend]
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ i₂ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
s₁ : StrictMember Component.rtr i₁ rtr
s₂ : StrictMember Component.rtr i₂ rtr
h₁ : object s₁{cpt}{j} = some o₁
h₂ : object s₂{cpt}{j} = some o₂
h : extend s₁ h₁ = extend s₂ h₂
⊢ i₁ = i₂
Tactic:
induction s₁ generalizing i₂ <;> cases s₂
Proof state after:
case final.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝¹ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝¹
i₂ : ID
h₁ : object (final a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (final a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case final.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (final a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂

case nested.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr₁✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (nested a✝² a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝
h₁ : object (final a✝¹){cpt}{j} = some o₁
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (final h₁) (final h₂)
⊢ i₁ = i₁
Tactic:
case final.final  => rfl
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
hi :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
case nested.nested hi _ _ => exact hi $ eq_of_heq h
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
case final.nested => exact absurd (eq_of_heq h).symm $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (extend a✝¹ h₁) (final h₂)
⊢ i₁ = j✝
Tactic:
case nested.final => exact absurd (eq_of_heq h) $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂
Tactic:
simp [extend] at h
Proof state after:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : j✝¹ = j✝ ∧ rtr₂✝¹ = rtr₂✝ ∧ HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : j✝¹ = j✝ ∧ rtr₂✝¹ = rtr₂✝ ∧ HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
obtain ⟨hj, hr, h⟩ := h
Proof state after:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
hj : j✝¹ = j✝
hr : rtr₂✝¹ = rtr₂✝
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂