internlm/Lean-Github huggingface dataset:
Theorem: SPL.splitComplete
Proof state before:
case right.left.h.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs

case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
(
    simp
    simp
    apply And.intro
    (
        apply Classical.byContradiction
        intros h₂
        simp at h₂
        apply h₁ h₂
        exact h₀
        exact h₀
    )
)
Proof state after:
no goals
Theorem: SPL.splitComplete
Proof state before:
case right.left.h.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs

case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
simp
Proof state after:
case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
simp
Proof state after:
case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply And.intro
Proof state after:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
(
    apply Classical.byContradiction
    intros h₂
    simp at h₂
    apply h₁ h₂
    exact h₀
    exact h₀
)
Proof state after:
no goals
Theorem: SPL.splitComplete
Proof state before:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
apply Classical.byContradiction
Proof state after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ¬c ∉ ⦃splitter⦄ → False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ¬c ∉ ⦃splitter⦄ → False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
intros h₂
Proof state after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : ¬c ∉ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : ¬c ∉ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
simp at h₂
Proof state after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
apply h₁ h₂
Proof state after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ c ∈ ⦃↑x⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ c ∈ ⦃↑x⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
exact h₀
Proof state after:
case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Theorem: SPL.splitComplete
Proof state before:
case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
exact h₀
Proof state after:
no goals
Theorem: liftedCIA.restrict_correct
Proof state before:
⊢ ∀ (ρ : Config F) (t : TraceRel') (d : Delta'), (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)
Tactic:
intros ρ t d
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)
Tactic:
simp [restrict']
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (({x | x ∈ t ∧ (x.1.1, x.2) ∈ d.add} ∪ {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.delete} ∪
        {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.modify}) |
      ρ) =
    restrict (t | ρ) (d | ρ)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (({x | x ∈ t ∧ (x.1.1, x.2) ∈ d.add} ∪ {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.delete} ∪
        {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.modify}) |
      ρ) =
    restrict (t | ρ) (d | ρ)
Tactic:
simp [←Set.setOf_or, Variational.index]
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ vset.index {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify}
      ρ =
    restrict (vset.index t ρ) (indexDelta d ρ)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ vset.index {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify}
      ρ =
    restrict (vset.index t ρ) (indexDelta d ρ)
Tactic:
unfold vset.index
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x =>
      {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify} (x, ρ)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x =>
      {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify} (x, ρ)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Tactic:
simp [setOf, ←(and_or_left)]
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Tactic:
simp [restrict, indexDelta, allElements, ←Set.setOf_or, index_mem, setOf]
Proof state after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) = fun x =>
    (x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)
Theorem: liftedCIA.restrict_correct
Proof state before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) = fun x =>
    (x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)
Tactic:
apply funext
Proof state after:
case h
ρ : Config F
t : TraceRel'
d : Delta'
⊢ ∀ (x : SysEl × GSNEl),
    ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
      ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Theorem: liftedCIA.restrict_correct
Proof state before:
case h
ρ : Config F
t : TraceRel'
d : Delta'
⊢ ∀ (x : SysEl × GSNEl),
    ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
      ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Tactic:
intros x
Proof state after:
case h
ρ : Config F
t : TraceRel'
d : Delta'
x : SysEl × GSNEl
⊢ ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Theorem: liftedCIA.restrict_correct
Proof state before:
case h
ρ : Config F
t : TraceRel'
d : Delta'
x : SysEl × GSNEl
⊢ ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Tactic:
simp [Set.mem_def]
Proof state after:
no goals
Theorem: liftedCIA.trace_correct
Proof state before:
⊢ ∀ (t : TraceRel') (es : vset F SysEl) (ρ : Config F), (trace' t es | ρ) = trace (t | ρ) (es | ρ)
Tactic:
intros t es ρ
Proof state after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (trace' t es | ρ) = trace (t | ρ) (es | ρ)
Theorem: liftedCIA.trace_correct
Proof state before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (trace' t es | ρ) = trace (t | ρ) (es | ρ)
Tactic:
simp [trace', Variational.index]
Proof state after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ vset.index ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) ρ = trace (vset.index t ρ) (vset.index es ρ)
Theorem: liftedCIA.trace_correct
Proof state before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ vset.index ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) ρ = trace (vset.index t ρ) (vset.index es ρ)
Tactic:
unfold vset.index
Proof state after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) (x, ρ)) =
    trace (fun x => t (x, ρ)) fun x => es (x, ρ)
