Theorem: Q_then_relate (Pdl/Modelgraphs.lean)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X Y : { x // x ∈ Worlds }
⊢ Q (↑MG).Rel α X Y → relate (↑MG) α X Y
Tactic:
cases α
State after:
case atom_prog
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y

case sequence
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹;'a✝) X Y → relate (↑MG) (a✝¹;'a✝) X Y

case union
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹⋓a✝) X Y → relate (↑MG) (a✝¹⋓a✝) X Y

case star
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Program
⊢ Q (↑MG).Rel (∗a✝) X Y → relate (↑MG) (∗a✝) X Y

case test
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Formula
⊢ Q (↑MG).Rel (?'a✝) X Y → relate (↑MG) (?'a✝) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y
Tactic:
case atom_prog =>
  simp only [instBot, Q, relate, imp_self]
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
case sequence α β =>
  have := Q_then_relate MG α
  have := Q_then_relate MG β
  simp only [instBot, Subtype.forall, Q, Relation.Comp, Subtype.exists,
    relate, forall_exists_index, and_imp] at *
  tauto
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
case union α β =>
  have := Q_then_relate MG α
  have := Q_then_relate MG β
  simp only [instBot, Subtype.forall, Q, relate] at *
  tauto
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Q (↑MG).Rel (∗α) X Y → relate (↑MG) (∗α) X Y
Tactic:
case star α =>
  simp only [instBot, Q, relate]
  apply Relation.ReflTransGen.lift
  intro a b Qab
  exact Q_then_relate MG α a b Qab
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y
Tactic:
simp only [instBot, Q, relate, imp_self]
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
have := Q_then_relate MG α
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
have := Q_then_relate MG β
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Tactic:
simp only [instBot, Subtype.forall, Q, Relation.Comp, Subtype.exists,
  relate, forall_exists_index, and_imp] at *
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ ∀ (x : Finset Formula) (x_1 : x ∈ Worlds),
    Q (↑MG).Rel α X ⟨x, x_1⟩ →
      Q (↑MG).Rel β ⟨x, x_1⟩ Y → ∃ a, ∃ (b : a ∈ Worlds), relate (↑MG) α X ⟨a, b⟩ ∧ relate (↑MG) β ⟨a, b⟩ Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ ∀ (x : Finset Formula) (x_1 : x ∈ Worlds),
    Q (↑MG).Rel α X ⟨x, x_1⟩ →
      Q (↑MG).Rel β ⟨x, x_1⟩ Y → ∃ a, ∃ (b : a ∈ Worlds), relate (↑MG) α X ⟨a, b⟩ ∧ relate (↑MG) β ⟨a, b⟩ Y
Tactic:
tauto
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
have := Q_then_relate MG α
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
have := Q_then_relate MG β
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Tactic:
simp only [instBot, Subtype.forall, Q, relate] at *
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ Q (↑MG).Rel α X Y ∨ Q (↑MG).Rel β X Y → relate (↑MG) α X Y ∨ relate (↑MG) β X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ Q (↑MG).Rel α X Y ∨ Q (↑MG).Rel β X Y → relate (↑MG) α X Y ∨ relate (↑MG) β X Y
Tactic:
tauto
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Q (↑MG).Rel (∗α) X Y → relate (↑MG) (∗α) X Y
Tactic:
simp only [instBot, Q, relate]
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Relation.ReflTransGen (Q (↑MG).Rel α) X Y → Relation.ReflTransGen (relate (↑MG) α) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Relation.ReflTransGen (Q (↑MG).Rel α) X Y → Relation.ReflTransGen (relate (↑MG) α) X Y
Tactic:
apply Relation.ReflTransGen.lift
State after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ ∀ (a b : { x // x ∈ Worlds }), Q (↑MG).Rel α a b → relate (↑MG) α a b

State before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ ∀ (a b : { x // x ∈ Worlds }), Q (↑MG).Rel α a b → relate (↑MG) α a b
Tactic:
intro a b Qab
State after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
a b : { x // x ∈ Worlds }
Qab : Q (↑MG).Rel α a b
⊢ relate (↑MG) α a b

State before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
a b : { x // x ∈ Worlds }
Qab : Q (↑MG).Rel α a b
⊢ relate (↑MG) α a b
Tactic:
exact Q_then_relate MG α a b Qab
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Tactic:
have := loadedTruthLemma MG X φ
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Tactic:
simp [Q, relate, Relation.Comp] at *
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ X = Y → φ ∈ ↑X → X = Y ∧ evaluate (↑MG) X φ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ X = Y → φ ∈ ↑X → X = Y ∧ evaluate (↑MG) X φ
Tactic:
intro X_is_Y phi_in_X
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
X_is_Y : X = Y
phi_in_X : φ ∈ ↑X
⊢ X = Y ∧ evaluate (↑MG) X φ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
X_is_Y : X = Y
phi_in_X : φ ∈ ↑X
⊢ X = Y ∧ evaluate (↑MG) X φ
Tactic:
subst X_is_Y
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X ∧ evaluate (↑MG) X φ

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X ∧ evaluate (↑MG) X φ
Tactic:
constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ evaluate (↑MG) X φ

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ X = X
Tactic:
tauto
State after:
no goals

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ evaluate (↑MG) X φ
Tactic:
tauto
State after:
no goals