internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)
Tactic:
intro _
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
simp [Set.insert]
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
push_neg
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e
Theorem: Execution.Step.Skip.unprocessed_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e
Tactic:
simp [and_comm]
Proof state after:
no goals
Theorem: Execution.Step.Skip.unprocessed_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ unprocessed s₂ ⊂ unprocessed s₁
Tactic:
simp [e.unprocessed_eq, Set.ssubset_iff_subset_ne]
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ rcn e ∈ unprocessed s₁
Theorem: Execution.Step.Skip.unprocessed_ssubset
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ rcn e ∈ unprocessed s₁
Tactic:
exact e.rcn_mem_unprocessed
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ Dependency.Acyclic rtr
Tactic:
simp [Dependency.Acyclic.iff_mem_acyclic]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
intro rcn hm
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
⊢ ¬rcn <[rtr] rcn
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
⊢ ¬rcn <[rtr] rcn
Tactic:
have ⟨_, e⟩ := p _ $ State.Over.forcing_not_terminal hm
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ w✝
⊢ ¬rcn <[rtr] rcn
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
cases e
Proof state after:
case skip
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
s✝ : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn

case exec
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e✝ : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn

case time
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
t✝ : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case time e => exact State.Over.forcing_not_time_step e hm |>.elim
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case skip e => exact State.Over.forcing_skip_step_rcn_eq e ▸ e.allows_rcn.acyclic
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case exec e => exact State.Over.forcing_exec_step_rcn_eq e ▸ e.allows_rcn.acyclic
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_not_time_step e hm |>.elim
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_skip_step_rcn_eq e ▸ e.allows_rcn.acyclic
Proof state after:
no goals
Theorem: Execution.Progress.to_deps_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_exec_step_rcn_eq e ▸ e.allows_rcn.acyclic
Proof state after:
no goals
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ rtr₁ = rtr₂
Tactic:
ext1
Proof state after:
case a
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ get? rtr₁ = get? rtr₂
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case a
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ get? rtr₁ = get? rtr₂
Tactic:
ext1 c
Proof state after:
case a.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
⊢ rtr₁{c} = rtr₂{c}
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case a.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
⊢ rtr₁{c} = rtr₂{c}
Tactic:
ext1 j
Proof state after:
case a.h.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case a.h.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
by_cases hc : c = cpt <;> by_cases hj : j = i
Proof state after:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact hc ▸ hj ▸ h
Proof state after:
no goals
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact hc ▸ e (.inr hj)
Proof state after:
no goals
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact e (.inl hc)
Proof state after:
no goals
Theorem: Reactor.RootEqualUpTo.ext
Proof state before:
case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact e (.inl hc)
Proof state after:
no goals
Theorem: Set.insert_union'
Proof state before:
α : Type u_1
s₁ s₂ : Set α
a : α
⊢ insert a s₁ ∪ s₂ = s₁ ∪ insert a s₂
Tactic:
rw [Set.insert_union, Set.union_comm, ←Set.insert_union, Set.union_comm]
Proof state after:
no goals
Theorem: Partial.mem_def
Proof state before:
α : Type u_1
β : Type u_2
a : α
f : α ⇀ β
⊢ a ∈ f ↔ a ∈ ids f
Tactic:
rfl
Proof state after:
no goals
Theorem: Partial.mem_iff
Proof state before:
α : Type u_1
β : Type u_2
a : α
f : α ⇀ β
⊢ a ∈ f ↔ ∃ b, f a = some b
Tactic:
rfl
Proof state after:
no goals
Theorem: Partial.empty_iff_ids_empty
Proof state before:
α : Type u_1
β : Type u_2
f : α ⇀ β
⊢ f = ∅ ↔ ids f = ∅
Tactic:
simp [ids, empty_iff, Set.eq_empty_iff_forall_not_mem, Option.eq_none_iff_forall_not_mem]
Proof state after:
no goals
Theorem: Partial.not_mem_empty
Proof state before:
α : Type u_1
β : Type u_2
a : α
⊢ a ∉ ∅
Tactic:
simp [mem_def, empty_ids]
Proof state after:
no goals
Theorem: Partial.Nonempty.iff_ids_nonempty
Proof state before:
α : Type u_1
β : Type u_2
f : α ⇀ β
⊢ Nonempty f ↔ Set.Nonempty (ids f)
Tactic:
simp [Nonempty, Set.nonempty_iff_ne_empty, empty_iff_ids_empty]
Proof state after:
no goals
Theorem: Partial.Nonempty.exists_mem
Proof state before:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Nonempty f
⊢ ∃ a, a ∈ f
Tactic:
simp [iff_ids_nonempty, mem_def] at *
Proof state after:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Set.Nonempty (ids f)
⊢ ∃ a, a ∈ ids f
Theorem: Partial.Nonempty.exists_mem
Proof state before:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Set.Nonempty (ids f)
⊢ ∃ a, a ∈ ids f
Tactic:
exact ⟨_, n.some_mem⟩
Proof state after:
no goals
Theorem: Partial.map_map
Proof state before:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ map g₂ (map g₁ f) = map (g₂ ∘ g₁) f
Tactic:
unfold map
Proof state after:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ (fun a => g₂ <$> g₁ <$> f a) = fun a => (g₂ ∘ g₁) <$> f a
Theorem: Partial.map_map
Proof state before:
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ (fun a => g₂ <$> g₁ <$> f a) = fun a => (g₂ ∘ g₁) <$> f a
Tactic:
simp
Proof state after:
no goals
Theorem: Partial.map_inj
Proof state before:
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
⊢ f₁ = f₂
Tactic:
funext a
Proof state after:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ f₁ a = f₂ a
Theorem: Partial.map_inj
Proof state before:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ f₁ a = f₂ a
Tactic:
replace h : f₁.map g a = f₂.map g a := by simp [h]
Proof state after:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
a : α
h : map g f₁ a = map g f₂ a
⊢ f₁ a = f₂ a
Theorem: Partial.map_inj
Proof state before:
case h
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
a : α
h : map g f₁ a = map g f₂ a
⊢ f₁ a = f₂ a
Tactic:
exact Option.map_injective hi h
Proof state after:
no goals
Theorem: Partial.map_inj
Proof state before:
α : Sort u_1
β β✝ : Type u_2
g : β → β✝
f₁ f₂ : α ⇀ β
hi : Function.Injective g
h : map g f₁ = map g f₂
a : α
⊢ map g f₁ a = map g f₂ a
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Partial.attach_map_val
Proof state before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
⊢ map Subtype.val (attach f) = f
Tactic:
funext a
Proof state after:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ map Subtype.val (attach f) a = f a
Theorem: Partial.attach_map_val
Proof state before:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ map Subtype.val (attach f) a = f a
Tactic:
simp [map, Option.map, attach]
Proof state after:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ (match
      match h : f a with
      | none => none
      | some b => some { val := b, property := ⋯ } with
    | some x => some ↑x
    | none => none) =
    f a
