internlm/Lean-Github huggingface dataset:
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
sameLast : ys.tail.last = ys.last
⊢ z = ys.tail.last
Tactic:
rw [sameLast]
Proof state after:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
sameLast : ys.tail.last = ys.last
⊢ z = ys.last
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
sameLast : ys.tail.last = ys.last
⊢ z = ys.last
Tactic:
exact z_is_last
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ys.tail.last = ys.last
Tactic:
cases ys using Vector.inductionOn
Proof state after:
case h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z x✝ : α
w✝ : Vector α (n + 1)
x_is_head : x = (x✝ ::ᵥ w✝).head
z_is_last : z = (x✝ ::ᵥ w✝).last
steprel : ∀ (i : Fin (n + 1)), r ((x✝ ::ᵥ w✝).get i.castSucc) ((x✝ ::ᵥ w✝).get i.succ)
y : α := (x✝ ::ᵥ w✝).tail.head
a✝ : (n + 1).succ = n + 1 → HEq (x✝ ::ᵥ w✝) w✝ → (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last
⊢ (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ : α
ys : Vector α (n + 1)
x_is_head : x = (y✝ ::ᵥ ys).head
z_is_last : z = (y✝ ::ᵥ ys).last
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ ys).get i.castSucc) ((y✝ ::ᵥ ys).get i.succ)
y : α := (y✝ ::ᵥ ys).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
⊢ (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
Tactic:
case h_cons y ys hyp =>
  cases ys using Vector.inductionOn
  rfl
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ : α
ys : Vector α (n + 1)
x_is_head : x = (y✝ ::ᵥ ys).head
z_is_last : z = (y✝ ::ᵥ ys).last
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ ys).get i.castSucc) ((y✝ ::ᵥ ys).get i.succ)
y : α := (y✝ ::ᵥ ys).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
⊢ (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
Tactic:
cases ys using Vector.inductionOn
Proof state after:
case h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ x✝ : α
w✝ : Vector α n
x_is_head : x = (y✝ ::ᵥ x✝ ::ᵥ w✝).head
z_is_last : z = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.castSucc) ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.succ)
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
⊢ (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ x✝ : α
w✝ : Vector α n
x_is_head : x = (y✝ ::ᵥ x✝ ::ᵥ w✝).head
z_is_last : z = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.castSucc) ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.succ)
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
⊢ (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
Tactic:
rfl
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ∀ (i : Fin n), r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Tactic:
intro i
Proof state after:
case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
i : Fin n
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
i : Fin n
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Tactic:
specialize steprel i.succ
Proof state after:
case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
i : Fin n
steprel : r (ys.get i.succ.castSucc) (ys.get i.succ.succ)
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
i : Fin n
steprel : r (ys.get i.succ.castSucc) (ys.get i.succ.succ)
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Tactic:
induction i
Proof state after:
case h.right.right.mk
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.right.mk
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.right.mk
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
⊢ ∀ (f : Formula) (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
Tactic:
intro mF mR moW
Proof state after:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨mR, moW⟩) mF ↔ evaluate (collection mR).snd.2.1 moW mF
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) Formula.bottom ↔
      evaluate (collection R).snd.2.1 oldWorld Formula.bottom
Tactic:
simp
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : ℕ),
    (fun φ =>
        ∀ (R : β) (oldWorld : (collection R).fst),
          evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
            evaluate (collection R).snd.2.1 oldWorld φ)
      (·a)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : Formula),
    (fun φ =>
          ∀ (R : β) (oldWorld : (collection R).fst),
            evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
              evaluate (collection R).snd.2.1 oldWorld φ)
        a →
      (fun φ =>
          ∀ (R : β) (oldWorld : (collection R).fst),
            evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
              evaluate (collection R).snd.2.1 oldWorld φ)
        (~a)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a a_1 : Formula),
    (fun φ =>
          ∀ (R : β) (oldWorld : (collection R).fst),
            evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
              evaluate (collection R).snd.2.1 oldWorld φ)
        a →
      (fun φ =>
            ∀ (R : β) (oldWorld : (collection R).fst),
              evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
                evaluate (collection R).snd.2.1 oldWorld φ)
          a_1 →
        (fun φ =>
            ∀ (R : β) (oldWorld : (collection R).fst),
              evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
                evaluate (collection R).snd.2.1 oldWorld φ)
          (a⋀a_1)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : Program) (a_1 : Formula),
    (fun π =>
          (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
              relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
                relate (collection R).snd.2.1 π oldWorld₁ oldWorld₂) ∧
            (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
                R₁ ≠ R₂ →
                  ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
              ∀ (R : β) (oldWorld : (collection R).fst),
                ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ()))
        a →
      (fun φ =>
            ∀ (R : β) (oldWorld : (collection R).fst),
              evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
                evaluate (collection R).snd.2.1 oldWorld φ)
          a_1 →
        (fun φ =>
            ∀ (R : β) (oldWorld : (collection R).fst),
              evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
                evaluate (collection R).snd.2.1 oldWorld φ)
          (⌈a⌉a_1)
Tactic:
intro α f IH_a IH_f R oldWorld
Proof state after:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f) ↔
    evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mp
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f) →
    evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f) →
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)
Tactic:
intro true_in_old
Proof state after:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
true_in_old : evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
true_in_old : evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)
Tactic:
unfold evaluate at true_in_old
Proof state after:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)
Tactic:
simp
Proof state after:
case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
⊢ (∀ (a : Unit),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl a) →
        evaluate (combinedModel collection newVal).1 (Sum.inl a) f) ∧
    ∀ (a : β) (b : (collection a).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨a, b⟩) →
        evaluate (combinedModel collection newVal).1 (Sum.inr ⟨a, b⟩) f