internlm/Lean-Github huggingface dataset:
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
constructor
Proof state after:
case mp
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true

case mpr
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
case mp =>
  intro ⟨equiv, mem, active⟩
  rw [Array.any_iff_mem_where]
  refine ⟨_, mem, ?_⟩
  exact Activates.iff_equiv_trigger_activated equiv |>.mp active
Proof state after:
no goals
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
Tactic:
case mpr =>
  intro h
  have ⟨t', mem, active⟩ := Array.any_iff_mem_where.mp h
  have ⟨_, equiv⟩ : ∃ t, t ≡ t' := ⟨_, Reaction.Trigger.Equiv.lift t'⟩
  refine .witness equiv mem ?_
  exact Activates.iff_equiv_trigger_activated equiv |>.mpr active
Proof state after:
no goals
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction →
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true
Tactic:
intro ⟨equiv, mem, active⟩
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
Tactic:
rw [Array.any_iff_mem_where]
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ ∃ a, a ∈ reaction.val.triggers.data ∧ Execution.Executable.triggers.activated exec reaction a = true
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ ∃ a, a ∈ reaction.val.triggers.data ∧ Execution.Executable.triggers.activated exec reaction a = true
Tactic:
refine ⟨_, mem, ?_⟩
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Execution.Executable.triggers.activated exec reaction t'✝ = true
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : Reaction.Trigger net✝
t'✝ : Reaction.triggerType reaction.val
equiv : t✝ ≡ t'✝
mem : t'✝ ∈ reaction.val.triggers.data
active : Activates exec t✝
⊢ Execution.Executable.triggers.activated exec reaction t'✝ = true
Tactic:
exact Activates.iff_equiv_trigger_activated equiv |>.mp active
Proof state after:
no goals
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
Tactic:
intro h
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
⊢ Triggers exec reaction
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
⊢ Triggers exec reaction
Tactic:
have ⟨t', mem, active⟩ := Array.any_iff_mem_where.mp h
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
⊢ Triggers exec reaction
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
⊢ Triggers exec reaction
Tactic:
have ⟨_, equiv⟩ : ∃ t, t ≡ t' := ⟨_, Reaction.Trigger.Equiv.lift t'⟩
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Triggers exec reaction
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Triggers exec reaction
Tactic:
refine .witness equiv mem ?_
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Activates exec w✝
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
      (Array.size reaction.val.triggers) =
    true
t' : Trigger reaction.val.portSources.vars reaction.val.actionSources.vars reaction.val.timers
mem : t' ∈ reaction.val.triggers.data
active : Execution.Executable.triggers.activated exec reaction t' = true
w✝ : Reaction.Trigger net✝
equiv : w✝ ≡ t'
⊢ Activates exec w✝
Tactic:
exact Activates.iff_equiv_trigger_activated equiv |>.mpr active
Proof state after:
no goals
Theorem: Network.Graph.Path.isNil_def
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isNil path = true ↔ path = nil
Tactic:
cases path <;> simp [isNil]
Proof state after:
no goals
Theorem: Network.Graph.Path.isCons_def
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true ↔ ∃ child subpath, path = cons child subpath
Tactic:
cases path <;> simp [isCons]
Proof state after:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ ∃ child subpath, child✝ = child ∧ HEq a✝ subpath
Theorem: Network.Graph.Path.isCons_def
Proof state before:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ ∃ child subpath, child✝ = child ∧ HEq a✝ subpath
Tactic:
exists ‹_›, ‹_›
Proof state after:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ child✝ = child✝ ∧ HEq a✝ a✝
Theorem: Network.Graph.Path.isCons_def
Proof state before:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ child✝ = child✝ ∧ HEq a✝ a✝
Tactic:
simp
Proof state after:
no goals
Theorem: Network.Graph.Path.isCons_iff_not_isNil
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true ↔ ¬isNil path = true
Tactic:
cases path <;> simp [isCons, isNil]
Proof state after:
no goals
Theorem: Network.Graph.Path.isNil_iff_not_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isNil path = true ↔ ¬isCons path = true
Tactic:
cases path <;> simp [isCons, isNil]
Proof state after:
no goals
Theorem: Time.ext
Proof state before:
time₁ time₂ : Time
x✝ : time₁.ns = time₂.ns
⊢ time₁ = time₂
Tactic:
cases time₁
Proof state after:
case _private.Runtime.Time.0.Time.mk
time₂ : Time
ns✝ : Nat
x✝ : { ns := ns✝ }.ns = time₂.ns
⊢ { ns := ns✝ } = time₂
Theorem: Time.ext
Proof state before:
case _private.Runtime.Time.0.Time.mk
time₂ : Time
ns✝ : Nat
x✝ : { ns := ns✝ }.ns = time₂.ns
⊢ { ns := ns✝ } = time₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: Time.of_to
Proof state before:
value : Nat
unit : Time.Unit
⊢ to (of value unit) unit = value
Tactic:
simp [of, to, Unit.nsRatio]
Proof state after:
value : Nat
unit : Time.Unit
⊢ ((value *
        match unit with
        | Unit.ns => 1
        | Unit.μs => 1000
        | Unit.ms => 1000 * 1000
        | Unit.s => 1000 * 1000 * 1000
        | Unit.mins => 1000 * 1000 * 1000 * 60
        | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
        | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
        | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) /
      match unit with
      | Unit.ns => 1
      | Unit.μs => 1000
      | Unit.ms => 1000 * 1000
      | Unit.s => 1000 * 1000 * 1000
      | Unit.mins => 1000 * 1000 * 1000 * 60
      | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
      | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
      | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) =
    value