Theorem: liftedCIA.trace_correct
Proof state before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) (x, ρ)) =
    trace (fun x => t (x, ρ)) fun x => es (x, ρ)
Tactic:
simp [trace, setOf]
Proof state after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ)) =
    (fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)
Theorem: liftedCIA.trace_correct
Proof state before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ)) =
    (fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)
Tactic:
apply funext
Proof state after:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ ∀ (x : GSNEl),
    ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
      ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Theorem: liftedCIA.trace_correct
Proof state before:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ ∀ (x : GSNEl),
    ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
      ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Tactic:
intros x
Proof state after:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
x : GSNEl
⊢ ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
    ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Theorem: liftedCIA.trace_correct
Proof state before:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
x : GSNEl
⊢ ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
    ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Tactic:
simp[Set.image, setOf, Set.mem_def]
Proof state after:
no goals
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
⊢ ∀ (g : GSN') (recheck revise : vset F GSNEl) (ρ : Config F),
    (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
intros g recheck revise ρ
Proof state after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
simp [createAnnotation', Set.image]
Proof state after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (({x | ∃ a b, (a, b) ∈ recheck ∧ ((a, Annotation.Recheck), b) = x} ∪
          {x | ∃ a b, (a, b) ∈ revise ∧ ((a, Annotation.Revise), b) = x} ∪
        {x | ∃ a b, ((a, b) ∈ g ∧ ¬((a, b) ∈ recheck ∨ (a, b) ∈ revise)) ∧ ((a, Annotation.Reuse), b) = x}) |
      ρ) =
    createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (({x | ∃ a b, (a, b) ∈ recheck ∧ ((a, Annotation.Recheck), b) = x} ∪
          {x | ∃ a b, (a, b) ∈ revise ∧ ((a, Annotation.Revise), b) = x} ∪
        {x | ∃ a b, ((a, b) ∈ g ∧ ¬((a, b) ∈ recheck ∨ (a, b) ∈ revise)) ∧ ((a, Annotation.Reuse), b) = x}) |
      ρ) =
    createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
simp [←Set.setOf_or, Variational.index]
Proof state after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ vset.index
      {a |
        ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
            ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
          ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
      ρ =
    createAnnotation (vset.index g ρ) (vset.index recheck ρ) (vset.index revise ρ)
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ vset.index
      {a |
        ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
            ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
          ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
      ρ =
    createAnnotation (vset.index g ρ) (vset.index recheck ρ) (vset.index revise ρ)
Tactic:
unfold vset.index
Proof state after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      {a |
          ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
              ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
            ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
        (x, ρ)) =
    createAnnotation (fun x => g (x, ρ)) (fun x => recheck (x, ρ)) fun x => revise (x, ρ)
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      {a |
          ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
              ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
            ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
        (x, ρ)) =
    createAnnotation (fun x => g (x, ρ)) (fun x => recheck (x, ρ)) fun x => revise (x, ρ)
Tactic:
simp [createAnnotation, Set.image, ←Set.setOf_or, setOf]
Proof state after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      ((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    ((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
        ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
      fun x =>
      ∃ a,
        ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
          (a, Annotation.Reuse) = x
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      ((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    ((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
        ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
      fun x =>
      ∃ a,
        ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
          (a, Annotation.Reuse) = x
Tactic:
apply funext
Proof state after:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ ∀ (x : GSNEl × Annotation),
    (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
      (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
            ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
          fun x =>
          ∃ a,
            ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
              (a, Annotation.Reuse) = x)
        x
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ ∀ (x : GSNEl × Annotation),
    (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
      (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
            ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
          fun x =>
          ∃ a,
            ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
              (a, Annotation.Reuse) = x)
        x
Tactic:
intros x
Proof state after:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
x : GSNEl × Annotation
⊢ (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
      ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
          ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
        fun x =>
        ∃ a,
          ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
            (a, Annotation.Reuse) = x)
      x
Theorem: liftedCIA.createAnnotation_correct
Proof state before:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
x : GSNEl × Annotation
⊢ (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
      ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
          ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
        fun x =>
        ∃ a,
          ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
            (a, Annotation.Reuse) = x)
      x
Tactic:
simp[Set.mem_def, Set.union_def, setOf]
Proof state after:
no goals
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
⊢ ∀ (S S' : Sys') (A : GSN') (R : TraceRel') (D : Delta') (ρ : Config F),
    (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
Tactic:
intros S S' A R D ρ
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
Theorem: liftedCIA.GSN_IA'_correct
Proof state before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
Tactic:
simp [GSN_IA', GSN_IA]
Proof state after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict (R | ρ) (D | ρ)) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)