internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.TC.progress_not_mem_rcns
Proof state before:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn e ∨ rcn ∈ rcns e')
Tactic:
simp [hi $ e.progress_monotonic h]
Proof state after:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn e
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ s₂.progress = s₁.progress ∪ {a | a ∈ rcns e}
Tactic:
induction e <;> simp [rcns]
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn a✝) s₁✝.progress

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn a✝¹ ∨ a ∈ rcns a✝}
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress
Tactic:
case single e     => exact e.progress_eq
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
case trans e _ hi => simp [hi, e.progress_eq]; apply Set.insert_union'
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress
Tactic:
exact e.progress_eq
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
simp [hi, e.progress_eq]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ Set.insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress ∪ {a | a ∈ rcns a✝} =
    s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Theorem: Execution.Instantaneous.Step.TC.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ Set.insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress ∪ {a | a ∈ rcns a✝} =
    s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
apply Set.insert_union'
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_ne_nil
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁✝ s₂✝¹ : State α
rcn : ID
s₁ s₂ s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
⊢ rcns (trans a✝¹ a✝) ≠ []
Tactic:
simp [rcns]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_cons
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁✝ s₂✝¹ : State α
rcn : ID
s₁ s₂ s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
⊢ ∃ hd tl, rcns (trans a✝¹ a✝) = hd :: tl
Tactic:
simp [rcns]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ rcns e₁ ~ rcns e₂
Tactic:
apply List.perm_ext_iff_of_nodup e₁.rcns_nodup e₂.rcns_nodup |>.mpr
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ ∀ (a : ID), a ∈ rcns e₁ ↔ a ∈ rcns e₂
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ ∀ (a : ID), a ∈ rcns e₁ ↔ a ∈ rcns e₂
Tactic:
intro rcn
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
by_cases hc : rcn ∈ s.progress
Proof state after:
case pos
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂

case neg
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
case pos => simp [e₁.progress_not_mem_rcns hc, e₂.progress_not_mem_rcns hc]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
case neg =>
  constructor <;> intro hm
  case' mp  => have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
  case' mpr => have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
  all_goals exact (Set.mem_union ..).mp h |>.resolve_left hc
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
simp [e₁.progress_not_mem_rcns hc, e₂.progress_not_mem_rcns hc]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
constructor <;> intro hm
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
case' mp  => have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
case' mpr => have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
Proof state after:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁

case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁

case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Tactic:
all_goals exact (Set.mem_union ..).mp h |>.resolve_left hc
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂
Tactic:
have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
Proof state after:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁
Theorem: Execution.Instantaneous.Step.TC.progress_eq_rcns_perm
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Tactic:
exact (Set.mem_union ..).mp h |>.resolve_left hc
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.rcns_trans_eq_cons
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ s₁
e₂ : s₁ ↓ᵢ+ s₂
⊢ rcns (trans e₁ e₂) = Execution.Instantaneous.Step.rcn e₁ :: rcns e₂
Tactic:
simp [rcns, Step.rcn]
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ rcns e
⊢ rcn ∉ s₁.progress
Tactic:
induction e
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single a✝)
⊢ rcn ∉ s₁✝.progress

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans a✝¹ a✝)
⊢ rcn ∉ s₁✝.progress
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single e)
⊢ rcn ∉ s₁✝.progress
Tactic:
case single e =>
  simp [rcns] at h
  exact h ▸ e.rcn_not_mem_progress
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
⊢ rcn ∉ s₁✝.progress
Tactic:
case trans e e' hi =>
  cases e'.rcns_trans_eq_cons e ▸ h
  case head   => exact e.rcn_not_mem_progress
  case tail h => exact mt e.progress_monotonic (hi h)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single e)
⊢ rcn ∉ s₁✝.progress
Tactic:
simp [rcns] at h
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ∉ s₁✝.progress
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ∉ s₁✝.progress
Tactic:
exact h ▸ e.rcn_not_mem_progress
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
⊢ rcn ∉ s₁✝.progress
Tactic:
cases e'.rcns_trans_eq_cons e ▸ h
Proof state after:
case head
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress

case tail
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
a✝ : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress
Tactic:
case head   => exact e.rcn_not_mem_progress
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h✝ : rcn ∈ rcns (trans e e')
h : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
Tactic:
case tail h => exact mt e.progress_monotonic (hi h)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress
Tactic:
exact e.rcn_not_mem_progress
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_not_mem_progress
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h✝ : rcn ∈ rcns (trans e e')
h : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
Tactic:
exact mt e.progress_monotonic (hi h)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₂.progress ∧ rcn ∉ s₁.progress
Tactic:
simp [e.progress_eq, or_and_right]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e → rcn ∉ s₁.progress
Theorem: Execution.Instantaneous.Step.TC.mem_rcns_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e → rcn ∉ s₁.progress
Tactic:
exact e.mem_rcns_not_mem_progress
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.head_minimal
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
⊢ Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
Tactic:
by_contra hc
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc : ¬Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_minimal
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc : ¬Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
simp [Minimal] at hc
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_minimal
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
have ⟨_, hm, h⟩ := hc e.acyclic
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_minimal
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
replace hc := mt e.progress_monotonic $ e'.mem_rcns_not_mem_progress hm
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
hc : w✝ ∉ s₁.progress
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_minimal
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
hc : w✝ ∉ s₁.progress
⊢ False
Tactic:
exact hc $ e.allows_rcn.deps h
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.head_not_mem_tail
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
⊢ Execution.Instantaneous.Step.rcn e ≠ i
Tactic:
intro hc
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_not_mem_tail
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
⊢ False
Tactic:
have := trans e e' |>.rcns_nodup
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this : Nodup (rcns (trans e e'))
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_not_mem_tail
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this : Nodup (rcns (trans e e'))
⊢ False
Tactic:
have := hc.symm ▸ List.not_nodup_cons_of_mem h
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this✝ : Nodup (rcns (trans e e'))
this : ¬Nodup (Execution.Instantaneous.Step.rcn e :: rcns e')
⊢ False
Theorem: Execution.Instantaneous.Step.TC.head_not_mem_tail
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this✝ : Nodup (rcns (trans e e'))
this : ¬Nodup (Execution.Instantaneous.Step.rcn e :: rcns e')
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ s₁.progress ⊂ s₂.progress
Tactic:
induction e
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ s₂✝.progress

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : s₂✝.progress ⊂ s₃✝.progress
⊢ s₁✝.progress ⊂ s₃✝.progress
Theorem: Execution.Instantaneous.Step.TC.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ s₂✝.progress
Tactic:
case single e     => exact e.progress_ssubset
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₂✝.progress ⊂ s₃✝.progress
⊢ s₁✝.progress ⊂ s₃✝.progress
Tactic:
case trans e _ hi => exact e.progress_ssubset |>.trans hi
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ s₂✝.progress
Tactic:
exact e.progress_ssubset
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₂✝.progress ⊂ s₃✝.progress
⊢ s₁✝.progress ⊂ s₃✝.progress
Tactic:
exact e.progress_ssubset |>.trans hi
Proof state after:
no goals