internlm/Lean-Github huggingface dataset:
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ Path.isCons path₂ = true
Tactic:
simp [isCons_def]
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ ∃ child subpath, path₂ = cons child subpath
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ ∃ child subpath, path₂ = cons child subpath
Tactic:
exists c₁, subpath
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ path₂ = cons c₁ subpath
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ path₂ = cons c₁ subpath
Tactic:
injection h with h
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h : cons c₁ subpath = path₂
⊢ path₂ = cons c₁ subpath
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h : cons c₁ subpath = path₂
⊢ path₂ = cons c₁ subpath
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
cases h : (Path.cons child path₁).prefix?
Proof state after:
case none
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

case some
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
val✝ : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some val✝
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
case none =>
  have h : ¬(Path.cons child path₁).prefix?.isSome := by simp_all [Option.isSome_iff_exists]
  have := mt prefix?_isSome_iff_isCons.mpr h
  contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
pre : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some pre
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
case some pre => exists pre
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
have h : ¬(Path.cons child path₁).prefix?.isSome := by simp_all [Option.isSome_iff_exists]
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
have := mt prefix?_isSome_iff_isCons.mpr h
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
this : ¬Path.isCons (Path.cons child path₁) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
this : ¬Path.isCons (Path.cons child path₁) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ¬Option.isSome (prefix? (Path.cons child path₁)) = true
Tactic:
simp_all [Option.isSome_iff_exists]
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.cons
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
pre : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some pre
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
exists pre
Proof state after:
no goals
Theorem: Network.Graph.Path.extend_prefix?_eq_self
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
leaf : Class.Child (class path)
⊢ prefix? (extend path leaf) = some path
Tactic:
induction path
Proof state after:
case nil
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : ∀ {leaf : Class.Child (class a✝)}, prefix? (extend a✝ leaf) = some a✝
leaf : Class.Child (class (cons child✝ a✝))
⊢ prefix? (extend (cons child✝ a✝) leaf) = some (cons child✝ a✝)
Theorem: Network.Graph.Path.extend_prefix?_eq_self
Proof state before:
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil
Tactic:
case nil => simp [extend, prefix?]
Proof state after:
no goals
Theorem: Network.Graph.Path.extend_prefix?_eq_self
Proof state before:
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
subpath : Path graph (Class.Child.class child✝)
hi : ∀ {leaf : Class.Child (class subpath)}, prefix? (extend subpath leaf) = some subpath
leaf : Class.Child (class (cons child✝ subpath))
⊢ prefix? (extend (cons child✝ subpath) leaf) = some (cons child✝ subpath)
Tactic:
case cons subpath hi => simp [extend, prefix?_cons_eq_cons_prefix? hi]
Proof state after:
no goals
Theorem: Network.Graph.Path.extend_prefix?_eq_self
Proof state before:
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil
Tactic:
simp [extend, prefix?]
Proof state after:
no goals
Theorem: Network.Graph.Path.extend_prefix?_eq_self
Proof state before:
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
subpath : Path graph (Class.Child.class child✝)
hi : ∀ {leaf : Class.Child (class subpath)}, prefix? (extend subpath leaf) = some subpath
leaf : Class.Child (class (cons child✝ subpath))
⊢ prefix? (extend (cons child✝ subpath) leaf) = some (cons child✝ subpath)
Tactic:
simp [extend, prefix?_cons_eq_cons_prefix? hi]
Proof state after:
no goals
Theorem: Interface.Subscheme.invEqType
Proof state before:
σ₁ σ₂ : Scheme
a : σ₁.vars
inst : Subscheme σ₁ σ₂
b✝ : σ₂.vars
h : inv b✝ = some a
⊢ Scheme.type σ₁ a = Scheme.type σ₂ b✝
Tactic:
rw [←inst.coeEqType (v := a), inst.invInj h (inst.coeInvId a)]
Proof state after:
no goals
Theorem: Interface?.isEmpty_def
Proof state before:
σ : Interface.Scheme
i : Interface? σ
⊢ isEmpty i ↔ i = Interface?.empty
Tactic:
simp [isEmpty]
Proof state after:
no goals
Theorem: Interface?.isPresent_def
Proof state before:
σ : Interface.Scheme
var : σ.vars
i : Interface? σ
⊢ isPresent i var = true ↔ ∃ v, i var = some v
Tactic:
simp [isPresent, Option.isSome_iff_exists]
Proof state after:
no goals
Theorem: Interface?.merge_val₁
Proof state before:
σ : Interface.Scheme
var : σ.vars
i₁ i₂ : Interface? σ
⊢ i₂ var = none → merge i₁ i₂ var = i₁ var
Tactic:
simp_all [merge, Option.orElse]
Proof state after:
no goals
Theorem: Interface?.merge_val₂
Proof state before:
σ : Interface.Scheme
var : σ.vars
v : Interface.Scheme.type σ var
i₁ i₂ : Interface? σ
⊢ i₂ var = some v → merge i₁ i₂ var = some v
Tactic:
simp_all [merge, Option.orElse]
Proof state after:
no goals
Theorem: Interface?.merge_idem
Proof state before:
σ✝ : Interface.Scheme
i : Interface? σ✝
⊢ merge i i = i
Tactic:
funext var
Proof state after:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ merge i i var = i var
Theorem: Interface?.merge_idem
Proof state before:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ merge i i var = i var
Tactic:
simp [merge, Option.orElse]
Proof state after:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ (match i var, fun x => i var with
    | some a, x => some a
    | none, b => b ()) =
    i var