Theorem: Time.of_to
Proof state before:
value : Nat
unit : Time.Unit
⊢ ((value *
        match unit with
        | Unit.ns => 1
        | Unit.μs => 1000
        | Unit.ms => 1000 * 1000
        | Unit.s => 1000 * 1000 * 1000
        | Unit.mins => 1000 * 1000 * 1000 * 60
        | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
        | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
        | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) /
      match unit with
      | Unit.ns => 1
      | Unit.μs => 1000
      | Unit.ms => 1000 * 1000
      | Unit.s => 1000 * 1000 * 1000
      | Unit.mins => 1000 * 1000 * 1000 * 60
      | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
      | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
      | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) =
    value
Tactic:
cases unit <;> simp only [Nat.mul_div_cancel]
Proof state after:
no goals
Theorem: Time.zero_eq_zero
Proof state before:
unit : Time.Unit
⊢ 0 = of 0 unit
Tactic:
simp [of]
Proof state after:
no goals
Theorem: Time.zero_le
Proof state before:
time : Time
⊢ 0 ≤ time
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: Tag.advance_time
Proof state before:
tag : Tag
time : Time.From tag.time
⊢ (advance tag time).time = time.val
Tactic:
simp [advance]
Proof state after:
tag : Tag
time : Time.From tag.time
⊢ (if tag.time < time.val then { time := time.val, microstep := 0 } else increment tag).time = time.val
Theorem: Tag.advance_time
Proof state before:
tag : Tag
time : Time.From tag.time
⊢ (if tag.time < time.val then { time := time.val, microstep := 0 } else increment tag).time = time.val
Tactic:
split <;> simp
Proof state after:
case inr
tag : Tag
time : Time.From tag.time
h✝ : ¬tag.time < time.val
⊢ (increment tag).time = time.val
Theorem: Tag.advance_time
Proof state before:
tag : Tag
time : Time.From tag.time
h : ¬tag.time < time.val
⊢ (increment tag).time = time.val
Tactic:
case _ h => simp_arith [LT.lt] at h; exact Time.le_antisymm time.property h
Proof state after:
no goals
Theorem: Tag.advance_time
Proof state before:
tag : Tag
time : Time.From tag.time
h : ¬tag.time < time.val
⊢ (increment tag).time = time.val
Tactic:
simp_arith [LT.lt] at h
Proof state after:
tag : Tag
time : Time.From tag.time
h : time.val.ns ≤ tag.time.ns
⊢ (increment tag).time = time.val
Theorem: Tag.advance_time
Proof state before:
tag : Tag
time : Time.From tag.time
h : time.val.ns ≤ tag.time.ns
⊢ (increment tag).time = time.val
Tactic:
exact Time.le_antisymm time.property h
Proof state after:
no goals
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
⊢ tag < advance tag t
Tactic:
simp [advance]
Proof state after:
tag : Tag
t : Time.From tag.time
⊢ tag < if tag.time < t.val then { time := t.val, microstep := 0 } else increment tag
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
⊢ tag < if tag.time < t.val then { time := t.val, microstep := 0 } else increment tag
Tactic:
split
Proof state after:
case inl
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }

