internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
⊢ False
Tactic:
have ⟨_, _, h'⟩ := e₁'.rcns_cons
Proof state after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
⊢ False
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
⊢ False
Tactic:
simp [h, h'] at hp he₂
Proof state after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
⊢ False
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
⊢ False
Tactic:
have h := he₂.right.symm ▸ List.erase_cons e₁.rcn hd tl
Proof state after:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h : [] = if (hd == rcn e₁) = true then tl else hd :: List.erase tl (rcn e₁)
⊢ False
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h : [] = if (hd == rcn e₁) = true then tl else hd :: List.erase tl (rcn e₁)
⊢ False
Tactic:
split at h <;> try assumption
Proof state after:
case inl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : (hd == rcn e₁) = true
h : [] = tl
⊢ False
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
case inl
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : (hd == rcn e₁) = true
h : [] = tl
⊢ False
Tactic:
simp [←h] at hp
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_perm_deterministic
Proof state before:
case inr
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
hd : ID
tl : List ID
h✝¹ : rcns e₂ = hd :: tl
w✝¹ : ID
w✝ : List ID
h' : rcns e₁' = w✝¹ :: w✝
hp : rcn e₁ :: w✝¹ :: w✝ ~ hd :: tl
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (hd :: tl) (rcn e₁)
h✝ : ¬(hd == rcn e₁) = true
h : False
⊢ False
Tactic:
assumption
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ s₁ = s₂
Tactic:
have := e₁.preserves_tag ▸ e₂.preserves_tag
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
⊢ s₁ = s₂
Theorem: Execution.Instantaneous.Step.TC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
have ⟨_, _⟩ := rcns_perm_deterministic e₁ e₂ $ progress_eq_rcns_perm e₁ e₂ hp
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁ = s₂
Theorem: Execution.Instantaneous.Step.TC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁ = s₂
Tactic:
ext1 <;> try assumption
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.deterministic
Proof state before:
case events
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁.events = s₂.events
Tactic:
assumption
Proof state after:
no goals
Theorem: Execution.Instantaneous.Closed.mem_rcns_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ| s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₁.rtr[Component.rcn] ∧ rcn ∉ s₁.progress
Tactic:
simp [Partial.mem_def, e.progress_def ▸ e.exec.mem_rcns_iff (rcn := rcn)]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Closed.rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e₁ : s ↓ᵢ| s₁
e₂ : s ↓ᵢ| s₂
⊢ rcns e₁ ~ rcns e₂
Tactic:
simp [List.perm_ext_iff_of_nodup e₁.rcns_nodup e₂.rcns_nodup, e₁.mem_rcns_iff, e₂.mem_rcns_iff]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Closed.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e₁ : s ↓ᵢ| s₁
e₂ : s ↓ᵢ| s₂
⊢ s₁.progress = s₂.progress
Tactic:
simp [e₁.progress_def, e₂.progress_def]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
induction u₁ generalizing rtr₂ <;> cases u₂
Proof state after:
case final.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
a✝⁵ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁴ : rtr₁✝{Component.val cpt}{i} = some o✝¹
a✝³ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case final.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝⁶ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁵ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝⁴ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁶ : 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₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝¹ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
a✝⁷ : 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₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
e₁ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝¹
h₁' : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂' : rtr₂{Component.val cpt}{i} = some v
e₂ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case final.final e₁ _ h₁' _ _ h₂' e₂ =>
  exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) (h₂' ▸ h₁')
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case nested.nested j₁ _ _ _ _ e₁ h₁ h₁' u₁ hi j₂ _ _ u₂ h₂ h₂' e₂ =>
  have h : j₁ = j₂ := by injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
  subst h; cases h₁ ▸ h₂; cases hi u₂
  exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) $ h₁' ▸ h₂'.symm
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝³ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case final.nested h₁ _ _ _ _ u h₂ _ _ =>
  injection (StrictMember.final h₁).unique (u.member₁.nested h₂)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
h₂ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case nested.final h₁ _ u _ _ h₂ _ _ =>
  injection (StrictMember.final h₂).unique (u.member₁.nested h₁)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
e₁ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝¹
h₁' : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂' : rtr₂{Component.val cpt}{i} = some v
e₂ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) (h₂' ▸ h₁')
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
have h : j₁ = j₂ := by injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
Proof state after:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
h : j₁ = j₂
⊢ rtr₂✝ = rtr₂
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
h : j₁ = j₂
⊢ rtr₂✝ = rtr₂
Tactic:
subst h
Proof state after:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
⊢ rtr₂✝ = rtr₂
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
cases h₁ ▸ h₂
Proof state after:
case refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₂✝ : Component.type α Component.rtr
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
⊢ rtr₂✝ = rtr₂
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
case refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₂✝ : Component.type α Component.rtr
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
⊢ rtr₂✝ = rtr₂
Tactic:
cases hi u₂
Proof state after:
case refl.refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
⊢ rtr₂✝ = rtr₂
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
case refl.refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
⊢ rtr₂✝ = rtr₂
Tactic:
exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) $ h₁' ▸ h₂'.symm
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ j₁ = j₂
Tactic:
injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝³ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
injection (StrictMember.final h₁).unique (u.member₁.nested h₂)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
h₂ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
injection (StrictMember.final h₂).unique (u.member₁.nested h₁)
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulUpdate cpt i v rtr rtr₁
u₂ : LawfulUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
cases u₁ <;> cases u₂
Proof state after:
case update.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝¹ : LawfulMemUpdate cpt i v rtr rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case update.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝ : LawfulMemUpdate cpt i v rtr rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case notMem.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂
Tactic:
case notMem.notMem => simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
case update.update u₁ u₂ => exact u₁.unique u₂
Proof state after:
no goals