Theorem: Interface?.merge_idem
Proof state before:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ (match i var, fun x => i var with
    | some a, x => some a
    | none, b => b ()) =
    i var
Tactic:
split
Proof state after:
case h.h_1
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
a✝ : Interface.Scheme.type σ✝ var
heq✝ : i var = some a✝
⊢ some a✝ = i var

case h.h_2
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
heq✝ : i var = none
⊢ (fun x => i var) () = i var
Theorem: ReactionT.Output.merge_stopRequested
Proof state before:
σPE✝ σAE✝ σS✝ : Interface.Scheme
min✝ : Time
o₁ o₂ : Output σPE✝ σAE✝ σS✝ min✝
⊢ ((merge o₁ o₂).stopRequested = true) = (o₁.stopRequested = true ∨ o₂.stopRequested = true)
Tactic:
simp [merge]
Proof state after:
no goals
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t : Reaction.triggerType reaction.val
⊢ Trigger.lift t ≡ t
Tactic:
cases t
Proof state after:
case startup
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.startup ≡ _root_.Trigger.startup

case shutdown
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.shutdown ≡ _root_.Trigger.shutdown

case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ Trigger.lift (_root_.Trigger.port p✝) ≡ _root_.Trigger.port p✝

case action
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
a✝ : reaction.val.actionSources.vars
⊢ Trigger.lift (_root_.Trigger.action a✝) ≡ _root_.Trigger.action a✝

case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case startup
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.startup ≡ _root_.Trigger.startup

case shutdown
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
⊢ Trigger.lift _root_.Trigger.shutdown ≡ _root_.Trigger.shutdown

case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ Trigger.lift (_root_.Trigger.port p✝) ≡ _root_.Trigger.port p✝

case action
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
a✝ : reaction.val.actionSources.vars
⊢ Trigger.lift (_root_.Trigger.action a✝) ≡ _root_.Trigger.action a✝

case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
Tactic:
all_goals
  simp [Trigger.lift]
  first
  | constructor
  | split <;> (constructor; assumption)
Proof state after:
no goals
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.lift (_root_.Trigger.timer t✝) ≡ _root_.Trigger.timer t✝
Tactic:
simp [Trigger.lift]
Proof state after:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
Tactic:
first
| constructor
| split <;> (constructor; assumption)
Proof state after:
no goals
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case timer
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
t✝ : reaction.val.timers
⊢ Trigger.timer { reactor := reactor, timer := (_ : reaction.val.timers = timers (Path.class reactor)) ▸ t✝ } ≡
    _root_.Trigger.timer t✝
Tactic:
constructor
Proof state after:
no goals
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ (match Interface.Subscheme.coe p✝ with
    | Sum.inl input => port { reactor := reactor, port := input }
    | Sum.inr { fst := c, snd := output } =>
      port
        { reactor := Path.extend reactor c,
          port :=
            cast
              (_ :
                ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars =
                  (interface (Path.class (Path.extend reactor c))
                      (match Reactor.PortKind.output with
                      | Reactor.PortKind.input => Reactor.InterfaceKind.inputs
                      | Reactor.PortKind.output => Reactor.InterfaceKind.outputs)).vars)
              output }) ≡
    _root_.Trigger.port p✝
Tactic:
split <;> (constructor; assumption)
Proof state after:
no goals
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case port.h_2
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ port
      { reactor := Path.extend reactor c✝,
        port :=
          cast
            (_ :
              ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars =
                (interface (Path.class (Path.extend reactor c✝))
                    (match Reactor.PortKind.output with
                    | Reactor.PortKind.input => Reactor.InterfaceKind.inputs
                    | Reactor.PortKind.output => Reactor.InterfaceKind.outputs)).vars)
            output✝ } ≡
    _root_.Trigger.port p✝
Tactic:
constructor
Proof state after:
case port.h_2.a
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
Theorem: Network.Graph.Class.Reaction.Trigger.Equiv.lift
Proof state before:
case port.h_2.a
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
Tactic:
assumption
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
⊢ Reaction.Trigger.port p ≡ Trigger.port p' →
    (Activates exec (Reaction.Trigger.port p) ↔
      Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true)
Tactic:
intro he
Proof state after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
⊢ Activates exec (Reaction.Trigger.port p) ↔
    Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
⊢ Activates exec (Reaction.Trigger.port p) ↔
    Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
constructor <;> intro h
Proof state after:
case mp
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true

case mpr
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
case mp reactor =>
  simp only [triggers.activated, reactionInputs]
  cases hp : reaction.subPS.coe p'
  case inl loc =>
    simp
    cases he
    case input hi =>
      simp [hi] at hp
      cases h
      case port h =>
        simp [portIsPresent, hp] at h
        exact h
    case output ho =>
      rw [ho] at hp
      contradiction
  case inr sub =>
    have ⟨c, output⟩ := sub
    simp at output ⊢
    cases he
    case input hi =>
      rw [hi] at hp
      contradiction
    case output c' output' ho =>
      simp [ho] at hp
      injection hp with hc ho
      subst hc
      subst ho
      cases h
      case port h =>
        simp [portIsPresent] at h
        have ⟨v, hv⟩ := h
        exists cast sorry v
        simp [hv]
        sorry
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)
Tactic:
case mpr =>
  sorry
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
Tactic:
simp only [triggers.activated, reactionInputs]
Proof state after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Interface.Subscheme.coe p') =
    true