internlm/Lean-Github huggingface dataset:
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.left
β : 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
Tactic:
intro newWorld
Proof state after:
case mpr.left
β : 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
newWorld : Unit
⊢ relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld) →
    evaluate (combinedModel collection newVal).1 (Sum.inl newWorld) f
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.left
β : 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
newWorld : Unit
⊢ relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld) →
    evaluate (combinedModel collection newVal).1 (Sum.inl newWorld) f
Tactic:
intro old_rel_new
Proof state after:
case mpr.left
β : 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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inl newWorld) f
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.left
β : 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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inl newWorld) f
Tactic:
absurd old_rel_new
Proof state after:
case mpr.left
β : 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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
⊢ ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.left
β : 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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
⊢ ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
Tactic:
rcases IH_a with ⟨IH_rel, sameR, noNewL⟩
Proof state after:
case mpr.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
IH_rel :
  ∀ (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₂
sameR :
  ∀ (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₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
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
newWorld : Unit
old_rel_new : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
IH_rel :
  ∀ (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₂
sameR :
  ∀ (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₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl newWorld)
Tactic:
apply noNewL
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.right
β : 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 : β) (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
Tactic:
intro otherR otherWorld
Proof state after:
case mpr.right
β : 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
otherR : β
otherWorld : (collection otherR).fst
⊢ relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩) →
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.right
β : 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
otherR : β
otherWorld : (collection otherR).fst
⊢ relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩) →
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Tactic:
intro rel_in_new_model
Proof state after:
case mpr.right
β : 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
otherR : β
otherWorld : (collection otherR).fst
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.right
β : 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
otherR : β
otherWorld : (collection otherR).fst
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Tactic:
specialize IH_f otherR otherWorld
Proof state after:
case mpr.right
β : 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 ())
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
otherR : β
otherWorld : (collection otherR).fst
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
IH_f :
  evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f ↔
    evaluate (collection otherR).snd.2.1 otherWorld f
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case mpr.right
β : 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 ())
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
otherR : β
otherWorld : (collection otherR).fst
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
IH_f :
  evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f ↔
    evaluate (collection otherR).snd.2.1 otherWorld f
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f
Tactic:
simp_all
Proof state after:
case mpr.right
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
R : β
oldWorld : (collection R).fst
otherR : β
otherWorld : (collection otherR).fst
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 ())
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
IH_f :
  evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f ↔
    evaluate (collection otherR).snd.2.1 otherWorld f
⊢ evaluate (collection otherR).snd.2.1 otherWorld f