case inr
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag
Tactic:
case inr => simp_arith [LT.lt, increment]
Proof state after:
no goals
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }
Tactic:
case inl => simp [LT.lt] at *; split <;> simp_all
Proof state after:
no goals
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag
Tactic:
simp_arith [LT.lt, increment]
Proof state after:
no goals
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }
Tactic:
simp [LT.lt] at *
Proof state after:
tag : Tag
t : Time.From tag.time
h✝ : tag.time.ns < t.val.ns
⊢ if tag.time = t.val then tag.microstep < 0 else tag.time.ns < t.val.ns
Theorem: Tag.lt_advance
Proof state before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time.ns < t.val.ns
⊢ if tag.time = t.val then tag.microstep < 0 else tag.time.ns < t.val.ns
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: Network.Graph.Path.Child.parent_eq_nil_class
Proof state before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
⊢ child.val = cons c nil → start = class path
Tactic:
intro h
Proof state after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
⊢ start = class path
Theorem: Network.Graph.Path.Child.parent_eq_nil_class
Proof state before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
⊢ start = class path
Tactic:
have h' := child.property
Proof state after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : child.val ≻ path
⊢ start = class path
Theorem: Network.Graph.Path.Child.parent_eq_nil_class
Proof state before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : child.val ≻ path
⊢ start = class path
Tactic:
simp [Succ, h, prefix?] at h'
Proof state after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : nil = path
⊢ start = class path
Theorem: Network.Graph.Path.Child.parent_eq_nil_class
Proof state before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : nil = path
⊢ start = class path
Tactic:
simp [←h']
Proof state after:
no goals
Theorem: Network.Graph.Path.Child.split_fst_eq_parent
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path : Path graph✝ a✝
child : Child path
⊢ (split child.val (_ : isCons child.val = true)).fst = path
Tactic:
sorry
Proof state after:
no goals
Theorem: Network.Graph.Path.Child.class_eq_class
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path : Path graph✝ a✝
child : Child path
⊢ Class.Child.class (class child) = Path.class child.val
Tactic:
sorry
Proof state after:
no goals
Theorem: Queue.all_events_bounded
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ ∀ {event : ε}, event ∈ queue.events.data → bound ≤ time event
Tactic:
sorry
Proof state after:
no goals
Theorem: Queue.getElem?_some_events_getElem?_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : { e // bound ≤ time e }
queue : Queue ε bound
i : Nat
⊢ queue[i]? = some event → queue.events[i]? = some event.val
Tactic:
intro h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
event : { e // bound ≤ time e }
queue : Queue ε bound
i : Nat
h : queue[i]? = some event
⊢ queue.events[i]? = some event.val
Theorem: Queue.getElem?_some_events_getElem?_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : { e // bound ≤ time e }
queue : Queue ε bound
i : Nat
h : queue[i]? = some event
⊢ queue.events[i]? = some event.val
Tactic:
sorry
Proof state after:
no goals
Theorem: Queue.getElem?_none_events_getElem?_none
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
⊢ queue[i]? = none → queue.events[i]? = none
Tactic:
intro h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
h : queue[i]? = none
⊢ queue.events[i]? = none
Theorem: Queue.getElem?_none_events_getElem?_none
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
h : queue[i]? = none
⊢ queue.events[i]? = none
Tactic:
sorry
Proof state after:
no goals
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
⊢ nextTime queue = some next → ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
intro h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h : nextTime queue = some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h : nextTime queue = some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
unfold nextTime at h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h :
  (match queue[0]? with
    | none => none
    | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
    some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h :
  (match queue[0]? with
    | none => none
    | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
    some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
split at h <;> simp at h
Proof state after:
case h_2
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
nextEvent✝ : { e // bound ≤ time e }
heq✝ : queue[0]? = some nextEvent✝
h : { val := time nextEvent✝.val, property := (_ : bound ≤ time nextEvent✝.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
case _ event h' =>
  exists event
  apply And.intro h'
  simp [←h]
Proof state after:
no goals
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
exists event
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ queue[0]? = some event ∧ time event.val ≥ next.val