Theorem: Partial.attach_map_val
Proof state before:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ (match
      match h : f a with
      | none => none
      | some b => some { val := b, property := ⋯ } with
    | some x => some ↑x
    | none => none) =
    f a
Tactic:
split <;> split at * <;> simp_all
Proof state after:
case h.h_1.h_2
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝¹ : f a = some b✝
heq✝ : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝
Theorem: Partial.attach_map_val
Proof state before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝ : f a = some b✝
h : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝
Tactic:
case _ h => simp [←h]
Proof state after:
no goals
Theorem: Partial.attach_map_val
Proof state before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝ : f a = some b✝
h : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝
Tactic:
simp [←h]
Proof state after:
no goals
Theorem: Partial.ext_restrict
Proof state before:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ restrict f s = restrict g s
Tactic:
unfold restrict
Proof state after:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun a => if a ∈ s then f a else none) = fun a => if a ∈ s then g a else none
Theorem: Partial.ext_restrict
Proof state before:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun a => if a ∈ s then f a else none) = fun a => if a ∈ s then g a else none
Tactic:
funext
Proof state after:
case h
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ (if x✝ ∈ s then f x✝ else none) = if x✝ ∈ s then g x✝ else none
Theorem: Partial.ext_restrict
Proof state before:
case h
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ (if x✝ ∈ s then f x✝ else none) = if x✝ ∈ s then g x✝ else none
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: Partial.insert_same
Proof state before:
α : Sort u_1
β : Type u_2
a : α
b : β
inst✝ : DecidableEq α
f : α ⇀ β
⊢ insert f a b a = some b
Tactic:
simp [insert]
Proof state after:
no goals
Theorem: Partial.insert_ne
Proof state before:
α : Sort u_1
β : Type u_2
a' a : α
b : β
inst✝ : DecidableEq α
f : α ⇀ β
h : autoParam (a' ≠ a) _auto✝
⊢ insert f a b a' = f a'
Tactic:
simp [insert, h]
Proof state after:
no goals
Theorem: Partial.update_ne_comm
Proof state before:
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
⊢ update (update f a₁ g₁) a₂ g₂ = update (update f a₂ g₂) a₁ g₁
Tactic:
ext1 a
Proof state after:
case h
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
a : α
⊢ update (update f a₁ g₁) a₂ g₂ a = update (update f a₂ g₂) a₁ g₁ a
Theorem: Partial.update_ne_comm
Proof state before:
case h
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
a : α
⊢ update (update f a₁ g₁) a₂ g₂ a = update (update f a₂ g₂) a₁ g₁ a
Tactic:
by_cases a = a₁ <;> by_cases a = a₂ <;> simp_all [update]
Proof state after:
no goals
Theorem: Partial.const_ids
Proof state before:
α : Type u_1
β : Type u_2
as : Set α
b : β
⊢ ids (const as b) = as
Tactic:
simp [const, ids]
Proof state after:
no goals
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
⊢ map (fun x => b) f = const (ids f) b
Tactic:
ext1 a
Proof state after:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ map (fun x => b) f a = const (ids f) b a
Theorem: Partial.const_eq_map_const
Proof state before:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ map (fun x => b) f a = const (ids f) b a
Tactic:
simp [const, map_val, ids]
Proof state after:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ Option.map (fun x => b) (f a) = if ∃ b, f a = some b then some b else none
Theorem: Partial.const_eq_map_const
Proof state before:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ Option.map (fun x => b) (f a) = if ∃ b, f a = some b then some b else none
Tactic:
split <;> simp [Option.map]
Proof state after:
case h.inl
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b

case h.inr
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
case inl h => have ⟨_, h⟩ := h; simp [h]
Proof state after:
no goals
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
Tactic:
case inr h =>
  cases hb : f a <;> simp
  case some b => push_neg at h; have := hb ▸ h b; contradiction
Proof state after:
no goals
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
have ⟨_, h⟩ := h
Proof state after:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
w✝ : β
h : f a = some w✝
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
w✝ : β
h : f a = some w✝
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
Tactic:
cases hb : f a <;> simp
Proof state after:
case some
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
val✝ : β
hb : f a = some val✝
⊢ False
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
h : ¬∃ b, f a = some b
b : β
hb : f a = some b
⊢ False
Tactic:
case some b => push_neg at h; have := hb ▸ h b; contradiction
Proof state after:
no goals
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
h : ¬∃ b, f a = some b
b : β
hb : f a = some b
⊢ False
Tactic:
push_neg at h
Proof state after:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
⊢ False
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
⊢ False
Tactic:
have := hb ▸ h b
Proof state after:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
this : some b ≠ some b
⊢ False
Theorem: Partial.const_eq_map_const
Proof state before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
this : some b ≠ some b
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Partial.mapIdx_ids
Proof state before:
α : Type u_1
β : Type u_2
g : α → β
f : α ⇀ β
⊢ ids (mapIdx g f) = ids f
Tactic:
simp [mapIdx, mem_iff, ids]
Proof state after:
no goals
Theorem: Execution.Step.Skip.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ ¬State.Trivial s₁
Tactic:
by_contra ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : State.Trivial s₁
⊢ False
Theorem: Execution.Step.Skip.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : State.Trivial s₁
⊢ False
Tactic:
simp [State.Trivial, Partial.empty_iff] at ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False
Theorem: Execution.Step.Skip.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₛ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False
Tactic:
cases (Partial.mem_iff.mp e.allows_rcn.mem).choose_spec ▸ ht e.rcn
Proof state after:
no goals
Theorem: Execution.Step.Exec.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ ¬State.Trivial s₁
Tactic:
by_contra ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : State.Trivial s₁
⊢ False
Theorem: Execution.Step.Exec.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : State.Trivial s₁
⊢ False
Tactic:
simp [State.Trivial, Partial.empty_iff] at ht
Proof state after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False
Theorem: Execution.Step.Exec.not_trivial
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False
Tactic:
cases (Partial.mem_iff.mp e.allows_rcn.mem).choose_spec ▸ ht e.rcn
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.tag_le
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e : RTC s₁ s₂
⊢ s₁.tag ≤ s₂.tag
Tactic:
induction e with
| refl         => exact le_refl _
| trans a _ hi => exact le_trans (le_of_lt a.tag_lt) hi
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.tag_le
Proof state before:
case refl
α : Type
inst✝ : Proper α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
exact le_refl _
Proof state after:
no goals