internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ∀ (x : Model T Γ), ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
Tactic:
intro u
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
have : [→ u].hom p ∈ ⛓️ := chainSet_ex nwf h u
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
have : ¬Eval (Model.structure T Γ) ![u] Semiterm.fvar p := by
  simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) this
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this✝ : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this✝ : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) this
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.Model.models
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → (structure T Γ).toStruc ⊧ f
Tactic:
intro σ hσ
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
hσ : σ ∈ T
⊢ (structure T Γ).toStruc ⊧ σ
Theorem: LO.FirstOrder.Completeness.Model.models
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
hσ : σ ∈ T
⊢ (structure T Γ).toStruc ⊧ σ
Tactic:
simpa using semanticMainLemma_val nwf _ (chainSet_id nwf hσ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.semanticMainLemmaTop
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticFormula L
h : p ∈ Γ
⊢ p ∈ {x | x ∈ ⛓️[0]}
Tactic:
simp[chain, chainU, h]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.rel
Proof state before:
x y : terminal.World
⊢ x ≺ y ↔ x = y
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr
Proof state before:
n : ℕ
x y : terminal.World
⊢ x ≺^[n] y ↔ x = y
Tactic:
induction n with
| zero => simp;
| succ n ih => simp; use x; simp [ih];
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr
Proof state before:
case zero
x y : terminal.World
⊢ x ≺^[0] y ↔ x = y
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr
Proof state before:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ x ≺^[n + 1] y ↔ x = y
Tactic:
simp
Proof state after:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ ∃ x, RelItr (fun x x_1 => x ≺ x_1) n x y
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr
Proof state before:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ ∃ x, RelItr (fun x x_1 => x ≺ x_1) n x y
Tactic:
use x
Proof state after:
case h
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ RelItr (fun x x_1 => x ≺ x_1) n x y
Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr
Proof state before:
case h
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ RelItr (fun x x_1 => x ≺ x_1) n x y
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.atom_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
a : α
⊢ w ⊧ atom a ↔ M.Valuation w a
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.top_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w ⊤ ↔ True
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.bot_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w ⊥ ↔ False
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.and_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⋏ q) ↔ Satisfies M w p ∧ Satisfies M w q
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.or_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⋎ q) ↔ Satisfies M w p ∨ Satisfies M w q
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.imp_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (p ⟶ q) ↔ Satisfies M w p → Satisfies M w q
Tactic:
simp [Satisfies, imp_iff_not_or]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.not_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (~p) ↔ ¬Satisfies M w p
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.box_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (□p) ↔ ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' p
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.dia_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
⊢ Satisfies M w (◇p) ↔ ∃ w', w ≺ w' ∧ Satisfies M w' p
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
n : ℕ
⊢ Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
Tactic:
induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h w' hww';
    simp at h;
    obtain ⟨v, hwv, hvw'⟩ := hww';
    exact (ih.mp $ h _ hwv) w' hvw';
  . simp;
    intro h w' hww';
    apply ih.mpr;
    intro v hwv;
    exact h v w' hww' hwv;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case zero
α : Type u_1
M : Model α
p q : Formula α
w : M.World
⊢ Satisfies M w (□^[0]p) ↔ ∀ (v : M.Frame.World), w ≺^[0] v → Satisfies M v p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) ↔ ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p
Tactic:
constructor
Proof state after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Tactic:
. intro h w' hww';
  simp at h;
  obtain ⟨v, hwv, hvw'⟩ := hww';
  exact (ih.mp $ h _ hwv) w' hvw';
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Tactic:
. simp;
  intro h w' hww';
  apply ih.mpr;
  intro v hwv;
  exact h v w' hww' hwv;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p
Tactic:
intro h w' hww'
Proof state after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : Satisfies M w (□^[(n + 1)]p)
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
⊢ Satisfies M w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : Satisfies M w (□^[(n + 1)]p)
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
⊢ Satisfies M w' p
Tactic:
simp at h
Proof state after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
⊢ Satisfies M w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
⊢ Satisfies M w' p
Tactic:
obtain ⟨v, hwv, hvw'⟩ := hww'
Proof state after:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
v : M.Frame.World
hwv : w ≺ v
hvw' : RelItr (fun x x_1 => x ≺ x_1) n v w'
⊢ Satisfies M w' p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
v : M.Frame.World
hwv : w ≺ v
hvw' : RelItr (fun x x_1 => x ≺ x_1) n v w'
⊢ Satisfies M w' p
Tactic:
exact (ih.mp $ h _ hwv) w' hvw'
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Tactic:
simp
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p) →
    ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p) →
    ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Tactic:
intro h w' hww'
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Tactic:
apply ih.mpr
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ∀ (v : M.Frame.World), w' ≺^[n] v → Satisfies M v p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ∀ (v : M.Frame.World), w' ≺^[n] v → Satisfies M v p
Tactic:
intro v hwv
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
v : M.Frame.World
hwv : w' ≺^[n] v
⊢ Satisfies M v p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
v : M.Frame.World
hwv : w' ≺^[n] v
⊢ Satisfies M v p
Tactic:
exact h v w' hww' hwv
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
n : ℕ
⊢ Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
Tactic:
induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h;
    obtain ⟨v, hwv, hv⟩ := by simpa using h;
    obtain ⟨x, hvx, hx⟩ := ih.mp hv;
    existsi x;
    constructor;
    . existsi v; simp_all;
    . simpa;
  . simp;
    intro x y hwy hyx hx;
    existsi y;
    constructor;
    . simpa;
    . apply ih.mpr;
      existsi x;
      simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case zero
α : Type u_1
M : Model α
p q : Formula α
w : M.World
⊢ Satisfies M w (◇^[0]p) ↔ ∃ v, w ≺^[0] v ∧ Satisfies M v p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) ↔ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
constructor
Proof state after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
. intro h;
  obtain ⟨v, hwv, hv⟩ := by simpa using h;
  obtain ⟨x, hvx, hx⟩ := ih.mp hv;
  existsi x;
  constructor;
  . existsi v; simp_all;
  . simpa;
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
. simp;
  intro x y hwy hyx hx;
  existsi y;
  constructor;
  . simpa;
  . apply ih.mpr;
    existsi x;
    simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
intro h
Proof state after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
obtain ⟨v, hwv, hv⟩ := by simpa using h;
Proof state after:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
obtain ⟨x, hvx, hx⟩ := ih.mp hv
Proof state after:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p