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

case right
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
⊢ (∀ (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 ())
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 : ℕ
⊢ ∀ (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₂
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 : ℕ
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₂
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 : ℕ
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₂
Tactic:
constructor <;>
( intro new_rel
  unfold relate at *
  unfold KripkeModel.Rel at *
  unfold combinedModel at *
  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 : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
⊢ relate (collection R).snd.2.1 (·a) oldWorld₁ oldWorld₂ →
    relate (combinedModel collection newVal).1 (·a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
intro new_rel
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : relate (collection R).snd.2.1 (·a) oldWorld₁ oldWorld₂
⊢ relate (combinedModel collection newVal).1 (·a) (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 : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : relate (collection R).snd.2.1 (·a) oldWorld₁ oldWorld₂
⊢ relate (combinedModel collection newVal).1 (·a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
unfold relate at *
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.Rel a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.Rel a (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 : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.Rel a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.Rel a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
unfold KripkeModel.Rel at *
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.2 a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.2 a (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 : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.2 a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.2 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
unfold combinedModel at *
Proof state after:
case left.mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.2 a oldWorld₁ oldWorld₂
⊢ ({
            val := fun world =>
              Sum.casesOn (motive := fun t => world = t → ℕ → Prop) world
                (fun val h => PUnit.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun h => newVal) ⋯)
                (fun val h =>
                  Sigma.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun R w h => (collection R).snd.2.1.val w)
                    ⋯)
                ⋯,
            Rel := fun prog worldOne worldTwo =>
              Sum.casesOn (motive := fun t => worldOne = t → Prop) worldOne
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val h => HEq val.snd (collection val.fst).snd.2 ∧ HEq prog (collection val.fst).snd.1) ⋯)
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val_1 h =>
                      Sigma.casesOn (motive := fun t => val = t → Prop) val
                        (fun kOne wOne h =>
                          Sigma.casesOn (motive := fun t => val_1 = t → Prop) val_1
                            (fun kTwo wTwo h =>
                              let_fun help := fun same =>
                                let_fun sameCol := ⋯;
                                (collection kOne).snd.2.1.Rel prog wOne (⋯.mp wTwo);
                              if same : kOne = kTwo then help same else False)
                            ⋯)
                        ⋯)
                    ⋯)
                ⋯ },
          Sum.inl ()).1.2
    a (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 : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
new_rel : (collection R).snd.2.1.2 a oldWorld₁ oldWorld₂
⊢ ({
            val := fun world =>
              Sum.casesOn (motive := fun t => world = t → ℕ → Prop) world
                (fun val h => PUnit.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun h => newVal) ⋯)
                (fun val h =>
                  Sigma.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun R w h => (collection R).snd.2.1.val w)
                    ⋯)
                ⋯,
            Rel := fun prog worldOne worldTwo =>
              Sum.casesOn (motive := fun t => worldOne = t → Prop) worldOne
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val h => HEq val.snd (collection val.fst).snd.2 ∧ HEq prog (collection val.fst).snd.1) ⋯)
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val_1 h =>
                      Sigma.casesOn (motive := fun t => val = t → Prop) val
                        (fun kOne wOne h =>
                          Sigma.casesOn (motive := fun t => val_1 = t → Prop) val_1
                            (fun kTwo wTwo h =>
                              let_fun help := fun same =>
                                let_fun sameCol := ⋯;
                                (collection kOne).snd.2.1.Rel prog wOne (⋯.mp wTwo);
                              if same : kOne = kTwo then help same else False)
                            ⋯)
                        ⋯)
                    ⋯)
                ⋯ },
          Sum.inl ()).1.2
    a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)
Tactic:
aesop
Proof state after:
no goals