internlm/Lean-Github huggingface dataset:
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
Tactic:
intro R oldWorld₁ oldWorld₂
Proof state after:
case left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
⊢ relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
    relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mp
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
⊢ relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) →
    relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
Tactic:
intro new_rel
Proof state after:
case left.mp
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
⊢ relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mp.intro.intro.intro.intro.inl
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂
sameR :
  ∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
    R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
u_new : Unit
a_rel_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inl u_new)
u_rel_b : relate (combinedModel collection newVal).1 b (Sum.inl u_new) (Sum.inr ⟨R, oldWorld₂⟩)
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inl u_new)
Tactic:
apply noNewL
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mp.intro.intro.intro.intro.inr.mk
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
otherR : β
otherWorld : (collection otherR).fst
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        ¬R₁ = R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
a_rel_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨otherR, otherWorld⟩)
u_rel_b : relate (combinedModel collection newVal).1 b (Sum.inr ⟨otherR, otherWorld⟩) (Sum.inr ⟨R, oldWorld₂⟩)
sameR : R = otherR
⊢ ∃ y, relate (collection R).snd.2.1 a oldWorld₁ y ∧ relate (collection R).snd.2.1 b y oldWorld₂
Tactic:
subst sameR
Proof state after:
case left.mp.intro.intro.intro.intro.inr.mk
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        ¬R₁ = R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
otherWorld : (collection R).fst
a_rel_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, otherWorld⟩)
u_rel_b : relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, otherWorld⟩) (Sum.inr ⟨R, oldWorld₂⟩)
⊢ ∃ y, relate (collection R).snd.2.1 a oldWorld₁ y ∧ relate (collection R).snd.2.1 b y oldWorld₂
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mp.intro.intro.intro.intro.inr.mk
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        ¬R₁ = R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
otherWorld : (collection R).fst
a_rel_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, otherWorld⟩)
u_rel_b : relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, otherWorld⟩) (Sum.inr ⟨R, oldWorld₂⟩)
⊢ ∃ y, relate (collection R).snd.2.1 a oldWorld₁ y ∧ relate (collection R).snd.2.1 b y oldWorld₂
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
⊢ relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂ →
    relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
intro old_rel
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
old_rel : relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
⊢ relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
old_rel : relate (collection R).snd.2.1 (a;'b) oldWorld₁ oldWorld₂
⊢ relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
unfold relate at old_rel
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
old_rel : ∃ y, relate (collection R).snd.2.1 a oldWorld₁ y ∧ relate (collection R).snd.2.1 b y oldWorld₂
⊢ relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case h
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld₁ oldWorld₂ u : (collection R).fst
a_rel_u : relate (collection R).snd.2.1 a oldWorld₁ u
u_rel_b : relate (collection R).snd.2.1 b u oldWorld₂
⊢ relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, u⟩) ∧
    relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, u⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
aesop
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case right.left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
    R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
Tactic:
intro R₁ R₂ oldWorld₁ oldWorld₂ hneq hrel
Proof state after:
case right.left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
hrel : relate (combinedModel collection newVal).1 (a;'b) (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
⊢ False